ZCesaroLeg

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

The Z^{(1)} leg: Markov on the kicking lemma, the centre union, and the tail

ABK26, §4.2. The chain is the one the manuscript performs:

1. The centre transfer. The per-centre window average at a centre y has the mass of the origin one (GoodEvents.measure_lt_mul_sum_indicator_goodEventAt, a consequence of the two proved translation identities).

2. The event inclusion 𝒢(k; s, s√δ) ⊆ 𝒢(k; s, 1) at s√δ ≤ 1 (goodEventBase_subset_one), which is what lets the kicking lemma — stated at the tolerance 1 — bound the frozen score's own gated average.

3. Markov on the Γ₂ fluctuation (measure_center_cesaro_le): the kicking lemma splits the average into Xdet ≤ C c⋆^{−1}s^{−7/2}√γ and a Γ₂ fluctuation at scale C c⋆^{−1}s^{−9/2}√γ j^{−1/2}; at the level t = √(A j) the weak-Orlicz definition returns exp(−A j) with A = c⋆² s⁹ δ² / (4 C_kick² γ).

4. The centre union and the geometric closure — Algsuperdiff.Probability's windowScale_tail_const_of_center_tails at D = 2d, on the proved centre enumeration centerFinset (card_centerFinset_le, and hcover as the theorem exists_center_finset_of_badCesaro), followed by the (N−1)-shift absorption of windowTailConst into the frozen prefactor.

The δ-floor is derived, not assumed — and the exponent closes exactly

The manuscript's Markov step needs δ ≥ (2C + 2d log 3) c⋆^{−1}s^{−7/2}γ^{1/2}, i.e. at the corrected fluctuation exponent δ ≥ 2C c⋆^{−1}s^{−9/2}γ^{1/2}. Squaring, that is

4 C_kick² γ ≤ c⋆² s⁹ δ², equivalently 1 ≤ A,

and minimal_scale_separation's regime clause supplies exactly γ ≤ C^{−10}·δ²c⋆²s⁹, so the floor holds as soon as 4 C_kick² ≤ C ≤ C^{10}. The condition-exponent and the rate-exponent are both s⁹: the kicking envelope's s^{−9/2}, squared, is the frozen clause's s⁹.

References

• ABK26, p.minimal.scale.separation.sec4.

1. The kicking lemma's constant

noncomputable def Algsuperdiff.Section4.Provider.MinimalScale.kickConst (d : ℕ) : ℝ

The kicking lemma's constant (e.good.scale.kicking, d only).

Equations

• Algsuperdiff.Section4.Provider.MinimalScale.kickConst d = ⋯.choose

theorem Algsuperdiff.Section4.Provider.MinimalScale.kickConst_pos (d : ℕ) : 0 < kickConst d

