Theta profile at the datum amplitude 2‖θ₀‖ in the big-bound premise block

ThetaProfile.thetaProfile_contract is stated for the step-down premise block (OnA8Instances), but its proof never uses the classical θ_m. The step-down part (i)/big-bound estimate consumers of the amplitude 2‖θ₀‖ (the gradient of HTilde_m, hmGradient_contract) live in the big-bound premise block, so this file restates it there (thetaProfileA7_contract). The private lemma of ThetaProfile.lean is reproduced (hg_theta_profile_of_explicit_A3_A5); making it public there would remove this duplication.

theorem AVenhance.Infra.Section5.Contracts.HmGradientTheta.hg_iterateSpatialWord_eq_classicalWordDerivative (w : List (Fin 2)) (f : Homogenization.Vec 2 → ℝ) : Section4.iterateSpatialWord w f = Section4.classicalWordDerivative w f

theorem AVenhance.Infra.Section5.Contracts.HmGradientTheta.hg_theta_profile_of_explicit_A3_A5 {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) {m M : ℕ} (hm : 2 ≤ m) (hmM : m ≤ M) {κ R : ℝ} {θ₀ : Homogenization.Vec 2 → ℝ} {θprev : ℝ → Homogenization.Vec 2 → ℝ} (hR : 0 < R) (hscale : epsilon β I.Λ (m - 1) ^ (1 + gamma β / 2) ≤ R) (hθ₀ : IsThetaAnalytic R θ₀) (hθprev : IsClassicalSol (streamVel (Φ (m - 1))) (I.kappaSeq κ M (m - 1)) (fun (x : ℝ) (x_1 : Homogenization.Vec 2) => 0) θ₀ θprev) {c C Cs : ℝ} (hc : 0 < c) (hcC : c < C) (hRadius : 8 * max (Section4.thetaAnalyticRadiusBase c) 2 ≤ Cs) (hA3 : ∀ (j : ℕ), 1 ≤ j → ∀ (t : ℝ) (n : ℕ), 2 ≤ n → barNorm n (2 ^ 8 * (epsilon β I.Λ j)⁻¹) (Φ j t) ≤ ENNReal.ofReal (2 ^ 5 * AVenhance.a β I.Λ j * epsilon β I.Λ j ^ 2 * ((↑n + 2) ^ 2 / (↑n + 1) ^ 3))) (hA5 : ∀ (j : ℕ), 1 ≤ j → j < M → c * (AVenhance.a β I.Λ j * epsilon β I.Λ j ^ (2 + gamma β)) ≤ I.kappaAt κ j (M - j) ∧ I.kappaAt κ j (M - j) ≤ C * (AVenhance.a β I.Λ j * epsilon β I.Λ j ^ (2 + gamma β))) : Section4.iterateCoordinateEnergyProfile θprev (I.kappaSeq κ M (m - 1)) (2 * √(l2NormSq θ₀)) (Cs * epsilon β I.Λ (m - 1) ^ (-1 - gamma β / 2)) 0

theorem AVenhance.Infra.Section5.Contracts.thetaProfileA7_contract (β C₀ : ℝ) : ∃ (CsReq : ℝ), 1 ≤ CsReq ∧ ∀ (Cs : ℝ), CsReq ≤ Cs → Integration.OnA7Instances β C₀ 0 fun (I : Ingredients β) (_Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ) (_hΦ : IsStreamSeq I _Φ) (κ : ℝ) (M : ℕ) (_R : ℝ) (θ₀ : Homogenization.Vec 2 → ℝ) (m : ℕ) (θprev : ℝ → Homogenization.Vec 2 → ℝ) (_T : ℕ → ℝ → Homogenization.Vec 2 → ℝ) => Integration.ThetaProfileContract I m (I.kappaSeq κ M (m - 1)) θprev Cs (2 * √(l2NormSq θ₀))

The exact theta-profile contract at the amplitude 2‖θ₀‖, in the big-bound premise block (constants fixed before the instance), for every profile constant Cs above an explicit threshold CsReq. Same proof as thetaProfile_contract, which does not use the classical θ_m of the step-down premise block.