Dimension-level Buckingham factorization for converting programs

LambdaS.Pi.den_mulScaleLaw uses independent rescaling of every unit symbol, which requires a convert-free program (or, for den_mulScaleLaw_driftFree, a drift-free one). Physics instead rescales dimensions. The coherent abstraction theorem supplies this weaker law even for converting programs, but compares denotations at V and V.comp ψ; a fixed-valuation scaling law needs one further argument.

The instrumented evaluator consults its oracle only after checking that source and target have the same dimension. Oracles agreeing on those pairs therefore produce identical evaluations, at every fuel and without a typing hypothesis. Normalization and adequacy carry that equality to a scalar denotation with scalar inputs. Coherent rescaling preserves precisely those oracle entries.

The resulting den_pi_coherent factors arbitrary signed outputs on positive inputs through a rational basis of the dimension matrix's kernel, and den_pi_coherent_dichotomy (the paper's Theorem 8.1) adds the unsolvable case, in which the program denotes zero. The external unit and dimension scope is closed (j = k = 0); the program must be parametric (no ucon) but may convert and bind units and dimensions internally. Extending this bridge to ungrounded external unit/dimension variables is not claimed here.

theorem LambdaS.eval_congr_sameDim {B D R : Type} [Fintype B] [DecidableEq B] [Fintype D] [DecidableEq D] [UnitSys B D] [Num R] (cf cf' : UExp B 0 → UExp B 0 → R) (hcf : ∀ (u v : UExp B 0), SameDim (DCtx.nil D) u v → cf u v = cf' u v) (n j k : ℕ) (η : UEnv B k) (δ : DEnv D j) (ρ : List (Val R B D)) (e : Tm B D j k) : eval cf n j k η δ ρ e = eval cf' n j k η δ ρ e

Conversion oracles that agree on same-dimension pairs produce identical instrumented evaluations, because the evaluator checks that condition before consulting either oracle. No typing assumption is needed.

def LambdaS.scalarVals {B D : Type} (us : List (UExp B 0)) : Env (scalarCtx us) → List (Val ℝ B D)

Scalar denotational environments as instrumented runtime values.

Equations

• LambdaS.scalarVals [] x_2 = []
• LambdaS.scalarVals (u :: us) ρ = LambdaS.Val.scalar { mag := ρ.1, unit := u } :: LambdaS.scalarVals us ρ.2

theorem LambdaS.den_eq_of_sameDim_conv {B D : Type} [Fintype B] [DecidableEq B] [Fintype D] [DecidableEq D] [UnitSys B D] {e : Tm B D 0 0} {us : List (UExp B 0)} {u : UExp B 0} (d : HasTy (DCtx.nil D) (scalarCtx us) e (Ty.Q u)) (V V' : Scaling B 0) (hconv : ∀ (u v : UExp B 0), SameDim (DCtx.nil D) u v → conv V u v = conv V' u v) (ρ : Env (scalarCtx us)) : den V d ρ = den V' d ρ

A first-order scalar denotation depends only on conversion factors between same-dimension units. Unit and dimension binders inside the term are allowed; the external unit/dimension scope is closed.

theorem LambdaS.den_eq_of_coherent {B D : Type} [Fintype B] [DecidableEq B] [Fintype D] [DecidableEq D] [UnitSys B D] {e : Tm B D 0 0} {us : List (UExp B 0)} {u : UExp B 0} (d : HasTy (DCtx.nil D) (scalarCtx us) e (Ty.Q u)) (V ψ : Scaling B 0) (hψ : Scaling.Coherent (DCtx.nil D) ψ) (ρ : Env (scalarCtx us)) : den (V.comp ψ) d ρ = den V d ρ

Composing the valuation with a coherent rescaling leaves the denotation of a first-order scalar program unchanged, even when the program converts.

theorem LambdaS.scaleLaw_coherent {B D : Type} [Fintype B] [DecidableEq B] [Fintype D] [DecidableEq D] [UnitSys B D] {e : Tm B D 0 0} {us : List (UExp B 0)} {u : UExp B 0} (d : HasTy (DCtx.nil D) (scalarCtx us) e (Ty.Q u)) (hp : e.Parametric) (V ψ : Scaling B 0) (Φ : Scaling D 0) (hψ : ψ.Factors (DCtx.nil D) Φ) (ρ : Env (scalarCtx us)) : den V d (scaleEnv ψ us ρ) = ψ.scale u * den V d ρ

The fixed-valuation coherent scaling law, for parametric first-order programs that may convert and may contain internal unit/dimension polymorphism.

def LambdaS.Pi.dimensionExponents {B D : Type} [Fintype B] [UnitSys B D] {m : ℕ} (eqv : Fin m ≃ D ⊕ Fin 0) (u : UExp B 0) : Fin m → ℚ