theorem Algsuperdiff.Section4.Provider.MinimalScale.kickConst_spec (d : ℕ) (M : Section3.ABKModel d) : M.gamma ≤ (kickConst d)⁻¹ ^ 10 * Section3.Disorder.cstar M ^ 10 → ∀ (s : { s : ℝ // 0 < s }), 8 * M.gamma ≤ ↑s → ↑s ≤ 1 / 4 → ∀ (n m : ℤ), n < m → ∃ (Xdet : Section3.Cutoff.CutoffSample d → ℝ) (Xfluc : Section3.Cutoff.CutoffSample d → ℝ), (∀ᵐ (omega : Section3.Cutoff.CutoffSample d) ∂↑(Section3.Cutoff.cutoffSampleLaw M), (↑(m - n).toNat + 1)⁻¹ * ∑ k ∈ Finset.Icc n m, (Support.goodEventBase M (Support.cgEllipLowerConstant d) k s 1).indicator (fun (omega' : Section3.Cutoff.CutoffSample d) => Support.fluxCorrectedErrorObservableSup M k s omega') omega ≤ ENNReal.ofReal (Xdet omega + Xfluc omega)) ∧ (∀ (omega : Section3.Cutoff.CutoffSample d), Xdet omega ≤ kickConst d * ((Section3.Disorder.cstar M)⁻¹ * (√↑s ^ 7)⁻¹ * √M.gamma)) ∧ HCPolySupport.IndependentSums.IsBigO (↑(Section3.Cutoff.cutoffSampleLaw M)) (HCPolySupport.IndependentSums.gammaSigma 2) Xfluc (kickConst d * ((Section3.Disorder.cstar M)⁻¹ * (√↑s ^ 9)⁻¹ * √M.gamma) * ↑(m - n) ^ (-1 / 2))

The kicking lemma at kickConst d.

2. The event inclusion 𝒢(k; s, ep) ⊆ 𝒢(k; s, 1)

theorem Algsuperdiff.Section4.Provider.MinimalScale.goodEventBase_subset_one {d : ℕ} (M : Section3.ABKModel d) (Ccg : ℝ) (k : ℤ) (s : { s : ℝ // 0 < s }) {ep : ℝ} (hep0 : 0 ≤ ep) (hep1 : ep ≤ 1) : Support.goodEventBase M Ccg k s ep ⊆ Support.goodEventBase M Ccg k s 1

𝒢(k; s, ep) ⊆ 𝒢(k; s, 1) for 0 ≤ ep ≤ 1. 𝒢₀ is untouched, 𝒢₁'s threshold carries the factor s·ep and 𝒢₂'s is ep, so both are monotone in ep.

theorem Algsuperdiff.Section4.Provider.MinimalScale.sum_indicator_le_of_le_one {d : ℕ} (M : Section3.ABKModel d) (Ccg : ℝ) (s : { s : ℝ // 0 < s }) {ep : ℝ} (hep0 : 0 ≤ ep) (hep1 : ep ≤ 1) (n m : ℤ) (c : ENNReal) (omega : Section3.Cutoff.CutoffSample d) : c * ∑ k ∈ Finset.Icc n m, (Support.goodEventBase M Ccg k s ep).indicator (fun (omega' : Section3.Cutoff.CutoffSample d) => Support.fluxCorrectedErrorObservableSup M k s omega') omega ≤ c * ∑ k ∈ Finset.Icc n m, (Support.goodEventBase M Ccg k s 1).indicator (fun (omega' : Section3.Cutoff.CutoffSample d) => Support.fluxCorrectedErrorObservableSup M k s omega') omega

The gated window average is monotone in the tolerance.

3. The √-arithmetic of the Markov level

theorem Algsuperdiff.Section4.Provider.MinimalScale.envNine_sq {d : ℕ} (M : Section3.ABKModel d) {s : ℝ} (hs : 0 < s) : ((Section3.Disorder.cstar M)⁻¹ * (√s ^ 9)⁻¹ * √M.gamma) ^ 2 = M.gamma / (Section3.Disorder.cstar M ^ 2 * s ^ 9)

The square of the envelope.

theorem Algsuperdiff.Section4.Provider.MinimalScale.rpow_neg_half_eq_inv_sqrt {x : ℝ} (hx : 0 ≤ x) : x ^ (-1 / 2) = (√x)⁻¹

The reciprocal square root, in √ form.

theorem Algsuperdiff.Section4.Provider.MinimalScale.rpow_two_eq_sq (t : ℝ) : t ^ 2 = t ^ 2

t ^ (2 : ℝ) = t ^ (2 : ℕ).

4. The per-centre Markov bound

theorem Algsuperdiff.Section4.Provider.MinimalScale.measure_center_cesaro_le {d : ℕ} (C : ℝ) (hC1 : 1 ≤ C) (hCa : kickConst d ≤ C) (hCb : 4 * kickConst d ^ 2 ≤ C) (M : Section3.ABKModel d) (s delta : ℝ) (hs : 0 < s) (hs4 : s ≤ 1 / 4) (hd0 : 0 < delta) (hd2 : delta ≤ 1 / 2) (hgam : M.gamma ≤ C⁻¹ ^ 10 * min (Section3.Disorder.cstar M ^ 10) (delta ^ 2 * Section3.Disorder.cstar M ^ 2 * s ^ 9)) (hwin : 8 * M.gamma ≤ s) (y : HCPolySupport.Vec d) (m : ℤ) (j : ℕ) (hj : 1 ≤ j) : (↑(Section3.Cutoff.cutoffSampleLaw M)).real {omega : Section3.Cutoff.CutoffSample d | ENNReal.ofReal delta < centerCesaroScore M s delta hs y (m - ↑j) m omega} ≤ Real.exp (-(delta ^ 2 * Section3.Disorder.cstar M ^ 2 * s ^ 9 / (4 * kickConst d ^ 2 * M.gamma)) * ↑j)

A = c⋆² s⁹ δ² / (4 C_kick² γ) ≥ 1.

Route: the centre transfer, the tolerance inclusion 𝒢(k;s,s√δ) ⊆ 𝒢(k;s,1), the kicking lemma, and Markov at the weak-Orlicz level t = √(A j). The δ-floor δ ≥ 2 C_kick c⋆^{−1}s^{−9/2}γ^{1/2} is derived from the regime clause — squared, it is exactly 1 ≤ A — and no power of s is absorbed.

5. hcover for the Cesàro leg, as a theorem

theorem Algsuperdiff.Section4.Provider.MinimalScale.exists_center_finset_of_badCesaro {d : ℕ} (M : Section3.ABKModel d) (s delta : ℝ) (hs : 0 < s) (m : ℤ) (j : ℕ) (omega : Section3.Cutoff.CutoffSample d) (h : badCesaro M s delta hs m j omega) : ∃ z ∈ centerFinset d m j, ENNReal.ofReal delta < centerCesaroScore M s delta hs (Support.triadicLatticePoint (m - ↑j - 1) z) (m - ↑j) m omega

hcover, as a theorem (the Cesàro leg). A bad Cesàro window is witnessed by a centre of the proved explicit enumeration; the mechanism is lt_iSup_iff in ℝ≥0∞, so no finiteness and no positivity of δ is used.

6. The assembled constant of the Z^{(1)} leg

noncomputable def Algsuperdiff.Section4.Provider.MinimalScale.zOneConst (d : ℕ) : ℝ

The Z^{(1)} leg's constant. Four floor duties, all functions of d alone: kickConst d (the kicking lemma's own regime clause), 8·kickConst d² (the δ-floor and the halving 2c₀ ≤ A that pays for the centre count), 2·3^{2d} (the union-bound prefactor against the geometric-summation constant (1 − e^{−c₀})⁻¹), and 4 d log 3 (the absorption 2d log 3 + c₀ ≤ A).

Equations

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

theorem Algsuperdiff.Section4.Provider.MinimalScale.kickConst_le_zOneConst (d : ℕ) : kickConst d ≤ zOneConst d

theorem Algsuperdiff.Section4.Provider.MinimalScale.eight_mul_kickConst_sq_le_zOneConst (d : ℕ) : 8 * kickConst d ^ 2 ≤ zOneConst d

theorem Algsuperdiff.Section4.Provider.MinimalScale.two_mul_three_pow_le_zOneConst (d : ℕ) : 2 * 3 ^ (2 * d) ≤ zOneConst d

theorem Algsuperdiff.Section4.Provider.MinimalScale.four_mul_log_three_le_zOneConst (d : ℕ) : 4 * ↑d * Real.log 3 ≤ zOneConst d

theorem Algsuperdiff.Section4.Provider.MinimalScale.one_le_zOneConst (d : ℕ) : 1 ≤ zOneConst d

7. The geometric tail of the Cesàro random scale

theorem Algsuperdiff.Section4.Provider.MinimalScale.measure_tail_badCesaro_le {d : ℕ} (C : ℝ) (hC : zOneConst d ≤ C) (M : Section3.ABKModel d) (s delta : ℝ) (hs : 0 < s) (hs4 : s ≤ 1 / 4) (hd0 : 0 < delta) (hd2 : delta ≤ 1 / 2) (hgam : M.gamma ≤ C⁻¹ ^ 10 * min (Section3.Disorder.cstar M ^ 10) (delta ^ 2 * Section3.Disorder.cstar M ^ 2 * s ^ 9)) (hwin : 8 * M.gamma ≤ s) (m : ℤ) (N : ℕ) : ↑(Section3.Cutoff.cutoffSampleLaw M) {omega : Section3.Cutoff.CutoffSample d | ↑N ≤ Probability.minimalScaleEN (badCesaro M s delta hs m) omega} ≤ ENNReal.ofReal (C * Real.exp (-((↑N - 1) * s ^ 9 * Section3.Disorder.cstar M ^ 2 * delta ^ 2) / (C * M.gamma)))

The geometric tail of the Cesàro-𝓔 random scale, at the frozen prefactor-tail shape

P[N ≤ Z¹] ≤ C exp(−(N−1) s⁹ c⋆² δ² /(C γ)).

The route: the per-centre Markov bound measure_center_cesaro_le, the proved centre count card_centerFinset_le and cover exists_center_finset_of_badCesaro (both theorems — neither is a binder), then Algsuperdiff.Probability.windowScale_tail_const_of_center_tails at D = 2d, whose windowTailConst (2d) c₀ prefactor is absorbed by the (N−1) shift of the frozen display. The regime clause is minimal_scale_separation's own, at s⁹.

8. The hZ1tail slot in its exact shape

theorem Algsuperdiff.Section4.Provider.MinimalScale.measure_tail_badCesaro_le_half {d : ℕ} (C : ℝ) (hC : 2 * zOneConst d ≤ C) (M : Section3.ABKModel d) (s delta : ℝ) (hs : 0 < s) (hs4 : s ≤ 1 / 4) (hd0 : 0 < delta) (hd2 : delta ≤ 1 / 2) (hgam : M.gamma ≤ C⁻¹ ^ 10 * min (Section3.Disorder.cstar M ^ 10) (delta ^ 2 * Section3.Disorder.cstar M ^ 2 * s ^ 9)) (hwin : 8 * M.gamma ≤ s) (m : ℤ) (N : ℕ) : ↑(Section3.Cutoff.cutoffSampleLaw M) {omega : Section3.Cutoff.CutoffSample d | ↑N ≤ Probability.minimalScaleEN (badCesaro M s delta hs m) omega} ≤ ENNReal.ofReal (C / 2 * Real.exp (-((↑N - 1) * s ^ 9 * Section3.Disorder.cstar M ^ 2 * delta ^ 2) / (C * M.gamma)))

The hZ1tail slot, discharged. The Z¹ tail at half the prefactor and the un-halved rate — the verbatim shape ZAssembly.frozen_body_of_cesaro_tail consumes.

Length-0 windows are free (measure ≤ 1 ≤ C/2), and for N ≥ 1 the rate num/((C/2)γ) delivered by measure_tail_badCesaro_le at C/2 dominates the displayed num/(Cγ). This is ZAssembly.measure_tail_badDensity_le_half's two-line rate-weakening pattern, applied to the Cesàro leg.