LocalizationParams

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

Provider: the corrected recurrence parameters at a free gap multiplier

Source displays in ABK26:

• e.recurrence.params (label; display) fixes the meso scale n:= m - h - 16 ceil|log_3 gamma| and asserts m - n <= 8 gamma^{-1}, "increasing M = M(d) in e.cgamma.constraints if necessary";
• e.lower.bound.principal.one.pre (label; display) consumes two gamma^6 remainders, both controlled by 3^{-(m-h-n)/4};

The corrected multiplier, and the arithmetic re-verified here

The printed multiplier 16 is too small: at that choice 3^{-(m-h-n)/4} = 3^{-4 ceil|log_3 gamma|} in (gamma^4/81, gamma^4] and gamma^4 <= gamma^6 is false on (0,1). The minimal correction replaces 16 by any a >= 28; the development adopts a = 32. This module renders n at a free multiplier a and proves, at explicit gates, exactly the facts Steps 2 and 3 consume.

1. The quadratic is printed as "2x - 2ax - a >= 0 in sqrt x". With u := sqrt x, x := gamma^{-1}, the inequality the argument needs is a(2u+1) <= 2u^2, i.e. 2u^2 - 2au - a >= 0; the printed middle term should be 2au, not 2ax.
2. The sufficient condition is often read as an equivalence ("i.e. sqrt x >= a+1"). It is sufficient, not necessary: the positive root of 2u^2 - 2au - a is (a + sqrt(a^2+2a))/2 < a + 1/2. Only sufficiency is claimed below, and it is what the coverage constant (a+1)^2 records: 289 at the printed a = 16, 1089 at the adopted a = 32.

Both auxiliary estimates are re-derived here from Real.log_le_sub_one_of_pos alone: ceil(log_3 x) <= 2 sqrt x + 1 (via log x <= 2(sqrt x - 1), log 3 >= 1) and ceil(log_3 gamma^{-1}) * gamma^{1/4} <= 4 (via log x <= 4(x^{1/4} - 1)).

What is proved

• logThreeCeil, recurrenceGap, recurrenceMesoScale -- the corrected buffer n := m - h - a * ceil|log_3 gamma| as a function of a free a : Nat.
• rpow_three_neg_recurrenceGap_div_four_le_rpow and its a >= 28 instance -- the Step-3 gate 3^{-(m-h-n)/4} <= gamma^{a/4} <= gamma^7.
• recurrenceGap_le_two_mul_inv, recurrenceMesoScale_budget -- the coverage condition gamma^{-1} >= (a+1)^2's budget, in c_star-free form: the constant c_star is carried into the conclusion (6 c_star + 2) gamma^{-1} rather than capped; see the recorded delta below.
• natCast_le_recurrenceGap_of_rpow_le, dim_add_three_le_recurrenceGap -- the d + 3 <= m - h - n check, at the explicit gate 3^{d+3} <= gamma^{-1}.

Divergences from the printed statement

• The corrected multiplier is encoded explicitly. Nothing below is stated at the printed multiplier 16. Every statement carries a as a free natural number and every use of a >= 28 is an explicit hypothesis.
• The c_star <= 1 step is refused; the constant moves instead. The printed argument passes from h <= 6 c_star gamma^{-1} to h <= 6 gamma^{-1} silently, i.e. it uses c_star <= 1. That bound is underivable here by the second-moment route, and the only proved cap is Provider.Disorder.cstar_le_three_halves, c_star <= 3/2. No declaration in this module carries a c_star <= 1 hypothesis. Instead recurrenceMesoScale_budget keeps c_star in the conclusion, at (6 c_star + 2) gamma^{-1} and with no cap assumed, so a caller holding the proved cap reads off 11 gamma^{-1} where the printed argument reads 8 gamma^{-1}.
• d + 3, not d + 2. The stage numeric is often quoted as d + 2 <= (a ceil|log_3 gamma|).toNat. The statement below is proved for an arbitrary N and instantiated at d + 3, which is what the localization argument needs; the d + 2 form is the same lemma at a smaller N.

What is not proved here

• The gamma-threshold bridge is open. Nothing here derives hcover or hgate from e.cgamma.constraints. Both thresholds are stated as binders precisely so that the missing bridge stays visible at every instantiation site; closing it is not attempted in this module.
• c_star <= 1 is NOT available, so the printed budget constant 8 is not reachable by this route; the proved cap c_star <= 3/2 gives 11.

The triadic logarithmic ceiling and the corrected buffer

noncomputable def Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.logThreeCeil (gamma : ℝ) : ℕ

ceil |log_3 gamma|, as a natural number. On 0 < gamma <= 1 this is ceil (log_3 gamma^{-1}), which is the manuscript's quantity.

Equations

• Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.logThreeCeil gamma = ⌈Real.logb 3 gamma⁻¹⌉₊

noncomputable def Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.recurrenceGap (a : ℕ) (gamma : ℝ) : ℕ

The scale gap m - h - n = a * ceil|log_3 gamma| of the corrected e.recurrence.params, at a free multiplier a. The printed choice is a = 16, any a >= 28 is admissible, and the development adopts a = 32.

