ProportionAssembly

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

The §4.1 proportion assembly, in the printed display

ABK26, §4.1, p.independence.between.scales. ShiftedInterface.exists_ratioTail_goodEventBase_shift composes the two proved lanes with the 𝒢₂ slot and delivers, at every base m₀ and every window n, a tail exp(−c₁n) for the clause avsum 𝟙{𝒢} ≤ 1 − θ. This module turns that lane package into the printed display itself:

ℙ[ (M_w+1)⁻¹ ∑_{k ≤ M_w} 𝟙{𝒢(m₀+k, 0; s, ε)} ≤ 1 − θ ] ≤ 6 exp(−A(M_w+1)) ,

with A read off the model. Three things separate the two shapes and all three are discharged here.

• The level ceiling. The two proved lanes need θ(r+1) < 1, which the printed θ ≤ ½ does not give once r ≥ 2. The lanes are run at θ/(8L), L = r+1, and the conclusion is read back at θ by measure_mono; the factor L is absorbed into the assembly's own constant (ProportionArith).
• The rate. With c₁ = 2A one has exp(−2A·M_w) ≤ 6 exp(−A(M_w+1)) for every M_w ≥ 1. The printed prefactor 6 is exactly what pays for the (M_w+1)-versus-M_w offset.
• The single-scale window. At M_w = 0 the composed tail is 1 and the printed right-hand side is 6exp(−A), so the lane package must be read at a different window: {ω ∉ 𝒢(m₀)} carries bad-density ½ over {m₀, m₀+1}, so the window-1 endpoint bounds it.

The form delivered, and what blocks the printed one

exists_proportionTail_of_honestG1 is the assembly proper: the display, at an abstract rate A, from the honest 𝒢₁ condition C(1+2A)γ ≤ θ c⋆ s⁶ ε². The frozen theorem's printed clauses (s⁻⁴, s⁵) do not imply that condition on a nonempty parameter region: the minimal sufficient strengthening is the level clause at s⁻⁶ and the rate at s⁷, proved in LaneCertificates (couplingG1_of_anchor). The honest 𝒢₁ condition is therefore an interface obligation of the consumer, not a source premise.

References

• ABK26, p.independence.between.scales; d.good.event.for.lambda, (e.lambda.good.events); e.theta.cond.two.

1. The common dependence range

noncomputable def Algsuperdiff.Section4.Provider.Proportion.laneRange (d : ℕ) : ℕ

The dependence range of the assembly. The three lanes are run at one range: the one the composed two-lane interface fixes, enlarged so that the count 3 + (2/3)√d ≤ 3^r also holds at it. The 𝒢₂ endpoint is stated at every admissible range, so this choice costs nothing.

Equations

• Algsuperdiff.Section4.Provider.Proportion.laneRange d = max ⋯.choose ⋯.choose

theorem Algsuperdiff.Section4.Provider.Proportion.one_le_laneRange (d : ℕ) : 1 ≤ laneRange d

theorem Algsuperdiff.Section4.Provider.Proportion.laneRange_gap (d : ℕ) : 3 + 2 * 3 ^ (1 - 2) * √↑d ≤ 3 ^ laneRange d

The assembly's range is admissible for the count, so the shifted 𝒢₂ endpoint can be read at it.

2. The display from the lane package

