The fundamental theorem, and what conversion costs

Every well-typed term is related to itself. This is what makes the logical relation say anything: without it, Rel is a definition and the free theorems are unproved conjectures about particular functions.

The point of this file

There are two fundamental theorems here, and the difference between them is the whole story about conversion.

• fundamental_free: a convert-free term is related to itself under every scaling. This is Kennedy's theorem, and it is what the Pi theorem consumes.
• fundamental: an arbitrary term is related to itself under every coherent scaling, one that factors through dimension.

Conversion is the only operation in Λs that can observe a unit, so it is the only operation that can pay. And cvt_rel_iff_coherent shows the price is exactly right rather than merely sufficient: for a single conversion applied to a nonzero argument, the relation holds if and only if the scaling identifies the two units. Coherence is not a convenient hypothesis that makes the proof go through; it is what the term forces.

That is the gap in the literature. Kennedy (POPL'97) and Atkey–Johann–Kennedy (POPL'13) have unconditional abstraction theorems because nothing in their calculi observes a unit: there is no conversion operator to break anything. Practical systems have conversion and no invariance theory. Λs has both, and this file is where they meet.

The semantics runs on typing derivations

den recurses over HasTy, which is Type-valued precisely so that it can: a denotation is data, and a Prop-valued derivation cannot eliminate into Type. There is no second, intrinsically typed syntax: the term a derivation types is its index, so the checker and the semantics are the same calculus by construction rather than by a bridging theorem. Derivations being unique (Subsingleton (HasTy Δ Γ e τ)) is what makes the denotation a function of the term, and what lets the syntactic side conditions below be predicates on terms rather than on derivations.

Unit and dimension application transport along Ty.den_subst and Ty.den_substDim. Those casts are not an artifact of the encoding: they are where "instantiating a unit moves no magnitudes" is discharged.

Why the denotation takes a valuation

den is parameterized by a Scaling B k: the declared valuation, what each base unit is worth. Nothing but convert reads it (den_indep proves exactly that; note that ucon does not read it), but convert must: a conversion factor is a ratio of declared magnitudes and cannot be recovered from the term alone.

This is also why the fundamental theorem relates den V to den (V.comp ψ) rather than den to itself. Rescaling is a change of the declared unit system, so it acts on the valuation as well as on the environment. For convert-free terms the distinction is invisible, which is precisely den_indep, with den_eq_of_convertFree its closed-scalar corollary, closed because an open term may have a free variable of quantified type whose family the environment chooses non-constantly.

No unit constants, and that is not an oversight

Tm.Parametric excludes ucon. Unit constants break parametricity, and the reason is worth stating because it explains a feature of Kennedy's calculus that otherwise looks arbitrary.

ucon m : Q m denotes the number 1. The relation at Q m demands the two readings differ by ψ(m), so self-relatedness would need 1 = ψ(m) · 1, false for any scaling that actually moves the meter. A term that can name a unit can detect a rescaling.

This is why Λu has no unit constants, and why Kennedy's own "converting kg into lb" example rewrites the literals: 1.0<kg> becomes 2.2<lb>. The rescaling acts on the program text, not only on the environment. Dimensioned values enter through the environment (as free variables), never by naming a unit.

Scope

Every form of Λs except ucon: variables, abstraction, application, literals, the arithmetic, rational powers, spaces and linear maps, the vector and matrix introduction forms, conversion, and unit and dimension abstraction and application. The one exclusion is Tm.Parametric's, argued in the previous section; a vector or matrix literal is parametric exactly when its component scalars are, and the ones that name units via ucon are not.

Rational powers are parametric. relQ_rpow holds with no sign hypothesis on the value, because the scale factor is positive by construction and a positive factor distributes over rpow for every real base (mul_rpow_of_pos_left): on a negative base, rpow is the real part of the principal complex power, and the cosine factor is common to both sides. The caveat carries over unchanged: on a negative argument the primitive's value is not a root at all ((-8) ^ (1/3 : ℝ) denotes 1 under rpow; the Float carrier returns NaN there, treating the point as it treats division by zero, see LambdaS.Num), so the theorems certify covariance of Mathlib's total extension. Kennedy's model avoids the point by taking every magnitude positive, at the price of excluding signed quantities; Λs admits them and pays with the undefined point.

From the paper's long form: The Price of Conversion

The paper's tag long-form carries this section in full; it is reproduced here, converted to Markdown, so the documentation develops what the paper now summarizes. Section references name the module that carries the section; theorem references name the declaration.

In this section, we develop the denotational semantics of Λs and prove two abstraction theorems. The first says that a parametric, convert-free term is invariant under every rescaling of the units (the theorem “Abstraction, convert-free” (fundamental_free)). The second says that a parametric term is invariant, conversions included, under the coherent rescalings, those that respect dimension (the theorem “Abstraction, coherent” (fundamental)). The gap between the two is the price of conversion, and for the canonical one-conversion program it closes to an equivalence. Conversion is the only construct that reads the declared magnitude of a unit, so it is the only construct that loses invariance, and the theorem “Single-conversion invariance” (cvt_rel_iff_coherent) identifies exactly the rescalings under which it keeps it. Note that multiplication cannot substitute, although conversion's semantics is multiplication by the magnitude ratio V(u)/V(v): a literal denotes the number the programmer wrote and 1_u denotes the number 1, so every product multiplies by a valuation-independent number, and no convert-free term denotes the factor (convert_not_definable). The artifact runs the sharpest instance: 1_yd/1_ft evaluates to the magnitude 1, at unit yd/ft, under every declaration table; ask for it in one and the declared 3 appears, by the one construct allowed to fetch it (ydPerFt, ydPerFtIn1) (see note 1). The engine of all three results is the family semantics of “Denotation over Derivations” below: unit abstraction denotes a family indexed by magnitude, and conversion is what makes the family vary.

Note 1. one is the SI's name: quantities of dimension one carry “the unit one, symbol 1,” which the brochure calls the neutral element of any system of units [BIPM 2019]; here it is the empty exponent vector. The object-oriented design [Allen et al. 2004] named it Unity.

Denotation over Derivations

