Λs, running

Every line below runs the checker at build time via #guard. If any result were different, this file would not compile.

A note on what that does and does not establish. #guard executes the compiled infer, so these are tests, not kernel-checked proofs: kernel reduction gets stuck on the Rat instance chain that Mathlib's algebraic hierarchy is built from, which is a known cost of building on it. The correctness guarantee does not come from here: it comes from LambdaS.Typing, where check returns the derivation (so soundness holds by construction) and check_eq is proved in the kernel, saying nothing well-typed is rejected. These examples show the verified checker running.

inductive LambdaS.Examples.Base : Type

Five base units; note that three of them measure Length. That is deliberate: it is the configuration a "one named unit per dimension" restriction forbids, and the one conversion factors live in.

• meter : Base
• foot : Base
• yard : Base
• kilogram : Base
• second : Base

@[instance_reducible]

instance LambdaS.Examples.instDecidableEqBase : DecidableEq Base

Equations

• LambdaS.Examples.instDecidableEqBase x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance LambdaS.Examples.instFintypeBase : Fintype Base

Equations

• One or more equations did not get rendered due to their size.

inductive LambdaS.Examples.Dim : Type

The dimensions those units measure.

• length : Dim
• mass : Dim
• time : Dim

@[instance_reducible]

instance LambdaS.Examples.instDecidableEqDim : DecidableEq Dim

Equations

• LambdaS.Examples.instDecidableEqDim x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance LambdaS.Examples.instFintypeDim : Fintype Dim

Equations

• LambdaS.Examples.instFintypeDim = { elems := {LambdaS.Examples.Dim.length, LambdaS.Examples.Dim.mass, LambdaS.Examples.Dim.time}, complete := LambdaS.Examples.instFintypeDim._proof_1 }

@[instance_reducible]

instance LambdaS.Examples.instUnitSysBaseDim : UnitSys Base Dim

The declared dimension of each base unit. Meter, foot, and yard collapse to the same dimension; nothing else does.

Note that dim lands in DExp Dim 0, a dimension expression, not a single base dimension. That is what lets a derived unit be declared directly at a compound dimension.

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

abbrev LambdaS.Examples.Δ₀ : DCtx Dim 0 0

The empty dimension context: a closed term has no unit variables in scope.

Equations

• LambdaS.Examples.Δ₀ i = i.elim0

@[reducible, inline]

abbrev LambdaS.Examples.Term₀ : Type

Terms and types of the running example, at the closed scope.

Equations

• LambdaS.Examples.Term₀ = LambdaS.Tm LambdaS.Examples.Base LambdaS.Examples.Dim 0 0

@[reducible, inline]

abbrev LambdaS.Examples.Type₀ : Type

Equations

• LambdaS.Examples.Type₀ = LambdaS.Ty LambdaS.Examples.Base LambdaS.Examples.Dim 0 0

@[reducible, inline]

abbrev LambdaS.Examples.typeOf (e : Term₀) : Option Type₀

The type a closed term is assigned.

Equations

• LambdaS.Examples.typeOf e = LambdaS.infer LambdaS.Examples.Δ₀ [] e

@[reducible, inline]

abbrev LambdaS.Examples.typeOfIn (Γ : Ctx Base Dim 0 0) (e : Term₀) : Option Type₀

The type a term is assigned in a non-empty value context.

Equations

• LambdaS.Examples.typeOfIn Γ e = LambdaS.infer LambdaS.Examples.Δ₀ Γ e

@[reducible, inline]

abbrev LambdaS.Examples.bu {k : ℕ} (b : Base) : UExp Base k

A base unit as a unit expression, at any scope.

Equations

• LambdaS.Examples.bu b = LambdaS.Term.ofBase b

@[reducible, inline]

abbrev LambdaS.Examples.m : UExp Base 0

Equations

• LambdaS.Examples.m = LambdaS.Examples.bu LambdaS.Examples.Base.meter

@[reducible, inline]

abbrev LambdaS.Examples.ft : UExp Base 0

Equations

• LambdaS.Examples.ft = LambdaS.Examples.bu LambdaS.Examples.Base.foot

@[reducible, inline]

abbrev LambdaS.Examples.yd : UExp Base 0

Equations

• LambdaS.Examples.yd = LambdaS.Examples.bu LambdaS.Examples.Base.yard

@[reducible, inline]

abbrev LambdaS.Examples.kg : UExp Base 0

Equations

• LambdaS.Examples.kg = LambdaS.Examples.bu LambdaS.Examples.Base.kilogram

@[reducible, inline]

abbrev LambdaS.Examples.sec : UExp Base 0

Equations

• LambdaS.Examples.sec = LambdaS.Examples.bu LambdaS.Examples.Base.second

Scalars

def LambdaS.Examples.length : Term₀

1.3 m: a literal times a unit constant.

Equations

• LambdaS.Examples.length = (LambdaS.Tm.lit 1.3).mul (LambdaS.Tm.ucon LambdaS.Examples.m)

def LambdaS.Examples.duration : Term₀

5 s.

Equations

• LambdaS.Examples.duration = (LambdaS.Tm.lit 5).mul (LambdaS.Tm.ucon LambdaS.Examples.sec)

def LambdaS.Examples.velocity : Term₀

1.3 m / 5 s.

Equations

• LambdaS.Examples.velocity = LambdaS.Tm.div LambdaS.Examples.length LambdaS.Examples.duration

The error that motivates the whole exercise

def LambdaS.Examples.mismatch : Term₀

Adding a length to a duration: the Mars Climate Orbiter failure, in one line.

Equations

• LambdaS.Examples.mismatch = LambdaS.Tm.add LambdaS.Examples.length LambdaS.Examples.duration

Roots, where ℚ exponents pay for themselves

Kennedy's Λu and F# both type sqrt : float<'u^2> -> float<'u>, which to apply at a volume requires solving 2·vec(u) = 3 over ℤ. There is no solution, so F# rejects the square root of a volume. Over ℚ the root is total, and this lands at m^(3/2).

def LambdaS.Examples.volume : Term₀

Equations

• LambdaS.Examples.volume = ((LambdaS.Tm.ucon LambdaS.Examples.m).mul (LambdaS.Tm.ucon LambdaS.Examples.m)).mul (LambdaS.Tm.ucon LambdaS.Examples.m)

Spaces

A state space whose components carry different units: position in meters, momentum in kg·m/s. This is the non-uniform case F# cannot express at all, since it parameterizes a type by a single unit.

def LambdaS.Examples.State : Sp Base 0

Equations

• LambdaS.Examples.State = [LambdaS.Examples.m, (LambdaS.Term.mul LambdaS.Examples.kg LambdaS.Examples.m).div LambdaS.Examples.sec]

Linear maps

def LambdaS.Examples.W : Sp Base 0

Equations

• LambdaS.Examples.W = [LambdaS.Examples.sec]

Unit polymorphism

The reason Kennedy's calculus exists, now over spaces, with the dimension bound that lets a polymorphic function still convert.

∀u. τ is not primitive. It is ∀δ. ∀u:δ. τ: a unit variable bounded by a dimension variable. That is what makes it genuinely unbounded, and the guards below check both halves: that δ matches any concrete dimension on instantiation, and that nothing concrete matches δ inside the binder.

@[reducible, inline]

abbrev LambdaS.Examples.uvar : UExp Base 1

The bound unit variable, inside one unit binder.

Equations

• LambdaS.Examples.uvar = LambdaS.Term.ofVar 0

@[reducible, inline]

abbrev LambdaS.Examples.dvar : DExp Dim 1

The bound dimension variable, inside one dimension binder.

Equations

• LambdaS.Examples.dvar = LambdaS.Term.ofVar 0

def LambdaS.Examples.sqr : Term₀

Λδ. Λu:δ. λ(x : Q u). x * x: squaring, at any unit.

Equations

• LambdaS.Examples.sqr = (LambdaS.Tm.ulam LambdaS.Examples.dvar (LambdaS.Tm.lam (LambdaS.Ty.Q LambdaS.Examples.uvar) ((LambdaS.Tm.var 0).mul (LambdaS.Tm.var 0)))).dlam

@[reducible, inline]

abbrev LambdaS.Examples.sqrAt (d : DExp Dim 0) (μ : UExp Base 0) : Term₀

Equations

• LambdaS.Examples.sqrAt d μ = (LambdaS.Tm.dapp LambdaS.Examples.sqr d).uapp μ

@[reducible, inline]

abbrev LambdaS.Examples.velDim : DExp Dim 0

Equations

• LambdaS.Examples.velDim = (LambdaS.Term.ofBase LambdaS.Examples.Dim.length).div (LambdaS.Term.ofBase LambdaS.Examples.Dim.time)

