SubLandmarkDisplays

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

Binder descriptions below are an informal inventory only, NOT a source certification; certification vocabulary is reserved for frozen source-facing declarations.

The recurrence binders below the base landmark, from the base-case plateau

The seam

l.approximate.recurrence.formula (ABK26) supplies its two displays e.what.do.we.have only on the range m** <= n <= m_0 - h, whereas its consumer l.integrate.approx.recurrence assumes e.assump.upper/e.assump.lower.modified at every pair n <= m <= m_0 with m <= n + c_star gamma^{-1}. bridges the two by bare citation.

This file pays that debt. It proves that on the uncovered range the two binders are consequences of the base-case plateau alone, and then re-derives the full conclusion of integrate_approx_recurrence_cstarPlus from an m**-floored recurrence family. No second integration engine is introduced: the headline theorem's proof is a call to the proved integrate_approx_recurrence_cstarPlus.

Why the uncovered range is small

The consumer's own admissible-scale restriction is (m: real) <= (n: real) + c_star gamma^{-1}. Hence for an uncovered pair (n < m**) one has m < m** + c_star gamma^{-1}, so both endpoints lie within c_star gamma^{-1} scales of m**. The landmark m** is defined by the gamma^{-3} threshold nu^2 >= 2 (log 3) c+ gamma^{-3} 3^{2 gamma m}, three powers of gamma below the m* threshold, and gamma (m - n) <= c_star <= 3/2 on the admissible range costs only the absolute factor 3^{2 c_star} <= 81. The plateau envelope e.small.scale.bound/e.plateau.region.bound therefore still pins the sequence at nu to relative accuracy O(gamma^2) at both endpoints, while the recurrence increment A_{n,m} is itself O(nu^2 gamma^2). Every term that the two displays are meant to track is thus dominated by the single slack term E gamma of the binders, and both binders hold with room to spare.

This is exactly the "vacuously-easily on the base-case plateau" reading suggested but never carried out. Note that it is the consumer's narrow shell budget c_star gamma^{-1} that makes it work; the argument below does not cover the source lemma's wider h <= 6 c_star gamma^{-1}, which is not needed here.

Main results

• recurrence_binders_of_below_landmark: at a single pair (n, m) whose lower endpoint meets the m** threshold, the plateau envelope alone gives both e.assump.upper and e.assump.lower.modified.
• integrate_approx_recurrence_of_landmark_floored: the conclusion e.concl.root.gamma.inv of l.integrate.approx.recurrence, from a recurrence family that is supplied only for mss <= n.
• sigmaBar_integrate_approx_recurrence_of_mStarStar_floored: the same, at the genuine running diffusivity Annealed.sigmaBar, the genuine constants Disorder.cstar/Disorder.cstarPlus, and the genuine landmark Section3.mStarStar.

What is NOT claimed

l.approximate.recurrence.formula is not proved here and nothing in this file asserts it; the hupper/hlower families of the headline theorems remain disclosed hypotheses. What is proved is that those families no longer need to be assumed below m**. No node is claimed closed.

References

• ABK26, e.mstarstar and e.mstar.
• ABK26, p.base.case; e.plateau.region.bound.
• ABK26, l.approximate.recurrence.formula.
• ABK26, l.integrate.approx.recurrence; the citation.

Scalar algebra

The three lemmas of this section are pure real algebra: no rpow, exp or log occurs in their statements, so the nonlinear arithmetic used to prove them never meets a transcendental atom.

