ProportionFinal

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

The §4.1 proportion display with the 𝒢₂ slot discharged

ProportionAssembly.exists_proportionTail_of_honestG1 proves the display with the 𝒢₂ lane left open as a caller-supplied obligation in LaneTailFrom shape, at the split level θ/(32(r+1)) and the assembly rate c₁ = 2A. G2ThresholdSharp.g2ThresholdSharp_le_of_anchor discharges the ε-threshold of that lane from the anchor's own clauses plus two d-only constant floors on the anchor constant. This module performs the stitch: the two floors are absorbed into one constant proportionConst d, and the resulting theorem has no hypothesis beyond the anchor's own printed clauses.

The constant, and what it dominates

proportionConst d = max (max (6·assemblyConst d)           -- the assembly's own C
                             (g2LaneConst d ^ 10))          -- the lane's regime clause
                        (max (g2SharpAnchorConst    d r C N) -- the binding 𝒢₂ floor
                             (g2SharpAnchorConstTwo d r C N)) -- the exp-small 𝒢₂ floor

with r = laneRange d, C = g2LaneConst d and N = 32(r+1). The max-fold works because the anchor's strength is linear in its constant: raising C only strengthens the regime and level clauses and only weakens the conclusion, while the assembly is applied at its own constant through ProportionArith.anchorRegime_shrink / anchorLevel_weaken, and the 𝒢₁ coupling is read at C_a = C/2 — which is exactly why the assembly's floor is 6·assemblyConst d and why the rate identity C_a·(2A γ) = c⋆²s⁷ε²θ holds with equality.

The stitch consumes the rate-parametrised assembly exists_proportionTail_of_honestG1 rather than a fixed-constant consumer of it, and this is forced: the rate of the 𝒢₂ obligation is 2A = 2c⋆²s⁷ε²θ/(Cγ), which decreases in C, so a lane endpoint produced at the absorbing constant is too weak for a slot read at a smaller one. Keeping A a free parameter — the assembly's own interface — lets the slot, the two floors and the displayed exponent all be read at the single constant proportionConst d. Nothing else about the composition changes: the level θ/(32(r+1)) and the rate 2A of the assembly's slot are, character for character, the level and rate of G2ThresholdSharp's endpoint at r = laneRange d, N = 32(r+1), C_a = proportionConst d, so no monotonicity step in the level or the rate is used.

What is and is not claimed

exists_proportion_good_scales_provider is a proved local Provider helper. No Frozen.Section4 statement module is imported.

Contents

• assemblyConst, g2LaneConst — the two constants entering the stitch;
• proportionConst and its four domination lemmas — the C-absorption record;
• laneTailFrom_eventG2_of_anchor — the 𝒢₂ obligation of the assembly, proved from the anchor's own clauses at proportionConst d;
• exists_proportion_good_scales_provider — the composed display.

References

• ABK26, p.independence.between.scales; l.ratio.of.good.scales.for.mathcal.E.

1. The two constants of the stitch

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

The constant of the proportion assembly at the honest 𝒢₁ condition (ProportionAssembly.exists_proportionTail_of_honestG1).

Equations

• Algsuperdiff.Section4.Provider.Proportion.assemblyConst d = ⋯.choose

theorem Algsuperdiff.Section4.Provider.Proportion.one_le_assemblyConst (d : ℕ) : 1 ≤ assemblyConst d

theorem Algsuperdiff.Section4.Provider.Proportion.assemblyConst_pos (d : ℕ) : 0 < assemblyConst d

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

The dimensional constant of the sharp 𝒢₂ lane endpoint (G2ThresholdSharp.ratioTail_eventG2_of_thresholdSharp_shift): the constant of the two-term per-cube display.

Equations

• Algsuperdiff.Section4.Provider.Proportion.g2LaneConst d = ⋯.choose

theorem Algsuperdiff.Section4.Provider.Proportion.g2LaneConst_pos (d : ℕ) : 0 < g2LaneConst d

2. The absorbing constant

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

The constant of the composed proportion provider.

A single max-fold of the four floors the stitch needs:

• 6·assemblyConst d — the assembly, read at C_a = C/2 in the 𝒢₁ coupling;
• g2LaneConst d ^ 10 — the lane's own regime clause γ ≤ C⁻¹⁰c⋆¹⁰;
• g2SharpAnchorConst d r — the binding clause of the sharp 𝒢₂` threshold;
• `g2SharpAnchorConstTwo d r — its exponentially small clause;

at r = laneRange d, C = g2LaneConst d, N = 32(r+1). All four are functions of d alone.

Equations

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

theorem Algsuperdiff.Section4.Provider.Proportion.six_assemblyConst_le_proportionConst (d : ℕ) : 6 * assemblyConst d ≤ proportionConst d

theorem Algsuperdiff.Section4.Provider.Proportion.g2LaneConst_pow_le_proportionConst (d : ℕ) : g2LaneConst d ^ 10 ≤ proportionConst d