def LambdaS.Examples.addPoly : Term₀

Addition at any unit, but the same unit on both sides.

Equations

• One or more equations did not get rendered due to their size.

def LambdaS.Examples.badPoly : Term₀

Polymorphism does not weaken the check. Λδ. Λu:δ. λ(x : Q u). x + 1 is rejected, because u is rigid inside the binder and cannot be 1.

Equations

• LambdaS.Examples.badPoly = (LambdaS.Tm.ulam LambdaS.Examples.dvar (LambdaS.Tm.lam (LambdaS.Ty.Q LambdaS.Examples.uvar) ((LambdaS.Tm.var 0).add (LambdaS.Tm.lit 1)))).dlam

def LambdaS.Examples.twoVars : Term₀

Two distinct unit variables cannot be added either: nested binders really introduce fresh variables rather than shadowing.

Equations

• One or more equations did not get rendered due to their size.

Conversion under a binder

This is what the dimension bound buys, and what an unbounded quantifier cannot express: a polymorphic function that converts its argument.

def LambdaS.Examples.inMeters : Term₀

Λu:Length. λ(x : Q u). convert x u meter: take a length in any unit, return it in meters.

Equations

• One or more equations did not get rendered due to their size.

def LambdaS.Examples.inMetersFree : Term₀

The unbounded quantifier cannot convert. The same body under ∀δ. ∀u:δ. is rejected: dimOf reports the dimension variable δ, which is not the dimension of the meter, so SameDim fails. This is the rejection an unbounded quantifier ought to give, and it is why the bound is a dimension variable rather than the trivial dimension: under the trivial dimension u would be claimed dimensionless and the conversion would wrongly be accepted.

Equations

• One or more equations did not get rendered due to their size.

Physics: where the exponents come from

@[reducible, inline]

abbrev LambdaS.Examples.Physics.hbar : UExp Base 0

ħ = kg·m²/s

Equations

• LambdaS.Examples.Physics.hbar = (LambdaS.Term.mul LambdaS.Examples.kg (LambdaS.Term.mul LambdaS.Examples.m LambdaS.Examples.m)).div LambdaS.Examples.sec

@[reducible, inline]

abbrev LambdaS.Examples.Physics.G : UExp Base 0

G = m³/(kg·s²)

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

abbrev LambdaS.Examples.Physics.c : UExp Base 0

c = m/s

Equations

• LambdaS.Examples.Physics.c = LambdaS.Term.div LambdaS.Examples.m LambdaS.Examples.sec

def LambdaS.Examples.Physics.planckLength : Term₀

Equations

• One or more equations did not get rendered due to their size.

def LambdaS.Examples.Physics.planckWrong : Term₀

Equations

• One or more equations did not get rendered due to their size.

def LambdaS.Examples.Physics.fermionField : Term₀

Equations

• One or more equations did not get rendered due to their size.

The base-measure problem, as a type error

A probability density over a space whose measure carries μ itself carries μ⁻¹; that is what makes ∫ p dμ dimensionless. So log p is not well-typed, which is the base-measure problem: a density means nothing except relative to the measure it was taken against, and representing a distribution by its density silently discards that measure.

Radul and Alexeev (arXiv:2010.09647) identify exactly this failure in probabilistic programming systems and fix it by library convention. Here the checker rejects it.

@[reducible, inline]

abbrev LambdaS.Examples.Measure.density : UExp Base 0

A probability density over a length-parameterized space: m⁻¹.

Equations

• LambdaS.Examples.Measure.density = LambdaS.Term.inv LambdaS.Examples.m

@[reducible, inline]

abbrev LambdaS.Examples.Measure.halfDensity : UExp Base 0

A wavefunction is a half-density, at m^(-1/2). Squaring it gives a weight-1 density, which is the normalization condition.

Equations

• LambdaS.Examples.Measure.halfDensity = (LambdaS.Term.inv LambdaS.Examples.m).rpow (1 / 2)

@[reducible, inline]

abbrev LambdaS.Examples.Measure.joule : UExp Base 0

Equations

• LambdaS.Examples.Measure.joule = (LambdaS.Term.mul LambdaS.Examples.kg (LambdaS.Term.mul LambdaS.Examples.m LambdaS.Examples.m)).div (LambdaS.Term.mul LambdaS.Examples.sec LambdaS.Examples.sec)

Conversion, and the ambiguity that never arises

Comp 311's unit-conversion assignment has a latent bug: with units nameable in terms of other units, convert walks a declared structure, and two routes from u to v need not agree. Λs cannot exhibit it. Conversion is a ratio of one valuation (LambdaS.Conversion), so convChain_eq makes path independence a theorem rather than a proof obligation on declarations.

What the checker enforces is the side condition (that the two units measure the same thing), and that is SameDim.

Declarations, and the conflict that cannot be declared away

unit yard = 3 foot declares a generator and an equation. Three such declarations give two routes from yard to meter, which is the Comp 311 bug. Here the redundant declaration is either arithmetically right or the system has no solution: there is never a choice of route to get wrong.

theorem LambdaS.Examples.sameDim_bu {b c : Base} (h : UnitSys.dim b = UnitSys.dim c) : SameDim Δ₀ (bu b) (bu c)

Base units of equal declared dimension are interchangeable, via dimOf_ofBase rather than decide, since kernel reduction sticks on ℚ's instance chain. The dimension equation is rfl for any two Length units.

theorem LambdaS.Examples.sameDim_m_ft : SameDim Δ₀ m ft

theorem LambdaS.Examples.sameDim_ft_m : SameDim Δ₀ ft m

def LambdaS.Examples.dYardFoot : Decl Base

unit yard = 3 foot

Equations

• LambdaS.Examples.dYardFoot = { lhs := LambdaS.Examples.Base.yard, factor := 3, pos := LambdaS.Examples.dYardFoot._proof_1, rhs := LambdaS.Examples.ft }

def LambdaS.Examples.dFootMeter : Decl Base

unit foot = 0.3048 meter

Equations

• LambdaS.Examples.dFootMeter = { lhs := LambdaS.Examples.Base.foot, factor := 3048 / 10000, pos := LambdaS.Examples.dFootMeter._proof_1, rhs := LambdaS.Examples.m }

def LambdaS.Examples.dYardMeter : Decl Base

unit yard = 0.9144 meter: the redundant declaration, stated correctly.

Equations

• LambdaS.Examples.dYardMeter = { lhs := LambdaS.Examples.Base.yard, factor := 9144 / 10000, pos := LambdaS.Examples.dYardMeter._proof_1, rhs := LambdaS.Examples.m }

def LambdaS.Examples.dYardMeterBad : Decl Base

unit yard = 0.9 meter: the same declaration, stated wrongly. This is the one that would have made convert route-dependent.

Equations

• LambdaS.Examples.dYardMeterBad = { lhs := LambdaS.Examples.Base.yard, factor := 9 / 10, pos := LambdaS.Examples.dYardMeterBad._proof_1, rhs := LambdaS.Examples.m }

theorem LambdaS.Examples.yard_forced (ψ : Scaling Base 0) (h1 : Decl.Satisfies ψ dYardFoot) (h2 : Decl.Satisfies ψ dFootMeter) (h3 : Decl.Satisfies ψ dYardMeter) : dYardFoot.factor * dFootMeter.factor = dYardMeter.factor

The consistent set forces the redundant factor. Any valuation satisfying the first two determines the third, so the second route cannot disagree with the first; it is not free to.

theorem LambdaS.Examples.yard_conflict : ¬∃ (ψ : Scaling Base 0), Decl.Satisfies ψ dYardFoot ∧ Decl.Satisfies ψ dFootMeter ∧ Decl.Satisfies ψ dYardMeterBad

The conflicting set has no valuation at all.

This is the Comp 311 bug, decided rather than papered over. The assignment's convert had to walk a declared structure and could walk the wrong way; here the configuration that would force a choice is exactly the configuration with no solution, so it is rejected at declaration time.

Dimension abbreviations, elaborated

Unit declarations constrain; dimension declarations abbreviate, and the only check they need is scoping (DimAbbrev.elabDimDefs, in LambdaS.Declare). The chain below elaborates, with Accel landing at the vector length·time⁻². The cyclic pair Velocity = Length/Time; Length = Velocity/Time is rejected at its second line for rebinding the generator Length, and a forward reference is rejected because an undefined name does not denote.

def LambdaS.Examples.dimName : String → Option Dim

The base dimensions' surface names.

Equations