The two binders below the landmark

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.recurrence_binders_of_below_landmark {nu cstar cstarPlus gamma E F : ℝ} {s : ℤ → ℝ} {n m : ℤ} (hnu : 0 < nu) (hcstar : 0 < cstar) (hcstar32 : cstar ≤ 3 / 2) (hcc : cstar ≤ cstarPlus) (hgamma : 0 < gamma) (hgamma128 : gamma ≤ 1 / 128) (hE : 1 ≤ E) (hF : 0 ≤ F) (hsmall : ∀ (k : ℤ), nu ≤ s k ∧ s k ≤ (1 + (nu ^ 2)⁻¹ * cstarPlus * gamma⁻¹ * 3 ^ (2 * gamma * ↑k)) * nu) (hfloor : 3 ^ (2 * gamma * ↑n) ≤ nu ^ 2 * gamma ^ 3 / (2 * Real.log 3 * cstarPlus)) (hnm : n ≤ m) (hrange : ↑m ≤ ↑n + cstar * gamma⁻¹) : s m ≤ (1 + E * gamma) * s n + RecurrenceIntegration.recurrenceIncrement cstar gamma n m * (s n)⁻¹ ∧ (1 - E * gamma) * s n + RecurrenceIntegration.recurrenceIncrement cstar gamma n m * (s n)⁻¹ ^ 2 * s m - F * (↑m - ↑n) ^ 2 * (s n)⁻¹ ^ 4 * s m * 3 ^ (4 * gamma * ↑m) ≤ s m

The uncovered range of the recurrence, discharged from the base-case plateau.

Let s satisfy the all-scale envelope e.small.scale.bound, which p.base.case supplies unconditionally for the genuine diffusivity (e.plateau.region.bound). Let (n, m) be admissible for l.integrate.approx.recurrence, i.e. n ≤ m and (m: ℝ) ≤ (n: ℝ) + c_star gamma⁻¹, and suppose the lower endpoint n meets the defining threshold of m** (e.mstarstar): 3 ^ (2 gamma n) ≤ nu ^ 2 gamma ^ 3 / (2 (log 3) c+).

Then both binders of l.integrate.approx.recurrence hold at (n, m), for any E ≥ 1 and any F ≥ 0. The approximate recurrence formula is not used.

The proof is quantitative: on this range s_n ≤ (1 + gamma²/2) nu, s_m ≤ (1 + 81 gamma²/2) nu and A_{n,m} ≤ (243/4) nu² gamma², all three O(gamma^2), while the binders' slack is E gamma ≥ gamma.

The integration lemma from a floored recurrence family

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.integrate_approx_recurrence_of_landmark_floored {nu cstar cstarPlus gamma E F : ℝ} {m0 mss : ℤ} {s : ℤ → ℝ} (hnu : 0 < nu) (hcstar : 0 < cstar) (hcstar32 : cstar ≤ 3 / 2) (hcc : cstar ≤ cstarPlus) (hgamma : 0 < gamma) (hE : 1 ≤ E) (hF : 1 ≤ F) (hsmall : ∀ (k : ℤ), nu ≤ s k ∧ s k ≤ (1 + (nu ^ 2)⁻¹ * cstarPlus * gamma⁻¹ * 3 ^ (2 * gamma * ↑k)) * nu) (hmss : 3 ^ (2 * gamma * ↑mss) ≤ nu ^ 2 * gamma ^ 3 / (2 * Real.log 3 * cstarPlus)) (hupper : ∀ (n m : ℤ), mss ≤ n → m ≤ m0 → n ≤ m → ↑m ≤ ↑n + cstar * gamma⁻¹ → s m ≤ (1 + E * gamma) * s n + RecurrenceIntegration.recurrenceIncrement cstar gamma n m * (s n)⁻¹) (hlower : ∀ (n m : ℤ), mss ≤ n → m ≤ m0 → n ≤ m → ↑m ≤ ↑n + cstar * gamma⁻¹ → (1 - E * gamma) * s n + RecurrenceIntegration.recurrenceIncrement cstar gamma n m * (s n)⁻¹ ^ 2 * s m - F * (↑m - ↑n) ^ 2 * (s n)⁻¹ ^ 4 * s m * 3 ^ (4 * gamma * ↑m) ≤ s m) : gamma ≤ (RecurrenceIntegration.recurrenceIntegrationConstant * (E * (1 + (cstar ^ 2)⁻¹ * F + (cstar ^ 2)⁻¹ * cstarPlus)))⁻¹ → ∀ m ≤ m0, |s m - √(nu ^ 2 + cstar * gamma⁻¹ * 3 ^ (2 * gamma * ↑m))| ≤ RecurrenceIntegration.recurrenceIntegrationConstant * √(E * (1 + (cstar ^ 2)⁻¹ * F + (cstar ^ 2)⁻¹ * cstarPlus) * gamma) * s m

