RootAssemblyParameters

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

t.regularity root assembly, part one: the parameter web and the single a.e. block

The two defects this module clears

The proved outer chain is → → →, each layer re-exporting its predecessor. Two structural defects block the root assembly, and both are fixed here at Z mathematical cost (no new estimate, no new hypothesis).

(D1) The chain is lossy. The Step-3 window/budget endpoint drops GoodScaleWindows, and the Step-7a selection endpoint drops in addition the ε_j cap. But GoodScaleWindows is exactly what's stepFiveConcreteOscillationResult_of_stepFourDecay demands, at the same ω, the same (n,m) and the same X-gate. Because each layer re-derives its OWN existential Z and its OWN (C₁,γ₀,C) cannot be invoked side by side and their witnesses identified. rootAssembly_aePackage below carries GoodScaleWindows, the window/budget package AND the Step-7a selection in ONE ∀ᵐ ω block under ONE Z and ONE (C₁,γ₀,C).

(D2) C₁ is opaque. The Step-1/3/7a producers export C₁ as an existential real with 2 ≤ C₁, while the Step-6 endpoint needs it spelled out as stepOneC1 d Cedos Cann Citer k, with Cann a further existential hidden inside the ε_j-cap proof (ae_stepOneEpsJ_le). rootAssembly_aePackage exports Cann and the defining identity, so the produced C₁ is consumable by the pointwise layer.

Enlarging the produced constant

The frozen root uses ONE letter C in four roles: the tail prefactor, the tail exponent (twice), the α-range α ≤ 1 - C√γ, and the prefactor of e.energy.density.estimate. The §4.4 chain produces its estimate constant independently of the minimal-scale constant, so the assembly must take a maximum. §3 proves that every role is MONOTONE-W in C: enlarging C weakens the tail bound and shrinks the admissible α-range, so a single maximum is legitimate. This is the arithmetic behind "the single C in all three roles", and it is proved here rather than asserted.

References

• ABK26, t.regularity; Steps 1--3 and 7a.

1. The per-ω payload of the single a.e. block

def Algsuperdiff.Section4.Provider.Regularity.RootWindowPayload {d : ℕ} (M : Section3.ABKModel d) (C1 alpha : ℝ) (n m : ℤ) (omega : Section3.Cutoff.CutoffSample d) : Prop