• LambdaS.Examples.dimName "Length" = some LambdaS.Examples.Dim.length
• LambdaS.Examples.dimName "Mass" = some LambdaS.Examples.Dim.mass
• LambdaS.Examples.dimName "Time" = some LambdaS.Examples.Dim.time
• LambdaS.Examples.dimName x✝ = none

def LambdaS.Examples.velocityDef : String × List (DimAbbrev.Ref Dim)

Equations

• LambdaS.Examples.velocityDef = ("Velocity", [(Sum.inl LambdaS.Examples.Dim.length, 1), (Sum.inl LambdaS.Examples.Dim.time, -1)])

def LambdaS.Examples.dimChain : List (String × List (DimAbbrev.Ref Dim))

Velocity = Length/Time; Accel = Velocity/Time.

Equations

• LambdaS.Examples.dimChain = [LambdaS.Examples.velocityDef, ("Accel", [(Sum.inr "Velocity", 1), (Sum.inl LambdaS.Examples.Dim.time, -1)])]

def LambdaS.Examples.dimCycle : List (String × List (DimAbbrev.Ref Dim))

Velocity = Length/Time; Length = Velocity/Time: rebinds a generator.

Equations

• LambdaS.Examples.dimCycle = [LambdaS.Examples.velocityDef, ("Length", [(Sum.inr "Velocity", 1), (Sum.inl LambdaS.Examples.Dim.time, -1)])]

def LambdaS.Examples.primaries : List (String × (Dim ⊕ String))

Primary-unit declarations: unit meter : Length; unit second : Time; unit hertz : Frequency with Frequency an abbreviation. Elaborates; the duplicate and the unknown dimension are rejected.

Equations

• LambdaS.Examples.primaries = [("meter", Sum.inl LambdaS.Examples.Dim.length), ("second", Sum.inl LambdaS.Examples.Dim.time), ("hertz", Sum.inr "Frequency")]

def LambdaS.Examples.freqDims : List (String × DExp Dim 0)

Equations

• LambdaS.Examples.freqDims = (LambdaS.DimAbbrev.elabDimDefs LambdaS.Examples.dimName [("Frequency", [(Sum.inl LambdaS.Examples.Dim.time, -1)])]).getD []

The valuation the declarations determine, and the evaluator using it

yard_conflict says the bad set has no valuation; this is the other half, exhibited rather than asserted: the consistent set has one, written down. Its factors then reach the evaluator through evalC_convert_declared: the number the evaluator multiplies by is the number the declaration names, with no route through an informal reading of "3". The theorems below run eval at carrier ℝ, with conv ψyd as the conversion oracle; LambdaS.Algorithms runs the same evaluator at Float with the declared magnitudes transcribed.

noncomputable def LambdaS.Examples.ψyd : Scaling Base 0

The valuation meter = 1, foot = 0.3048, yard = 0.9144 (in log space).

Equations

• One or more equations did not get rendered due to their size.

theorem LambdaS.Examples.ψyd_yardFoot : Decl.Satisfies ψyd dYardFoot

theorem LambdaS.Examples.ψyd_footMeter : Decl.Satisfies ψyd dFootMeter

theorem LambdaS.Examples.ψyd_yardMeter : Decl.Satisfies ψyd dYardMeter

theorem LambdaS.Examples.yard_satisfiable : ∃ (ψ : Scaling Base 0), Decl.Satisfies ψ dYardFoot ∧ Decl.Satisfies ψ dFootMeter ∧ Decl.Satisfies ψ dYardMeter

The consistent set is satisfiable: the counterpart to yard_conflict, with the witness constructed rather than assumed.

Cycles are constraints, not definitions

Declarations carry no order and no acyclicity condition, and need none: each is an equation, the set is a simultaneous system, and a cycle is just a dependency the criterion decides. Nothing can reference an undeclared generator either, since the base units are the parameter B. The benign cycle below is satisfiable, by the same valuation as the straight set; the vicious one forces 3 = 1 and no valuation exists.

def LambdaS.Examples.dFootYard : Decl Base

unit foot = 1/3 yard, the converse of dYardFoot: a benign cycle.

Equations

• LambdaS.Examples.dFootYard = { lhs := LambdaS.Examples.Base.foot, factor := 1 / 3, pos := LambdaS.Examples.dFootYard._proof_1, rhs := LambdaS.Examples.yd }

def LambdaS.Examples.dFootYardBad : Decl Base

unit foot = yard, closing the cycle wrongly.

Equations

• LambdaS.Examples.dFootYardBad = { lhs := LambdaS.Examples.Base.foot, factor := 1, pos := LambdaS.Examples.dFootYardBad._proof_1, rhs := LambdaS.Examples.yd }

theorem LambdaS.Examples.ψyd_footYard : Decl.Satisfies ψyd dFootYard

theorem LambdaS.Examples.cycle_satisfiable : ∃ (ψ : Scaling Base 0), Decl.Satisfies ψ dYardFoot ∧ Decl.Satisfies ψ dFootYard

A benign cycle is satisfiable: yard = 3 foot and foot = 1/3 yard say the same thing, and the criterion sees a passing dependency, not a loop.

theorem LambdaS.Examples.cycle_conflict : ¬∃ (ψ : Scaling Base 0), Decl.Satisfies ψ dYardFoot ∧ Decl.Satisfies ψ dFootYardBad

A vicious cycle is rejected: yard = 3 foot and foot = yard force 3 = 1, so no valuation exists.

theorem LambdaS.Examples.one_yard_is_three_feet : ∃ (n : ℕ), evalC (conv ψyd) n [] ((Tm.ucon yd).convert yd ft) = some (Val.scalar { mag := 3, unit := ft })

One yard is three feet, on the evaluator. Evaluating (1 yd) in ft at carrier ℝ, with the conversion oracle the declarations determine, multiplies by exactly the declared 3 and lands at ft: evalC_convert_declared, instantiated. The binary runs the same eval at Float (LambdaS.Algorithms).

theorem LambdaS.Examples.one_yard_in_meters : ∃ (n : ℕ), evalC (conv ψyd) n [] ((Tm.ucon yd).convert yd m) = some (Val.scalar { mag := ↑(9144 / 10000), unit := m })

And directly to meters, by the redundant declaration: the same number the chain through feet produces, which is yard_forced made numeric.

theorem LambdaS.Examples.one_yard_in_meters_via_feet : ∃ (n : ℕ), evalC (conv ψyd) n [] (((Tm.ucon yd).convert yd ft).convert ft m) = some (Val.scalar { mag := ↑(9144 / 10000), unit := m })

The route through feet lands on the same number. ((1 yd) in ft) in m multiplies by the declared 3 and then by the declared 0.3048, and 3 × 0.3048 = 0.9144 is exactly the magnitude the direct route produces: evalC_convert_declared applied twice, the inner conversion's value read off through Decl.conv_eq_factor.

theorem LambdaS.Examples.yard_routes_agree : ∃ (n₁ : ℕ) (n₂ : ℕ), evalC (conv ψyd) n₁ [] ((Tm.ucon yd).convert yd m) = evalC (conv ψyd) n₂ [] (((Tm.ucon yd).convert yd ft).convert ft m)

The two routes agree: whatever fuel each needs, the evaluator returns the same value for one yard in meters whether it converts directly or through feet. This is path independence (conv_trans) at the evaluator, for the declared factors.

Regression: substitution under nested binders

Attempting the type-soundness proof turned up a genuine defect in Ty.subst.

Inside ∀u. τ, de Bruijn index 0 is the bound variable and 1 is the outer one, so substituting for the outer variable must leave the binder alone. The original definition recursed as τ.subst σ.weaken, which substitutes index 0 (the bound variable) and shifts the outer one down into its place. Ty.weaken had the matching defect, inserting the fresh variable at index 0 rather than past the binder.

Nothing here reached it. Every single-binder use is unaffected, and the one test with nested unit binders (twoVars) is rejected by the checker before substitution runs. The two definitions were also wrong in a way that canceled, so subst_weaken (the only theorem about them) held regardless.

It took writing the soundness proof to surface it: the composition lemma for substitution refused to hold, and the reason was that liftU had no counterpart in the quantifier case. The fix was to define subst and weaken as instances of a simultaneous substitution that lifts properly. These guards pin the corrected behavior.

That is the argument for mechanizing a calculus rather than describing one. The defect is invisible to inspection, invisible to the examples, and invisible to the one property anybody would have thought to state about it.

@[reducible, inline]

abbrev LambdaS.Examples.dLen : DExp Dim 0

Equations

• LambdaS.Examples.dLen = LambdaS.Term.ofBase LambdaS.Examples.Dim.length

@[reducible, inline]

abbrev LambdaS.Examples.polyOuter : Ty Base Dim 0 1

