Input contracts of the main theorem

This module states, in one place, every named input of the following assemblies; each input is proved in another module (the main theorem is unconditional). The named inputs of

• Big-bound estimate (BigBoundInputs, one instance),
• Step-down part (i) (IndyPartIInputs, one instance),
• Step-down part (ii) (RelativeLeaves, one instance), including the leaf inputs of the conditional producers section_four_ansatz_bound and RelativeError.relative_leading_error_of_jets,
• Main theorem (anomalous_dissipation_of_A8_A1c: the step-down and classical well-posedness statements),

is a def <Name>Contract … : Prop below, stated exactly as its consumer uses it. The three per-instance input records are defined here with fields typed by these contracts, and the family-level contracts (BigBoundFamilyContract, PartIFamilyContract, RelativeFamilyContract) are the corresponding fields of IndyStepDownV2Inputs. Producers prove exactly <Name>Contract (per instance), quantified as in the family contract that contains it: constants first (chosen before I), then a Λ-threshold, then the step-down premise block.

Conventions.

• Open time: every contract that involves the ansatz, HTilde_m or Amnr is stated for t > 0 only (the Amnr uses the two-sided time deriv, so these objects are extension-dependent at t ≤ 0). No consumer field carries a t = 0 form (RelativeError.relative_step uses the open-time energy estimate and the proved open-time HTilde_m regularity).
• Centered slots: the relative term bounds are on section5CenteredTerm (slots 3, 4, 8 centered), with the grouped mean zero GroupMeanZeroContract.
• Abstract amplitude: contracts used with both normalisations (B = ‖θ₀‖_{L²} for big-bound/step-down part (i) and B = S = √κ_{m-1} ‖∇θ_{m-1}‖ for step-down part (ii)) take the amplitude B/N as a parameter.

Source lines refer to the pinned source/enhance.tex.

big-bound estimate (e.bigbound): per-instance contracts

Notation: N := T (Nstar β), d := sourceErrorD I hΦ m κm N, e := iterateError I hΦ m κm κprev T. Abstract amplitude: every *SourceContract has right side C ε_{m-1}^δ √κ_m B. big-bound estimate (BigBoundInputs) uses B = ‖θ₀‖_{L²} (then the scale is section5SourceScale β I.Λ m κm C θ₀, definitionally); the relative term bounds of step-down part (ii) use the same objects at B = S, so one producer per term with a free amplitude serves both. The mean-zero, flux regularity and continuity contracts are amplitude-free and shared by big-bound estimate and step-down part (ii).

