Conditional assembly of the positive-time H_m bound

The one-instance quantitative leaves are the HmGradientContract and SourceErrorDContract, together with the spacetime rate for the regular part of the source. The family wrapper obtains the first two from their datum producers, leaving only the regular-source rate as an input. The assembly consumes the actual positive-time joint regularity fields and the HmMeasurability adapters; no measurability premise is exposed to callers.

theorem AVenhance.Infra.Section5.Contracts.HmSup.hm_gradNormSq_nonneg (F : Homogenization.Vec 2 → Homogenization.Vec 2) : 0 ≤ gradNormSq F

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

Conditional spacetime rate for the Piola scalar source in the actual endpoint split. The old estimate for (flux - Kmat) : ∇Gbar does not discharge this producer obligation.

Equations

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

noncomputable def AVenhance.Infra.Section5.Contracts.hmSupKappaLower (β C₀ : ℝ) : ℝ

The chosen constants from the l_recurse and its scale consequence. Their definitions depend only on (β,C₀), before any instance data is supplied.

Equations

• AVenhance.Infra.Section5.Contracts.hmSupKappaLower β C₀ = Classical.choose ⋯

noncomputable def AVenhance.Infra.Section5.Contracts.hmSupKappaUpper (β C₀ : ℝ) : ℝ

Chosen upper diffusivity bound from the Hm recursion existence theorem.

Equations

• AVenhance.Infra.Section5.Contracts.hmSupKappaUpper β C₀ = Classical.choose ⋯

theorem AVenhance.Infra.Section5.Contracts.hmSupKappaBounds_spec (β C₀ : ℝ) : 0 < hmSupKappaLower β C₀ ∧ hmSupKappaLower β C₀ < hmSupKappaUpper β C₀ ∧ ∀ (I : Ingredients β), I.Czeta ≤ C₀ → I.Cxi ≤ C₀ → I.Chat ≤ C₀ → ∀ κ ∈ permissibleSet β I.Λ, ∀ (M : ℕ), 1 ≤ M → κ ∈ permittedInterval β I.Λ M → (∀ (m : ℕ), 1 ≤ m → m < M → hmSupKappaLower β C₀ * (AVenhance.a β I.Λ m * epsilon β I.Λ m ^ (2 + gamma β)) ≤ I.kappaAt κ m (M - m) ∧ I.kappaAt κ m (M - m) ≤ hmSupKappaUpper β C₀ * (AVenhance.a β I.Λ m * epsilon β I.Λ m ^ (2 + gamma β))) ∧ ∀ (m : ℕ), 2 ≤ m → m < M → hmSupKappaLower β C₀ * epsilon β I.Λ (m - 1) ^ (4 * delta β) ≤ epsilon β I.Λ m ^ 2 / (I.kappaAt κ m (M - m) * tau β I.Λ m) ∧ epsilon β I.Λ m ^ 2 / (I.kappaAt κ m (M - m) * tau β I.Λ m) ≤ hmSupKappaUpper β C₀ * epsilon β I.Λ (m - 1) ^ (4 * delta β)

noncomputable def AVenhance.Infra.Section5.Contracts.hmSupScalesK (β C₀ : ℝ) : ℝ

Chosen scale constant satisfying the remaining Hm scale estimates.

Equations

• AVenhance.Infra.Section5.Contracts.hmSupScalesK β C₀ = Classical.choose ⋯