∀u. Q v₁: the body mentions the outer variable, not the bound one.

Equations

• LambdaS.Examples.polyOuter = LambdaS.Ty.all LambdaS.Examples.dLen (LambdaS.Ty.Q (LambdaS.Term.ofVar 1))

@[reducible, inline]

abbrev LambdaS.Examples.polyBound : Ty Base Dim 0 0

∀u. Q v₀: the body mentions the bound variable.

Equations

• LambdaS.Examples.polyBound = LambdaS.Ty.all LambdaS.Examples.dLen (LambdaS.Ty.Q (LambdaS.Term.ofVar 0))

Algebraic units, in types and in measurements

Two expressibility checks worth keeping visible, because a reader of the grammar can miss both. Unit expressions are the free abelian group: a type may be indexed by an algebraic combination of bound unit variables, and a measurement is a literal times a unit constant at any compound unit.

def LambdaS.Examples.compoundPoly : Term₀

Λu:Length. Λv:Time. λx : Q (u·v). x: a polymorphic identity at a compound unit built from two distinct bound variables. Inside the two binders, de Bruijn variable 1 is u and 0 is v.

Equations

• One or more equations did not get rendered due to their size.

def LambdaS.Examples.fiveMps : Term₀

5 m/s: a literal times the unit constant at a compound unit. The type is Q (1 · m/s), and the exponent-vector representation makes that the same index as Q (m/s); the #guard compares the vectors.

Equations

• LambdaS.Examples.fiveMps = (LambdaS.Tm.lit 5).mul (LambdaS.Tm.ucon (LambdaS.Term.div LambdaS.Examples.m LambdaS.Examples.sec))

The drift diagnostic, exercised

Three programs, three answers. Converting meters to feet and back cancels: unitDrift answers 1, and the result is unit-system independent. Converting one way does not: the drift is m/ft, and the diagnostic names it. And a sum whose branches share a variable carries the branches' shared drift.

def LambdaS.Examples.roundTrip : Term₀

x : Q m ⊢ (x in ft) in m: a round trip.

Equations

• LambdaS.Examples.roundTrip = ((LambdaS.Tm.var 0).convert LambdaS.Examples.m LambdaS.Examples.ft).convert LambdaS.Examples.ft LambdaS.Examples.m

def LambdaS.Examples.oneWay : Term₀

x : Q m ⊢ x in ft, left in feet: drifted.

Equations

• LambdaS.Examples.oneWay = (LambdaS.Tm.var 0).convert LambdaS.Examples.m LambdaS.Examples.ft

def LambdaS.Examples.roundTripDeriv : HasTy Δ₀ (scalarCtx [m]) roundTrip (Ty.Q m)

Equations

• LambdaS.Examples.roundTripDeriv = ((LambdaS.HasTy.var LambdaS.Examples.roundTripDeriv._proof_1).convert LambdaS.Examples.sameDim_m_ft).convert LambdaS.Examples.sameDim_ft_m

def LambdaS.Examples.oneWayDeriv : HasTy Δ₀ (scalarCtx [m]) oneWay (Ty.Q ft)

Equations

• LambdaS.Examples.oneWayDeriv = (LambdaS.HasTy.var LambdaS.Examples.roundTripDeriv._proof_1).convert LambdaS.Examples.sameDim_m_ft

def LambdaS.Examples.addSame : Term₀

Addition demands agreeing branch ratios, and x in ft + x in ft has them: both branches carry the drift m/ft.

Equations

• LambdaS.Examples.addSame = ((LambdaS.Tm.var 0).convert LambdaS.Examples.m LambdaS.Examples.ft).add ((LambdaS.Tm.var 0).convert LambdaS.Examples.m LambdaS.Examples.ft)

def LambdaS.Examples.addSameDeriv : HasTy Δ₀ (scalarCtx [m]) addSame (Ty.Q ft)

Equations

• One or more equations did not get rendered due to their size.

def LambdaS.Examples.addTwoVars : Term₀

x in ft + y in ft for distinct measurements x y : Q m is accepted too, with the same drift m/ft. This is the frees-at-one assignment at work: x and y are inputs, inputs rescale ideally, so each contributes the ratio 1 rather than an opaque atom, and the branch ratios are the same exponent vector. An earlier design gave every free variable an atom and declined this program, answering a stronger question than the certified theorems ask: the theorems instantiate the inputs' ratios at 1 (oneTwEnv), and at that instantiation the two branches agree.

Equations

• LambdaS.Examples.addTwoVars = ((LambdaS.Tm.var 0).convert LambdaS.Examples.m LambdaS.Examples.ft).add ((LambdaS.Tm.var 1).convert LambdaS.Examples.m LambdaS.Examples.ft)

def LambdaS.Examples.addTwoVarsDeriv : HasTy Δ₀ (scalarCtx [m, m]) addTwoVars (Ty.Q ft)

Equations

• One or more equations did not get rendered due to their size.

def LambdaS.Examples.addMixed : Term₀

What add still declines at first order: a genuine drift disagreement. x in ft + y with x : Q m and y : Q ft converts one branch and not the other, so the branch drifts are m/ft and 1, distinct exponent vectors, and the sum has no uniform drift; indeed the program is not scale-invariant. By Tw.normEq_iff_eval_eq such disagreements are the only declines at add between atom-free ratios, which is what a first-order program produces once its internal applications are normalized away (hoSum below).

Equations

• LambdaS.Examples.addMixed = ((LambdaS.Tm.var 0).convert LambdaS.Examples.m LambdaS.Examples.ft).add (LambdaS.Tm.var 1)

def LambdaS.Examples.addMixedDeriv : HasTy Δ₀ (scalarCtx [m, ft]) addMixed (Ty.Q ft)

Equations

• One or more equations did not get rendered due to their size.

def LambdaS.Examples.hoApp : Term₀

A residue of internal abstraction. An abstraction applied inside a first-order program leaves a redex behind: (λf. f x) (λy. y in ft) has the ratio m/ft under every scaling, and unitDrift names it, because deciding triviality normalizes the ratio fully (Tw.nfOne). But twistOf reduces one β-step at construction, and the redex the outer application creates, (λy. ...) 1, survives in the ratio as an app node, which Tw.flat treats as an opaque atom. The ratio as built is not atom-free; its normal form is, and the branch comparison runs on normal forms (Tw.normEq).

Equations

• One or more equations did not get rendered due to their size.

def LambdaS.Examples.hoAppDeriv : HasTy Δ₀ (scalarCtx [m]) hoApp (Ty.Q ft)

Equations

• One or more equations did not get rendered due to their size.

def LambdaS.Examples.hoSum : Term₀

Summing hoApp with x in ft, two branches worth m/ft under every scaling, is accepted at that drift: the comparison normalizes both branches first, so the residue is reduced away and two unit expressions are compared. Before the comparison ran on normal forms this sum was declined, an atom against a unit.

Equations

• LambdaS.Examples.hoSum = LambdaS.Tm.add LambdaS.Examples.hoApp ((LambdaS.Tm.var 0).convert LambdaS.Examples.m LambdaS.Examples.ft)

def LambdaS.Examples.hoSumDeriv : HasTy Δ₀ (scalarCtx [m]) hoSum (Ty.Q ft)

Equations

• LambdaS.Examples.hoSumDeriv = LambdaS.Examples.hoAppDeriv.add ((LambdaS.HasTy.var LambdaS.Examples.roundTripDeriv._proof_1).convert LambdaS.Examples.sameDim_m_ft)

theorem LambdaS.Examples.div_self_unit (u : UExp Base 0) : Term.div u u = 1

Division of a unit by itself is the trivial unit: exponent vectors subtract to zero.

def LambdaS.Examples.logRoundTrip : Term₀

log ((x in ft)/(x in ft)): the argument's conversions cancel, so it is drift-free, and a drift-free value at Q 1 is declaration-independent under every rescaling. Its logarithm is declaration-independent too, and the analysis now accepts it: log runs the add-style check against the literal ratio 1 rather than declining unconditionally.

Equations

• LambdaS.Examples.logRoundTrip = (((LambdaS.Tm.var 0).convert LambdaS.Examples.m LambdaS.Examples.ft).div ((LambdaS.Tm.var 0).convert LambdaS.Examples.m LambdaS.Examples.ft)).log

def LambdaS.Examples.logRoundTripDeriv : HasTy Δ₀ (scalarCtx [m]) logRoundTrip (Ty.Q 1)

Equations

• One or more equations did not get rendered due to their size.

def LambdaS.Examples.logDrifting : Term₀

What log still declines: an argument at Q 1 whose ratio genuinely drifts. (x in ft)/y for x : Q m, y : Q ft is dimensionless but carries the drift m/ft, and no ratio describes how its logarithm moves.

