Fuel-free comparison of open first-order ratios

Every scalar component of a first-order context receives its own fresh unit variable. Tw.nf evaluates in that symbolic environment by structural recursion: internal functions, higher-order applications, and unit binders impose no fuel bound. Unknown function and unit-family inputs are outside this interface. The correctness and exactness statements quantify over arbitrary positive input drifts, not an all-ones environment. The normal form is Tw.openNF; Tw.openNF_eq_iff is the exactness theorem, and Tw.normEq (in LambdaS.Twist) uses it at first-order contexts.

def LambdaS.Shape.firstOrder : Shape → Bool

Shapes whose unknown values have finitely many independent scalar components.

Equations

• LambdaS.Shape.scalar.firstOrder = true
• (LambdaS.Shape.vec a).firstOrder = true
• (LambdaS.Shape.mat a a_1).firstOrder = true
• (a.arrow a_1).firstOrder = false
• a.bind.firstOrder = false

@[reducible]

def LambdaS.Shape.cells : Shape → ℕ

Number of independent scalar components. Higher-order inputs are excluded.

Equations

• LambdaS.Shape.scalar.cells = 1
• (LambdaS.Shape.vec a).cells = a
• (LambdaS.Shape.mat a a_1).cells = a_1 * a
• (a.arrow a_1).cells = 0
• a.bind.cells = 0

def LambdaS.Shape.decode (s : Shape) : (Fin s.cells → SemScalar) → SemTw s

Reconstruct a value from its scalar components.

Equations

• LambdaS.Shape.scalar.decode f = f 0
• (LambdaS.Shape.vec a).decode f = f
• (LambdaS.Shape.mat a a_1).decode f = fun (j : Fin a_1) (i : Fin a) => f (finProdFinEquiv (j, i))
• (a.arrow t).decode x_2 = LambdaS.oneSem (a.arrow t)
• t.bind.decode x_2 = LambdaS.oneSem t.bind

def LambdaS.Shape.encode (s : Shape) : SemTw s → Fin s.cells → SemScalar

Read scalar components out of a value.

Equations

• LambdaS.Shape.scalar.encode v x_3 = v
• (LambdaS.Shape.vec a).encode v i = v i
• (LambdaS.Shape.mat a a_1).encode v i = v (finProdFinEquiv.symm i).1 (finProdFinEquiv.symm i).2
• (a.arrow a_1).encode x_3 i = i.elim0
• a.bind.encode x_3 i = i.elim0

theorem LambdaS.Shape.decode_encode (s : Shape) (h : s.firstOrder = true) (v : SemTw s) : s.decode (s.encode v) = v

Component reconstruction preserves every first-order value.

def LambdaS.Shape.reflect {B : Type} {k : ℕ} (s : Shape) : (Fin s.cells → UExp B k) → SynTw B k s

Reflect symbolic scalar components at their shape.

Equations

• LambdaS.Shape.scalar.reflect f = f 0
• (LambdaS.Shape.vec a).reflect f = f
• (LambdaS.Shape.mat a a_1).reflect f = fun (j : Fin a_1) (i : Fin a) => f (finProdFinEquiv (j, i))
• (s.arrow t).reflect x_2 = LambdaS.SynTw.one (s.arrow t)
• t.bind.reflect x_2 = LambdaS.SynTw.one t.bind

theorem LambdaS.Shape.reflect_correct {B : Type} [Fintype B] {k : ℕ} (ψ : Scaling B k) (s : Shape) (f : Fin s.cells → UExp B k) : SRel ψ s (s.reflect f) (s.decode fun (i : Fin s.cells) => ⟨ψ.scale (f i), ⋯⟩)

Reflection respects the symbolic logical relation.

@[reducible]

def LambdaS.ratioCells : List Shape → ℕ

Total number of independent context components.

Equations

• LambdaS.ratioCells [] = 0
• LambdaS.ratioCells (s :: Θ) = s.cells + LambdaS.ratioCells Θ

def LambdaS.ratioFirstOrder (Θ : List Shape) : Bool

A first-order context may contain scalars, vectors and matrices, but no functions or unit families.

Equations

• LambdaS.ratioFirstOrder Θ = Θ.all LambdaS.Shape.firstOrder

def LambdaS.decodeRatioEnv (Θ : List Shape) : (Fin (ratioCells Θ) → SemScalar) → TwEnv Θ

Reconstruct an environment from independent scalar components.

Equations

• One or more equations did not get rendered due to their size.
• LambdaS.decodeRatioEnv [] x_2 = PUnit.unit

def LambdaS.encodeRatioEnv (Θ : List Shape) : TwEnv Θ → Fin (ratioCells Θ) → SemScalar

Read all scalar components of a context.

Equations

• LambdaS.encodeRatioEnv [] x_3 i = i.elim0
• LambdaS.encodeRatioEnv (s :: Θ) ρ i = Fin.addCases (s.encode ρ.1) (LambdaS.encodeRatioEnv Θ ρ.2) i