theorem Algsuperdiff.Section4.Provider.Proportion.g2SharpAnchorConst_le_proportionConst (d : ℕ) : g2SharpAnchorConst d (laneRange d) (g2LaneConst d) (32 * (↑(laneRange d) + 1)) ≤ proportionConst d

theorem Algsuperdiff.Section4.Provider.Proportion.g2SharpAnchorConstTwo_le_proportionConst (d : ℕ) : g2SharpAnchorConstTwo d (laneRange d) (g2LaneConst d) (32 * (↑(laneRange d) + 1)) ≤ proportionConst d

theorem Algsuperdiff.Section4.Provider.Proportion.six_le_proportionConst (d : ℕ) : 6 ≤ proportionConst d

theorem Algsuperdiff.Section4.Provider.Proportion.one_le_proportionConst (d : ℕ) : 1 ≤ proportionConst d

theorem Algsuperdiff.Section4.Provider.Proportion.proportionConst_pos (d : ℕ) : 0 < proportionConst d

theorem Algsuperdiff.Section4.Provider.Proportion.assemblyConst_le_proportionConst (d : ℕ) : assemblyConst d ≤ proportionConst d

3. The 𝒢₂ obligation of the assembly, discharged

theorem Algsuperdiff.Section4.Provider.Proportion.laneTailFrom_eventG2_of_anchor (d : ℕ) (M : Section3.ABKModel d) {s ep theta : ℝ} (hs : 0 < s) (hs12 : s ≤ 1 / 2) (hep0 : 0 < ep) (hep12 : ep ≤ 1 / 2) (hth0 : 0 < theta) (hth12 : theta ≤ 1 / 2) (hreg : M.gamma ≤ (proportionConst d)⁻¹ * Section3.Disorder.cstar M ^ 10) (hgam : 8 * M.gamma ≤ s) (hlevel : proportionConst d * (Section3.Disorder.cstar M)⁻¹ ^ 2 * s⁻¹ ^ 6 * ep⁻¹ ^ 2 * M.gamma ≤ theta) : LaneTailFrom M (fun (k : ℤ) => Support.eventG2 M k ⟨s, hs⟩ ep) (theta / (32 * (↑(laneRange d) + 1))) (2 * (Section3.Disorder.cstar M ^ 2 * s ^ 7 * ep ^ 2 * theta / (proportionConst d * M.gamma)))

The assembly's 𝒢₂ slot, proved from the anchor's own clauses.

The LaneTailFrom hypothesis hG2 of ProportionAssembly.exists_proportionTail_of_honestG1 — at the split level θ/(32(r+1)) and the assembly rate 2A, A = c⋆²s⁷ε²θ/(Cγ) — holds at C = proportionConst d for every model and every parameter triple obeying the anchor's parameter ranges, its regime clause, its standing window 8γ ≤ s and its level clause at s⁻⁶.

The route: G2ThresholdSharp.g2ThresholdSharp_le_of_anchor turns the level clause into the lane's ε-threshold (its two constant floors are the third and fourth summands of proportionConst), and G2ThresholdSharp.ratioTail_eventG2_of_thresholdSharp_shift — read at the assembly's own range laneRange d, admissible by laneRange_gap — delivers the tail at every base. No hypothesis of the lane survives: the level admissibility θ/(32(r+1))·(r+1) < 1 is θ/32 < 1, and the regime is the anchor's own, weakened through g2LaneConst d ^ 10 ≤ proportionConst d.

4. The composed display

theorem Algsuperdiff.Section4.Provider.Proportion.exists_proportion_good_scales_provider (d : ℕ) : ∃ (C : ℝ), 0 < C ∧ ∀ (M : Section3.ABKModel d) (s ep theta : ℝ), s ∈ Set.Ioc 0 (1 / 2) → ep ∈ Set.Ioc 0 (1 / 2) → theta ∈ Set.Ioc 0 (1 / 2) → M.gamma ≤ C⁻¹ * min (Section3.Disorder.cstar M ^ 10) (Section3.Disorder.cstar M ^ 2 * s ^ 5 * ep ^ 2) → 8 * M.gamma ≤ s → C * (Section3.Disorder.cstar M)⁻¹ ^ 2 * s⁻¹ ^ 6 * ep⁻¹ ^ 2 * M.gamma ≤ theta → ∀ (m0 : ℤ) (Mw : ℕ) (hs : 0 < s), ↑(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 (-(Section3.Disorder.cstar M ^ 2 * s ^ 7 * ep ^ 2 * theta * (↑Mw + 1)) / (C * M.gamma)))

The §4.1 proportion display at the s⁻⁶/s⁷ anchor clauses, with every lane discharged.

The standing window clause 8γ ≤ s, unconsumed by the two proved lanes at the split level, is genuinely consumed here: it is the lane's own standing window.

Disclosure: a proved local Provider helper.