Units are erased from the semantic universe: a quantity denotes a real number, a vector a function from indices to reals, and a unit abstraction Λu:d. e denotes a family ℝ → ⟦τ⟧, indexed by the log-magnitude the bound unit is declared to have (here τ ranges over the types of Figure 1 of the paper (the UExp, DExp, Ty, and Tm inductives of Syntax.lean), and ⟦τ⟧ is its set of denotations). The family is the case that did not exist in prior mechanizations. It must exist: Λu:Length. convert x u meter means something different depending on how big u is, and in a calculus without conversion there is nothing for the family to depend on. That is why the mechanized semantics of Kennedy [2008], which discards units entirely (“units ignored”), could interpret a unit abstraction as just its body, and ours cannot: the body's meaning depends on the bound unit's magnitude. We index by the log-magnitude because taking logs turns the multiplicative rescaling action into translation: unit abstraction then denotes a family over an additive parameter, the invariance theory becomes linear algebra, and the Pi theorem of “Dimensional Analysis” (PiTheorem.lean) consumes it in this form.

The denotation ⟦𝒟⟧_V is defined by recursion on typing derivations 𝒟 (which the theorem “Completeness” (check_eq, Typing.lean) makes a recursion on terms), parameterized by a valuation V giving each base unit its declared magnitude. Valuations, like rescalings, are represented logarithmically, so family indices live in log space. Exactly two clauses consult V: conversion multiplies by conv_V(u,v), and unit application samples a family at the log-magnitude V assigns the instantiating unit; only conversion reads V as a number that reaches the computed value. Hence a closed convert-free term of quantity type denotes the same number under every valuation (den_eq_of_convertFree; at higher types, den_indep). A program that does not convert cannot tell you how big a meter is.

The Two Abstraction Theorems

