What invariance detects

fundamental says a parametric term is scale-invariant for coherent scalings, and fundamental_free says a parametric convert-free term is invariant for all of them (parametric meaning no ucon). This file proves the converse: invariance under all scalings detects exactly the conversions that do something.

The theorem that is not available

The tempting statement ("invariant under all scalings implies definable") is false, and not for any interesting reason. Take f x = π · x at type Q u → Q u. It satisfies the scaling law for every ψ, since f (k·x) = k·f x. No parametric, convert-free term denotes it: literals are rational, and the arithmetic of Λs over rationals and the input cannot produce π. Definability results of that shape fail in System F too, and units have nothing to do with it.

So the right target is not definability in general but a completeness result for convert in particular. That is what is proved here.

The theorem that is available

Call a conversion inert when it converts a unit to itself. An inert conversion multiplies by conv V u u = 1, so it is denotationally invisible; exists_convertFree_of_inert turns a term whose conversions are all inert into a convert-free term with the same denotation.

The converse is cvt_invariant_iff_eq: a single conversion applied to a nonzero argument is invariant under all scalings if and only if u = v on the nose. Not "same dimension": literally the same exponent vector. The mechanism is scale_eq_iff: scalings separate points of the unit group, so ∀ψ, ψ.scale u = ψ.scale v collapses to u = v.

Putting the two together, for the canonical conversion program the three conditions

• invariant under every scaling,
• inert,
• denotationally convert-free,

coincide. Coherent invariance, by contrast, is strictly weaker and holds for every conversion between same-dimension units, and that gap is exactly what conversion costs.

And the first-order dichotomy

scaleLaw_forces_zero is the general form of NonDef.convert_not_definable: if a first-order term's result unit mentions a base unit that none of its arguments mention, then all-scalings invariance forces the term to denote zero. This is Pi.eq_zero_of_appears_once (the pendulum argument) reappearing as a statement about terms rather than about exponent matrices.

Scalings separate units

noncomputable def LambdaS.Scaling.coord {B : Type} [DecidableEq B] {k : ℕ} (b : B) : Scaling B k

The scaling that reads off one base coordinate.

Equations

