Step-down part (i) wiring: IndyStepDownPartIStatement from the explicit inputs

indystepdown_part_i_of_inputs turns the conditional conjunct-(i) theorem indyStepDown_part_i_conditional into the literal step-down estimate conjunct-(i) proposition IndyStepDownPartIStatement β C₀, given the literal big-bound estimate proposition BigBoundStatement β C₀ (the conclusion of the public statement is taken literally) and, for each admissible instance, the Prop-valued IndyPartIInputs.

Conjunct (ii) (the ratio form) is deliberately untouched.

Hypotheses of indyStepDown_part_i_conditional that are derived here and so are not fields:

• the four MemL2On hypotheses hU hAT hTP hAP. They follow from continuity of the classical solutions θ_m, θ_{m-1} and of the iterate T_{m-1} on each time slice, continuity of the ΧTilde-corrector series of the ansatz (finite sum at fixed time of continuous terms), and the smoothness of the slices of HTilde_m at positive times (Hm_slice_contDiff_pos);
• the HTilde_m regularity (joint C^∞ on (0,∞) × ℝ², smooth and periodic positive-time slices): unconditional for the actual iterates (PartIHmRegularity*), so no longer an input;
• the classical forced energy estimate IndyPartIInputs.energy (with Cenergy = 2), proved from forced_energy_estimate_Ioi using that regularity, the ansatz regularity on the open half space (ansatz_contDiffOn_two_Ioi) and the finiteness of the L²H⁻¹ norm of the ansatz residual (which follows from the big-bound estimate hypothesis);

Open-time form. The Amnr uses two-sided time derivatives, so θTilde_m(0) and the regularity of HTilde_m at t = 0 depend on the arbitrary negative-time extension of T. Everything that involves the ansatz is therefore stated for t > 0 (initial defect as s → 0⁺, the ansatz bound on (0,1]); t = 0 is recovered in indyStepDown_part_i_conditional_Ioc from θ_m(0) = θ₀ = θ_{m-1}(0) and the time-independence of the gradient term.

• the big-bound estimate hypothesis hA7 (from the big-bound estimate body, by timeHMinusOneNorm_le_of_bigbound_conclusion);
• 0 ≤ C₇ (take max C 0), positivity of κ_m, and hβ hβ' hΛ (from the Ingredients API).

Slice continuity of the pieces of the ansatz

theorem AVenhance.Infra.Section5.Integration.continuous_spaceGrad_of_contDiff_two {g : Homogenization.Vec 2 → ℝ} (hg : ContDiff ℝ 2 g) : Continuous (spaceGrad g)

The spatial gradient of a C² function is continuous.

theorem AVenhance.Infra.Section5.Integration.continuous_uShear (β : ℝ) (Λ m : ℕ) (k : ℤ) : Continuous (uShear β Λ m k)

The shear field u_{m,k} is continuous.