The Step-1/3/7a payload at one window [n,m]: the good-scale windows of p.minimal.scale.separation.sec4 (the input's Step-5 endpoint reads)'s window family / bad set / budget / separation package's Step-7a selection at every printed lattice centre.

Packaging the three together is what lets ONE filter_upwards serve the whole per-ω chain.

Equations

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

theorem Algsuperdiff.Section4.Provider.Regularity.rootWindowPayload_of_goodScaleWindows {d : ℕ} {M : Section3.ABKModel d} {C1 alpha : ℝ} {n m : ℤ} {omega : Section3.Cutoff.CutoffSample d} (hdelta : stepOneDelta C1 alpha ∈ Set.Ioc 0 (1 / 2)) (hwin : 14 ≤ m - n) (hgood : GoodScaleWindows M stepOneSEighth (stepOneDelta C1 alpha) stepOneSEighth_pos n m omega) : RootWindowPayload M C1 alpha n m omega

The payload from the good-scale windows alone, at the gate. Every component beyond GoodScaleWindows is a proved pointwise consequence:'s stepThreeWindowsAndBudget_of_goodScaleWindows's exists_stepSevenSelectionData_of_stepThreeWindowsAndBudget.

2. The single a.e. endpoint, with C₁ transparent

theorem Algsuperdiff.Section4.Provider.Regularity.rootAssembly_aePackage (d : ℕ) (cstar : ℝ) (hcstar : 0 < cstar) (Cedos Citer Cann : ℝ) (k : ℕ) (hk : 11 ≤ k) : ∃ (gamma0 : ℝ) (C : ℝ), 0 < gamma0 ∧ 0 < C ∧ 2 ≤ stepOneC1 d Cedos Cann Citer k ∧ 2 * ↑d + 2 ≤ stepOneC1 d Cedos Cann Citer k ∧ 4 * Citer * (↑k + 1) / Real.log 3 ≤ stepOneC1 d Cedos Cann Citer k ∧ ∀ (M : Section3.ABKModel d), Section3.Disorder.cstar M = cstar → M.gamma ≤ gamma0 → ∀ (alpha : ℝ), 0 < alpha → alpha ≤ 1 - C * √M.gamma → ∀ (m : ℤ), ∃ (Z : Section3.Cutoff.CutoffSample d → ℕ∞), Measurable (minimalScaleX Z k) ∧ (∀ (N : ℕ), ↑(Section3.Cutoff.cutoffSampleLaw M) {omega : Section3.Cutoff.CutoffSample d | ↑N ≤ minimalScaleX Z k omega} ≤ ENNReal.ofReal (C * Real.exp (-((1 - alpha) ^ 2 * (↑N - C)) / (C * M.gamma)))) ∧ ∀ᵐ (omega : Section3.Cutoff.CutoffSample d) ∂↑(Section3.Cutoff.cutoffSampleLaw M), ∀ n ≤ m, minimalScaleX Z k omega ≤ ↑(m - n).toNat → RootWindowPayload M (stepOneC1 d Cedos Cann Citer k) alpha n m omega

t.regularity Steps 1--3 and 7a, as one a.e. theorem with a transparent C₁.

The frozen root's binder block with the minimal scale X, its measurability, its tail, and a single ∀ᵐ ω block whose payload is RootWindowPayload — good-scale windows, the 14 ≤ m-n gate consequence, the window/bad-set/budget/separation package and the Step-7a selection at every printed lattice centre, all at one Z and one (C₁,γ₀,C).

C₁ is produced spelled out as stepOneC1 d Cedos Cann Citer k, at a caller-supplied Cann and a caller-supplied Step-1 index k ≥ 11, so the pointwise §4.4 layer — whose statements name stepOneC1 transparently — can be applied at the produced constant. The three floors travel with it.

C_edos is the abstract excess-decay one-step constant, C_iter the abstract Step-6 iteration constant.

3. Enlarging the produced constant

theorem Algsuperdiff.Section4.Provider.Regularity.minimalScaleTail_mono_const {gamma alpha C0 C N : ℝ} (hC0 : 0 < C0) (hle : C0 ≤ C) (hgamma : 0 < gamma) (hN : 0 ≤ N) : C0 * Real.exp (-((1 - alpha) ^ 2 * (N - C0)) / (C0 * gamma)) ≤ C * Real.exp (-((1 - alpha) ^ 2 * (N - C)) / (C * gamma))

The tail bound is monotone-weakening in C.

The frozen root prints ONE constant in the tail's three slots, so an assembly that must also serve e.energy.density.estimate needs to enlarge it. The enlargement is free: with 0 < C₀ ≤ C and N ≥ 0,

  C₀·exp(−(1−α)²(N−C₀)/(C₀γ))  ≤  C·exp(−(1−α)²(N−C)/(Cγ)) .

The prefactor grows and the exponent rises (because N/C ≤ N/C₀), so the right-hand side dominates.

theorem Algsuperdiff.Section4.Provider.Regularity.minimalScaleTail_ofReal_mono_const {gamma alpha C0 C : ℝ} {N : ℕ} (hC0 : 0 < C0) (hle : C0 ≤ C) (hgamma : 0 < gamma) : ENNReal.ofReal (C0 * Real.exp (-((1 - alpha) ^ 2 * (↑N - C0)) / (C0 * gamma))) ≤ ENNReal.ofReal (C * Real.exp (-((1 - alpha) ^ 2 * (↑N - C)) / (C * gamma)))

The tail bound at an enlarged constant, in the ℝ≥0∞ shape the frozen root prints.

theorem Algsuperdiff.Section4.Provider.Regularity.alphaRange_of_mono_const {gamma alpha C0 C : ℝ} (hle : C0 ≤ C) (halpha : alpha ≤ 1 - C * √gamma) : alpha ≤ 1 - C0 * √gamma

The α-range at an enlarged constant. Enlarging C shrinks the admissible range, so the producer's own range hypothesis follows from the enlarged one — the direction the assembly needs.