Equations

• LambdaS.Examples.logDrifting = (((LambdaS.Tm.var 0).convert LambdaS.Examples.m LambdaS.Examples.ft).div (LambdaS.Tm.var 1)).log

def LambdaS.Examples.logDriftingDeriv : HasTy Δ₀ (scalarCtx [m, ft]) logDrifting (Ty.Q 1)

Equations

• One or more equations did not get rendered due to their size.

def LambdaS.Examples.betaShared : Term₀

β at the ratio level. The left branch wraps x in ft in an identity application, so its ratio arrives as a β-redex; twistOf reduces it on the spot (Tw.appE), the flat form sees the bare exponent vector m/ft rather than an opaque atom, and the sum is accepted with the shared drift. Before the reduction this program was declined for a spelling difference.

Equations

• One or more equations did not get rendered due to their size.

def LambdaS.Examples.betaSharedDeriv : HasTy Δ₀ (scalarCtx [m]) betaShared (Ty.Q ft)

Equations

• One or more equations did not get rendered due to their size.

def LambdaS.Examples.lamKernel : Term₀

The λ-wrapped kernel: λx:Q m. λy:Q m. (x in ft) + (y in ft). Closed, so unitDrift has no context to pin; unitDriftLam strips the two leading binders, treats x and y as inputs, and reports the kernel's drift, the same verdict addTwoVars receives as an open term: by unitDriftLam_eq_unitDrift the two spellings' verdicts are one computation, and unitDriftLam_spec makes the verdict exact for the applied kernel.

Equations

• One or more equations did not get rendered due to their size.

def LambdaS.Examples.lamKernelDeriv : HasTy Δ₀ [] lamKernel ((Ty.Q m).arrow ((Ty.Q m).arrow (Ty.Q ft)))

Equations

• One or more equations did not get rendered due to their size.

def LambdaS.Examples.addAssoc : Term₀

Branch ratios compare up to the unit algebra, not up to spelling. The two branches below convert the same product of meters to feet, placed differently: the first converts the product once at m·m, the second converts each factor at m. Their ratio terms differ syntactically (the syntactic check Tw.beq rejects exactly this pair), but Tw.normEq flattens both to the unit vector m²/ft² with atom exponent 1 on each of x and y, so the analysis answers, and the answer is the drift the branches share.

Equations

• One or more equations did not get rendered due to their size.

theorem LambdaS.Examples.sameDim_mm_ftft : SameDim Δ₀ (Term.mul m m) (Term.mul ft ft)

def LambdaS.Examples.addAssocDeriv : HasTy Δ₀ (scalarCtx [m, m]) addAssoc (Ty.Q (Term.mul ft ft))

Equations

• One or more equations did not get rendered due to their size.

The generic caster

Under ∀δ. ∀u:δ, conversion out of u is not blocked wholesale: it can target any expression of dimension δ, and in particular another variable bounded by the same δ. The generic caster

Λδ. Λu:δ. Λv:δ. λx:Q u. convert x u v

typechecks, at the polymorphic cast type, and instantiating both unit quantifiers at same-dimension ground units yields an ordinary cast. What remains rejected is conversion from u to a concrete unit, since no concrete unit has dimension δ. The caster is a term the two abstraction theorems separate: coherent rescalings give u and v one shared factor and leave it invariant; independent factors move it.

def LambdaS.Examples.caster : Term₀

Λδ. Λu:δ. Λv:δ. λx:Q u. convert x u v.

Equations

• One or more equations did not get rendered due to their size.

Drift through the unit quantifiers

The caster's ratio is a family: at bind shape it is indexed by the instantiating unit, and its body's drift is the open exponent vector u/v. The normalizer reads the family at chosen units, so reading it at two fresh unit variables exhibits the open vector itself; and an instantiation is a recorded uapp that twistOf performs on the spot (Tw.uappE).

def LambdaS.Examples.driftOf (Γ : Ctx Base Dim 0 0) (e : Term₀) : Option (UExp Base 0)

Checker plus diagnostic, for the guards below: the drift of a quantity-typed term over Γ, or none where either the checker or the analysis declines.

Equations

• One or more equations did not get rendered due to their size.

def LambdaS.Examples.casterRound : Term₀

The polymorphic round trip: Λδ. Λu:δ. Λv:δ. λx:Q u. (x in v) in u.

Equations

• One or more equations did not get rendered due to their size.

The coherent fundamental theorem, at a rescaling that moves a dimension

fundamental quantifies over dimension rescalings Φ. This section instantiates it at a Φ that is not the identity: it multiplies every Length by 2 and fixes Mass and Time. The term is a conversion from meters to feet, so the instantiation exercises the convert case of the theorem, the case that requires coherence.

noncomputable def LambdaS.Examples.ΦDouble : Scaling Dim 0

A dimension rescaling that doubles Length and fixes Mass and Time. In log coordinates the Length entry is log 2, which is nonzero, so this rescaling moves a dimension.

Equations

• One or more equations did not get rendered due to their size.

theorem LambdaS.Examples.ΦDouble_moves_length : ΦDouble.base Dim.length ≠ 0

ΦDouble is not the trivial rescaling: it moves the Length dimension.

noncomputable def LambdaS.Examples.ψDouble : Scaling Base 0

The unit rescaling ΦDouble pulls back to: each base unit scales by the factor of its dimension, so meter, foot, and yard all scale by 2 while kilogram and second are fixed.

Equations

• One or more equations did not get rendered due to their size.

theorem LambdaS.Examples.ψDouble_factors : ψDouble.Factors Δ₀ ΦDouble

ψDouble factors through dimension via ΦDouble, by construction: its base field is definitionally the sum Scaling.Factors requires.

def LambdaS.Examples.cvtMFDeriv : HasTy Δ₀ [] (Tm.lam (Ty.Q m) (cvtTm m ft)) ((Ty.Q m).arrow (Ty.Q ft))

λ(x : Q m). convert x m ft, closed and parametric: the conversion is the only non-variable subterm, and Tm.Parametric admits convert.

Equations

• LambdaS.Examples.cvtMFDeriv = (LambdaS.cvtDeriv LambdaS.Examples.sameDim_m_ft).lam

theorem LambdaS.Examples.fundamental_at_moving_rescale (V : Scaling Base 0) : RelCo Δ₀ ΦDouble ((Ty.Q m).arrow (Ty.Q ft)) ψDouble (den V cvtMFDeriv PUnit.unit) (den (V.comp ψDouble) cvtMFDeriv PUnit.unit)

fundamental, instantiated at a rescaling that moves a dimension. The conversion program is related to itself under ΦDouble, which rescales Length by 2. Unfolding RelCo at the arrow type: for inputs related by ψDouble.scale m, the outputs are related by ψDouble.scale ft. The convert case of fundamental carries the content here, since the conversion factor conv V m ft must be invariant under the rescaling, and coherence of ψDouble (every Length unit scales by the same factor 2) is exactly what makes it so.

Vector and matrix literals

Until the introduction forms existed, vectors and matrices entered only as free variables: the calculus could consume its data but not construct it. These guards exercise the forms that close the gap: a State vector built one component at a time, matrices built one row at a time, the rejections the rules impose, and the zero-row width story that mnil's annotation exists to tell.

@[reducible, inline]

abbrev LambdaS.Examples.pmom : UExp Base 0

The momentum unit of State, kg·m/s.

Equations

• LambdaS.Examples.pmom = (LambdaS.Term.mul LambdaS.Examples.kg LambdaS.Examples.m).div LambdaS.Examples.sec

def LambdaS.Examples.stateVec : Term₀

The State vector as a literal: position 1.3 m consed onto momentum 21 kg·m/s.

Equations

• LambdaS.Examples.stateVec = ((LambdaS.Tm.lit 1.3).mul (LambdaS.Tm.ucon LambdaS.Examples.m)).vcons (((LambdaS.Tm.lit 21).mul (LambdaS.Tm.ucon LambdaS.Examples.pmom)).vcons LambdaS.Tm.vnil)

def LambdaS.Examples.wrongVec : Term₀

Equations

• LambdaS.Examples.wrongVec = ((LambdaS.Tm.lit 1.3).mul (LambdaS.Tm.ucon LambdaS.Examples.m)).vcons (LambdaS.Tm.vcons LambdaS.Examples.duration LambdaS.Tm.vnil)

def LambdaS.Examples.toTime : Term₀

A map from State to W = [sec] as a literal: one row whose entry i carries sec / δ_State(i), which is the rank-one condition the mcons rule checks.

Equations

• One or more equations did not get rendered due to their size.

def LambdaS.Examples.fromTime : Term₀

