ClosureTerminal

Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.

The closure contract, wired to the diffusivity-asymptotics conclusion

ABK26, e.what.do.we.have, l.integrate.approx.recurrence.

What this module composes

Two proved conditional A were left unconnected:

• Closure.NodeContract.TwoSidedClosure d --- the closure node's contract, whose conclusion is the pair of printed displays Closure.TwoSidedTargets.RecurrenceUpperDisplay / Closure.TwoSidedTargets.RecurrenceLowerDisplay at the wide shell window h <= 6 cstar cgamma^{-1}, written with Closure.ShellIncrementCap.shellDrift and Closure.TwoSidedTargets.recurrenceFlatError;
• Provider.Diffusivity.diffusivity_asymptotics_of_recurrence_displays --- the deterministic flow spine, whose two disclosed binders hforward/hreverse are the same two displays at the narrow window (m : R) <= (n : R) + cstar cgamma^{-1}, written with RecurrenceIntegration.recurrenceIncrement and |log cgamma|^2, and floored at mStarStar M <= n.

displays_window_pair performs the conversion at one admissible pair, exactly as Closure.ClosureRecurrenceFeed.feed_pair does for the integration engine's own binders: h := (m - n).toNat turns the narrow window into an admissible (n, h), Closure.TwoSidedTargets.shellDrift_eq turns shellDrift into recurrenceIncrement gauged by shom_n^{-2}, and sq_abs turns (log cgamma)^2 into |log cgamma|^2. The display constant is enlarged to Crec:= max 1 C, which both displays tolerate because every coefficient they carry is nonnegative.

What is proved

• displays_window_pair --- the window conversion at one pair (n, m).
• diffusivity_asymptotics_of_twoSidedClosure --- the composite: from Closure.NodeContract.TwoSidedClosure d and the standing 2 <= d, the three conclusions carried by Algsuperdiff.Frozen.Section3.diffusivity_asymptotics on that statement's own premise list with the landmark gate weakened to the mStarStar M < m0.

How the premises meet

The premise list here is mStarStar M < m0, inductionState M (m0 - 1) E, Cflow cstar^{-1} <= E and cgamma <= (E^{-1})^{10}. The contract asks for the same landmark gate and induction state and for C cstar^{-1} <= E and cgamma <= E^{-5}; the offered flow constant is max Cflow (max 1 C), so the regime premise delivers both the spine's and the contract's, and (E^{-1})^{10} <= E^{-5} for E >= 1 delivers the contract's gate. No premise is added, reordered or dropped, and the enlarged flow constant only weakens the first conclusion.

The scale gate on m0 (-bin statement change)

The landmark gate above is mStarStar M < m0, not the printed m0 in (mstar, infty) cap Z.

Binders

hd : 2 <= d (the contract's own antecedent) and hclosure: TwoSidedClosure d. Nothing else.

Scope

Internal Provider infrastructure: a conditional A. There is no sorry, no admit, no custom axiom and no set_option maxHeartbeats.

References

• ABK26, l.approximate.recurrence.formula; e.what.do.we.have.
• ABK26, l.integrate.approx.recurrence; e.mstarstar.

The window conversion

The composite

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.Closure.diffusivity_asymptotics_of_twoSidedClosure (d : ℕ) (hd : 2 ≤ d) (hclosure : TwoSidedClosure d) : ∃ (Cflow : ℝ), 0 < Cflow ∧ ∀ (M : ABKModel d) (m0 : ℤ) (E : { E : ℝ // 1 ≤ E }), mStarStar M < m0 → Frozen.Section3.inductionState M (m0 - 1) E → Cflow * (Disorder.cstar M)⁻¹ ≤ ↑E → M.gamma ≤ (↑E)⁻¹ ^ 10 → (∀ m ≤ m0, |↑(Annealed.sigmaBar M m) - √(M.nu ^ 2 + Disorder.cstar M * M.gamma⁻¹ * 3 ^ (2 * M.gamma * ↑m))| ≤ Cflow * (Disorder.cstar M)⁻¹ * ↑E * √M.gamma * |Real.log M.gamma| * ↑(Annealed.sigmaBar M m)) ∧ 1 / 4 * max (Disorder.cstar M * M.gamma⁻¹ * 3 ^ (2 * M.gamma * ↑m0)) (M.nu ^ 2) ≤ ↑(Annealed.sigmaBar M m0) ^ 2 ∧ ↑(Annealed.sigmaBar M m0) ^ 2 ≤ 4 * max (Disorder.cstar M * M.gamma⁻¹ * 3 ^ (2 * M.gamma * ↑m0)) (M.nu ^ 2)

The diffusivity asymptotics, from the closure node's contract.

From Closure.NodeContract.TwoSidedClosure d and the standing dimension hypothesis, the three conclusions carried by Algsuperdiff.Frozen.Section3.diffusivity_asymptotics hold on that statement's own premise list, with the landmark gate weakened to the mStarStar M < m0 ( option (i)).

exactly on hd : 2 <= d and on hclosure : TwoSidedClosure d. The contract is carried as a Prop binder and nothing below proves any part of it; this is a conditional A, not a claim about any source node.