Step-down assembly: IndyStepDownStatement from named inputs

indystepdown_v2_of_inputs proves the literal step-down proposition IndyStepDownStatement β C₀ (conjuncts (i) and (ii), one constant) from the Prop-valued input record IndyStepDownV2Inputs.

• conjunct (i) is indystepdown_part_i_of_all_inputs (big-bound estimate inputs BigBoundInputs and step-down part (i) inputs IndyPartIInputs);
• conjunct (ii) is RelativeError.relative_step, fed by the same BigBoundInputs / IndyPartIInputs instances for the leaves they already contain (residual identity, the ten-term joint continuity, the HTilde_m regularity is currently carried by RelativeLeaves, see its provisional fields) and by the additional record RelativeLeaves;
• the joint continuity of leadingGrad … (T (Nstar β)) is proved here (leadingGrad_continuousOn_Ici) from leadingMatrix_continuous and spaceGrad_continuousOn.

No field is (or contains) a step-down estimate conjunct. The statement files are not imported.

Continuity of the leading gradient (a derived leaf)

theorem AVenhance.Infra.Section5.Integration.leadingGrad_continuousOn_Ici {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) {m : ℕ} (hm : 1 ≤ m) {κm : ℝ} (hκm : 0 < κm) {T : ℝ → Homogenization.Vec 2 → ℝ} (hT : ContDiffOn ℝ (↑⊤) (fun (p : ℝ × Homogenization.Vec 2) => T p.1 p.2) (Set.Ici 0 ×ˢ Set.univ)) : ContinuousOn (fun (p : ℝ × Homogenization.Vec 2) => LeftToShow.leadingGrad I hΦ m κm T p.1 p.2) (Set.Ici 0 ×ˢ Set.univ)

∇^{lead} T = F ∇T is jointly continuous on [0,∞) × ℝ² when T is smooth up to t = 0.

The relative leaves