A two-row map the other way, one row per component of State.

Equations

• One or more equations did not get rendered due to their size.

Row extraction

mrow is the elimination form for Lin, dual to mcons as idx is to vcons. Introduction and elimination meet on the nose: row 0 of mcons w r M has exactly the type r was checked at. Without it a matrix could be built and applied but never read, so no closed term could name a matrix element, a column, or a transpose.

def LambdaS.Examples.fromTimeT : Term₀

A transpose, at fixed arity. The transpose of a map V → W is the map W* → V* on the dual spaces, whose units are the reciprocals. Here fromTime : Lin W State, so its transpose lives at Lin [1/m, 1/pmom] [1/sec], and the one row of the transpose is the one column of fromTime, assembled entry by entry from row extractions. The mcons rule checks that the entries m/sec and pmom/sec are exactly (1/sec) / (1/m) and (1/sec) / (1/pmom), which is where the dual spaces come from.

Equations

• One or more equations did not get rendered due to their size.

Drift for vectors and matrices

The drift of a vector is a vector of drifts, and the drift of a matrix is a matrix of drifts. A literal whose component converts one way is reported with a drift vector naming the component's ratio, not declined; idx projects the component's drift back out; and a matrix application carries the add-style agreement condition per output row, across the summed index, so a row whose summands carry genuinely different drifts is declined.

def LambdaS.Examples.driftVec : Term₀

x : Q m, t : Q s ⊢ ⟨x in ft, t⟩: a vector literal whose first component converts one way and whose second does not.

Equations

• LambdaS.Examples.driftVec = ((LambdaS.Tm.var 0).convert LambdaS.Examples.m LambdaS.Examples.ft).vcons ((LambdaS.Tm.var 1).vcons LambdaS.Tm.vnil)

def LambdaS.Examples.driftVecDeriv : HasTy Δ₀ (scalarCtx [m, sec]) driftVec (Ty.vec [ft, sec])

Equations

• One or more equations did not get rendered due to their size.

def LambdaS.Examples.driftIdx : Term₀

Indexing the drifting component recovers exactly the scalar diagnosis the one-way conversion would get on its own.

Equations

• LambdaS.Examples.driftIdx = LambdaS.Tm.idx LambdaS.Examples.driftVec 0

def LambdaS.Examples.driftIdxDeriv : HasTy Δ₀ (scalarCtx [m, sec]) driftIdx (Ty.Q ft)

Equations

• LambdaS.Examples.driftIdxDeriv = LambdaS.Examples.driftVecDeriv.idx LambdaS.Examples.driftIdxDeriv._proof_1

def LambdaS.Examples.driftIdx1Deriv : HasTy Δ₀ (scalarCtx [m, sec]) (Tm.idx driftVec 1) (Ty.Q sec)

Equations

• LambdaS.Examples.driftIdx1Deriv = LambdaS.Examples.driftVecDeriv.idx LambdaS.Examples.driftIdx1Deriv._proof_1

@[reducible, inline]

abbrev LambdaS.Examples.Γv : Ctx Base Dim 0 0

A context for the matrix-application examples: a length, and a dimensionless entry at exactly the unit ft/ft the rank-one row space demands.

Equations

• LambdaS.Examples.Γv = LambdaS.scalarCtx [LambdaS.Examples.m, LambdaS.Term.div LambdaS.Examples.ft LambdaS.Examples.ft]

def LambdaS.Examples.mappOk : Term₀

A 1×2 matrix applied to a drifting vector, agreement holding: both argument components carry the same variable through the same conversion, and both row entries are the same variable, so the two products across the sum agree and the output row's drift is their common value.

Equations

• One or more equations did not get rendered due to their size.

def LambdaS.Examples.mappOkDeriv : HasTy Δ₀ Γv mappOk (Ty.vec [ft])

Equations

• One or more equations did not get rendered due to their size.

def LambdaS.Examples.mappOkIdxDeriv : HasTy Δ₀ Γv (Tm.idx mappOk 0) (Ty.Q ft)

Equations

• LambdaS.Examples.mappOkIdxDeriv = LambdaS.Examples.mappOkDeriv.idx LambdaS.Examples.mappOkIdxDeriv._proof_1

@[reducible, inline]

abbrev LambdaS.Examples.Γv₂ : Ctx Base Dim 0 0

The same shape with distinct measurements in the argument components: the mapp analogue of addTwoVars. Under the frees-at-one assignment both components contribute the ratio 1 through their own variable, so the products across the sum agree at the exponent vector m/ft and the application is accepted; an earlier design gave x and y distinct atoms and declined it.

Equations

• LambdaS.Examples.Γv₂ = LambdaS.scalarCtx [LambdaS.Examples.m, LambdaS.Examples.m, LambdaS.Term.div LambdaS.Examples.ft LambdaS.Examples.ft]

def LambdaS.Examples.mappTwoVars : Term₀

Equations

• One or more equations did not get rendered due to their size.

def LambdaS.Examples.mappTwoVarsDeriv : HasTy Δ₀ Γv₂ mappTwoVars (Ty.vec [ft])

Equations

• One or more equations did not get rendered due to their size.

def LambdaS.Examples.mappTwoVarsIdxDeriv : HasTy Δ₀ Γv₂ (Tm.idx mappTwoVars 0) (Ty.Q ft)

Equations

• LambdaS.Examples.mappTwoVarsIdxDeriv = LambdaS.Examples.mappTwoVarsDeriv.idx LambdaS.Examples.mappOkIdxDeriv._proof_1

@[reducible, inline]

abbrev LambdaS.Examples.Γv₃ : Ctx Base Dim 0 0

What mapp still declines at first order: a genuine drift disagreement across the summed index, the mapp analogue of addMixed. One argument component converts (x in ft, drift m/ft) and the other is already in feet (drift 1), so the row's two products carry distinct exponent vectors and no uniform output drift exists.

Equations

• LambdaS.Examples.Γv₃ = LambdaS.scalarCtx [LambdaS.Examples.m, LambdaS.Examples.ft, LambdaS.Term.div LambdaS.Examples.ft LambdaS.Examples.ft]

def LambdaS.Examples.mappMixed : Term₀

Equations

• One or more equations did not get rendered due to their size.

def LambdaS.Examples.mappMixedDeriv : HasTy Δ₀ Γv₃ mappMixed (Ty.vec [ft])

Equations

• One or more equations did not get rendered due to their size.

Case study: a mixed-unit ballistics kernel

The drift diagnostic has so far run on one-line programs. This section runs it on a small straight-line kernel with the shape real conversion bugs have: field data arrives in imperial units, the physics is metric, and the report goes back out in imperial units.

Inputs: a distance in feet (variable 0) and a time in seconds (variable 1). The shared pipeline converts the distance to meters, forms the velocity in m/s, and computes the kinetic energy per unit mass v²/2 in m²/s². Four reporting variants, four verdicts, all decided at build time:

• kernelConsistent converts the metric energy back to ft²/s² for the report. The input conversion cancels against the output conversion through the arithmetic, and unitDrift certifies the whole multi-step routine drift-free: by den_indep_of_driftFree, the reported number does not depend on the declared unit magnitudes.
• kernelOneWay reports in metric, so the input conversion is never undone. The diagnostic names the exact ratio, ft²/m²: the drift ft/m of one foot-to-meter conversion, squared through v².
• kernelMixedPaths computes v² twice in one sum: once by converting the input and squaring the metric velocity, once by squaring the imperial velocity and converting the square at ft²/s². The branch ratios differ syntactically (Tw.beq rejects the pair), but Tw.normEq flattens both to the exponent vector ft²/m² with atom exponents x² / t², so the sum is accepted and carries the branches' shared drift.
• kernelRoot takes the speed back out of the energy with a square root, and the analysis follows it through: Tw.qpow lifts the energy's drift ft²/m² to the power 1/2, and the diagnostic names the speed's drift ft/m exactly. The exponent arithmetic is sound because ratio values are positive by type (SemScalar), the same positivity fundamental uses through relQ_rpow.

Every routine typechecks by a #guard on the inferred type, and every drift claim is a #guard on unitDrift, so a wrong claim fails the build.

@[reducible, inline]

abbrev LambdaS.Examples.Ballistics.Γb : Ctx Base Dim 0 0

The kernel's input context: a distance in feet and a time in seconds.

Equations

• LambdaS.Examples.Ballistics.Γb = LambdaS.scalarCtx [LambdaS.Examples.ft, LambdaS.Examples.sec]

@[reducible, inline]

abbrev LambdaS.Examples.Ballistics.mps : UExp Base 0

Metric velocity, m/s.

Equations