• LambdaS.Scaling.coord b = { base := fun (b' : B) => if b' = b then 1 else 0, vars := fun (x : Fin k) => 0 }

noncomputable def LambdaS.Scaling.coordVar {B : Type} {k : ℕ} (i : Fin k) : Scaling B k

The scaling that reads off one unit-variable coordinate.

Equations

• LambdaS.Scaling.coordVar i = { base := fun (x : B) => 0, vars := fun (i' : Fin k) => if i' = i then 1 else 0 }

@[simp]

theorem LambdaS.Scaling.scale_coord {B : Type} [Fintype B] [DecidableEq B] {k : ℕ} (b : B) (u : UExp B k) : (coord b).scale u = Real.exp ↑(u.base b)

@[simp]

theorem LambdaS.Scaling.scale_coordVar {B : Type} [Fintype B] {k : ℕ} (i : Fin k) (u : UExp B k) : (coordVar i).scale u = Real.exp ↑(u.vars i)

theorem LambdaS.scale_eq_iff {B : Type} [Fintype B] [DecidableEq B] {k : ℕ} {u v : UExp B k} : (∀ (ψ : Scaling B k), ψ.scale u = ψ.scale v) ↔ u = v

Scalings separate units. Two unit expressions are scaled alike by every scaling exactly when they are the same exponent vector.

This is what makes all-scalings invariance so much stronger than coherent invariance: coherence identifies units of equal dimension, whereas quantifying over every scaling identifies nothing at all.

Inert conversions

A conversion is inert when it converts a unit to itself, so multiplies by 1. That is much stronger than the typing side condition, which asks only for equal dimensions.

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

A term's conversions are all inert.

Equations

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

theorem LambdaS.Tm.inert_of_convertFree {B D : Type} {j k : ℕ} (e : Tm B D j k) : e.ConvertFree → e.Inert

Convert-free terms are inert, vacuously.

theorem LambdaS.exists_convertFree_of_inert {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.Inert → ∃ (e' : Tm B D j k) (d' : HasTy Δ Γ e' τ), e'.ConvertFree ∧ (e.Parametric → e'.Parametric) ∧ ∀ (V : Scaling B k) (ρ : Env Γ), den V d' ρ = den V d ρ

Inert conversions are removable. A term whose conversions are all inert denotes exactly what some convert-free term denotes: at the same type, in every environment, under every valuation.

Stated over derivations this says what it should: there is another term, convert-free, with a derivation at the same type and the same denotation. Over an intrinsically typed syntax the term and its derivation are one object, so the statement could not distinguish them.

Carrying the source unit on convert is what makes this work: with u = v the rule is type-preserving, so the conversion can simply be deleted.

theorem LambdaS.fundamental_of_inert {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 τ) (hp : e.Parametric) (hi : e.Inert) (V ψ : Scaling B k) {ρ ρ' : Env Γ} (hr : RelEnv Γ ψ ρ ρ') : Rel τ ψ (den V d ρ) (den (V.comp ψ) d ρ')

Inert terms are invariant under every scaling, not merely the coherent ones, because they are convert-free in all but name.

The converse

cvt_rel_iff_coherent said invariance of the canonical one-conversion program under a given ψ is equivalent to ψ identifying the two units. Quantifying over every ψ and applying scale_eq_iff collapses that to u = v.

theorem LambdaS.cvt_invariant_iff_eq {B D : Type} [Fintype B] [DecidableEq 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) : (∀ (ψ : Scaling B k), Rel (Ty.Q v) ψ (den V (cvtDeriv h) (x, PUnit.unit)) (den (V.comp ψ) (cvtDeriv h) (ψ.scale u * x, PUnit.unit))) ↔ u = v

All-scalings invariance is exactly inertness, for the canonical conversion applied to a nonzero argument.

The three conditions coincide: invariant under every scaling, inert, and (by exists_convertFree_of_inert) denotationally convert-free. Contrast fundamental, which holds for every well-typed conversion once the scalings are restricted to coherent ones.

theorem LambdaS.cvt_detectable {B D : Type} [Fintype B] [DecidableEq 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) (huv : u ≠ v) : ∃ (ψ : Scaling B k), ¬Rel (Ty.Q v) ψ (den V (cvtDeriv h) (x, PUnit.unit)) (den (V.comp ψ) (cvtDeriv h) (ψ.scale u * x, PUnit.unit))

Restated as the design claim: a conversion that actually converts is detectable. Some rescaling of the unit system changes what the program computes, which is the precise sense in which convert reads the units.

The first-order dichotomy

NonDef.convert_not_definable collapsed a function between two distinct base units to zero. The same argument works for any first-order signature, and the hypothesis is the pendulum condition: a base unit the result mentions and no argument does.

theorem LambdaS.scaleEnv_eq_self {B D : Type} [Fintype B] {j k : ℕ} (ψ : Scaling B k) (us : List (UExp B k)) : (∀ u ∈ us, ψ.scale u = 1) → ∀ (ρ : Env (scalarCtx us)), scaleEnv ψ us ρ = ρ

Rescaling by a scaling that fixes every argument unit changes nothing.

@[simp]

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

The trivial scaling fixes every environment.

theorem LambdaS.scaleLaw_forces_zero {B D : Type} [Fintype B] [DecidableEq B] {j k : ℕ} {us : List (UExp B k)} {u₀ : UExp B k} (f : Env (scalarCtx us) → ℝ) (hlaw : ∀ (ψ : Scaling B k) (ρ : Env (scalarCtx us)), f (scaleEnv ψ us ρ) = ψ.scale u₀ * f ρ) (b : B) (hus : ∀ u ∈ us, u.base b = 0) (h0 : u₀.base b ≠ 0) (ρ : Env (scalarCtx us)) : f ρ = 0

Invariance forces zero when the result escapes the arguments.

If some base unit occurs in the result unit but in no argument unit, then a first-order function invariant under every scaling is the zero function.

This is the semantic form of the pendulum argument: the scaling that moves only that base unit fixes every input and moves the output, so the output has nowhere to go but zero. Compare Pi.eq_zero_of_appears_once, which says the same thing about exponent matrices.

It is also the one-variable special case of the solvability dichotomy (Pi.mulScaleLaw_eq_zero_of_unsolvable, in LambdaS.PiTheorem): a base unit missing from every argument but present in the result makes A X = b unsolvable with the annihilator being that base unit's coordinate direction, and the general collapse specializes to this one.

theorem LambdaS.forced_zero {B D : Type} [Fintype B] [DecidableEq B] [UnitSys B D] {j k : ℕ} {Δ : DCtx D j k} {us : List (UExp B k)} {u₀ : UExp B k} {e : Tm B D j k} (d : HasTy Δ (scalarCtx us) e (Ty.Q u₀)) (V : Scaling B k) (hlaw : ∀ (ψ : Scaling B k) (ρ : Env (scalarCtx us)), den V d (scaleEnv ψ us ρ) = ψ.scale u₀ * den V d ρ) (b : B) (hus : ∀ u ∈ us, u.base b = 0) (h0 : u₀.base b ≠ 0) (ρ : Env (scalarCtx us)) : den V d ρ = 0

The dichotomy for actual terms: a first-order term whose result unit escapes its arguments denotes zero, if it is invariant under every scaling. Otherwise it is not invariant, so by the contrapositive of fundamental_free it is not both parametric and convert-free.

Trivial ratios

@[simp]

theorem LambdaS.Term.one_mul' {B V : Type} (t : Term B V) : mul 1 t = t

@[simp]

theorem LambdaS.Term.mul_one' {B V : Type} (t : Term B V) : t.mul 1 = t

@[simp]

theorem LambdaS.Term.div_one' {B V : Type} (t : Term B V) : t.div 1 = t

theorem LambdaS.div_eq_one_iff {B : Type} {k : ℕ} {u v : UExp B k} : Term.div u v = 1 ↔ u = v

A ratio is trivial exactly when its two units agree. This is cancellation and needs nothing but the group structure; it would hold just as well over ℤ exponents.