Dimension-level Buckingham factorization for converting programs

PiTheorem.den_mulScaleLaw uses independent rescaling of every unit symbol, which requires conversion freedom or a drift-free diagnosis. 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. Its external unit and dimension scope is closed (j = k = 0); the program may use all term constructors, including unit and dimension binders 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 ρ

Coherent rescaling leaves the valuation dependence of any first-order scalar program unchanged, even when the program contains conversion.

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 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. The matrix is over dimensions; positive arguments and arbitrary signed output are exactly the domain of mulScaleLaw_factorization_reduced.