structure AVenhance.Infra.Section5.Integration.RelativeLeaves {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (κm κprev : ℝ) (θm θprev : ℝ → Homogenization.Vec 2 → ℝ) (T : ℕ → ℝ → Homogenization.Vec 2 → ℝ) (A Ci Cr Ca Ct : ℝ) : Prop

The relative-step leaves of one step-down instance that are not already fields of BigBoundInputs or IndyPartIInputs (and not proved here). For one instance (I, Φ, m, κ_m = κm, κ_{m-1} = κprev, θ_m = θm, θ_{m-1} = θprev, T), with N = T (Nstar β), ε = ε_{m-1}, S = √κ_{m-1} ‖∇θ_{m-1}‖_{L²((0,1)×𝕋²)} and v = θTilde_m the ansatz built from N. The field types are exactly the hypotheses of AVenhance.Infra.Section5.RelativeError.relative_step (S, ε, v unfolded), each an OpenInputs contract; no field involves t = 0. Deduplicated against the big-bound estimate / step-down part (i) inputs (taken from there, not fields): the residual identity, the ten-term joint continuity. Proved in this file (not a field): joint continuity of leadingGrad … N on [0,∞) × ℝ² (leadingGrad_continuousOn_Ici).

• hT0 : TGradientContract β κprev T A (√κprev * √(spaceTimeGradNormSq fun (s : ℝ) (x : Homogenization.Vec 2) => spaceGrad (θprev s) x))

  ‖∇T_{m-1}‖ at most A ‖∇θ_{m-1}‖ (l.Tm.minus.thetam gradient form, positive-temperature premise hT0).

• hDt : TMaterialContract I Φ m κprev T A (√κprev * √(spaceTimeGradNormSq fun (s : ℝ) (x : Homogenization.Vec 2) => spaceGrad (θprev s) x))

  The material-derivative bound hDt for T_{m-1} at scale ε^{3δ} κ_{m-1}^{-1/2} S τ_m^{-1}.

• hJets : TPositiveJetsContract I m T A (√κprev * √(spaceTimeGradNormSq fun (s : ℝ) (x : Homogenization.Vec 2) => spaceGrad (θprev s) x))

  Positive-temperature jets of T_{m-1} (PositiveTemperatureJets: positive jets and integrated gradients only).

• hInitial : InitialLayerContract I hΦ m κm θm T Ci (√κprev * √(spaceTimeGradNormSq fun (s : ℝ) (x : Homogenization.Vec 2) => spaceGrad (θprev s) x))

  Relative initial layer from the right, ‖θ_m(s) − θTilde_m(s)‖_{L²} ≤ C_i ε^δ S as s → 0⁺ (InitialLayerContract at amplitude S).

• hterms : RelativeTermsContract I hΦ m κm κprev T Cr (√κprev * √(spaceTimeGradNormSq fun (s : ℝ) (x : Homogenization.Vec 2) => spaceGrad (θprev s) x))

  The ten relative HDot⁻¹ term bounds ‖term_i‖_{L²_t HDot⁻¹} ≤ C_r √κ_m ε^δ S, i < 10 (relative §5.2 term estimates, with slots 3,4,8 centered).

• hLeadingError : LeadingErrorContract I hΦ m κm T Ca (√κprev * √(spaceTimeGradNormSq fun (s : ℝ) (x : Homogenization.Vec 2) => spaceGrad (θprev s) x))

  Leading-order gradient error of the ansatz, √κ_m ‖∇v − ∇^{lead} N‖ ≤ C_a ε^{2δ} S (e.leading comparison).

• hTemperatureError : TemperatureErrorContract I m κprev θprev T Ct (√κprev * √(spaceTimeGradNormSq fun (s : ℝ) (x : Homogenization.Vec 2) => spaceGrad (θprev s) x))

  Gradient distance of the last iterate to the previous solution, √κ_{m-1} ‖∇T_{m-1} − ∇θ_{m-1}‖ ≤ C_t ε^{2δ} S (l.Tm.minus.thetam).

def AVenhance.Infra.Section5.Integration.RelativeFamilyContract (β C₀ CΛ A Ci Cr Ca Ct : ℝ) : Prop

Family contract for step-down part (ii) (IndyStepDownV2Inputs.relative): for constants A Ci Cr Ca Ct and the Λ-threshold CΛ (all chosen before I), RelativeLeaves on the step-down premise block OnA8Instances, under the gate 6/5 ≤ β and the later-scale condition.

Equations

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

The input record for the whole of step-down

structure AVenhance.Infra.Section5.Integration.IndyStepDownV2Inputs (β C₀ : ℝ) : Type

All remaining inputs of the literal step-down proposition IndyStepDownStatement β C₀. bigbound is exactly the big-bound estimate input hypothesis of indystepdown_part_i_of_all_inputs, partI exactly its step-down part (i) input hypothesis, and relative supplies RelativeLeaves under the gate (6/5 ≤ β and the later scale condition) once the Λ-threshold CΛ ≤ Λ holds. The reals A Ci Cr Ca Ct are the constants of RelativeError.relative_step. No field is (or contains) a step-down estimate conjunct.

• A : ℝ

  Constant A of RelativeError.relative_step (positive-jet constant).

• Ci : ℝ

  Constant of the relative initial defect.

• Cr : ℝ

  Constant of the ten relative term bounds.

• Ca : ℝ

  Constant of the leading gradient error.

• Ct : ℝ

  Constant of the temperature gradient error.

• hA : 2 ^ 14 ≤ self.A

  Side condition 2 ^ 14 ≤ A.

• hCi : 0 ≤ self.Ci

  Side condition 0 ≤ Ci.

• hCr : 0 ≤ self.Cr

  Side condition 0 ≤ Cr.

• hCa : 0 ≤ self.Ca

  Side condition 0 ≤ Ca.

• hCt : 0 ≤ self.Ct

  Side condition 0 ≤ Ct.

• bigbound : BigBoundFamilyContract β C₀

  The big-bound estimate inputs (BigBoundInputs for every admissible instance).

• partI : PartIFamilyContract β C₀

  The step-down part (i) inputs (IndyPartIInputs for every admissible instance).

• CΛ : ℝ

  Λ-threshold beyond which the relative leaves are supplied.

• relative : RelativeFamilyContract β C₀ self.CΛ self.A self.Ci self.Cr self.Ca self.Ct

  The relative leaves (RelativeLeaves), needed only under the gate.

The assembly theorem

theorem AVenhance.Infra.Section5.Integration.indystepdown_v2_of_inputs (β C₀ : ℝ) (h : IndyStepDownV2Inputs β C₀) : IndyStepDownStatement β C₀

Step-down assembly. The literal step-down proposition from the named inputs: conjunct (i) by indystepdown_part_i_of_all_inputs, conjunct (ii) by RelativeError.relative_step, with one constant C = max (max C_i C_ii) (max (max C₁ᵇᵇ C₁ᴵ) CΛ).