Actual primitive fields and budget reserves in the normal-order induction.

noncomputable def AVenhance.Infra.Section4.amnrNormalField (b : AmnrSpace → Homogenization.Vec 2) (f : AmnrSpace → ℝ) : Option (Fin 2 × Fin 2) → AmnrSpace → ℝ

The scalar and the four actual velocity-gradient coefficients are the only primitive fields needed by material/spatial normal ordering.

Equations

• AVenhance.Infra.Section4.amnrNormalField b f none = f
• AVenhance.Infra.Section4.amnrNormalField b f (some (p, i)) = AVenhance.Infra.Section4.amnrVelocityGradient b p i

def AVenhance.Infra.Section4.amnrNormalFieldCost : Option (Fin 2 × Fin 2) → ℕ

Two weighted units reserve the velocity gradient's stream derivatives.

Equations

• AVenhance.Infra.Section4.amnrNormalFieldCost none = 0
• AVenhance.Infra.Section4.amnrNormalFieldCost (some val) = 2

def AVenhance.Infra.Section4.amnrNormalFieldReserve : Option (Fin 2 × Fin 2) → ℕ

Gradient coefficients consume a strictly lower material level.

Equations

• AVenhance.Infra.Section4.amnrNormalFieldReserve none = 0
• AVenhance.Infra.Section4.amnrNormalFieldReserve (some val) = 1

def AVenhance.Infra.Section4.amnrNormalFieldAmplitude (F Cb H : ℝ) : Option (Fin 2 × Fin 2) → ℝ

Actual primitive amplitudes in the source derivative calculus.

Equations

• AVenhance.Infra.Section4.amnrNormalFieldAmplitude F Cb H none = F
• AVenhance.Infra.Section4.amnrNormalFieldAmplitude F Cb H (some val) = Cb * H

theorem AVenhance.Infra.Section4.amnrNormalField_contDiff {b : AmnrSpace → Homogenization.Vec 2} {f : AmnrSpace → ℝ} (hb : ContDiff ℝ (↑⊤) b) (hf : ContDiff ℝ (↑⊤) f) (a : Option (Fin 2 × Fin 2)) : ContDiff ℝ (↑⊤) (amnrNormalField b f a)

theorem AVenhance.Infra.Section4.amnrNormalFieldAmplitude_nonneg {F Cb H : ℝ} (hF : 0 ≤ F) (hCb : 0 ≤ Cb) (hH : 0 ≤ H) (a : Option (Fin 2 × Fin 2)) : 0 ≤ amnrNormalFieldAmplitude F Cb H a

theorem AVenhance.Infra.Section4.amnrMaterialCount_sublist {u v : List (Option (Fin 2))} (hu : u.Sublist v) : amnrMaterialCount u ≤ amnrMaterialCount v

Subword material counts never exceed the outer word's count.

theorem AVenhance.Infra.Section4.amnrAdjacent_subword_budgets (u v : List (Option (Fin 2))) (i p : Fin 2) {s : List (Option (Fin 2))} (hs : s.Sublist u) (c : ℕ) : amnrBudget s + 2 < amnrBudget (u ++ none :: some i :: v) + c ∧ amnrBudget (s ++ some p :: v) + c < amnrBudget (u ++ none :: some i :: v) + c

Each correction factor consumes a strictly smaller weighted budget, including the primitive gradient reserve.

theorem AVenhance.Infra.Section4.amnrAdjacent_subword_material_counts (u v : List (Option (Fin 2))) (i p : Fin 2) {s : List (Option (Fin 2))} (hs : s.Sublist u) : amnrMaterialCount s + 1 ≤ amnrMaterialCount (u ++ none :: some i :: v) ∧ amnrMaterialCount (s ++ some p :: v) + 1 ≤ amnrMaterialCount (u ++ none :: some i :: v)

Both correction factors remain below the material count of the original word. This is the strict lower-level condition needed by the source induction.

theorem AVenhance.Infra.Section4.amnrAdjacent_weight (S H : ℝ) (u v : List (Option (Fin 2))) (i : Fin 2) : amnrWeight S H (u ++ none :: some i :: v) = amnrWeight S H (u ++ some i :: none :: v)

An adjacent swap preserves both rates exactly.

theorem AVenhance.Infra.Section4.amnrAdjacent_weight_factor (S H : ℝ) (u v : List (Option (Fin 2))) (i : Fin 2) : amnrWeight S H (u ++ none :: some i :: v) = amnrWeight S H u * H * S * amnrWeight S H v

Exact factorization of the rates in the original commutator word.

theorem AVenhance.Infra.Section4.amnrMaterialCount_mixed (α : List (Fin 2)) (n : ℕ) : amnrMaterialCount (amnrMixedWord α n) = n

theorem AVenhance.Infra.Section4.amnrAdjacent_budget (u v : List (Option (Fin 2))) (i : Fin 2) : amnrBudget (u ++ none :: some i :: v) = amnrBudget (u ++ some i :: none :: v)

theorem AVenhance.Infra.Section4.amnrAdjacent_material_count (u v : List (Option (Fin 2))) (i : Fin 2) : amnrMaterialCount (u ++ none :: some i :: v) = amnrMaterialCount (u ++ some i :: none :: v)