• LambdaS.Examples.Ballistics.mps = LambdaS.Term.div LambdaS.Examples.m LambdaS.Examples.sec

@[reducible, inline]

abbrev LambdaS.Examples.Ballistics.fps : UExp Base 0

Imperial velocity, ft/s.

Equations

• LambdaS.Examples.Ballistics.fps = LambdaS.Term.div LambdaS.Examples.ft LambdaS.Examples.sec

@[reducible, inline]

abbrev LambdaS.Examples.Ballistics.mps2 : UExp Base 0

Metric energy per unit mass, m²/s².

Equations

• LambdaS.Examples.Ballistics.mps2 = LambdaS.Term.mul LambdaS.Examples.Ballistics.mps LambdaS.Examples.Ballistics.mps

@[reducible, inline]

abbrev LambdaS.Examples.Ballistics.fps2 : UExp Base 0

Imperial energy per unit mass, ft²/s².

Equations

• LambdaS.Examples.Ballistics.fps2 = LambdaS.Term.mul LambdaS.Examples.Ballistics.fps LambdaS.Examples.Ballistics.fps

theorem LambdaS.Examples.Ballistics.sameDim_mps2_fps2 : SameDim Δ₀ mps2 fps2

Meter and foot share a dimension, so velocity squared does too: the side condition the energy conversions below discharge, proved by the homomorphism laws for dimOf rather than by decide.

theorem LambdaS.Examples.Ballistics.sameDim_fps2_mps2 : SameDim Δ₀ fps2 mps2

The shared pipeline

Real code shares subterms, so the variants do too: one converted distance, one metric velocity, one imperial velocity, each with its derivation.

def LambdaS.Examples.Ballistics.distM : Term₀

The distance input, converted to meters: x in m.

Equations

• LambdaS.Examples.Ballistics.distM = (LambdaS.Tm.var 0).convert LambdaS.Examples.ft LambdaS.Examples.m

def LambdaS.Examples.Ballistics.velM : Term₀

Metric velocity: the converted distance over the raw time input.

Equations

• LambdaS.Examples.Ballistics.velM = LambdaS.Tm.div LambdaS.Examples.Ballistics.distM (LambdaS.Tm.var 1)

def LambdaS.Examples.Ballistics.velF : Term₀

Imperial velocity: the raw inputs, no conversion.

Equations

• LambdaS.Examples.Ballistics.velF = (LambdaS.Tm.var 0).div (LambdaS.Tm.var 1)

def LambdaS.Examples.Ballistics.distMDeriv : HasTy Δ₀ Γb distM (Ty.Q m)

Equations

• LambdaS.Examples.Ballistics.distMDeriv = (LambdaS.HasTy.var LambdaS.Examples.Ballistics.distMDeriv._proof_1).convert LambdaS.Examples.sameDim_ft_m

def LambdaS.Examples.Ballistics.velMDeriv : HasTy Δ₀ Γb velM (Ty.Q mps)

Equations

• LambdaS.Examples.Ballistics.velMDeriv = LambdaS.Examples.Ballistics.distMDeriv.div (LambdaS.HasTy.var LambdaS.Examples.Ballistics.velMDeriv._proof_1)

def LambdaS.Examples.Ballistics.velFDeriv : HasTy Δ₀ Γb velF (Ty.Q fps)

Equations

• LambdaS.Examples.Ballistics.velFDeriv = (LambdaS.HasTy.var LambdaS.Examples.Ballistics.distMDeriv._proof_1).div (LambdaS.HasTy.var LambdaS.Examples.Ballistics.velMDeriv._proof_1)

@[reducible, inline]

abbrev LambdaS.Examples.Ballistics.driftSq : UExp Base 0

The one-way drift both drifted variants share: one foot-to-meter conversion, squared through v².

Equations

• LambdaS.Examples.Ballistics.driftSq = (LambdaS.Term.mul LambdaS.Examples.ft LambdaS.Examples.ft).div (LambdaS.Term.mul LambdaS.Examples.m LambdaS.Examples.m)

Variant 1: convert in, compute, convert out

def LambdaS.Examples.Ballistics.kernelConsistent : Term₀

(1/2) · ((velM · velM) in ft²/s²): metric energy, reported imperial. The ft → m conversion inside velM enters the ratio twice through the square; the output conversion contributes m²/ft² and cancels it exactly.

Equations

• One or more equations did not get rendered due to their size.

def LambdaS.Examples.Ballistics.kernelConsistentDeriv : HasTy Δ₀ Γb kernelConsistent (Ty.Q (Term.mul 1 fps2))

Equations

• One or more equations did not get rendered due to their size.

Variant 2: convert in, report metric

def LambdaS.Examples.Ballistics.kernelOneWay : Term₀

(1/2) · (velM · velM): the same computation, left in m²/s².

Equations

• LambdaS.Examples.Ballistics.kernelOneWay = (LambdaS.Tm.lit (1 / 2)).mul (LambdaS.Tm.mul LambdaS.Examples.Ballistics.velM LambdaS.Examples.Ballistics.velM)

def LambdaS.Examples.Ballistics.kernelOneWayDeriv : HasTy Δ₀ Γb kernelOneWay (Ty.Q (Term.mul 1 mps2))

Equations

• LambdaS.Examples.Ballistics.kernelOneWayDeriv = LambdaS.HasTy.lit.mul (LambdaS.Examples.Ballistics.velMDeriv.mul LambdaS.Examples.Ballistics.velMDeriv)

Variant 3: the same quantity, two ways, in one sum

def LambdaS.Examples.Ballistics.kernelMixedPaths : Term₀

(1/2) · (velM·velM + ((velF·velF) in m²/s²)): the left branch converts the input then squares, the right squares the raw imperial velocity then converts once at ft²/s². Averaging the two would divide by a further literal; adding them keeps the branch comparison the interesting step.

Equations

• One or more equations did not get rendered due to their size.

def LambdaS.Examples.Ballistics.kernelMixedPathsDeriv : HasTy Δ₀ Γb kernelMixedPaths (Ty.Q (Term.mul 1 mps2))

Equations

• One or more equations did not get rendered due to their size.

Variant 4: the rooted variant, followed through the root

def LambdaS.Examples.Ballistics.kernelRoot : Term₀

√(2 · kernelOneWay): the speed recovered from the energy. Well-typed at m/s (rational powers are total over ℚ exponents), and inside the analysis: Tw.qpow lifts the energy's drift to the power.

Equations

• LambdaS.Examples.Ballistics.kernelRoot = LambdaS.Tm.pow (1 / 2) ((LambdaS.Tm.lit 2).mul LambdaS.Examples.Ballistics.kernelOneWay)

def LambdaS.Examples.Ballistics.kernelRootDeriv : HasTy Δ₀ Γb kernelRoot (Ty.Q ((Term.mul 1 (Term.mul 1 mps2)).rpow (1 / 2)))

Equations

• LambdaS.Examples.Ballistics.kernelRootDeriv = (LambdaS.HasTy.lit.mul LambdaS.Examples.Ballistics.kernelOneWayDeriv).pow

A Jacobi rotation, and what the units force

The reason ifle was added. Section 5 classifies dimensioned maps, and svd_entry_const says a singular value decomposition needs a uniform space because sorting singular values requires a shared unit. That is a claim about types, and until now nothing in the development ran an actual kernel against it. This does.

The setting is the symmetric eigenvalue problem, the fourth Hart class: A : V ⊸ dual V on a uniform V, so every entry carries 1 / (V j * V i) and, uniformly, m⁻². A Jacobi sweep annihilates the off-diagonal entry by a rotation whose angle is computed from the entries themselves.

def LambdaS.Examples.U2 : Sp Base 0

A uniform two-component space.

Equations

• LambdaS.Examples.U2 = [LambdaS.Examples.m, LambdaS.Examples.m]

def LambdaS.Examples.U2d : Sp Base 0

Its dual, carrying reciprocal units.

Equations

• LambdaS.Examples.U2d = [LambdaS.Term.div 1 LambdaS.Examples.m, LambdaS.Term.div 1 LambdaS.Examples.m]

def LambdaS.Examples.ΓA : Ctx Base Dim 0 0

The context the kernel runs in: one symmetric matrix.

Equations

• LambdaS.Examples.ΓA = [LambdaS.Ty.lin LambdaS.Examples.U2 LambdaS.Examples.U2d]

def LambdaS.Examples.tau : Term₀

The tangent parameter of the rotation angle.

Every entry carries m⁻², so the difference is legal and the ratio is dimensionless. The rotation is forced to be a pure number, and it is the uniformity of the space that forces it: on a non-uniform space the numerator below does not typecheck.

Equations

