ClosureRecurrenceFeed

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

What the closure node feeds: the two binders of l.integrate.approx.recurrence

ABK26, e.what.do.we.have, e.assump.upper, e.assump.lower.modified, l.integrate.approx.recurrence.

Closure.NodeContract.integrationHypotheses_of_displays converts the two printed displays at one admissible pair (n, n+h) into the two integration hypotheses. This module runs that conversion over the whole admissible range and hands the result to the proved frozen-root splice

ApproximateRecurrence.SubLandmarkDisplays.sigmaBar_integrate_approx_recurrence_of_mStarStar_floored
  ,

whose hupper/hlower binders are exactly what comes out. The shapes meet with no bridge: the splice quantifies over pairs mss <= n <= m <= m0 with (m : R) <= (n : R) + cstar cgamma^{-1}, while the contract quantifies over (n, h) with mstarstar <= n, n <= m0 - h and h <= 6 cstar cgamma^{-1}; h := (m - n).toNat translates one into the other, and the splice's narrow shell budget cstar cgamma^{-1} sits inside the contract's wide one.

The two constants

The integration engine wants a single E with 1 <= E and a single F with 1 <= F; they are

  E_integration = recurrenceIntegrationSlack M C E
                = max 1 ((2 + shellIncrementCap) (C E^2 |log cgamma|^2)) ,
  F             = max 1 C ,

the two maxes being the only bookkeeping: both displays are monotone in the constant, so enlarging is free.

Binders

recurrenceIntegrationBinders_of_twoSidedClosure carries exactly

• hclosure --- the closure node's contract Closure.TwoSidedClosure d, i.e. the statement this lane is assembling; it is a hypothesis here, and nothing in this module proves any part of it;
• hd : 2 <= d --- the standing dimension hypothesis, which is the contract's own antecedent;
• the contract's own standing premises mStarStar M < m0 (the gate; see below), the induction state, the regime C cstar^{-1} <= E and the gate cgamma <= E^{-5};
• herr : recurrenceFlatError M <= 1 --- the smallness of the printed error, supplied by e.cgamma.constraints; it is what integrationHypotheses_of_displays needs to move the error across the ratio.

No estimate is proved here and no node is claimed: this is the consumption shape, and it is arithmetic.

The scale gate on m0 (-bin statement change)

Both theorems below gate m0 at mStarStar M < m0, not at the printed m0 in (mstar, infty) cap Z.

References

• ABK26, l.approximate.recurrence.formula.
• ABK26, l.integrate.approx.recurrence; e.mstarstar.

noncomputable def Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.Closure.recurrenceIntegrationSlack {d : ℕ} (M : ABKModel d) (C E : ℝ) : ℝ

The integration constant the two displays deliver.

Equations

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

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.Closure.one_le_recurrenceIntegrationSlack {d : ℕ} (M : ABKModel d) (C E : ℝ) : 1 ≤ recurrenceIntegrationSlack M C E

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.Closure.recurrenceIntegrationBinders_of_twoSidedClosure {d : ℕ} (hd : 2 ≤ d) (hclosure : TwoSidedClosure d) : ∃ (C : ℝ), 0 < C ∧ ∀ (M : ABKModel d) (m0 : ℤ) (Ec : { E : ℝ // 1 ≤ E }), mStarStar M < m0 → Frozen.Section3.inductionState M (m0 - 1) Ec → C * (Disorder.cstar M)⁻¹ ≤ ↑Ec → M.gamma ≤ ↑Ec ^ (-5) → recurrenceFlatError M C ↑Ec ≤ 1 → (∀ (n m : ℤ), mStarStar M ≤ n → m ≤ m0 → n ≤ m → ↑m ≤ ↑n + Disorder.cstar M * M.gamma⁻¹ → ↑(Annealed.sigmaBar M m) ≤ (1 + recurrenceIntegrationSlack M C ↑Ec * M.gamma) * ↑(Annealed.sigmaBar M n) + RecurrenceIntegration.recurrenceIncrement (Disorder.cstar M) M.gamma n m * (↑(Annealed.sigmaBar M n))⁻¹) ∧ ∀ (n m : ℤ), mStarStar M ≤ n → m ≤ m0 → n ≤ m → ↑m ≤ ↑n + Disorder.cstar M * M.gamma⁻¹ → (1 - recurrenceIntegrationSlack M C ↑Ec * M.gamma) * ↑(Annealed.sigmaBar M n) + RecurrenceIntegration.recurrenceIncrement (Disorder.cstar M) M.gamma n m * (↑(Annealed.sigmaBar M n))⁻¹ ^ 2 * ↑(Annealed.sigmaBar M m) - max 1 C * (↑m - ↑n) ^ 2 * (↑(Annealed.sigmaBar M n))⁻¹ ^ 4 * ↑(Annealed.sigmaBar M m) * 3 ^ (4 * M.gamma * ↑m) ≤ ↑(Annealed.sigmaBar M m)