theorem AVenhance.Infra.Section5.Contracts.hmSupScalesK_spec (β C₀ : ℝ) : 1 ≤ hmSupScalesK β C₀ ∧ ∀ (I : Ingredients β), I.Czeta ≤ C₀ → I.Cxi ≤ C₀ → I.Chat ≤ C₀ → ∀ κ ∈ permissibleSet β I.Λ, ∀ (M : ℕ), 1 ≤ M → κ ∈ permittedInterval β I.Λ M → ∀ (m : ℕ), 2 ≤ m → m ≤ M → 0 < I.kappaSeq κ M m ∧ I.kappaSeq κ M m ≤ I.kappaSeq κ M (m - 1) ∧ I.kappaSeq κ M (m - 1) ≤ hmSupScalesK β C₀ ∧ AVenhance.a β I.Λ m ^ 2 * epsilon β I.Λ m ^ 4 / I.kappaSeq κ M m ≤ hmSupScalesK β C₀ * I.kappaSeq κ M (m - 1) ∧ epsilon β I.Λ m ^ 2 / (I.kappaSeq κ M m * tau β I.Λ m) ≤ hmSupScalesK β C₀ * epsilon β I.Λ (m - 1) ^ (2 * delta β) ∧ AVenhance.a β I.Λ m * epsilon β I.Λ m ^ 2 / I.kappaSeq κ M m ≤ hmSupScalesK β C₀ * epsilon β I.Λ m ^ (-gamma β) ∧ epsilon β I.Λ m ≤ hmSupScalesK β C₀ * epsilon β I.Λ (m - 1) ^ q β

noncomputable def AVenhance.Infra.Section5.Contracts.hmSupRateConstant (β C₀ Cgrad Cd Creg : ℝ) : ℝ

Uniform coefficient delivered by the moving half-cell FTC.

Equations

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

theorem AVenhance.Infra.Section5.Contracts.hmSup_contract_of_rates {β C₀ Cgrad Cd Creg : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (hCzeta : I.Czeta ≤ C₀) (hCxi : I.Cxi ≤ C₀) (hChat : I.Chat ≤ C₀) (κ : ℝ) (hκPerm : κ ∈ permissibleSet β I.Λ) (M : ℕ) (hM : 1 ≤ M) (hPerm : κ ∈ permittedInterval β I.Λ M) (m : ℕ) (R : ℝ) (hR : 0 < R) (hmStart : mTheta0 β I.Λ R ≤ m) (hmM : m ≤ M) (θ₀ : Homogenization.Vec 2 → ℝ) (θprev : ℝ → Homogenization.Vec 2 → ℝ) (T : ℕ → ℝ → Homogenization.Vec 2 → ℝ) (hθprev : IsClassicalSol (streamVel (Φ (m - 1))) (I.kappaSeq κ M (m - 1)) (fun (x : ℝ) (x_1 : Homogenization.Vec 2) => 0) θ₀ θprev) (hT : I.IsTIterates hΦ m (I.kappaSeq κ M m) (I.kappaSeq κ M (m - 1)) θ₀ θprev T) (hCgrad : 0 ≤ Cgrad) (hCd : 0 ≤ Cd) (hCreg : 0 ≤ Creg) (hGradient : Integration.HmGradientContract I hΦ m (I.kappaSeq κ M m) (I.kappaSeq κ M (m - 1)) T Cgrad √(l2NormSq θ₀)) (hDcontract : Integration.SourceErrorDContract I hΦ m (I.kappaSeq κ M m) T Cd √(l2NormSq θ₀)) (hRegular : HmPiolaSourceRate I hΦ m (I.kappaSeq κ M m) (I.kappaSeq κ M (m - 1)) T Creg √(l2NormSq θ₀)) : Integration.HmSupContract I hΦ m (I.kappaSeq κ M m) θ₀ T (hmSupRateConstant β C₀ Cgrad Cd Creg)

Assemble the positive-time HmSupContract from exactly the three quantitative rates used by its proof: the gradient, d_m, and the Piola-source rate. The field-measurability and spacetime-rate adapters discharge the measurability and vector L² inputs internally.

theorem AVenhance.Infra.Section5.Contracts.hmSup_contract_onA7_of_piola_source_rate (β C₀ Creg : ℝ) : ∃ (CHs : ℝ) (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 → ℝ) => HmPiolaSourceRate I hΦ m (I.kappaSeq κ M m) (I.kappaSeq κ M (m - 1)) T Creg √(l2NormSq θ₀) → Integration.HmSupContract I hΦ m (I.kappaSeq κ M m) θ₀ T CHs

Family producer for the positive-time HmSupContract, conditional on the Piola-source rate. The gradient and d_m rates are obtained from their unconditional datum producers; their constants and the combined cutoff are chosen before the OnA7Instances block.