theorem Algsuperdiff.Section4.Provider.Proportion.measure_scalePropFrom_le_of_lanes {d : ℕ} (M : Section3.ABKModel d) (Ccg : ℝ) (s : { s : ℝ // 0 < s }) (ep theta thetaL A : ℝ) (htheta0 : 0 < theta) (htheta1 : theta ≤ 1) (hLle : thetaL ≤ theta) (hLhalf : thetaL < 1 / 2) (hA0 : 0 ≤ A) (hbad : ∀ (m0 : ℤ) (n : ℕ), ↑(Section3.Cutoff.cutoffSampleLaw M) {omega : Section3.Cutoff.CutoffSample d | thetaL < Probability.IndicatorDensity.scaleProp (fun (k : ℤ) => (Support.goodEventBase M Ccg (m0 + k) s ep)ᶜ) n omega} ≤ ENNReal.ofReal (Real.exp (-(2 * A) * ↑n))) (hgood : ∀ (m0 : ℤ) (n : ℕ), ↑(Section3.Cutoff.cutoffSampleLaw M) {omega : Section3.Cutoff.CutoffSample d | Probability.IndicatorDensity.scaleProp (fun (k : ℤ) => Support.goodEventBase M Ccg (m0 + k) s ep) n omega ≤ 1 - thetaL} ≤ ENNReal.ofReal (Real.exp (-(2 * A) * ↑n))) (m0 : ℤ) (Mw : ℕ) : ↑(Section3.Cutoff.cutoffSampleLaw M) {omega : Section3.Cutoff.CutoffSample d | scalePropFrom (fun (m : ℤ) => Support.goodEventBase M Ccg m s ep) m0 Mw omega ≤ 1 - theta} ≤ ENNReal.ofReal (6 * Real.exp (-(A * (↑Mw + 1))))

The printed display from the two output forms of the lane package.

The good-proportion endpoint at the split level θ_L covers every window M_w ≥ 1; the bad-density endpoint at window 1 covers M_w = 0, where the printed clause is the single bad event 𝒢(m₀)ᶜ. Running the lanes at the rate 2A is what makes both branches land under 6exp(−A(M_w+1)).

3. The assembly at the honest 𝒢₁ condition

theorem Algsuperdiff.Section4.Provider.Proportion.exists_proportionTail_of_honestG1 (d : ℕ) : ∃ (C : ℝ), 1 ≤ C ∧ ∀ (M : Section3.ABKModel d) (s ep theta A : ℝ), 0 < s → s ≤ 1 / 2 → 0 < ep → ep ≤ 1 / 2 → 0 < theta → theta ≤ 1 / 2 → M.gamma ≤ C⁻¹ * Section3.Disorder.cstar M ^ 10 → C * (Section3.Disorder.cstar M)⁻¹ ^ 2 * s⁻¹ ^ 4 * ep⁻¹ ^ 2 * M.gamma ≤ theta → 0 ≤ A → 2 * A * M.gamma ≤ 1 → C * (1 + 2 * A) * M.gamma ≤ theta * Section3.Disorder.cstar M * s ^ 6 * ep ^ 2 → ∀ (m0 : ℤ) (Mw : ℕ) (hs : 0 < s), LaneTailFrom M (fun (k : ℤ) => Support.eventG2 M k ⟨s, hs⟩ ep) (theta / (32 * (↑(laneRange d) + 1))) (2 * A) → ↑(Section3.Cutoff.cutoffSampleLaw M) {omega : Section3.Cutoff.CutoffSample d | 1 / (↑Mw + 1) * ∑ k ∈ Finset.range (Mw + 1), (Frozen.Section4.goodEventAt M (Support.cgEllipLowerConstant d) (m0 + ↑k) 0 ⟨s, hs⟩ ep).indicator (fun (x : Section3.Cutoff.CutoffSample d) => 1) omega ≤ 1 - theta} ≤ ENNReal.ofReal (6 * Real.exp (-(A * (↑Mw + 1))))

The §4.1 proportion display, at an abstract rate, from the honest 𝒢₁ condition.

One constant C(d) ≥ 1, fixed before the model and before every parameter. For every model, every s, ε ∈ (0, ½], every level θ ∈ (0, ½] and every rate A ≥ 0 subject to

• the printed regime γ ≤ C⁻¹c⋆¹⁰,
• the printed level clause C c⋆⁻²s⁻⁴ε⁻²γ ≤ θ,
• the honest 𝒢₁ condition C(1+2A)γ ≤ θ c⋆ s⁶ ε²,

the printed display holds at every base m₀ and every window length M_w, including M_w = 0, with right-hand side 6exp(−A(M_w+1)).

The 𝒢₂ lane enters as the named hypothesis hG2, in the LaneTailFrom shape, at exactly the one level θ/(32(r+1)) and the one rate 2A the assembly consumes — the shape the shifted 𝒢₂ lane produces at r = laneRange d (admissible by laneRange_gap), for every ε above its own threshold ε₀. It is a caller-supplied interface obligation, not a source premise.