def AVenhance.Infra.Section5.Integration.ResidualContract {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (κm κprev : ℝ) (T : ℕ → ℝ → Homogenization.Vec 2 → ℝ) : Prop

The exact residual identity e.monster for the ansatz built from N = T (Nstar β) with the source errors d_m (e.dm) and e_{m-1}, on t ∈ (0,1) (enhance.tex 6886–6990).

Equations

• AVenhance.Infra.Section5.Integration.ResidualContract I hΦ m κm κprev T = ∀ t ∈ Set.Ioo 0 1, ∀ (x : Homogenization.Vec 2), AVenhance.Infra.Section5.sourceResidualIdentity I hΦ m κm κprev T t x

def AVenhance.Infra.Section5.Integration.Cutoff1MeanZeroContract {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (κm : ℝ) (T : ℕ → ℝ → Homogenization.Vec 2 → ℝ) : Prop

Mean zero of cutoff1(t) on the cube, t ∈ (0,1).

Equations

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

def AVenhance.Infra.Section5.Integration.Cutoff1SourceContract {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (κm : ℝ) (T : ℕ → ℝ → Homogenization.Vec 2 → ℝ) (C B : ℝ) : Prop

Source-scale space-time L² bound for cutoff1 (e.monster.est.*, 7300–7500).

Equations

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

def AVenhance.Infra.Section5.Integration.Twistie1MeanZeroContract {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (κm : ℝ) (T : ℕ → ℝ → Homogenization.Vec 2 → ℝ) : Prop

Mean zero of twistie1(t) (source mean condition), t ∈ (0,1). Not a field of BigBoundInputs: a producer input of Twistie1HMinusSourceContract (the ergodic lemma needs the product mean).

Equations

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

def AVenhance.Infra.Section5.Integration.Twistie1HMinusSourceContract {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (κm : ℝ) (T : ℕ → ℝ → Homogenization.Vec 2 → ℝ) (C B : ℝ) : Prop

Negative-norm source bound for twistie1 (e.monster.est.5, 7371–7460): the time HDot⁻¹ norm of twistie1 is at most C ε^δ √κ_m B. The source proves it with the ergodic lemma (Remark r.Hminusone.flow, choice e.fg.choice.1), whose gain ε_m is a negative-norm gain: an L² bound of twistie1 at this scale is NOT available (it is larger by ≈ ε_{m-1}^{8δ-q}). Replaces the former Twistie1SourceContract (L²).

Equations

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

def AVenhance.Infra.Section5.Integration.Twistie3FluxSmoothContract {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (κm : ℝ) (T : ℕ → ℝ → Homogenization.Vec 2 → ℝ) : Prop

Smoothness of the divergence flux of twistie3 (e.monster.twistie3, 6912), t ∈ (0,1).

Equations

• AVenhance.Infra.Section5.Integration.Twistie3FluxSmoothContract I hΦ m κm T = ∀ t ∈ Set.Ioo 0 1, ContDiff ℝ (↑⊤) (AVenhance.Infra.Section5.twistie3Flux I hΦ m κm (T (AVenhance.Nstar β)) t)

def AVenhance.Infra.Section5.Integration.Twistie3FluxPeriodicContract {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (κm : ℝ) (T : ℕ → ℝ → Homogenization.Vec 2 → ℝ) : Prop

ℤ²-periodicity of the twistie3 flux, t ∈ (0,1).

Equations

• AVenhance.Infra.Section5.Integration.Twistie3FluxPeriodicContract I hΦ m κm T = ∀ t ∈ Set.Ioo 0 1, AVenhance.IsZ2Periodic (AVenhance.Infra.Section5.twistie3Flux I hΦ m κm (T (AVenhance.Nstar β)) t)

def AVenhance.Infra.Section5.Integration.Twistie3SourceContract {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (κm : ℝ) (T : ℕ → ℝ → Homogenization.Vec 2 → ℝ) (C B : ℝ) : Prop

Source-scale space-time L² bound on the twistie3 flux gradient.

Equations

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

def AVenhance.Infra.Section5.Integration.GroupMeanZeroContract {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (κm : ℝ) (T : ℕ → ℝ → Homogenization.Vec 2 → ℝ) : Prop

Grouped mean zero: the sum twistie4 + twistie5 + normie3 is mean zero on the cube, t ∈ (0,1) (the three are not individually so). Used by big-bound estimate and, through RelativeError.relative_step, by step-down part (ii).

Equations

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

def AVenhance.Infra.Section5.Integration.Twistie4CenteredSourceContract {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (κm : ℝ) (T : ℕ → ℝ → Homogenization.Vec 2 → ℝ) (C B : ℝ) : Prop

Centered negative-norm bound for twistie4.

Equations

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

def AVenhance.Infra.Section5.Integration.Twistie5CenteredSourceContract {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (κm : ℝ) (T : ℕ → ℝ → Homogenization.Vec 2 → ℝ) (C B : ℝ) : Prop

Centered negative-norm bound for twistie5.

Equations

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

def AVenhance.Infra.Section5.Integration.Normie3CenteredSourceContract {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (κm : ℝ) (T : ℕ → ℝ → Homogenization.Vec 2 → ℝ) (C B : ℝ) : Prop

Centered negative-norm bound for normie3.

Equations

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

def AVenhance.Infra.Section5.Integration.Normie1FluxSmoothContract {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (κm : ℝ) (T : ℕ → ℝ → Homogenization.Vec 2 → ℝ) : Prop

Smoothness of the divergence flux of normie1 (e.monster.normie1, 6950), t ∈ (0,1).

Equations

• AVenhance.Infra.Section5.Integration.Normie1FluxSmoothContract I hΦ m κm T = ∀ t ∈ Set.Ioo 0 1, ContDiff ℝ (↑⊤) (AVenhance.Infra.Section5.normie1Flux I hΦ m κm (T (AVenhance.Nstar β)) t)

def AVenhance.Infra.Section5.Integration.Normie1FluxPeriodicContract {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (κm : ℝ) (T : ℕ → ℝ → Homogenization.Vec 2 → ℝ) : Prop

ℤ²-periodicity of the normie1 flux, t ∈ (0,1).

Equations

• AVenhance.Infra.Section5.Integration.Normie1FluxPeriodicContract I hΦ m κm T = ∀ t ∈ Set.Ioo 0 1, AVenhance.IsZ2Periodic (AVenhance.Infra.Section5.normie1Flux I hΦ m κm (T (AVenhance.Nstar β)) t)

def AVenhance.Infra.Section5.Integration.Normie1SourceContract {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (κm : ℝ) (T : ℕ → ℝ → Homogenization.Vec 2 → ℝ) (C B : ℝ) : Prop

Source-scale space-time L² bound on the normie1 flux gradient.

Equations

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

def AVenhance.Infra.Section5.Integration.Normie2FluxSmoothContract {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (κm : ℝ) (T : ℕ → ℝ → Homogenization.Vec 2 → ℝ) : Prop

Smoothness of the divergence flux of normie2 (e.monster.normie2, 6959), t ∈ (0,1).

Equations

• AVenhance.Infra.Section5.Integration.Normie2FluxSmoothContract I hΦ m κm T = ∀ t ∈ Set.Ioo 0 1, ContDiff ℝ (↑⊤) (AVenhance.Infra.Section5.normie2Flux I hΦ m κm (T (AVenhance.Nstar β)) t)

def AVenhance.Infra.Section5.Integration.Normie2FluxPeriodicContract {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (κm : ℝ) (T : ℕ → ℝ → Homogenization.Vec 2 → ℝ) : Prop

ℤ²-periodicity of the normie2 flux, t ∈ (0,1).

Equations

• AVenhance.Infra.Section5.Integration.Normie2FluxPeriodicContract I hΦ m κm T = ∀ t ∈ Set.Ioo 0 1, AVenhance.IsZ2Periodic (AVenhance.Infra.Section5.normie2Flux I hΦ m κm (T (AVenhance.Nstar β)) t)

def AVenhance.Infra.Section5.Integration.Normie2SourceContract {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (κm : ℝ) (T : ℕ → ℝ → Homogenization.Vec 2 → ℝ) (C B : ℝ) : Prop

Source-scale space-time L² bound on the normie2 flux gradient (H_m estimates).

Equations

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

def AVenhance.Infra.Section5.Integration.TinyMeanZeroContract {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (κm κprev : ℝ) (T : ℕ → ℝ → Homogenization.Vec 2 → ℝ) : Prop

Mean zero of tiny(t), t ∈ (0,1). Not a field of BigBoundInputs: a producer input of TinyHMinusSourceContract (it gives the mean of tinyNondivergencePart).

Equations

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

def AVenhance.Infra.Section5.Integration.TinyHMinusSourceContract {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (κm κprev : ℝ) (T : ℕ → ℝ → Homogenization.Vec 2 → ℝ) (C B : ℝ) : Prop

Negative-norm source bound for tiny (e.monster.est.tiny, 7930–8000): the time HDot⁻¹ norm of tiny is at most C ε^δ √κ_m B. The source proves it in divergence form — ‖d_m + e_{m-1}‖_{L²} (e.dm.bounds, e.Em-1.thetam with n = 0) plus the L² norm of tinyNondivergencePart (e.Em-1.thetam with n = 2); see hMinusOneNorm_tiny_le_of_components (Terms/Tiny.lean). It never bounds ∇·(d_m + e_{m-1}) in L², so this replaces the former TinySourceContract (L² of tiny).

Equations

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

def AVenhance.Infra.Section5.Integration.SourceErrorDContract {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (κm : ℝ) (T : ℕ → ℝ → Homogenization.Vec 2 → ℝ) (Cd B : ℝ) : Prop

d_m bound, abstract amplitude B (e.monster.est.11.a.d, 7860–7880, from e.dm.bounds): the time-L² of the spatial L² norm of sourceErrorD is at most Cd ε_{m-1}^{2δ} √κ_m B. Producer input of TinyHMinusSourceContract (with VIncrementContract for e_{m-1}).

Equations

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

def AVenhance.Infra.Section5.Integration.R46FluxSmoothContract {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (κm : ℝ) (T : ℕ → ℝ → Homogenization.Vec 2 → ℝ) : Prop

Smoothness of the transition-window flux of R46 (the transition remainder), t ∈ (0,1).

Equations

• AVenhance.Infra.Section5.Integration.R46FluxSmoothContract I hΦ m κm T = ∀ t ∈ Set.Ioo 0 1, ContDiff ℝ (↑⊤) (AVenhance.Infra.Section5.r46Flux I hΦ m κm (T (AVenhance.Nstar β)) t)

def AVenhance.Infra.Section5.Integration.R46FluxPeriodicContract {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (κm : ℝ) (T : ℕ → ℝ → Homogenization.Vec 2 → ℝ) : Prop

ℤ²-periodicity of the R46 flux, t ∈ (0,1).

Equations

• AVenhance.Infra.Section5.Integration.R46FluxPeriodicContract I hΦ m κm T = ∀ t ∈ Set.Ioo 0 1, AVenhance.IsZ2Periodic (AVenhance.Infra.Section5.r46Flux I hΦ m κm (T (AVenhance.Nstar β)) t)

def AVenhance.Infra.Section5.Integration.R46SourceContract {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (κm : ℝ) (T : ℕ → ℝ → Homogenization.Vec 2 → ℝ) (C B : ℝ) : Prop

Source-scale L² bound on the R46 flux gradient (transition-window estimate the source does not state).

Equations

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

def AVenhance.Infra.Section5.Integration.TermContinuousContract {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (κm κprev : ℝ) (T : ℕ → ℝ → Homogenization.Vec 2 → ℝ) : Prop

Joint continuity of each of the ten §5.1 terms on (0,1) × ℝ² (all pieces are smooth for t > 0). Used by big-bound estimate and by step-down part (ii).

Equations

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

step-down part (i) (indystepdown conjunct (i)): per-instance contracts

def AVenhance.Infra.Section5.Integration.InitialLayerContract {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (κm : ℝ) (θm : ℝ → Homogenization.Vec 2 → ℝ) (T : ℕ → ℝ → Homogenization.Vec 2 → ℝ) (Cᵢ B : ℝ) : Prop

Initial layer, abstract amplitude B. The defect ‖θ_m(s) − θTilde_m(s)‖_{L²} ≤ Cᵢ ε^δ B for all small s > 0 (right limit; the ansatz at t = 0 itself is extension-dependent). Source: e.tildethetam.to.Tm initial data (oscillatory corrector ε^{4δ}, HTilde_m only ε^δ). Used with B = ‖θ₀‖_{L²} by step-down part (i) (IndyPartIInputs.hInitial) and with B = S by step-down part (ii) (RelativeLeaves.hInitial, consumed by RelativeError.relative_step through forced_energy_estimate_Ioi).

Equations

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

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

e.tildethetam.to.Tm (8882–9133): ‖θTilde_m(t) − T_{m-1}(t)‖_{L²} ≤ Cₐ ε^δ ‖θ₀‖ for t ∈ (0,1]. Produced by Integration.section_four_ansatz_bound from FirstOrderSliceJetContract (amplitude ‖θ₀‖) and HmSupContract.

Equations

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

def AVenhance.Infra.Section5.Integration.SectionFourIterateContract {β : ℝ} (I : Ingredients β) (m : ℕ) (θ₀ : Homogenization.Vec 2 → ℝ) (θprev : ℝ → Homogenization.Vec 2 → ℝ) (T : ℕ → ℝ → Homogenization.Vec 2 → ℝ) (Cₜ : ℝ) : Prop

e.Tm.thetam / l.Tm.minus.thetam: ‖T_{m-1}(t) − θ_{m-1}(t)‖_{L²} ≤ Cₜ ε^δ ‖θ₀‖, t ∈ [0,1] (both are classical up to t = 0, so the closed interval is legitimate).

Equations

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

def AVenhance.Infra.Section5.Integration.FirstOrderSliceJetContract {β : ℝ} (I : Ingredients β) (m : ℕ) (T : ℕ → ℝ → Homogenization.Vec 2 → ℝ) (AT B : ℝ) : Prop

Leaf of section_four_ansatz_bound (hTjet), abstract amplitude B: first-order slice jet ‖∂_i T_{m-1}(s)‖_{L²} ≤ AT · B · ε_{m-1}^{-(1+γ/2)}, s ∈ [0,1] (e.Tm.reg.upgrade, first order). Step-down part (i) uses B = ‖θ₀‖_{L²}. Implied by the second conjunct of the T upgrade (iterate_T_upgrade_of_theta*, v = [i]) with amplitude N = 2‖θ₀‖ .

Equations

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

def AVenhance.Infra.Section5.Integration.HmSupContract {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (κm : ℝ) (θ₀ : Homogenization.Vec 2 → ℝ) (T : ℕ → ℝ → Homogenization.Vec 2 → ℝ) (CHs : ℝ) : Prop

Leaf of section_four_ansatz_bound (hHsup): e.Hm.Linfty, ‖HTilde_m(t)‖_{L²} ≤ CHs ε^δ ‖θ₀‖ for t ∈ (0,1] (open time). See frozen_hm_halfCell_eLpNorm_bound, HmDmScales.

Equations

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

def AVenhance.Infra.Section5.Integration.HmGradientContract {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (κm κprev : ℝ) (T : ℕ → ℝ → Homogenization.Vec 2 → ℝ) (CH B : ℝ) : Prop

HTilde_m gradient, abstract amplitude B, κ_{m-1} normalisation (e.Hm.gradient.L2, 5990; e.hcorrm): √κ_{m-1} ‖∇HTilde_m‖_{L²((0,1)×𝕋²)} ≤ CH ε_{m-1}^{4δ} B. Input of Normie2SourceContract (e.monster.est.11 multiplies by ‖κ_m + ψTilde_m σ‖_∞ ≲ √(κ_m κ_{m-1})). At B = ‖θ₀‖ this is p.Hm.bounds; at B = S note that RelativeError.relative_Hm_gradient_actual gives only the weaker κ_m normalisation √κ_m ‖∇HTilde_m‖ ≤ CH ε^{4δ} S.

Equations

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

step-down part (ii) (indystepdown conjunct (ii), relative step): per-instance contracts

Here S is the relative amplitude √κ_{m-1} ‖∇θ_{m-1}‖_{L²((0,1)×𝕋²)}; it is a parameter of each contract and is instantiated by that expression in RelativeLeaves.

def AVenhance.Infra.Section5.Integration.TGradientContract (β κprev : ℝ) (T : ℕ → ℝ → Homogenization.Vec 2 → ℝ) (A S : ℝ) : Prop

hT0: √κ_{m-1} ‖∇T_{m-1}‖ ≤ A S (l.Tm.minus.thetam, gradient form). First conjunct of the T upgrade with amplitude N = S.

Equations

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

def AVenhance.Infra.Section5.Integration.TMaterialContract {β : ℝ} (I : Ingredients β) (Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ) (m : ℕ) (κprev : ℝ) (T : ℕ → ℝ → Homogenization.Vec 2 → ℝ) (A S : ℝ) : Prop

hDt: the material derivative of T_{m-1} at scale ε^{3δ} κ_{m-1}^{-1/2} S τ'_m^{-1} (e.barf.cascade).

Equations

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

def AVenhance.Infra.Section5.Integration.TPositiveJetsContract {β : ℝ} (I : Ingredients β) (m : ℕ) (T : ℕ → ℝ → Homogenization.Vec 2 → ℝ) (A S : ℝ) : Prop

hJets: positive spatial jets of T_{m-1} with amplitude S (RelativeError.PositiveTemperatureJets; positive orders only, no zeroth-order norm). Slice part of the T upgrade with N = S .

Equations

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

def AVenhance.Infra.Section5.Integration.RelativeTermsContract {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (κm κprev : ℝ) (T : ℕ → ℝ → Homogenization.Vec 2 → ℝ) (Cr S : ℝ) : Prop

hterms: the ten relative HDot⁻¹ term bounds ≤ C_r √κ_m ε^δ S on the centered family section5CenteredTerm (slots 3, 4, 8 centered).

Equations

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

def AVenhance.Infra.Section5.Integration.LeadingErrorContract {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (κm : ℝ) (T : ℕ → ℝ → Homogenization.Vec 2 → ℝ) (Ca S : ℝ) : Prop

hLeadingError: √κ_m ‖∇θTilde_m − F∇T_{m-1}‖ ≤ C_a ε^{2δ} S (e.leading). Produced by RelativeError.relative_leading_error_of_jets from TGradientContract, FirstOrderGradJetContract, ThetaProfileContract and VIncrementContract (all amplitude S).

Equations

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

def AVenhance.Infra.Section5.Integration.TemperatureErrorContract {β : ℝ} (I : Ingredients β) (m : ℕ) (κprev : ℝ) (θprev : ℝ → Homogenization.Vec 2 → ℝ) (T : ℕ → ℝ → Homogenization.Vec 2 → ℝ) (Ct S : ℝ) : Prop

hTemperatureError: √κ_{m-1} ‖∇T_{m-1} − ∇θ_{m-1}‖ ≤ C_t ε^{2δ} S (l.Tm.minus.thetam). Produced by upstream RelativeError.temperatureError_leaf_of_abstract_V / temperature_error_of_V_zero_bounds from the V increments (VIncrementContract, amplitude S).

Equations

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

def AVenhance.Infra.Section5.Integration.FirstOrderGradJetContract {β : ℝ} (I : Ingredients β) (m : ℕ) (κprev : ℝ) (T : ℕ → ℝ → Homogenization.Vec 2 → ℝ) (A S : ℝ) : Prop

Leaf of relative_leading_error_of_jets (hT1): first-order word part of the coordinate energy profile, √κ_{m-1} ‖∇ ∂_i T_{m-1}‖ ≤ A (A/ε^{1+γ/2}) S. Gradient part of the T upgrade (w = [i]) with N = S.

Equations

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

def AVenhance.Infra.Section5.Integration.SecondOrderGradJetContract {β : ℝ} (I : Ingredients β) (m : ℕ) (κprev : ℝ) (T : ℕ → ℝ → Homogenization.Vec 2 → ℝ) (A S : ℝ) : Prop

Second-order word part of the coordinate energy profile, abstract amplitude B (e.nabm2 with n = 2): √κ_{m-1} ‖∇ ∂_i ∂_j T_{m-1}‖ ≤ A (A/ε^{1+γ/2})² B. Input of Twistie1HMinusSourceContract (the ergodic gain ε_m multiplies the space-time L² norm of ∇∇·((K_m + s_{m-1})∇T); slice-only jets lose ≈ ε^{-(2-β)/2}). Gradient part of the T upgrade (v = w = [i, j]) with N = B.

Equations

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

def AVenhance.Infra.Section5.Integration.ThetaProfileContract {β : ℝ} (I : Ingredients β) (m : ℕ) (κprev : ℝ) (θprev : ℝ → Homogenization.Vec 2 → ℝ) (Cs N : ℝ) : Prop

θ_{m-1} base profile, abstract amplitude N: iterateCoordinateEnergyProfile θ_{m-1} κ_{m-1} N (Cs ε^{-1-γ/2}) 0 (gradient-only at order zero). step-down part (ii) uses N = S (requires the S-amplitude initial trace); Step-down part (i) uses N = 2‖θ₀‖ (theta_iterate_profile_of_analytic_*).

Equations

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

def AVenhance.Infra.Section5.Integration.VIncrementContract {β : ℝ} (I : Ingredients β) (m : ℕ) (κprev : ℝ) (T : ℕ → ℝ → Homogenization.Vec 2 → ℝ) (Cs Rθ N : ℝ) : Prop

V increments, abstract amplitude N: the literal conclusion of the iterate_V_abstract_amplitude_of_diffusivity_and_flow (Section4/IteratesVAbstractAmplitude.lean). Used with N = S by relative_leading_error_of_jets and by the temperature-error leaf.

Equations

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

Quantifier blocks for producers

A producer of a per-instance contract P proves ∃ C₁, OnA7Instances β C₀ C₁ P (or the step-down estimate version), with all its constants chosen before this (i.e. before I).

def AVenhance.Infra.Section5.Integration.OnA7Instances (β C₀ C₁ : ℝ) (P : (I : Ingredients β) → (Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ) → IsStreamSeq I Φ → ℝ → ℕ → ℝ → (Homogenization.Vec 2 → ℝ) → ℕ → (ℝ → Homogenization.Vec 2 → ℝ) → (ℕ → ℝ → Homogenization.Vec 2 → ℝ) → Prop) : Prop

The big-bound estimate / step-down part (i) premise block (IndyStepDownV2Inputs.bigbound): cutoff bounds, Λ-threshold C₁, stream sequence, permissible κ, analytic mean-zero datum, m ≥ m_θ₀(R), classical θ_{m-1}, the T-iterates.

Equations

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

def AVenhance.Infra.Section5.Integration.OnA8Instances (β C₀ C₁ : ℝ) (P : (I : Ingredients β) → (Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ) → IsStreamSeq I Φ → ℝ → ℕ → ℝ → (Homogenization.Vec 2 → ℝ) → ℕ → (ℝ → Homogenization.Vec 2 → ℝ) → (ℝ → Homogenization.Vec 2 → ℝ) → (ℕ → ℝ → Homogenization.Vec 2 → ℝ) → Prop) : Prop

The full step-down premise block (IndyStepDownV2Inputs.partI / .relative): OnA7Instances plus the classical θ_m.

Equations

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

main theorem main contracts

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

The literal step-down body (AVenhance.indystepdown), consumed by main theorem (anomalous_dissipation_of_A8_A1c). Produced by indystepdown_v2_of_inputs from IndyStepDownV2Inputs.

Equations

• AVenhance.Infra.Section5.Integration.IndyStepDownContract β C₀ = AVenhance.Infra.Section5.Integration.IndyStepDownStatement β C₀

def AVenhance.Infra.Section5.Integration.ClassicalWellposedContract : Prop

The literal classical well-posedness body (AVenhance.classical_wellposed, public), consumed by main theorem (anomalous_dissipation_of_A8_A1c) for the classical solvability of every finite drift.

Equations

• AVenhance.Infra.Section5.Integration.ClassicalWellposedContract = AVenhance.Infra.Section5.Integration.ClassicalWellposedStatement