Conversion, and why paths cannot disagree

Λs has a conversion operator (convert, a core term constructor), and conversion is the place to be careful: with units nameable and definable in terms of combinations of other units, a system that defines conversion by walking a declared structure can offer more than one route between two units, with no guarantee the routes agree.

This file answers that. Conversion is not a path at all; it is a ratio of valuations, and the object that supplies the valuations already exists: Scaling. A scaling assigns a positive magnitude to every base unit and extends to a homomorphism, which is exactly what "reduce every unit to a canonical value" means in the specification of Fortress, a language whose standard library carried units of measure.

Once conversion is a ratio, path independence is not a condition to check but a theorem: convChain_eq says any chain of intermediate conversions collapses to the direct one, because the intermediate factors telescope. The multiple-paths problem does not arise, and there is nothing an implementation could get wrong.

The contrast worth recording

There is a real alternative, and it is the one a unit-conversion programming assignment (Rice's Comp 311, Fall 2016) adopts: restrict compound units to at most one named unit per dimension, so that lining up two compounds has a unique pairing. That works, and it kills the ambiguity, but it buys uniqueness by shrinking the algebra. Under it meter / foot is illegal, because both are units of Length; yet that is exactly a conversion factor, dimensionless, and worth naming.

The exponent-vector representation needs no such restriction. meter and foot are distinct generators that happen to share a dimension, meter * foot is a perfectly good vector, and no pairing question ever arises because a vector's components are already indexed.

noncomputable def LambdaS.conv {B : Type} [Fintype B] {k : ℕ} (ψ : Scaling B k) (u v : UExp B k) : ℝ

The conversion factor from u to v, relative to a valuation.

A valuation is a Scaling: it fixes what each base unit is worth, and extends to a homomorphism on all units. The factor is then just the ratio.

Equations

• LambdaS.conv ψ u v = ψ.scale u / ψ.scale v

@[simp]

theorem LambdaS.conv_pos {B : Type} [Fintype B] {k : ℕ} (ψ : Scaling B k) (u v : UExp B k) : 0 < conv ψ u v

theorem LambdaS.conv_ne_zero {B : Type} [Fintype B] {k : ℕ} (ψ : Scaling B k) (u v : UExp B k) : conv ψ u v ≠ 0

@[simp]

theorem LambdaS.conv_self {B : Type} [Fintype B] {k : ℕ} (ψ : Scaling B k) (u : UExp B k) : conv ψ u u = 1

Converting a unit to itself does nothing.

theorem LambdaS.conv_eq_scale_div {B : Type} [Fintype B] {k : ℕ} (ψ : Scaling B k) (u v : UExp B k) : conv ψ u v = ψ.scale (Term.div u v)

The conversion factor is the scale of the ratio, so it is itself the valuation of a dimensionless unit, which is what makes conversion factors nameable as units.

theorem LambdaS.conv_trans {B : Type} [Fintype B] {k : ℕ} (ψ : Scaling B k) (u v w : UExp B k) : conv ψ u v * conv ψ v w = conv ψ u w

Transitivity. Converting through an intermediate unit gives the same factor as converting directly.

theorem LambdaS.conv_symm {B : Type} [Fintype B] {k : ℕ} (ψ : Scaling B k) (u v : UExp B k) : conv ψ u v * conv ψ v u = 1

Converting back undoes converting forward.

noncomputable def LambdaS.convChain {B : Type} [Fintype B] {k : ℕ} (ψ : Scaling B k) : UExp B k → List (UExp B k) → UExp B k → ℝ

The factor along a chain of intermediate units.

Equations

• LambdaS.convChain ψ x✝¹ [] x✝ = LambdaS.conv ψ x✝¹ x✝
• LambdaS.convChain ψ x✝¹ (w :: ws) x✝ = LambdaS.conv ψ x✝¹ w * LambdaS.convChain ψ w ws x✝

theorem LambdaS.convChain_eq {B : Type} [Fintype B] {k : ℕ} (ψ : Scaling B k) (u : UExp B k) (ws : List (UExp B k)) (v : UExp B k) : convChain ψ u ws v = conv ψ u v

Path independence. Any chain of intermediate conversions from u to v gives exactly the direct factor.

This is the theorem the multiple-paths problem asks for. It holds because the factors are ratios of a single valuation, so intermediates telescope, not because anyone checked the declarations for consistency. There is no route by which two paths could disagree.

theorem LambdaS.conv_preserves {B : Type} [Fintype B] {k : ℕ} (ψ : Scaling B k) (u v : UExp B k) (m : ℝ) : ψ.scale v * (m * conv ψ u v) = ψ.scale u * m

Conversion preserves the quantity. A measurement ⟨m, u⟩ converted into unit v denotes the same physical quantity: its interpretation under the valuation is unchanged.

This is the correctness statement for an in operator, and it is what the Comp 311 assignment needs of its def in(v: PhysicalUnit) and never states.

def LambdaS.Scaling.comp {B : Type} {k : ℕ} (V ψ : Scaling B k) : Scaling B k

Composing two scalings: in log space, pointwise addition.

Equations

• V.comp ψ = { base := fun (b : B) => V.base b + ψ.base b, vars := fun (i : Fin k) => V.vars i + ψ.vars i }

@[simp]

theorem LambdaS.Scaling.comp_cons {B : Type} {k : ℕ} (V ψ : Scaling B k) (r s : ℝ) : (V.cons r).comp (ψ.cons s) = (V.comp ψ).cons (r + s)

Composing scalings commutes with extending them: a new variable's factors add, like everything else.

@[simp]

theorem LambdaS.Scaling.comp_zero {B : Type} {k : ℕ} (V : Scaling B k) : V.comp zero = V

The trivial scaling is the unit of composition.

theorem LambdaS.Scaling.logScale_comp {B : Type} [Fintype B] {k : ℕ} (V ψ : Scaling B k) (u : UExp B k) : (V.comp ψ).logScale u = V.logScale u + ψ.logScale u

theorem LambdaS.Scaling.scale_comp {B : Type} [Fintype B] {k : ℕ} (V ψ : Scaling B k) (u : UExp B k) : (V.comp ψ).scale u = V.scale u * ψ.scale u

theorem LambdaS.conv_comp {B : Type} [Fintype B] {k : ℕ} (V ψ : Scaling B k) (u v : UExp B k) : conv (V.comp ψ) u v = conv V u v * (ψ.scale u / ψ.scale v)

Rescaling the valuation multiplies a conversion factor by the ratio of the two units' scale factors. The engine of every coherence result: the factor is almost invariant, off by exactly the amount coherence sets to one.

Dimensions

dimOf lives in LambdaS.Syntax, since the typing rule for convert needs it. These are the homomorphism laws the design requires of it: dimension is a group homomorphism from units to dimensions, which is what makes "same dimension" an equivalence compatible with the algebra.

theorem LambdaS.dimOf_mul {B D : Type} [Fintype B] {k : ℕ} [UnitSys B D] {j : ℕ} (Δ : DCtx D j k) (u v : UExp B k) : dimOf Δ (Term.mul u v) = Term.mul (dimOf Δ u) (dimOf Δ v)

@[simp]

theorem LambdaS.dimOf_one {B D : Type} [Fintype B] {k : ℕ} [UnitSys B D] {j : ℕ} (Δ : DCtx D j k) : dimOf Δ 1 = 1

theorem LambdaS.dimOf_div {B D : Type} [Fintype B] {k : ℕ} [UnitSys B D] {j : ℕ} (Δ : DCtx D j k) (u v : UExp B k) : dimOf Δ (Term.div u v) = Term.div (dimOf Δ u) (dimOf Δ v)

theorem LambdaS.dimOf_rpow {B D : Type} [Fintype B] {k : ℕ} [UnitSys B D] {j : ℕ} (Δ : DCtx D j k) (u : UExp B k) (q : ℚ) : dimOf Δ (Term.rpow u q) = Term.rpow (dimOf Δ u) q

theorem LambdaS.dimOf_ratio_one {B D : Type} [Fintype B] {k : ℕ} [UnitSys B D] {j : ℕ} (Δ : DCtx D j k) {u v : UExp B k} (h : SameDim Δ u v) : dimOf Δ (Term.div u v) = 1

Interchangeable units have a dimensionless ratio, which is why their conversion factor is a pure number and can itself be named as a unit.

Under the "one named unit per dimension" restriction this ratio is not even expressible, since u and v would be two units of one dimension in a single compound.

A linear extension lemma

The classical fact both this file and LambdaS.Declare consume: a value assignment on a finite family extends to a linear map exactly when it respects the family's linear dependencies.

theorem LambdaS.exists_linearMap_of_dependencies {K : Type u_1} {M : Type u_2} {V : Type u_3} [Field K] [AddCommGroup M] [Module K M] [AddCommGroup V] [Module K V] {ι : Type u_4} [Fintype ι] [DecidableEq ι] (r : ι → M) (v : ι → V) (h : ∀ (c : ι → K), ∑ i : ι, c i • r i = 0 → ∑ i : ι, c i • v i = 0) : ∃ (φ : M →ₗ[K] V), ∀ (i : ι), φ (r i) = v i

Prescribed values extend to a linear map when dependencies are respected. Given finite families r in M and v in V over a field K, a single linear map sends each r i to v i exactly when every K-linear dependency among the r i also annihilates the corresponding combination of the v i. This is the extension step behind Scaling.Coherent.factors in this file and dependency_sufficient in LambdaS.Declare: the value assignment factors through the span of the family and then extends to the whole space.

Coherence: which scalings are physically meaningful

Parametricity quantifies over all scalings, including ones that scale meter and foot independently. That is physical nonsense (rescale the meter and the foot must follow), but it is exactly the freedom that lets Λs treat same-dimension units as independent generators, and so avoid restricting compound units to one named unit per dimension.

The physically meaningful scalings are those that factor through dimension, and they are precisely the ones that leave conversion factors alone. This is the bridge between the two roles a Scaling plays: fixed declared data on the one hand, quantified-over transformation on the other.

It is also the exact price of convert. A parametric term without convert is scale-invariant for every scaling: that is fundamental_free, and it is what the Pi theorem consumes. A term with convert is scale-invariant for the coherent ones, and conv_invariant_of_coherent is the lemma that discharges its case. Nothing else in Λs can observe a unit, so nothing else pays.

def LambdaS.Scaling.Coherent {B D : Type} [Fintype B] {k : ℕ} [UnitSys B D] {j : ℕ} (Δ : DCtx D j k) (ψ : Scaling B k) : Prop

A scaling is coherent for Δ when interchangeable units scale alike; that is, when it factors through dim.

Equations

• LambdaS.Scaling.Coherent Δ ψ = ∀ (u v : LambdaS.UExp B k), LambdaS.SameDim Δ u v → ψ.scale u = ψ.scale v

theorem LambdaS.conv_invariant_of_coherent {B D : Type} [Fintype B] {k : ℕ} [UnitSys B D] {j : ℕ} (V : Scaling B k) {Δ : DCtx D j k} {ψ : Scaling B k} (hψ : Scaling.Coherent Δ ψ) {u v : UExp B k} (h : SameDim Δ u v) : conv (V.comp ψ) u v = conv V u v

Conversion factors are invariant under coherent rescaling.

Change the unit system by any scaling that respects dimensions and every conversion factor is unchanged: 1 m = 3.28 ft whatever reference you measure against.

structure LambdaS.Scaling.Factors {B D : Type} {k : ℕ} [UnitSys B D] {j : ℕ} [Fintype D] (ψ : Scaling B k) (Δ : DCtx D j k) (Φ : Scaling D j) : Prop

ψ factors through dimension via the dimension scaling Φ.

This is Coherent with its witness named, and split into the two facts that determine it: what each base unit is worth, and what each unit variable is worth. Coherence says interchangeable units scale alike, which is precisely the statement that the scaling is pulled back from one on dimensions.

Naming the dimension scaling is what makes unit abstraction tractable. Under Λu:δ the factor the bound unit must receive is then not merely constrained to some coherent value; it is determined, namely Φ δ. A coherent rescaling is a rescaling of dimensions, and unit abstraction has no freedom left.

• base (b : B) : ψ.base b = ∑ d : D, ↑((UnitSys.dim b).base d) * Φ.base d

  A base unit scales by its dimension's factor.

• vars (i : Fin k) : ψ.vars i = Φ.logScale (Δ i)

  A unit variable scales by its declared dimension's factor.

theorem LambdaS.Scaling.Factors.logScale {B D : Type} [Fintype B] {k : ℕ} [UnitSys B D] {j : ℕ} [Fintype D] {ψ : Scaling B k} {Δ : DCtx D j k} {Φ : Scaling D j} (h : ψ.Factors Δ Φ) (u : UExp B k) : ψ.logScale u = Φ.logScale (dimOf Δ u)

Factoring is pointwise, so it extends to every unit expression. The content is that logScale and dimOf are both linear, so this is a change in summation order rather than an induction.

theorem LambdaS.Scaling.Factors.coherent {B D : Type} [Fintype B] {k : ℕ} [UnitSys B D] {j : ℕ} [Fintype D] {ψ : Scaling B k} {Δ : DCtx D j k} {Φ : Scaling D j} (h : ψ.Factors Δ Φ) : Coherent Δ ψ

Factoring through dimension is coherence.

theorem LambdaS.Scaling.Factors.cons {B D : Type} {k : ℕ} [UnitSys B D] {j : ℕ} [Fintype D] {ψ : Scaling B k} {Δ : DCtx D j k} {Φ : Scaling D j} (h : ψ.Factors Δ Φ) (d : DExp D j) : (ψ.cons (Φ.logScale d)).Factors (DCtx.cons d Δ) Φ

Factoring survives a unit binder, at the factor the bound dimension dictates. There is no choice to make, which is the whole point.

theorem LambdaS.Scaling.Factors.weakenDim {B D : Type} {k : ℕ} [UnitSys B D] {j : ℕ} [Fintype D] {ψ : Scaling B k} {Δ : DCtx D j k} {Φ : Scaling D j} (h : ψ.Factors Δ Φ) (t : ℝ) : ψ.Factors Δ.weakenDim (Φ.cons t)

Factoring survives a dimension binder, at whatever the new dimension is worth: dimension abstraction is unconstrained, which is what makes ∀δ. ∀u:δ genuinely unbounded.

theorem LambdaS.Scaling.Coherent.factors {B D : Type} [Fintype B] {k : ℕ} [UnitSys B D] {j : ℕ} [Fintype D] {ψ : Scaling B k} {Δ : DCtx D j k} (hcoh : Coherent Δ ψ) : ∃ (Φ : Scaling D j), ψ.Factors Δ Φ

Every coherent scaling factors through dimension. This is the converse of Scaling.Factors.coherent, and together they give the equivalence the paper's introduction asserts when it defines coherence as inheriting factors from dimensions.

The proof is ℚ-linear algebra with values in ℝ. Each generator (base unit or unit variable) has a dimension exponent vector and a log factor. A rational dependency among the vectors assembles a dimensionless unit expression, which coherence sends to the scale of 1, so the corresponding combination of log factors vanishes. exists_linearMap_of_dependencies then extends the assignment to a ℚ-linear functional on the whole dimension space, and reading that functional on the standard basis gives the dimension scaling.

theorem LambdaS.Scaling.coherent_iff_factors {B D : Type} [Fintype B] {k : ℕ} [UnitSys B D] {j : ℕ} [Fintype D] {ψ : Scaling B k} {Δ : DCtx D j k} : Coherent Δ ψ ↔ ∃ (Φ : Scaling D j), ψ.Factors Δ Φ

Coherence is factoring through dimension. A scaling respects interchangeability exactly when it is pulled back from some scaling of dimensions. The paper defines coherence by the right-hand side; this equivalence shows the two readings agree.

theorem LambdaS.Scaling.coherent_id {B D : Type} [Fintype B] {k : ℕ} [UnitSys B D] {j : ℕ} (Δ : DCtx D j k) : Coherent Δ (id B k)

The trivial scaling is coherent, so the coherent theorems are never vacuous.