HmGradientContract (e.Hm.gradient.L2, enhance.tex 5975-5995)

√κ_{m-1} ‖∇HTilde_m‖_{L²((0,1)×𝕋²)} ≤ CH ε_{m-1}^{4δ} B, the κ_{m-1}-normalised gradient bound.

Route (all pieces exist; this file only wires them):

• thetaProfile (amplitude B) and iterate_V_upgrade_of_theta give the V-increment amplitude;
• RelativeError.relative_iterate_gradient_jets (ATA): positive spatial jets of ∇T_i, every i ≤ N*;
• RelativeError.relative_Amnr_tensor_of_jets (ATB): the AMNR Hessian tensor bound at amplitude B;
• hm_gradient_sharp_actual (HmGradientActual.lean): the κ_{m-1}-sharp HTilde gradient bound with the open-time regularity discharged.

Normalisation check: the sharp bound needs a_m² ε_m⁴/κ_m ≲ κ_{m-1} (left_to_show_scales, one-sided at m = M), the diffusivity upper bound for κ_{m-1} (index m - 1 < M), ε_m²/(κ_m τ_m) ≤ 1 (which only needs ε_m²/(κ_m τ_m) ≲ ε_{m-1}^{2δ} from left_to_show_scales, valid through m = M) and the Params bounds. The κ_{m-1} form is therefore true and proved through m = M; no printed m = M diffusivity bound is used.

Producers:

• hmGradient_of_thetaProfile_contract: abstract amplitude B (step-down part (ii) use at B = S), conditional on ThetaProfileContract at amplitude B;
• hmGradient_contract: the unconditional producer at B = ‖θ₀‖.

theorem AVenhance.Infra.Section5.Contracts.hmGradient_of_thetaProfile_contract (β Ccut CsReq : ℝ) (hReq : 1 ≤ CsReq) : ∃ (Cs : ℝ) (CH : ℝ) (C₁ : ℝ), CsReq ≤ Cs ∧ 0 ≤ CH ∧ Integration.OnA7Instances β Ccut C₁ fun (I : Ingredients β) (_Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ) (hΦ : IsStreamSeq I _Φ) (κ : ℝ) (M : ℕ) (_R : ℝ) (_θ₀ : Homogenization.Vec 2 → ℝ) (m : ℕ) (θprev : ℝ → Homogenization.Vec 2 → ℝ) (T : ℕ → ℝ → Homogenization.Vec 2 → ℝ) => ∀ (B : ℝ), 0 ≤ B → Integration.ThetaProfileContract I m (I.kappaSeq κ M (m - 1)) θprev Cs B → Integration.HmGradientContract I hΦ m (I.kappaSeq κ M m) (I.kappaSeq κ M (m - 1)) T CH B

HmGradientContract at an abstract amplitude B, conditional only on the θ profile at amplitude B (profile constant Cs ≥ CsReq, chosen before the instance).

theorem AVenhance.Infra.Section5.Contracts.hmGradient_contract (β C₀ : ℝ) : ∃ (C : ℝ) (C₁ : ℝ), Integration.OnA7Instances β C₀ C₁ fun (I : Ingredients β) (_Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ) (hΦ : IsStreamSeq I _Φ) (κ : ℝ) (M : ℕ) (_R : ℝ) (θ₀ : Homogenization.Vec 2 → ℝ) (m : ℕ) (_θprev : ℝ → Homogenization.Vec 2 → ℝ) (T : ℕ → ℝ → Homogenization.Vec 2 → ℝ) => Integration.HmGradientContract I hΦ m (I.kappaSeq κ M m) (I.kappaSeq κ M (m - 1)) T C √(l2NormSq θ₀)

HmGradientContract (e.Hm.gradient.L2) at the datum amplitude B = ‖θ₀‖_{L²}: the exact unconditional producer.