Exponents of a unit's dimension, in an enumerated dimension basis. The empty summand is retained to reuse the general scaling enumeration.

Equations

• LambdaS.Pi.dimensionExponents eqv u v = Sum.elim (LambdaS.dimOf (LambdaS.DCtx.nil D) u).base (LambdaS.dimOf (LambdaS.DCtx.nil D) u).vars (eqv v)

def LambdaS.Pi.dimensionMatrix {B D : Type} [Fintype B] [UnitSys B D] {m : ℕ} (eqv : Fin m ≃ D ⊕ Fin 0) (us : List (UExp B 0)) : ExpMatrix m us.length

The dimension matrix: different units of one dimension have identical columns, unlike the stronger unit-level matrix used by den_mulScaleLaw.

Equations

• LambdaS.Pi.dimensionMatrix eqv us = Matrix.of fun (v : Fin m) (i : Fin us.length) => LambdaS.Pi.dimensionExponents eqv (us.get i) v

theorem LambdaS.Pi.den_mulScaleLaw_coherent {B D : Type} [Fintype B] [DecidableEq B] [Fintype D] [DecidableEq D] [UnitSys B D] {m : ℕ} {e : Tm B D 0 0} {us : List (UExp B 0)} {u : UExp B 0} (d : HasTy (DCtx.nil D) (scalarCtx us) e (Ty.Q u)) (hp : e.Parametric) (V : Scaling B 0) (eqv : Fin m ≃ D ⊕ Fin 0) : MulScaleLaw (dimensionMatrix eqv us) (dimensionExponents eqv u) fun (x : Fin us.length → ℝ) => den V d (envOf us x)

The classical dimension-level scaling law for converting programs. Any parametric first-order program in closed external unit/dimension scope obeys the multiplicative law over dimensions, for a fixed valuation. The program may contain internal polymorphism and conversion.

theorem LambdaS.Pi.den_pi_coherent {B D : Type} [Fintype B] [DecidableEq B] [Fintype D] [DecidableEq D] [UnitSys B D] {m : ℕ} {e : Tm B D 0 0} {us : List (UExp B 0)} {u : UExp B 0} (d : HasTy (DCtx.nil D) (scalarCtx us) e (Ty.Q u)) (hp : e.Parametric) (V : Scaling B 0) (eqv : Fin m ≃ D ⊕ Fin 0) (X : Fin us.length → ℝ) (hX : ∀ (v : Fin m), ∑ i : Fin us.length, ↑(dimensionMatrix eqv us v i) * X i = ↑(dimensionExponents eqv u v)) : ∃ (G : (Fin (us.length - Matrix.rank (dimensionMatrix eqv us)) → ℝ) → ℝ), ∀ (x : Fin us.length → ℝ), (∀ (i : Fin us.length), 0 < x i) → den V d (envOf us x) = (∏ i : Fin us.length, x i ^ X i) * G (piCoordinates (dimensionMatrix eqv us) fun (i : Fin us.length) => Real.log (x i))

Buckingham's reduced-arity factorization for converting programs. Given a solution X of the dimension-level system, the program factors as in mulScaleLaw_factorization_reduced: over the dimension matrix, on positive arguments, with output of either sign.

theorem LambdaS.Pi.den_pi_coherent_dichotomy {B D : Type} [Fintype B] [DecidableEq B] [Fintype D] [DecidableEq D] [UnitSys B D] {m : ℕ} {e : Tm B D 0 0} {us : List (UExp B 0)} {u : UExp B 0} (d : HasTy (DCtx.nil D) (scalarCtx us) e (Ty.Q u)) (hp : e.Parametric) (V : Scaling B 0) (eqv : Fin m ≃ D ⊕ Fin 0) : (∃ (X : Fin us.length → ℝ), (∀ (v : Fin m), ∑ i : Fin us.length, ↑(dimensionMatrix eqv us v i) * X i = ↑(dimensionExponents eqv u v)) ∧ ∃ (G : (Fin (us.length - Matrix.rank (dimensionMatrix eqv us)) → ℝ) → ℝ), ∀ (x : Fin us.length → ℝ), (∀ (i : Fin us.length), 0 < x i) → den V d (envOf us x) = (∏ i : Fin us.length, x i ^ X i) * G (piCoordinates (dimensionMatrix eqv us) fun (i : Fin us.length) => Real.log (x i))) ∨ ∀ (x : Fin us.length → ℝ), den V d (envOf us x) = 0

The Pi theorem for programs with conversion, as a dichotomy. Either some power product of the arguments has the result's dimension, and the program factors on positive arguments through the dimensionless products (den_pi_coherent), or none does, and the program denotes zero on every argument (den_mulScaleLaw_coherent with mulScaleLaw_eq_zero_of_unsolvable). This is the statement the paper's Pi theorem cites.