theorem AVenhance.Infra.Section5.Integration.continuous_chiTilde {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (κm : ℝ) (k : ℤ) (t : ℝ) : Continuous (I.chiTilde hΦ m κm k t)

The twisted corrector ΧTilde_{m,k}(t,·) is continuous at each fixed time.

theorem AVenhance.Infra.Section5.Integration.continuous_ansatz_series {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (κm : ℝ) {T : ℝ → Homogenization.Vec 2 → ℝ} {t : ℝ} (hT : ContDiff ℝ 2 (T t)) : Continuous fun (x : Homogenization.Vec 2) => ∑' (k : ℤ), I.xiMK m k t * Homogenization.vecDot (I.chiTilde hΦ m κm k t x) (spaceGrad (fun (y : Homogenization.Vec 2) => T t (I.xFlow hΦ m (lIdx β I.Λ m k) t y)) (I.xFlowInv hΦ m (lIdx β I.Λ m k) t x))

At a fixed time, the series of the ansatz is continuous in the position, provided the iterate T_{m-1}(t) is C² in the position.

theorem AVenhance.Infra.Section5.Integration.tNstar_contDiff_of_nonneg {β : ℝ} (I : Ingredients β) {m : ℕ} {κm κprev : ℝ} {θ₀ : Homogenization.Vec 2 → ℝ} {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} {hΦ : IsStreamSeq I Φ} {θprev : ℝ → Homogenization.Vec 2 → ℝ} {T : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hθprev : IsClassicalSol (streamVel (Φ (m - 1))) κprev (fun (x : ℝ) (x_1 : Homogenization.Vec 2) => 0) θ₀ θprev) (hT : I.IsTIterates hΦ m κm κprev θ₀ θprev T) {t : ℝ} (ht : 0 ≤ t) : ContDiff ℝ (↑⊤) (T (Nstar β) t)

The iterate T_{m-1} = T (Nstar β) is smooth in the position at every nonnegative time.

The explicit conditional theorem (constant exposed, open-time)

theorem AVenhance.Infra.Section5.Integration.indyStepDown_part_i_conditional_Ioc {β : ℝ} (I : Ingredients β) (hβ : 1 < β) (hβ' : β < 4 / 3) (hΛ : 2 ^ 7 ≤ I.Λ) (Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ) (hΦ : IsStreamSeq I Φ) (m M : ℕ) (κ : ℝ) (θ₀ : Homogenization.Vec 2 → ℝ) (θm θprev : ℝ → Homogenization.Vec 2 → ℝ) (T : ℕ → ℝ → Homogenization.Vec 2 → ℝ) (hκm : 0 < I.kappaSeq κ M m) (hθm0 : ∀ (x : Homogenization.Vec 2), θm 0 x = θ₀ x) (hθprev0 : ∀ (x : Homogenization.Vec 2), θprev 0 x = θ₀ x) (C₇ Cᵢ Cₐ Cₜ Cenergy : ℝ) (hC₇ : 0 ≤ C₇) (hCenergy : 0 ≤ Cenergy) (hU : ∀ t ∈ Set.Ioc 0 1, Homogenization.MemL2On unitCube fun (x : Homogenization.Vec 2) => θm t x - I.ansatz hΦ m (I.kappaSeq κ M m) (T (Nstar β)) t x) (hAT : ∀ t ∈ Set.Ioc 0 1, Homogenization.MemL2On unitCube fun (x : Homogenization.Vec 2) => I.ansatz hΦ m (I.kappaSeq κ M m) (T (Nstar β)) t x - T (Nstar β) t x) (hTP : ∀ t ∈ Set.Ioc 0 1, Homogenization.MemL2On unitCube fun (x : Homogenization.Vec 2) => T (Nstar β) t x - θprev t x) (hAP : ∀ t ∈ Set.Ioc 0 1, Homogenization.MemL2On unitCube fun (x : Homogenization.Vec 2) => I.ansatz hΦ m (I.kappaSeq κ M m) (T (Nstar β)) t x - θprev t x) (hA7 : (timeHMinusOneNorm fun (t : ℝ) (x : Homogenization.Vec 2) => advDiffOp (streamVel (Φ m)) (I.kappaSeq κ M m) (I.ansatz hΦ m (I.kappaSeq κ M m) (T (Nstar β))) t x) ≤ ENNReal.ofReal (C₇ * epsilon β I.Λ (m - 1) ^ delta β * √(I.kappaSeq κ M m) * √(l2NormSq θ₀))) (hEnergy : ∀ t ∈ Set.Ioc 0 1, √(l2NormSq fun (x : Homogenization.Vec 2) => θm t x - I.ansatz hΦ m (I.kappaSeq κ M m) (T (Nstar β)) t x) + √(I.kappaSeq κ M m) * √(spaceTimeGradNormSq fun (s : ℝ) (x : Homogenization.Vec 2) => spaceGrad (θm s) x - spaceGrad (I.ansatz hΦ m (I.kappaSeq κ M m) (T (Nstar β)) s) x) ≤ Cenergy * (Cᵢ * epsilon β I.Λ (m - 1) ^ delta β * √(l2NormSq θ₀) + (timeHMinusOneNorm fun (s : ℝ) (x : Homogenization.Vec 2) => advDiffOp (streamVel (Φ m)) (I.kappaSeq κ M m) (I.ansatz hΦ m (I.kappaSeq κ M m) (T (Nstar β))) s x).toReal / √(I.kappaSeq κ M m))) (hSectionFourAnsatz : ∀ t ∈ Set.Ioc 0 1, √(l2NormSq fun (x : Homogenization.Vec 2) => I.ansatz hΦ m (I.kappaSeq κ M m) (T (Nstar β)) t x - T (Nstar β) t x) ≤ Cₐ * epsilon β I.Λ (m - 1) ^ delta β * √(l2NormSq θ₀)) (hSectionFourIterate : ∀ t ∈ Set.Icc 0 1, √(l2NormSq fun (x : Homogenization.Vec 2) => T (Nstar β) t x - θprev t x) ≤ Cₜ * epsilon β I.Λ (m - 1) ^ delta β * √(l2NormSq θ₀)) (t : ℝ) : t ∈ Set.Icc 0 1 → √(l2NormSq fun (x : Homogenization.Vec 2) => θm t x - θprev t x) + √(I.kappaSeq κ M m) * √(spaceTimeGradNormSq fun (s : ℝ) (x : Homogenization.Vec 2) => spaceGrad (θm s) x - spaceGrad (I.ansatz hΦ m (I.kappaSeq κ M m) (T (Nstar β)) s) x) ≤ (Cenergy * (Cᵢ + C₇) + Cₐ + Cₜ) * epsilon β I.Λ (m - 1) ^ delta β * √(l2NormSq θ₀)

AVenhance.Infra.Section5.indyStepDown_part_i_conditional with its constant named, and with the ansatz-dependent hypotheses on the half-open time interval (0,1] only. The Amnr uses two-sided time derivatives, so θTilde_m and HTilde_m at t = 0 depend on the arbitrary negative-time extension of T; none of the hypotheses below mentions the ansatz at t = 0. The initial defect enters through the energy hypothesis hEnergy (with the constant D = Cᵢ ε^δ ‖θ₀‖, a bound valid for the energy estimate by forced_energy_estimate_Ioi once the defect is small as s → 0⁺).

The conclusion is still on the closed interval [0,1]: at t = 0 the first term vanishes (θ_m(0) = θ₀ = θ_{m-1}(0)) and the gradient term does not depend on t, so it is bounded by the t = 1 instance.

The inputs structure

structure AVenhance.Infra.Section5.Integration.IndyPartIInputs {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (κm : ℝ) (θ₀ : Homogenization.Vec 2 → ℝ) (θm θprev : ℝ → Homogenization.Vec 2 → ℝ) (T : ℕ → ℝ → Homogenization.Vec 2 → ℝ) (Cᵢ Cₐ Cₜ : ℝ) : Prop

The remaining estimates feeding step-down part (i), for one instance (κm = κ_m, θm = θ_m, θprev = θ_{m-1}, T = T^{(·)} the iterates, T_{m-1} = T (Nstar β)). No field is (or contains) the step-down estimate conclusion or the big-bound estimate; the four MemL2On hypotheses of the conditional theorem, the HTilde_m regularity and the classical forced energy estimate are not fields (see IndyPartIInputs.memL2 and IndyPartIInputs.energy).

• hInitial: the aggregate initial defect ‖θ_m(s) − θTilde_m(s)‖_{L²} ≤ Cᵢ ε^δ ‖θ₀‖ for all small s > 0 (s → 0⁺; the ansatz at t = 0 itself depends on the negative-time extension of T). Source: e.tildethetam.to.Tm initial data (oscillatory corrector gives ε^{4δ}, HTilde_m only ε^δ).
• hSectionFourAnsatz: ‖θTilde_m(t) − T_{m-1}(t)‖_{L²} ≤ Cₐ ε^δ ‖θ₀‖ for t ∈ (0,1]. Source: e.tildethetam.to.Tm (8882–9133).
• hSectionFourIterate: ‖T_{m-1}(t) − θ_{m-1}(t)‖_{L²} ≤ Cₜ ε^δ ‖θ₀‖. Source: e.Tm.thetam / l.Tm.minus.thetam.

• hInitial : InitialLayerContract I hΦ m κm θm T Cᵢ √(l2NormSq θ₀)

  Aggregate initial defect from the right, e.tildethetam.to.Tm initial data.

• hSectionFourAnsatz : SectionFourAnsatzContract I hΦ m κm θ₀ T Cₐ

  e.tildethetam.to.Tm, 8882–9133, for t ∈ (0,1].

• hSectionFourIterate : SectionFourIterateContract I m θ₀ θprev T Cₜ

  e.Tm.thetam / l.Tm.minus.thetam.

theorem AVenhance.Infra.Section5.Integration.IndyPartIInputs.memL2 {β : ℝ} {I : Ingredients β} {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} {hΦ : IsStreamSeq I Φ} {m : ℕ} {κm κprev : ℝ} {θ₀ : Homogenization.Vec 2 → ℝ} {θm θprev : ℝ → Homogenization.Vec 2 → ℝ} {T : ℕ → ℝ → Homogenization.Vec 2 → ℝ} {Cᵢ Cₐ Cₜ : ℝ} (_h : IndyPartIInputs I hΦ m κm θ₀ θm θprev T Cᵢ Cₐ Cₜ) (hm : 1 ≤ m) (hκm : 0 < κm) {κ' : ℝ} (hθm : IsClassicalSol (streamVel (Φ m)) κ' (fun (x : ℝ) (x_1 : Homogenization.Vec 2) => 0) θ₀ θm) (hθprev : IsClassicalSol (streamVel (Φ (m - 1))) κprev (fun (x : ℝ) (x_1 : Homogenization.Vec 2) => 0) θ₀ θprev) (hT : I.IsTIterates hΦ m κm κprev θ₀ θprev T) : (∀ t ∈ Set.Ioc 0 1, Homogenization.MemL2On unitCube fun (x : Homogenization.Vec 2) => θm t x - I.ansatz hΦ m κm (T (Nstar β)) t x) ∧ (∀ t ∈ Set.Ioc 0 1, Homogenization.MemL2On unitCube fun (x : Homogenization.Vec 2) => I.ansatz hΦ m κm (T (Nstar β)) t x - T (Nstar β) t x) ∧ (∀ t ∈ Set.Ioc 0 1, Homogenization.MemL2On unitCube fun (x : Homogenization.Vec 2) => T (Nstar β) t x - θprev t x) ∧ ∀ t ∈ Set.Ioc 0 1, Homogenization.MemL2On unitCube fun (x : Homogenization.Vec 2) => I.ansatz hΦ m κm (T (Nstar β)) t x - θprev t x

The four MemL2On hypotheses of indyStepDown_part_i_conditional_Ioc on (0,1], derived from the premises (θ_m, θ_{m-1} classical solutions, T the iterates) and the unconditional positive-time smoothness of HTilde_m (Hm_slice_contDiff_pos; a smooth slice is continuous, hence L² on the cube). The inputs record _h is not used: this is a statement about the actual iterates, stated as a method for uniformity with IndyPartIInputs.energy.

theorem AVenhance.Infra.Section5.Integration.tNstar_isClassicalSol {β : ℝ} {I : Ingredients β} {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} {m : ℕ} {κm κprev : ℝ} {θ₀ : Homogenization.Vec 2 → ℝ} {hΦ : IsStreamSeq I Φ} {θprev : ℝ → Homogenization.Vec 2 → ℝ} {T : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hθprev : IsClassicalSol (streamVel (Φ (m - 1))) κprev (fun (x : ℝ) (x_1 : Homogenization.Vec 2) => 0) θ₀ θprev) (hT : I.IsTIterates hΦ m κm κprev θ₀ θprev T) : ∃ (F : ℝ → Homogenization.Vec 2 → ℝ), IsClassicalSol (streamVel (Φ (m - 1))) κprev F θ₀ (T (Nstar β))

The iterate T_{m-1} = T (Nstar β) is a classical solution of some forced equation (for Nstar β = 0 it is θ_{m-1}), hence jointly smooth and periodic in the position.

theorem AVenhance.Infra.Section5.Integration.IndyPartIInputs.energy {β : ℝ} {I : Ingredients β} {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} {hΦ : IsStreamSeq I Φ} {m : ℕ} {κm κprev : ℝ} {θ₀ : Homogenization.Vec 2 → ℝ} {θm θprev : ℝ → Homogenization.Vec 2 → ℝ} {T : ℕ → ℝ → Homogenization.Vec 2 → ℝ} {Cᵢ Cₐ Cₜ : ℝ} (h : IndyPartIInputs I hΦ m κm θ₀ θm θprev T Cᵢ Cₐ Cₜ) (hm : 1 ≤ m) (hκm : 0 < κm) (hθm : IsClassicalSol (streamVel (Φ m)) κm (fun (x : ℝ) (x_1 : Homogenization.Vec 2) => 0) θ₀ θm) (hθprev : IsClassicalSol (streamVel (Φ (m - 1))) κprev (fun (x : ℝ) (x_1 : Homogenization.Vec 2) => 0) θ₀ θprev) (hT : I.IsTIterates hΦ m κm κprev θ₀ θprev T) (hfin : (timeHMinusOneNorm fun (s : ℝ) (x : Homogenization.Vec 2) => advDiffOp (streamVel (Φ m)) κm (I.ansatz hΦ m κm (T (Nstar β))) s x) ≠ ⊤) (t : ℝ) : t ∈ Set.Ioc 0 1 → √(l2NormSq fun (x : Homogenization.Vec 2) => θm t x - I.ansatz hΦ m κm (T (Nstar β)) t x) + √κm * √(spaceTimeGradNormSq fun (s : ℝ) (x : Homogenization.Vec 2) => spaceGrad (θm s) x - spaceGrad (I.ansatz hΦ m κm (T (Nstar β)) s) x) ≤ 2 * (Cᵢ * epsilon β I.Λ (m - 1) ^ delta β * √(l2NormSq θ₀) + (timeHMinusOneNorm fun (s : ℝ) (x : Homogenization.Vec 2) => advDiffOp (streamVel (Φ m)) κm (I.ansatz hΦ m κm (T (Nstar β))) s x).toReal / √κm)

The classical forced energy estimate for θ_m − θTilde_m (Cenergy = 2) on (0,1], derived from forced_energy_estimate_Ioi with u = θ_m, v = θTilde_m, φ = Φ m: the admissibility of Φ m is hΦ.adm_pred (m + 1), the regularity of the ansatz on the open half space comes from the unconditional HTilde_m regularity (PartIHmRegularity*) and the iterate T_{m-1}, the initial defect is the field hInitial (as s → 0⁺), and hfin is the finiteness of the L²H⁻¹ norm of the ansatz residual.

The step-down part (i) wiring theorem

def AVenhance.Infra.Section5.Integration.PartIFamilyContract (β C₀ : ℝ) : Prop

Family contract for step-down part (i) (IndyStepDownV2Inputs.partI): constants C₁ (Λ-threshold), Cᵢ, Cₐ, Cₜ chosen before I, then IndyPartIInputs on the step-down premise block OnA8Instances.

Equations

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

theorem AVenhance.Infra.Section5.Integration.indystepdown_part_i_of_inputs (β C₀ : ℝ) (hA7 : BigBoundStatement β C₀) (hin : PartIFamilyContract β C₀) : IndyStepDownPartIStatement β C₀

Step-down part (i) wiring. Given the big-bound estimate proposition BigBoundStatement β C₀ and, for every admissible instance with C₁ ≤ Λ, the explicit IndyPartIInputs (the remaining §4/initial-layer/energy estimates), the step-down estimate conjunct-(i) proposition IndyStepDownPartIStatement β C₀ holds with C = max (max C₇ C₁) (2 * (Cᵢ + max C₇ 0) + Cₐ + Cₜ), C₇ the big-bound estimate constant.

theorem AVenhance.Infra.Section5.Integration.indystepdown_part_i_of_all_inputs (β C₀ : ℝ) (hbb : BigBoundFamilyContract β C₀) (hin : PartIFamilyContract β C₀) : IndyStepDownPartIStatement β C₀

Step-down estimate conjunct (i) from the big-bound estimate input list and the step-down part (i) input list (composition of bigbound_of_inputs and indystepdown_part_i_of_inputs); no statement file is used.