l.integrate.approx.recurrence from an m**-floored recurrence.

Same conclusion as Provider.Diffusivity.RecurrenceIntegration.integrate_approx_recurrence_cstarPlus, but the two recurrence families are only required at pairs whose lower endpoint lies at or above a scale mss meeting the m** threshold hmss -- which is precisely the range that l.approximate.recurrence.formula delivers. Below mss the binders are supplied by recurrence_binders_of_below_landmark from the plateau envelope hsmall alone.

The gamma ≤ 1/128 smallness needed there is derived from the gamma-threshold that integrate_approx_recurrence_cstarPlus already imposes; it is not an extra hypothesis.

There is no second integration engine: the final step is a call to the proved integrate_approx_recurrence_cstarPlus.

At the genuine diffusivity and the genuine landmark

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.cstar_le_cstarPlus {d : ℕ} (M : ABKModel d) : Disorder.cstar M ≤ Disorder.cstarPlus M

c_star ≤ c+ for the genuine constants: J4's directional constant never exceeds the normalized Frobenius origin mass, because the dimension is at least two.

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.sigmaBar_integrate_approx_recurrence_of_mStarStar_floored {d : ℕ} (M : ABKModel d) {m0 : ℤ} {E F : ℝ} (hE : 1 ≤ E) (hF : 1 ≤ F) (hupper : ∀ (n m : ℤ), mStarStar M ≤ n → m ≤ m0 → n ≤ m → ↑m ≤ ↑n + Disorder.cstar M * M.gamma⁻¹ → ↑(Annealed.sigmaBar M m) ≤ (1 + E * M.gamma) * ↑(Annealed.sigmaBar M n) + RecurrenceIntegration.recurrenceIncrement (Disorder.cstar M) M.gamma n m * (↑(Annealed.sigmaBar M n))⁻¹) (hlower : ∀ (n m : ℤ), mStarStar M ≤ n → m ≤ m0 → n ≤ m → ↑m ≤ ↑n + Disorder.cstar M * M.gamma⁻¹ → (1 - E * M.gamma) * ↑(Annealed.sigmaBar M n) + RecurrenceIntegration.recurrenceIncrement (Disorder.cstar M) M.gamma n m * (↑(Annealed.sigmaBar M n))⁻¹ ^ 2 * ↑(Annealed.sigmaBar M m) - F * (↑m - ↑n) ^ 2 * (↑(Annealed.sigmaBar M n))⁻¹ ^ 4 * ↑(Annealed.sigmaBar M m) * 3 ^ (4 * M.gamma * ↑m) ≤ ↑(Annealed.sigmaBar M m)) : M.gamma ≤ (RecurrenceIntegration.recurrenceIntegrationConstant * (E * (1 + (Disorder.cstar M ^ 2)⁻¹ * F + (Disorder.cstar M ^ 2)⁻¹ * Disorder.cstarPlus M)))⁻¹ → ∀ m ≤ m0, |↑(Annealed.sigmaBar M m) - √(M.nu ^ 2 + Disorder.cstar M * M.gamma⁻¹ * 3 ^ (2 * M.gamma * ↑m))| ≤ RecurrenceIntegration.recurrenceIntegrationConstant * √(E * (1 + (Disorder.cstar M ^ 2)⁻¹ * F + (Disorder.cstar M ^ 2)⁻¹ * Disorder.cstarPlus M) * M.gamma) * ↑(Annealed.sigmaBar M m)

The seam, at the genuine carriers.

l.integrate.approx.recurrence for the running diffusivity sigmaBar, from a recurrence family supplied only on mStarStar M ≤ n -- exactly the range that l.approximate.recurrence.formula delivers.

The envelope is the proved annealedPlateau_smallScaleBound (e.plateau.region.bound), the landmark threshold is the proved Provider.Scales.rpow_mStarStar_le (e.mstarstar), and c_star ≤ 3/2 is the proved Provider.Disorder.cstar_le_three_halves; none of them is assumed.

This theorem is conditional on hupper/hlower and claims no node status. Those two families are the conclusion of l.approximate.recurrence.formula, which this repository does not prove.