theorem LambdaS.decode_encode_ratioEnv (Θ : List Shape) (h : ratioFirstOrder Θ = true) (ρ : TwEnv Θ) : decodeRatioEnv Θ (encodeRatioEnv Θ ρ) = ρ

No information is lost for first-order contexts.

def LambdaS.reflectRatioEnv {B : Type} {k : ℕ} (Θ : List Shape) : (Fin (ratioCells Θ) → UExp B k) → SynEnv B k Θ

Reflect a context using distinct symbolic scalar components.

Equations

• One or more equations did not get rendered due to their size.
• LambdaS.reflectRatioEnv [] x_2 = PUnit.unit

theorem LambdaS.reflectRatioEnv_correct {B : Type} [Fintype B] {k : ℕ} (ψ : Scaling B k) (Θ : List Shape) (f : Fin (ratioCells Θ) → UExp B k) : SRelEnv ψ Θ (reflectRatioEnv Θ f) (decodeRatioEnv Θ fun (i : Fin (ratioCells Θ)) => ⟨ψ.scale (f i), ⋯⟩)

Context reflection is related to its componentwise interpretation.

def LambdaS.Tw.openNF {B : Type} {k : ℕ} {Θ : List Shape} (t : Tw B k Θ Shape.scalar) : UExp B (k + ratioCells Θ)

Fuel-free scalar normal form, with fresh coordinates for every input component. Exactness for arbitrary environments requires ratioFirstOrder Θ = true.

Equations

• One or more equations did not get rendered due to their size.

def LambdaS.ratioUnitScaling {B : Type} {k : ℕ} {Θ : List Shape} (χ : Scaling B (k + ratioCells Θ)) : Scaling B k

Split the enlarged scaling into the original unit scope.

Equations

• LambdaS.ratioUnitScaling χ = { base := χ.base, vars := fun (i : Fin k) => χ.vars (Fin.castAdd (LambdaS.ratioCells Θ) i) }

noncomputable def LambdaS.ratioInputEnv {B : Type} {k : ℕ} (Θ : List Shape) (χ : Scaling B (k + ratioCells Θ)) : TwEnv Θ

Interpret the fresh coordinates as independent positive input drifts.

Equations

• LambdaS.ratioInputEnv Θ χ = LambdaS.decodeRatioEnv Θ fun (i : Fin (LambdaS.ratioCells Θ)) => ⟨Real.exp (χ.vars (Fin.natAdd k i)), ⋯⟩

theorem LambdaS.Tw.openNF_correct {B : Type} [Fintype B] {k : ℕ} {Θ : List Shape} (t : Tw B k Θ Shape.scalar) (χ : Scaling B (k + ratioCells Θ)) : ↑(eval (ratioUnitScaling χ) t (ratioInputEnv Θ χ)) = χ.scale t.openNF

Correctness under every assignment of original and fresh coordinates.

noncomputable def LambdaS.extendRatioScaling {B : Type} {k : ℕ} {Θ : List Shape} (ψ : Scaling B k) (ρ : TwEnv Θ) : Scaling B (k + ratioCells Θ)

Extend any original scaling with the logarithms of the actual input drifts.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem LambdaS.ratioUnitScaling_extend {B : Type} {k : ℕ} {Θ : List Shape} (ψ : Scaling B k) (ρ : TwEnv Θ) : ratioUnitScaling (extendRatioScaling ψ ρ) = ψ

Restriction recovers the original unit scaling.

@[simp]

theorem LambdaS.ratioInputEnv_extend {B : Type} {k : ℕ} {Θ : List Shape} (h : ratioFirstOrder Θ = true) (ψ : Scaling B k) (ρ : TwEnv Θ) : ratioInputEnv Θ (extendRatioScaling ψ ρ) = ρ

Every first-order environment is represented by fresh coordinates.

theorem LambdaS.Tw.openNF_sound {B : Type} [Fintype B] {k : ℕ} {Θ : List Shape} (a b : Tw B k Θ Shape.scalar) (hΘ : ratioFirstOrder Θ = true) (h : a.openNF = b.openNF) (ψ : Scaling B k) (ρ : TwEnv Θ) : eval ψ a ρ = eval ψ b ρ

Equal open normal forms agree at arbitrary positive first-order inputs.

theorem LambdaS.Tw.openNF_eq_iff {B : Type} [Fintype B] {k : ℕ} {Θ : List Shape} (a b : Tw B k Θ Shape.scalar) (hΘ : ratioFirstOrder Θ = true) : a.openNF = b.openNF ↔ ∀ (ψ : Scaling B k) (ρ : TwEnv Θ), eval ψ a ρ = eval ψ b ρ

Exactness includes all internal higher-order applications and unit binders; only the unknown input context must be first-order.