Exact amplitude cancellation in material correction products.

theorem AVenhance.Infra.Section4.amnr_correction_scale_cancel {V S H : ℝ} (hVS : V * S = H) (L M k n : ℕ) (hn : M + L = n) : V ^ (L + 1) * S ^ (L + k) * H ^ M = V * S ^ k * H ^ n

Each fast factor supplies exactly the material rate consumed by its advection. This identity avoids losing a scale factor at higher levels.

theorem AVenhance.Infra.Section4.amnrCorrectionTerm_abs_le {c : AmnrSpace → Homogenization.Vec 2} {v : Fin 2 → AmnrSpace → ℝ} {f : AmnrSpace → ℝ} {S H V C F : ℝ} (hS : 0 ≤ S) (hH : 0 ≤ H) (hV : 0 ≤ V) (hC : 0 ≤ C) (hVS : V * S = H) (α : List (Fin 2)) (n : ℕ) (t : AmnrAdvectionTerm) (ht : t ∈ amnrSpatialAdvectionTerms α (amnrMaterialErrorTerms n)) (z : AmnrSpace) (hA : ∀ a ∈ t.factors, |amnrWord c a.2 (v a.1) z| ≤ C * V * amnrWeight S H a.2) (hf : |amnrWord c t.scalarWord f z| ≤ F * V * amnrWeight S H t.scalarWord) : |amnrAdvectionTermValue c v f t z| ≤ C ^ t.factors.length * F * V * S ^ α.length * H ^ n

A genuine material correction has only lower-level jets; their actual product has the correct current-scale amplitude and derivative rates.