Equations

• Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.recurrenceGap a gamma = a * Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.logThreeCeil gamma

noncomputable def Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.recurrenceMesoScale (a : ℕ) (gamma : ℝ) (m h : ℤ) : ℤ

The corrected buffer n := m - h - a * ceil|log_3 gamma|.

Equations

• Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.recurrenceMesoScale a gamma m h = m - h - ↑(Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.recurrenceGap a gamma)

def Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.recurrenceGapMultiplierFloor : ℕ

The floor of the admissible multiplier gate.

Equations

• Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.recurrenceGapMultiplierFloor = 28

def Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.recurrenceGapMultiplier : ℕ

The round multiplier adopted by the development.

Equations

• Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.recurrenceGapMultiplier = 32

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.recurrenceGapMultiplierFloor_le_recurrenceGapMultiplier : recurrenceGapMultiplierFloor ≤ recurrenceGapMultiplier

@[simp]

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.sub_recurrenceMesoScale (a : ℕ) (gamma : ℝ) (m h : ℤ) : m - h - recurrenceMesoScale a gamma m h = ↑(recurrenceGap a gamma)

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.recurrenceMesoScale_le (a : ℕ) (gamma : ℝ) (m h : ℤ) : recurrenceMesoScale a gamma m h ≤ m - h

Elementary facts about the ceiling

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.logb_le_logThreeCeil (gamma : ℝ) : Real.logb 3 gamma⁻¹ ≤ ↑(logThreeCeil gamma)

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.logThreeCeil_lt_logb_add_one {gamma : ℝ} (hgamma0 : 0 < gamma) (hgamma1 : gamma ≤ 1) : ↑(logThreeCeil gamma) < Real.logb 3 gamma⁻¹ + 1

The two analytic cores

The coverage condition

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.logThreeCeil_le_two_mul_sqrt_add_one {gamma : ℝ} (hgamma0 : 0 < gamma) (hgamma1 : gamma ≤ 1) : ↑(logThreeCeil gamma) ≤ 2 * √gamma⁻¹ + 1

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.recurrenceGap_le_two_mul_inv (a : ℕ) {gamma : ℝ} (hgamma0 : 0 < gamma) (hgamma1 : gamma ≤ 1) (hcover : (↑a + 1) ^ 2 ≤ gamma⁻¹) : ↑(recurrenceGap a gamma) ≤ 2 * gamma⁻¹

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.recurrenceMesoScale_budget (a : ℕ) {gamma cstar : ℝ} (m h : ℤ) (hgamma0 : 0 < gamma) (hgamma1 : gamma ≤ 1) (hcover : (↑a + 1) ^ 2 ≤ gamma⁻¹) (hshell : ↑h ≤ 6 * cstar * gamma⁻¹) : ↑(m - recurrenceMesoScale a gamma m h) ≤ (6 * cstar + 2) * gamma⁻¹

The budget at the corrected gap, in c_star-free form.

: hgamma0, hgamma1, hcover and the shell-width cap hshell are caller-supplied and are not discharged here. No cap on c_star is assumed: the constant c_star is carried into the conclusion, so the statement is available at whatever cap the caller actually holds.

The Step-3 gap gate

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.rpow_three_neg_recurrenceGap_div_four_le_rpow (a : ℕ) {gamma t : ℝ} (hgamma0 : 0 < gamma) (hgamma1 : gamma ≤ 1) (hta : t ≤ ↑a / 4) : 3 ^ (-(↑(recurrenceGap a gamma) / 4)) ≤ gamma ^ t

The Step-3 gap gate: at the corrected gap m - h - n = a ceil|log_3 gamma| one has 3^{-(m-h-n)/4} <= gamma^{a/4}.

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.rpow_three_neg_recurrenceGap_div_four_le_rpow_seven (a : ℕ) {gamma : ℝ} (hgamma0 : 0 < gamma) (hgamma1 : gamma ≤ 1) (ha : recurrenceGapMultiplierFloor ≤ a) : 3 ^ (-(↑(recurrenceGap a gamma) / 4)) ≤ gamma ^ 7

The instance the two gamma^6 remainders consume: at any multiplier a >= 28 the switch factor and the Young remainder are controlled by gamma^7, leaving one spare power of gamma for the dimensional constant.

The d + 3 check

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.natCast_le_recurrenceGap_of_rpow_le {a N : ℕ} {gamma : ℝ} (hgamma0 : 0 < gamma) (ha : 1 ≤ a) (hgate : 3 ^ ↑N ≤ gamma⁻¹) : N ≤ recurrenceGap a gamma

If gamma^{-1} clears 3^N then the corrected gap clears N.

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.dim_add_three_le_recurrenceGap {a : ℕ} (d : ℕ) {gamma : ℝ} (hgamma0 : 0 < gamma) (ha : 1 ≤ a) (hgate : 3 ^ (↑d + 3) ≤ gamma⁻¹) : d + 3 ≤ recurrenceGap a gamma

The d + 3 <= m - h - n check, at the explicit gate 3^{d+3} <= gamma^{-1}. Nothing below asserts that e.cgamma.constraints supplies the gate.