• LambdaS.Examples.tau = ((((LambdaS.Tm.var 0).mrow 1).idx 1).add ((LambdaS.Tm.lit (-1)).mul (((LambdaS.Tm.var 0).mrow 0).idx 0))).div ((LambdaS.Tm.lit 2).mul (((LambdaS.Tm.var 0).mrow 0).idx 1))

def LambdaS.Examples.tanRot : Term₀

t = sign(τ) / (|τ| + √(1 + τ²)), the standard stable form, written with the two branches the sign requires. This is the term that could not be written before ifle.

Equations

• One or more equations did not get rendered due to their size.

def LambdaS.Examples.cosRot : Term₀

Cosine and sine of the rotation, both dimensionless.

Equations

• LambdaS.Examples.cosRot = (LambdaS.Tm.lit 1).div (LambdaS.Tm.pow (1 / 2) ((LambdaS.Tm.lit 1).add (LambdaS.Tm.mul LambdaS.Examples.tanRot LambdaS.Examples.tanRot)))

def LambdaS.Examples.sinRot : Term₀

Equations

• LambdaS.Examples.sinRot = LambdaS.Tm.mul LambdaS.Examples.tanRot LambdaS.Examples.cosRot

def LambdaS.Examples.rot : Term₀

The rotation itself, an endomorphism of the uniform space. Its entries carry V j / V i = 1, so a rotation is a matrix of plain numbers, which is entry_id_diag and entry_perm_prod seen from the term side.

Equations

• One or more equations did not get rendered due to their size.

def LambdaS.Examples.rotT : Term₀

Its transpose, assembled column by column with mrow. The rotation is orthogonal, so this is also its inverse, and it lands at the dual spaces.

Equations

• One or more equations did not get rendered due to their size.

def LambdaS.Examples.sweep : Term₀

One Jacobi sweep, the congruence Rᵀ A R. It needs both extensions at once: mrow to build the transpose and ifle to choose the angle. The type is preserved exactly, so sweeps compose.

Equations

• LambdaS.Examples.sweep = LambdaS.Tm.comp LambdaS.Examples.rotT ((LambdaS.Tm.var 0).comp LambdaS.Examples.rot)

What the units refuse

The rotation algebra above is not merely typeable on a uniform space; it is typeable only there. On a non-uniform space the two diagonal entries carry different units, so the numerator of tau is an addition at unequal units and the term is rejected before any question of correctness arises. Hart's uniformity condition is visible here as a typing constraint of this particular Jacobi kernel. svd_entry_const supplies the unit identity; the checker guard under ΓN below demonstrates the rejection. No typed general SVD algorithm is mechanized.

def LambdaS.Examples.N2 : Sp Base 0

Equations

• LambdaS.Examples.N2 = [LambdaS.Examples.m, LambdaS.Examples.sec]

def LambdaS.Examples.N2d : Sp Base 0

Equations

• LambdaS.Examples.N2d = [LambdaS.Term.div 1 LambdaS.Examples.m, LambdaS.Term.div 1 LambdaS.Examples.sec]

def LambdaS.Examples.ΓN : Ctx Base Dim 0 0

Equations

• LambdaS.Examples.ΓN = [LambdaS.Ty.lin LambdaS.Examples.N2 LambdaS.Examples.N2d]

What the units say about the stopping test

A convergence test compares the off-diagonal to a tolerance, and the tolerance must carry the entries' unit. Both forms below typecheck; parametricity distinguishes how their tolerances are supplied.

A relative tolerance scales a quantity already in hand by a dimensionless factor. It names no unit, so it stays inside the parametric fragment and Theorem 6.1 applies to the kernel.

The fixed absolute tolerance below is written using a named unit constant ucon, which Tm.Parametric excludes. The kernel still typechecks and runs, but the abstraction theorem no longer applies. An absolute tolerance passed as an input could remain parametric and would rescale with the inputs; absolute tolerances are not excluded in general.

def LambdaS.Examples.stopRelative : Term₀

Equations

• LambdaS.Examples.stopRelative = (((LambdaS.Tm.var 0).mrow 0).idx 1).ifle ((LambdaS.Tm.lit 1e-9).mul (((LambdaS.Tm.var 0).mrow 0).idx 0)) (LambdaS.Tm.var 0) LambdaS.Examples.sweep

def LambdaS.Examples.stopAbsolute : Term₀

Equations

• One or more equations did not get rendered due to their size.

The diagnostic at the sweep

unitDriftGen takes an arbitrary context and a .lin result, so it applies to the kernel exactly as written, matrix argument and matrix result. This is the guard that says so.

What the experiment found

Three things the kernel confirms, one of which took a generalization to reach.

Confirmed: uniformity is not a hypothesis but a precondition for writing the code at all, and the parametric fragment separates a relative tolerance from an absolute one. Both were predicted before the kernel was written.

Not confirmed at first: the drift analysis did not reach this program. unitDrift is typed HasTy Δ (scalarCtx us) e (.Q u) → Option (UExp B k), so it wanted scalar arguments and a scalar result, and sweep has a matrix argument and a matrix result. No rearrangement of the kernel helped, because the restriction was on the shape of the judgment rather than on the term.

That was a coverage gap between two parts of the development rather than an unsoundness, and the diagnosis said where to look: twistOf, the analysis underneath, is indexed by Ctx.shapes and already handled vector and matrix shapes, which is why Tw.agree needed cases at those shapes at all. Only the wrapper was scalar-only. The gap mattered because it fell exactly between two claims the development makes: LambdaS.Map classifies dimensioned linear operators, the diagnostic decides invariance, and the kernels motivating the first sat outside the second.

The wrapper did generalize, on both axes. unitDriftLin reports one ratio per entry of a matrix result, and unitDriftGen drops the scalar-context restriction as well, so it applies to sweep exactly as written. The guard above runs it and finds every entry trivial, which is the answer the congruence of rotations should have: the kernel converts nowhere, so nothing drifts. Neither axis needed a new theorem, and Twist.scaling turned out to have been fully general already.

The kernel restated over scalar arguments

Written when the gap above was open, as the workaround: pass the entries rather than the matrix, so that the context is a scalarCtx and only the result shape stands between the kernel and the diagnostic. unitDriftGen has since removed the need for it. It stays because it exercises a genuinely different path, a scalar context with a matrix result, and because the same rotation algebra written two ways is a check that the shapes are doing no work the units are not.

def LambdaS.Examples.e2 : UExp Base 0

The entry unit of a symmetric matrix on the uniform space.

Equations

• LambdaS.Examples.e2 = (LambdaS.Term.div 1 LambdaS.Examples.m).div LambdaS.Examples.m

def LambdaS.Examples.ΓS : Ctx Base Dim 0 0

Three scalar arguments, which is a scalarCtx.

Equations

• LambdaS.Examples.ΓS = [LambdaS.Ty.Q LambdaS.Examples.e2, LambdaS.Ty.Q LambdaS.Examples.e2, LambdaS.Ty.Q LambdaS.Examples.e2]

def LambdaS.Examples.asymm : Term₀

The matrix assembled from them, symmetric by construction.

Equations

• One or more equations did not get rendered due to their size.

def LambdaS.Examples.tauS : Term₀

Equations

• LambdaS.Examples.tauS = ((LambdaS.Tm.var 2).add ((LambdaS.Tm.lit (-1)).mul (LambdaS.Tm.var 0))).div ((LambdaS.Tm.lit 2).mul (LambdaS.Tm.var 1))

def LambdaS.Examples.tanS : Term₀

Equations

• One or more equations did not get rendered due to their size.

def LambdaS.Examples.cosS : Term₀

Equations

• LambdaS.Examples.cosS = (LambdaS.Tm.lit 1).div (LambdaS.Tm.pow (1 / 2) ((LambdaS.Tm.lit 1).add (LambdaS.Tm.mul LambdaS.Examples.tanS LambdaS.Examples.tanS)))

def LambdaS.Examples.sinS : Term₀

Equations

• LambdaS.Examples.sinS = LambdaS.Tm.mul LambdaS.Examples.tanS LambdaS.Examples.cosS

def LambdaS.Examples.rotS : Term₀

Equations

• One or more equations did not get rendered due to their size.

def LambdaS.Examples.rotTS : Term₀

Equations

• One or more equations did not get rendered due to their size.

def LambdaS.Examples.sweepS : Term₀

The sweep over a scalar context. Everything unitDrift asks of the context is satisfied here; only the result shape remains.

Equations

• LambdaS.Examples.sweepS = LambdaS.Tm.comp LambdaS.Examples.rotTS (LambdaS.Tm.comp LambdaS.Examples.asymm LambdaS.Examples.rotS)