A rescaling ψ assigns each base unit and each unit variable a positive factor, extended homomorphically; it acts on quantity types by x ↦ ψ(u)· x. For example, let ψ send meter to 0.9144 · meter and fix every other base unit (the yard rescaling: 0.9144 is the artifact's declared magnitude for the yard). Then ψ multiplies every value of type Q meter by 0.9144, every value of type Q meter/second by 0.9144 as well, and every value of type Q meter² by 0.9144²: the factor for a composite unit is the base factor raised to the unit's exponent. The invariance proofs use a logical relation ℛ, which relates each value of type Q u to its rescaling by ψ(u); it is standard at first order. At ∀u:d. τ it relates two families at every factor the bound variable might receive, with the rescaled side read at a shifted index: families are indexed by log-magnitude, and rescaling the instantiating unit by k translates that index by log k. The relation therefore compares one family at a with the other at a + logψ(u). We say a term is parametric when it contains no unit constant 1_u.

Theorem (Abstraction, convert-free; fundamental_free). Every parametric, convert-free term is ℛ-related to itself under every rescaling ψ: rescaling the inputs by their units' factors rescales the output by its unit's factor.

This is Kennedy's theorem [1997], here at a calculus with vectors, linear maps, and both quantifiers. We call the theorem's equation, rescaled inputs to rescaled output, a term's scaling law. The side condition parametric excludes exactly one construct. Unit constants are excluded because 1_u : Q u denotes the number 1, and self-relatedness would demand 1 = ψ(u): a term that can name a unit can detect a rescaling! This is why Kennedy's calculus has no unit constants, and why his own kilograms-to-pounds example rewrites the program's literals rather than its environment; Λs keeps the construct because a language needs it, and the side condition is the cost. Zero alone is scale-invariant (see note 2), and we meet the exception again in the theorem “Single-conversion invariance” (cvt_rel_iff_coherent) and throughout “Accumulated Ratios, and a Decidable Diagnostic” (Twist.lean).

Note 2. Whether there is one zero or many is the subject of Russell's Chapter XXII [§§172–178, Russell 1903]. He canvasses a limit construction that makes zero single and, in his phrase, “not one among the magnitudes whose zero it is” (§176), then concludes that each kind of magnitude has its own zero (§177). Λs takes both sides, and the seam is exactly the one between types and semantics: 0 : Q m and 0 : Q s are distinct terms at distinct types, but they denote the same real number, the unique fixed point of every rescaling. The action is free on the nonzero reals and trivial at 0; this is Russell's remark in algebraic form. That is why the theorem “Single-conversion invariance” (cvt_rel_iff_coherent) must assume a nonzero denotation: at zero the conversion factor is unobservable, so a converting program and a parametric one agree. The affine scales [Allen et al. 2004] (temperatures, timestamps, where zero is not preserved) are the case in which Russell's per-class answer is the right one; see the paper's conclusion. His zero quantities require 0 of any unit to equal them, and Atkey et al. [2013]'s relational interpretation acquires an explicit x = 0 disjunct for polymorphic zero.

Powers, restricted to positive values in Kennedy's 2008 Coq model, need no exclusion. For a positive factor k, the identity (k· x)^q = k^q· x^q holds at every real x under the artifact's semantics (mul_rpow_of_pos_left), where a power of a negative argument denotes the real part of the principal complex power, |x|^qcos(qπ). On negative arguments that value is not a root: (-8)^(1/3) denotes 1, and the binary returns NaN there. The theorem therefore certifies covariance of the total function, not root-ness. The two concerns are separable: covariance is what abstraction theorems trade in, and the real-part convention differs from real odd roots as well as from floating-point NaNs. And the artifact instantiates the strengthened statement at λ x:Q u · u. √x (sqrt_scales).

For terms that do convert, invariance under all rescalings is false and should be: converting meters to feet multiplies by a specific declared number, and a rescaling that moves the meter but not the foot changes the answer. The right class is the rescalings that cannot separate interchangeable units. Recall that a rescaling is coherent when it factors through dimension; the artifact carries the factoring as data: a coherent rescaling of units is a rescaling Φ of dimensions, read back through dim. The two readings agree: a rescaling that cannot separate interchangeable units factors through some Φ, and conversely (coherent_iff_factors). The relation for coherent rescalings, ℛᶜᵒ_Φ, is ℛ with one change, at the quantifier: the factor the bound unit receives is not quantified over but determined, namely Φ(d) under Λu:d. Coherence is not an assumption imposed at the binder: the binder's dimension annotation determines the factor. The two relations agree at quantifier-free types.

Theorem (Abstraction, coherent; fundamental). Every parametric term, conversions included, is ℛᶜᵒ_Φ-related to itself for every dimension rescaling Φ.

The artifact exercises the theorem at a rescaling that doubles every length, applied to a meters-to-feet conversion, the case in which coherence has content (fundamental_at_moving_rescale).

The theorems “Abstraction, convert-free” (fundamental_free) and the theorem “Abstraction, coherent” (fundamental) bound the cost of conversion from above. A converse is needed to show the bound is tight, and the converse holds per term and per rescaling rather than in aggregate. It is stated over ℛ, since the program's type is quantifier-free, where the two relations agree:

Theorem (Single-conversion invariance; cvt_rel_iff_coherent). For the one-conversion program convert x u v, its sole free variable x:Q u given any nonzero value by the environment, and any rescaling ψ: the relation holds at ψ if and only if ψ(u) = ψ(v).

Note that the nonzero hypothesis is necessary: it is the zero exception again. Beyond it there is no slack. A conversion that actually converts is detectable, in that some rescaling changes what the program computes; a rescaling that agrees on the converted pair is exactly one under which nothing changes. Conversion is not definable from the parametric constructs (no convert-free term denotes it: convert_not_definable), and the coherence hypothesis of the theorem “Abstraction, coherent” (fundamental) is forced by the term rather than by the proof: the rescalings under which a conversion is invariant are exactly those with ψ(u) = ψ(v), which is the equation every coherent rescaling satisfies at a same-dimension pair.

@[reducible]

def LambdaS.Env {B D : Type} {j k : ℕ} : Ctx B D j k → Type

An environment: a denotation for each type in the context.

@[reducible] for the same reason Ty.den is: the elaborator must see through it to project a pair.

Equations

• LambdaS.Env [] = PUnit.{1}
• LambdaS.Env (τ :: Γ) = (τ.den × LambdaS.Env Γ)

def LambdaS.Env.lookup {B D : Type} {j k : ℕ} {Γ : Ctx B D j k} {τ : Ty B D j k} (n : ℕ) : Γ[n]? = some τ → Env Γ → τ.den

Looking a variable up in an environment, given the proof that the context assigns it that type. This replaces a separate well-typed-variable inductive: HasTy.var already carries the lookup as a hypothesis, so nothing else is needed.

Equations

• LambdaS.Env.lookup x_1 x_2 x_7 = absurd x_2 ⋯
• LambdaS.Env.lookup 0 h ρ = ⋯ ▸ ρ.1
• LambdaS.Env.lookup n.succ h ρ = LambdaS.Env.lookup n h ρ.2

def LambdaS.Env.weaken {B D : Type} {j k : ℕ} {Γ : Ctx B D j k} : Env Γ → Env Γ.weaken

Reading an environment under a unit binder. The magnitudes are untouched; only the types they are indexed by move, and Ty.den_weaken says that costs nothing.

Equations

• x_2.weaken = PUnit.unit
• ρ.weaken = (cast ⋯ ρ.1, ρ.2.weaken)

def LambdaS.Env.weakenDim {B D : Type} {j k : ℕ} {Γ : Ctx B D j k} : Env Γ → Env Γ.weakenDim

Reading an environment under a dimension binder.

Equations

• x_2.weakenDim = PUnit.unit
• ρ.weakenDim = (cast ⋯ ρ.1, ρ.2.weakenDim)

def LambdaS.denDapp {B D : Type} {j k : ℕ} {τ : Ty B D (j + 1) k} (d : DExp D j) (x : τ.allDim.den) : (τ.substDim d).den

Transport a denotation across a dimension instantiation. Phrased with the quantified type on the argument so that elaboration reads the body's type off the derivation rather than having to guess it.

Equations

• LambdaS.denDapp d x = cast ⋯ x

noncomputable def LambdaS.den {B D : Type} [Fintype B] [UnitSys B D] {j k : ℕ} {Δ : DCtx D j k} {Γ : Ctx B D j k} {e : Tm B D j k} {τ : Ty B D j k} : Scaling B k → HasTy Δ Γ e τ → Env Γ → τ.den

The denotation, over typing derivations. Units are erased; only magnitudes remain.

The valuation V is read by convert and by nothing else; ucon denotes 1 without consulting it. Under a unit binder it is extended by Scaling.cons, which is what gives Λu:δ. e its family: the body is denoted once for each magnitude the bound unit might be declared to have, and e[μ] selects the one at V's reading of μ.

Unit and dimension application transport along Ty.den_subst and Ty.den_substDim. Those casts are the erasure content of the definition: they are where "instantiating a unit moves no magnitudes" is discharged.

def LambdaS.RelEnv {B D : Type} [Fintype B] {j k : ℕ} (Γ : Ctx B D j k) : Scaling B k → Env Γ → Env Γ → Prop

Two environments are related when they are related pointwise.

Equations

• LambdaS.RelEnv [] x✝ x_5 x_6 = True
• LambdaS.RelEnv (τ :: Γ) x✝ ρ ρ' = (LambdaS.Rel τ x✝ ρ.1 ρ'.1 ∧ LambdaS.RelEnv Γ x✝ ρ.2 ρ'.2)

The relation for coherent rescalings

Rel at ∀u:δ. τ quantifies over every scaling of the bound variable. That is right for convert-free terms, which cannot observe one, and wrong as soon as conversion is admitted: Λu:Length. convert x u meter is related to itself only when the bound unit is rescaled the way meter is.

RelCo is that relation. It is indexed by a scaling of dimensions, which is what a coherent rescaling really is, and then the ∀ case needs no side condition at all: the factor the bound unit receives is Φ δ, determined rather than quantified. The two relations agree at quantifier-free types.

def LambdaS.RelCo {B D : Type} [Fintype B] [Fintype D] {j k : ℕ} : DCtx D j k → Scaling D j → (τ : Ty B D j k) → Scaling B k → τ.den → τ.den → Prop

The logical relation for coherent rescalings.

Equations

• LambdaS.RelCo x✝² x✝¹ (LambdaS.Ty.Q u) x✝ x_12 y = (y = x✝.scale u * x_12)
• LambdaS.RelCo x✝² x✝¹ (a.arrow b) x✝ f g = ∀ (x y : a.den), LambdaS.RelCo x✝² x✝¹ a x✝ x y → LambdaS.RelCo x✝² x✝¹ b x✝ (f x) (g y)
• LambdaS.RelCo x✝² x✝¹ (LambdaS.Ty.vec V) x✝ v w = ∀ (i : Fin (List.length V)), w i = x✝.scale (List.get V i) * v i
• LambdaS.RelCo x✝² x✝¹ (LambdaS.Ty.lin V W) x✝ A C = ∀ (a : Fin (List.length W)) (i : Fin (List.length V)), C a i = x✝.scale (List.get W a) / x✝.scale (List.get V i) * A a i
• LambdaS.RelCo x✝² x✝¹ (LambdaS.Ty.all d τ) x✝ F G = ∀ (r : ℝ), LambdaS.RelCo (LambdaS.DCtx.cons d x✝²) x✝¹ τ (x✝.cons (x✝¹.logScale d)) (F r) (G (r + x✝¹.logScale d))
• LambdaS.RelCo x✝² x✝¹ τ.allDim x✝ F G = ∀ (t : ℝ), LambdaS.RelCo x✝².weakenDim (x✝¹.cons t) τ x✝ F G

def LambdaS.Respects {B D : Type} [Fintype B] [UnitSys B D] {j k j₀ k₀ : ℕ} (Δ : DCtx D j k) (Δ₀ : DCtx D j₀ k₀) (η : Fin k → UExp B k₀) (δ : Fin j → DExp D j₀) : Prop

The substitution respects the declared dimensions: each unit substituted has the dimension the source context gave the variable it replaces.

Equations

• LambdaS.Respects Δ Δ₀ η δ = ∀ (i : Fin k), LambdaS.substU δ (Δ i) = LambdaS.dimOf Δ₀ (η i)

theorem LambdaS.relCo_ground {B D : Type} [Fintype B] [Fintype D] [UnitSys B D] {j k : ℕ} (τ : Ty B D j k) {j₀ k₀ : ℕ} (Δ : DCtx D j k) (Δ₀ : DCtx D j₀ k₀) (Φ₀ : Scaling D j₀) (η : Fin k → UExp B k₀) (δ : Fin j → DExp D j₀) (ψ : Scaling B k₀) : Respects Δ Δ₀ η δ → ∀ {x y : τ.den} {x' y' : (Ty.ground η δ τ).den}, x ≍ x' → y ≍ y' → (RelCo Δ₀ Φ₀ (Ty.ground η δ τ) ψ x' y' ↔ RelCo Δ (Φ₀.pull δ) τ (ψ.pull η) x y)

RelCo transports along grounding, exactly as Rel does, with the dimension scaling pulled back alongside the unit scaling.

theorem LambdaS.relCo_subst {B D : Type} [Fintype B] [Fintype D] [UnitSys B D] {j k : ℕ} (Δ : DCtx D j k) (Φ : Scaling D j) (τ : Ty B D j (k + 1)) (σ : UExp B k) (ψ : Scaling B k) {x y : τ.den} {x' y' : (τ.subst σ).den} (hx : x ≍ x') (hy : y ≍ y') : RelCo Δ Φ (τ.subst σ) ψ x' y' ↔ RelCo (DCtx.cons (dimOf Δ σ) Δ) Φ τ (ψ.cons (ψ.logScale σ)) x y

Instantiating a unit variable, for RelCo.

theorem LambdaS.relCo_weaken {B D : Type} [Fintype B] [Fintype D] [UnitSys B D] {j k : ℕ} (Δ : DCtx D j k) (Φ : Scaling D j) (d : DExp D j) (τ : Ty B D j k) (ψ : Scaling B k) (s : ℝ) {x y : τ.den} {x' y' : τ.weaken.den} (hx : x ≍ x') (hy : y ≍ y') : RelCo (DCtx.cons d Δ) Φ τ.weaken (ψ.cons s) x' y' ↔ RelCo Δ Φ τ ψ x y

Weakening under a unit binder, for RelCo.

theorem LambdaS.relCo_substDim {B D : Type} [Fintype B] [Fintype D] [UnitSys B D] {j k : ℕ} (Δ : DCtx D j k) (Φ : Scaling D j) (τ : Ty B D (j + 1) k) (d : DExp D j) (ψ : Scaling B k) {x y : τ.den} {x' y' : (τ.substDim d).den} (hx : x ≍ x') (hy : y ≍ y') : RelCo Δ Φ (τ.substDim d) ψ x' y' ↔ RelCo Δ.weakenDim (Φ.cons (Φ.logScale d)) τ ψ x y

Instantiating a dimension variable, for RelCo.

theorem LambdaS.relCo_weakenDim {B D : Type} [Fintype B] [Fintype D] [UnitSys B D] {j k : ℕ} (Δ : DCtx D j k) (Φ : Scaling D j) (t : ℝ) (τ : Ty B D j k) (ψ : Scaling B k) {x y : τ.den} {x' y' : τ.weakenDim.den} (hx : x ≍ x') (hy : y ≍ y') : RelCo Δ.weakenDim (Φ.cons t) τ.weakenDim ψ x' y' ↔ RelCo Δ Φ τ ψ x y

Weakening under a dimension binder, for RelCo.

def LambdaS.RelEnvCo {B D : Type} [Fintype B] [Fintype D] {j k : ℕ} (Γ : Ctx B D j k) : DCtx D j k → Scaling D j → Scaling B k → Env Γ → Env Γ → Prop

Environments related coherently, pointwise.

Equations

• LambdaS.RelEnvCo [] x✝² x✝¹ x✝ x_9 x_10 = True
• LambdaS.RelEnvCo (τ :: Γ) x✝² x✝¹ x✝ ρ ρ' = (LambdaS.RelCo x✝² x✝¹ τ x✝ ρ.1 ρ'.1 ∧ LambdaS.RelEnvCo Γ x✝² x✝¹ x✝ ρ.2 ρ'.2)

theorem LambdaS.relCo_lookup {B D : Type} [Fintype B] [Fintype D] {j k : ℕ} {Γ : Ctx B D j k} {τ : Ty B D j k} (n : ℕ) (h : Γ[n]? = some τ) {Δ : DCtx D j k} {Φ : Scaling D j} {ψ : Scaling B k} {ρ ρ' : Env Γ} : RelEnvCo Γ Δ Φ ψ ρ ρ' → RelCo Δ Φ τ ψ (Env.lookup n h ρ) (Env.lookup n h ρ')

theorem LambdaS.relEnvCo_weaken {B D : Type} [Fintype B] [Fintype D] [UnitSys B D] {j k : ℕ} (Γ : Ctx B D j k) (Δ : DCtx D j k) (Φ : Scaling D j) (d : DExp D j) (ψ : Scaling B k) (s : ℝ) (ρ ρ' : Env Γ) : RelEnvCo Γ Δ Φ ψ ρ ρ' → RelEnvCo Γ.weaken (DCtx.cons d Δ) Φ (ψ.cons s) ρ.weaken ρ'.weaken

theorem LambdaS.relEnvCo_weakenDim {B D : Type} [Fintype B] [Fintype D] [UnitSys B D] {j k : ℕ} (Γ : Ctx B D j k) (Δ : DCtx D j k) (Φ : Scaling D j) (t : ℝ) (ψ : Scaling B k) (ρ ρ' : Env Γ) : RelEnvCo Γ Δ Φ ψ ρ ρ' → RelEnvCo Γ.weakenDim Δ.weakenDim (Φ.cons t) ψ ρ.weakenDim ρ'.weakenDim

Two syntactic conditions

Both are properties of terms, not of derivations. That is legitimate because derivations are unique (Subsingleton (HasTy Δ Γ e τ)), so a predicate on terms is exactly as expressive and considerably simpler.

def LambdaS.Tm.Parametric {B D : Type} {j k : ℕ} : Tm B D j k → Prop

A term is parametric when it never names a unit.

The exclusion is forced. ucon u : Q u denotes the number 1, so self-relatedness would demand 1 = ψ(u) · 1, false for any scaling that actually moves the unit. A term that can name a unit can detect a rescaling. This is why Kennedy's calculus has no unit constants, and why his "converting kg into lb" example rewrites the literals rather than the environment: 1.0<kg> becomes 2.2<lb>. Λs does have unit constants, because a language needs them; the cost is that they sit outside the invariance theory, and this predicate is where that is recorded.

pow is not excluded. Its scaling law is relQ_rpow, which needs no sign condition on the value: the scale factor is positive, and a positive factor distributes over rpow for every real base (mul_rpow_of_pos_left). On a negative argument the primitive does not compute a root (under rpow it is the real part of the principal complex power; at Float it is NaN), and the fundamental theorem certifies covariance of that total function.

Equations

• (LambdaS.Tm.var a).Parametric = True
• (LambdaS.Tm.lam a b).Parametric = b.Parametric
• (f.app a).Parametric = (f.Parametric ∧ a.Parametric)
• (LambdaS.Tm.lit a).Parametric = True
• (LambdaS.Tm.ucon a).Parametric = False
• (a.mul b).Parametric = (a.Parametric ∧ b.Parametric)
• (a.div b).Parametric = (a.Parametric ∧ b.Parametric)
• (a.add b).Parametric = (a.Parametric ∧ b.Parametric)
• (a.ifle b t f).Parametric = (a.Parametric ∧ b.Parametric ∧ t.Parametric ∧ f.Parametric)
• (LambdaS.Tm.pow a a_1).Parametric = a_1.Parametric
• (a.idx a_1).Parametric = a.Parametric
• (a.mrow a_1).Parametric = a.Parametric
• (f.mapp x_5).Parametric = (f.Parametric ∧ x_5.Parametric)
• (f.comp g).Parametric = (f.Parametric ∧ g.Parametric)
• LambdaS.Tm.vnil.Parametric = True
• (e.vcons v).Parametric = (e.Parametric ∧ v.Parametric)
• (LambdaS.Tm.mnil a).Parametric = True
• (LambdaS.Tm.mcons a r M).Parametric = (r.Parametric ∧ M.Parametric)
• a.log.Parametric = a.Parametric
• a.exp.Parametric = a.Parametric
• (LambdaS.Tm.ulam a b).Parametric = b.Parametric
• (f.uapp a).Parametric = f.Parametric
• b.dlam.Parametric = b.Parametric
• (f.dapp a).Parametric = f.Parametric
• (a.convert a_1 a_2).Parametric = a.Parametric

def LambdaS.Tm.ConvertFree {B D : Type} {j k : ℕ} : Tm B D j k → Prop

A term is convert-free when it contains no conversion.

This is the syntactic condition that decides which fundamental theorem applies, and it is a property of terms rather than of types: no type forces a term to convert. That is why the parametricity split does not live in the quantifier.

Equations

• (LambdaS.Tm.var a).ConvertFree = True
• (LambdaS.Tm.lam a b).ConvertFree = b.ConvertFree
• (f.app a).ConvertFree = (f.ConvertFree ∧ a.ConvertFree)
• (LambdaS.Tm.lit a).ConvertFree = True
• (LambdaS.Tm.ucon a).ConvertFree = True
• (a.mul b).ConvertFree = (a.ConvertFree ∧ b.ConvertFree)
• (a.div b).ConvertFree = (a.ConvertFree ∧ b.ConvertFree)
• (a.add b).ConvertFree = (a.ConvertFree ∧ b.ConvertFree)
• (a.ifle b t f).ConvertFree = (a.ConvertFree ∧ b.ConvertFree ∧ t.ConvertFree ∧ f.ConvertFree)
• (LambdaS.Tm.pow a a_1).ConvertFree = a_1.ConvertFree
• (a.idx a_1).ConvertFree = a.ConvertFree
• (a.mrow a_1).ConvertFree = a.ConvertFree
• (f.mapp x_5).ConvertFree = (f.ConvertFree ∧ x_5.ConvertFree)
• (f.comp g).ConvertFree = (f.ConvertFree ∧ g.ConvertFree)
• LambdaS.Tm.vnil.ConvertFree = True
• (e.vcons v).ConvertFree = (e.ConvertFree ∧ v.ConvertFree)
• (LambdaS.Tm.mnil a).ConvertFree = True
• (LambdaS.Tm.mcons a r M).ConvertFree = (r.ConvertFree ∧ M.ConvertFree)
• a.log.ConvertFree = a.ConvertFree
• a.exp.ConvertFree = a.ConvertFree
• (LambdaS.Tm.ulam a b).ConvertFree = b.ConvertFree
• (f.uapp a).ConvertFree = f.ConvertFree
• b.dlam.ConvertFree = b.ConvertFree
• (f.dapp a).ConvertFree = f.ConvertFree
• (a.convert a_1 a_2).ConvertFree = False

theorem LambdaS.rel_lookup {B D : Type} [Fintype B] {j k : ℕ} {Γ : Ctx B D j k} {τ : Ty B D j k} (n : ℕ) (h : Γ[n]? = some τ) {ψ : Scaling B k} {ρ ρ' : Env Γ} : RelEnv Γ ψ ρ ρ' → Rel τ ψ (Env.lookup n h ρ) (Env.lookup n h ρ')

Variable lookup respects the relation.

theorem LambdaS.relEnv_weaken {B D : Type} [Fintype B] {j k : ℕ} (Γ : Ctx B D j k) (ψ : Scaling B k) (s : ℝ) (ρ ρ' : Env Γ) : RelEnv Γ ψ ρ ρ' → RelEnv Γ.weaken (ψ.cons s) ρ.weaken ρ'.weaken

Weakening an environment preserves relatedness, at whatever factor the fresh unit variable is given. This is what lets the body of a Λu appeal to the induction hypothesis.

theorem LambdaS.relEnv_weakenDim {B D : Type} [Fintype B] {j k : ℕ} (Γ : Ctx B D j k) (ψ : Scaling B k) (ρ ρ' : Env Γ) : RelEnv Γ ψ ρ ρ' → RelEnv Γ.weakenDim ψ ρ.weakenDim ρ'.weakenDim

The same under a dimension binder, where nothing moves at all.

Independence of the valuation

A convert-free term cannot read how big a meter is. Stating that as "it denotes the same thing under V and V'" is too naive once unit abstraction is in the language: at e[μ] the two readings consult the family at V μ and at V' μ, which are different points. For a Λu body the family is constant and nothing goes wrong, but a free variable of quantified type has whatever family the environment supplies, and that need not be constant.

The fix is the usual one: state it as a logical relation. Indep is equality at every observable type and, at ∀u:δ. τ, relates the two families at independent indices, which is exactly the constancy the naive statement silently assumed.

def LambdaS.Indep {B D : Type} {j k : ℕ} (τ : Ty B D j k) : τ.den → τ.den → Prop

Two denotations are independent of the valuation when they agree observably, and their unit-indexed families agree at any two indices.

Equations

• LambdaS.Indep (LambdaS.Ty.Q a) x_7 y = (x_7 = y)
• LambdaS.Indep (a.arrow b) f g = ∀ (x y : a.den), LambdaS.Indep a x y → LambdaS.Indep b (f x) (g y)
• LambdaS.Indep (LambdaS.Ty.vec a) v w = (v = w)
• LambdaS.Indep (LambdaS.Ty.lin a a_1) A C = (A = C)
• LambdaS.Indep (LambdaS.Ty.all a τ) F G = ∀ (r r' : ℝ), LambdaS.Indep τ (F r) (G r')
• LambdaS.Indep τ.allDim F G = LambdaS.Indep τ F G

theorem LambdaS.eq_iff_of_heq {α β : Sort u_1} {x y : α} {x' y' : β} (hx : x ≍ x') (hy : y ≍ y') : x' = y' ↔ x = y

Heterogeneous equalities transfer an equation across a type equality.

theorem LambdaS.indep_ground {B D : Type} {j k : ℕ} (τ : Ty B D j k) {j₀ k₀ : ℕ} (η : Fin k → UExp B k₀) (δ : Fin j → DExp D j₀) {x y : τ.den} {x' y' : (Ty.ground η δ τ).den} : x ≍ x' → y ≍ y' → (Indep (Ty.ground η δ τ) x' y' ↔ Indep τ x y)

Independence transports along grounding. Simpler than rel_ground, because Indep does not mention units at all.

def LambdaS.IndepEnv {B D : Type} {j k : ℕ} (Γ : Ctx B D j k) : Env Γ → Env Γ → Prop

Environments independent of the valuation, pointwise.

Equations

• LambdaS.IndepEnv [] x_3 x_4 = True
• LambdaS.IndepEnv (τ :: Γ) ρ ρ' = (LambdaS.Indep τ ρ.1 ρ'.1 ∧ LambdaS.IndepEnv Γ ρ.2 ρ'.2)

theorem LambdaS.indep_lookup {B D : Type} {j k : ℕ} {Γ : Ctx B D j k} {τ : Ty B D j k} (n : ℕ) (h : Γ[n]? = some τ) {ρ ρ' : Env Γ} : IndepEnv Γ ρ ρ' → Indep τ (Env.lookup n h ρ) (Env.lookup n h ρ')

theorem LambdaS.indepEnv_weaken {B D : Type} {j k : ℕ} (Γ : Ctx B D j k) (ρ ρ' : Env Γ) : IndepEnv Γ ρ ρ' → IndepEnv Γ.weaken ρ.weaken ρ'.weaken

theorem LambdaS.indepEnv_weakenDim {B D : Type} {j k : ℕ} (Γ : Ctx B D j k) (ρ ρ' : Env Γ) : IndepEnv Γ ρ ρ' → IndepEnv Γ.weakenDim ρ.weakenDim ρ'.weakenDim

theorem LambdaS.den_indep {B D : Type} [Fintype B] [UnitSys B D] {j k : ℕ} {Δ : DCtx D j k} {Γ : Ctx B D j k} {e : Tm B D j k} {τ : Ty B D j k} (d : HasTy Δ Γ e τ) : e.ConvertFree → ∀ (V V' : Scaling B k) {ρ ρ' : Env Γ}, IndepEnv Γ ρ ρ' → Indep τ (den V d ρ) (den V' d ρ')

A convert-free term cannot read the valuation.

Note that ucon is not excluded: naming a unit breaks parametricity, but it does not read how big that unit is: ucon u denotes 1 whatever u is worth. Only convert consults the valuation, which is the precise sense in which units are static.

theorem LambdaS.den_eq_of_convertFree {B D : Type} [Fintype B] [UnitSys B D] {j k : ℕ} {Δ : DCtx D j k} {e : Tm B D j k} {u : UExp B k} (d : HasTy Δ [] e (Ty.Q u)) (hf : e.ConvertFree) (V V' : Scaling B k) : den V d PUnit.unit = den V' d PUnit.unit

The valuation is invisible to closed convert-free terms. A program that does not convert cannot tell you how big a meter is.

This is the precise sense in which units are static, and it is stated for closed terms because that is where it is true: an open term may have a free variable of quantified type whose family the environment chooses non-constantly, and then the two readings land at different indices. den_indep is the general form.

theorem LambdaS.fundamental {B D : Type} [Fintype B] [Fintype D] [UnitSys B D] {j k : ℕ} {Δ : DCtx D j k} {Γ : Ctx B D j k} {e : Tm B D j k} {τ : Ty B D j k} (d : HasTy Δ Γ e τ) : e.Parametric → ∀ (V ψ : Scaling B k) (Φ : Scaling D j), ψ.Factors Δ Φ → ∀ {ρ ρ' : Env Γ}, RelEnvCo Γ Δ Φ ψ ρ ρ' → RelCo Δ Φ τ ψ (den V d ρ) (den (V.comp ψ) d ρ')

The fundamental theorem, for coherent rescalings.

Every parametric term (conversions and all) is related to itself at its type, under every rescaling that factors through dimension.

convert is the only operation that pays, and this is where it pays: the case is conv_invariant_of_coherent together with coherence at the converted pair. Every other case is the convert-free proof unchanged, read at RelCo.

Note what the Λu case does not need: no side condition, no quantification over admissible extensions. The factor the bound unit receives is Φ δ, determined by its dimension, because a coherent rescaling is a rescaling of dimensions. That is the sense in which coherence is exactly what conversion under a binder forces.

theorem LambdaS.fundamental_free {B D : Type} [Fintype B] [UnitSys B D] {j k : ℕ} {Δ : DCtx D j k} {Γ : Ctx B D j k} {e : Tm B D j k} {τ : Ty B D j k} (d : HasTy Δ Γ e τ) : e.Parametric → e.ConvertFree → ∀ (V ψ : Scaling B k) {ρ ρ' : Env Γ}, RelEnv Γ ψ ρ ρ' → Rel τ ψ (den V d ρ) (den (V.comp ψ) d ρ')

The fundamental theorem, unconditionally, for convert-free terms.

Every parametric, convert-free term is related to itself at its type, under every scaling. This is Kennedy's theorem, and it is the version the Pi theorem consumes, now at the whole calculus rather than a first-order fragment, so the quantifier cases are present and carry their weight.

Rescaling acts on the declared valuation as well as on the environment, which is why V appears on one side and V.comp ψ on the other.

The three binder cases are where the work is. Λu extends both valuation and scaling and appeals to relEnv_weaken; e[μ] reads the family at μ's magnitude on one side and at the rescaled magnitude on the other, which is exactly logScale_comp; Λδ and e{d} move nothing, because dimensions have no magnitudes.

Coherence is necessary, not merely sufficient

The theorems above say coherence suffices. This section says it is forced: one conversion, applied to a nonzero argument, is scale-invariant exactly when the scaling identifies the two units.

So fundamental's hypothesis is not an artifact of the proof. A term that converts can detect any rescaling that separates units of the same dimension, and the coherent scalings are precisely the ones it cannot detect.

The canonical one-conversion program

def LambdaS.cvtTm {B D : Type} {j k : ℕ} (u v : UExp B k) : Tm B D j k

convert x u v, with x the sole free variable.

Equations

• LambdaS.cvtTm u v = (LambdaS.Tm.var 0).convert u v

def LambdaS.cvtDeriv {B D : Type} [Fintype B] [UnitSys B D] {j k : ℕ} {Δ : DCtx D j k} {u v : UExp B k} (h : SameDim Δ u v) : HasTy Δ [Ty.Q u] (cvtTm u v) (Ty.Q v)

Its derivation.

Equations

• LambdaS.cvtDeriv h = (LambdaS.HasTy.var ⋯).convert h

theorem LambdaS.cvt_rel_iff_coherent {B D : Type} [Fintype B] [UnitSys B D] {j k : ℕ} {Δ : DCtx D j k} {u v : UExp B k} (h : SameDim Δ u v) (V ψ : Scaling B k) {x : ℝ} (hx : x ≠ 0) : Rel (Ty.Q v) ψ (den V (cvtDeriv h) (x, PUnit.unit)) (den (V.comp ψ) (cvtDeriv h) (ψ.scale u * x, PUnit.unit)) ↔ ψ.scale u = ψ.scale v

Coherence at a pair is exactly what one conversion requires.

Left to right is the converse of fundamental, restricted to this term: if the relation holds for a nonzero input then the scaling must identify u and v. Right to left is fundamental itself.

The hypothesis x ≠ 0 is necessary and not a technicality: the zero function is invariant under everything, which is the same degeneracy that makes eq_zero_of_relQ_self true.

theorem LambdaS.closed_invariant {B D : Type} [Fintype B] [UnitSys B D] {j k : ℕ} {Δ : DCtx D j k} {e : Tm B D j k} {u : UExp B k} (d : HasTy Δ [] e (Ty.Q u)) (hp : e.Parametric) (hf : e.ConvertFree) (V ψ : Scaling B k) : den V d PUnit.unit = ψ.scale u * den V d PUnit.unit

Scaling invariance for closed terms. A closed convert-free term of scalar type denotes a number invariant under every rescaling of the units, which forces it to be zero unless its unit is trivial.

The immediate corollary, and the reason ucon had to be excluded from Parametric: a term that could name a unit would be a counterexample.

The bridge to first-order signatures

The fundamental theorem states scale-invariance for an arbitrary type. The Pi theorem needs it in the specific shape of a first-order signature: n scalar arguments and a scalar result. That is what this section extracts.

def LambdaS.scalarCtx {B D : Type} {j k : ℕ} (us : List (UExp B k)) : Ctx B D j k

The context of scalar types for a list of argument units.

Equations

• LambdaS.scalarCtx us = List.map LambdaS.Ty.Q us

noncomputable def LambdaS.scaleEnv {B D : Type} [Fintype B] {j k : ℕ} (ψ : Scaling B k) (us : List (UExp B k)) : Env (scalarCtx us) → Env (scalarCtx us)

Rescale an environment of scalars componentwise.

Equations

• LambdaS.scaleEnv ψ [] ρ = ρ
• LambdaS.scaleEnv ψ (u :: us) ρ = (ψ.scale u * ρ.1, LambdaS.scaleEnv ψ us ρ.2)

theorem LambdaS.relEnv_scaleEnv {B D : Type} [Fintype B] {j k : ℕ} (ψ : Scaling B k) (us : List (UExp B k)) (ρ : Env (scalarCtx us)) : RelEnv (scalarCtx us) ψ ρ (scaleEnv ψ us ρ)

An environment is related to its own rescaling.

theorem LambdaS.indepEnv_scalarCtx {B D : Type} {j k : ℕ} (us : List (UExp B k)) (ρ : Env (scalarCtx us)) : IndepEnv (scalarCtx us) ρ ρ

An environment of scalars is trivially independent of the valuation: at scalar type the relation is equality, and the environment is compared with itself.

theorem LambdaS.scaleLaw {B D : Type} [Fintype B] [UnitSys B D] {j k : ℕ} {Δ : DCtx D j k} {e : Tm B D j k} {us : List (UExp B k)} {u₀ : UExp B k} (d : HasTy Δ (scalarCtx us) e (Ty.Q u₀)) (hp : e.Parametric) (hf : e.ConvertFree) (V ψ : Scaling B k) (ρ : Env (scalarCtx us)) : den V d (scaleEnv ψ us ρ) = ψ.scale u₀ * den V d ρ

The scaling law of a first-order term, derived from the fundamental theorem.

Rescaling every argument by the scale factor of its unit rescales the result by the scale factor of its unit. This is the hypothesis the Pi theorem consumes, supplied by an actual well-typed term rather than assumed.

Stated for convert-free terms, and that restriction is what makes the Pi theorem's unrestricted quantification over scalings legitimate: a term that converts obeys the law only for coherent ψ, which is not enough freedom for the argument the Pi theorem runs.

def LambdaS.velocityTm {B D : Type} {j k : ℕ} : Tm B D j k

A program using two unit constants, with the constants as free variables: x / y at type Q (u/v). This is 1 u / 1 v with ucon compiled away.

Equations

• LambdaS.velocityTm = (LambdaS.Tm.var 0).div (LambdaS.Tm.var 1)

def LambdaS.velocityDeriv {B D : Type} [Fintype B] [UnitSys B D] {j k : ℕ} {Δ : DCtx D j k} (u v : UExp B k) : HasTy Δ (scalarCtx [u, v]) velocityTm (Ty.Q (Term.div u v))

Its derivation, in the context of the two constants.

Equations

• LambdaS.velocityDeriv u v = (LambdaS.HasTy.var ⋯).div (LambdaS.HasTy.var ⋯)

theorem LambdaS.velocityTm_parametric {B D : Type} {j k : ℕ} : velocityTm.Parametric

theorem LambdaS.velocityTm_convertFree {B D : Type} {j k : ℕ} : velocityTm.ConvertFree

theorem LambdaS.velocity_scales {B D : Type} [Fintype B] [UnitSys B D] {j k : ℕ} {Δ : DCtx D j k} (u v : UExp B k) (V ψ : Scaling B k) (ρ : Env (scalarCtx [u, v])) : den V (velocityDeriv u v) (scaleEnv ψ [u, v] ρ) = ψ.scale (Term.div u v) * den V (velocityDeriv u v) ρ

A program that mentions units is scale-invariant once its constants scale with it.

Supplying "one u" and "one v" gives one answer; supplying the rescaled constants gives that answer times the scale factor of u/v. Derived straight from the fundamental theorem, with the environment relation carrying the whole content: each constant is related to its rescaled self.

A square root inside the fragment

Witness of the strengthened relQ_rpow: a term that takes a square root is parametric, and the fundamental theorem applies to it with no positivity side condition.

def LambdaS.sqrtTm {B D : Type} {j k : ℕ} (u : UExp B k) : Tm B D j k

λ x : Q (u·u). pow (1/2) x.

Equations

• LambdaS.sqrtTm u = LambdaS.Tm.lam (LambdaS.Ty.Q (LambdaS.Term.mul u u)) (LambdaS.Tm.pow (1 / 2) (LambdaS.Tm.var 0))

def LambdaS.sqrtDeriv {B D : Type} [Fintype B] [UnitSys B D] {j k : ℕ} {Δ : DCtx D j k} (u : UExp B k) : HasTy Δ [] (sqrtTm u) ((Ty.Q (Term.mul u u)).arrow (Ty.Q ((Term.mul u u).rpow (1 / 2))))

Its derivation. The result type is Q ((u·u)^(1/2)), which the unit algebra puts over ℚ exponents; nothing about the term needs its argument to be non-negative.

Equations

• LambdaS.sqrtDeriv u = (LambdaS.HasTy.var ⋯).pow.lam

theorem LambdaS.sqrtTm_parametric {B D : Type} {j k : ℕ} (u : UExp B k) : (sqrtTm u).Parametric

theorem LambdaS.sqrtTm_convertFree {B D : Type} {j k : ℕ} (u : UExp B k) : (sqrtTm u).ConvertFree

theorem LambdaS.sqrt_scales {B D : Type} [Fintype B] [UnitSys B D] {j k : ℕ} {Δ : DCtx D j k} (u : UExp B k) (V ψ : Scaling B k) : Rel ((Ty.Q (Term.mul u u)).arrow (Ty.Q ((Term.mul u u).rpow (1 / 2)))) ψ (den V (sqrtDeriv u) PUnit.unit) (den (V.comp ψ) (sqrtDeriv u) PUnit.unit)

The fundamental theorem covers rational powers. The square root term, now pow (1/2), is related to itself under every scaling: inputs related at u·u give outputs related at (u·u)^(1/2), whose scale factor is ψ(u·u)^(1/2). Before relQ_rpow lost its sign hypothesis this instance was out of reach of fundamental_free, because Tm.Parametric rejected the term.

Where unit constants belong

The exclusion of ucon is not a hole in the theorem; it locates a design decision.

A term that names a unit is not scale-invariant, and it should not be. 1.3 m is a definite physical quantity, but the number 1.3 is its magnitude in meters. Rescale the meter and the same quantity has a different magnitude, so the numeral must change with it, which is exactly why Kennedy's kg-to-lb example rewrites 1.0<kg> as 2.2<lb> rather than leaving the program alone.

The fix is to stop treating unit constants as term constructors and treat them as environment entries: precisely Kennedy's "pervasive environment", now with a reason rather than a convention. A program mentioning meters is a program with a free variable standing for one meter, and it is scale-invariant relative to environments that scale that variable along with everything else.

Nothing new is needed: ucon u compiles to a variable in a context prefixed by the unit constants, and the fundamental theorem applies unchanged. velocityTm and velocity_scales above are the whole construction.