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 for the canonical one-conversion program (cvt_invariant_iff_eq): invariance under all scalings detects exactly the conversions that do something. Twist.invariant_iff (the paper's Theorem 6.1) extends it to first-order scalar programs of nonzero denotation.

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 = c · x at type Q u → Q u. It satisfies the scaling law for every ψ, since f (k·x) = k·f x. Terms are countable and reals are not, so for all but countably many c no term denotes f. 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 exactly. 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 the result unit of a first-order scaling law mentions a base unit that no argument unit mentions, then every function obeying the law under all scalings is zero (forced_zero states this for terms). It is the single-base-unit case of Pi.mulScaleLaw_eq_zero_of_unsolvable, stated over environments rather than 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 and parametric whenever the original is, 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 ρ')

Parametric 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 in which some base unit occurs in the result and in no argument.

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.

The proof uses the pendulum argument's device, a scaling that moves only one base unit: here it fixes every input and moves the output, so the output must be zero. Pi.eq_zero_of_appears_once applies the same device to exponent matrices.

It is also the single-base-unit 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.