ParameterWeb

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

Provider: the parameter web of p.multiscale.estimate

This module collects the parameter-discharge obligations accumulated across the proved Section 3.6 modules and routes all of them through a single arithmetic core: the two scalar binders of the multiscale proposition's own hypothesis list,

(c⋆)⁻¹ ε^{-Cms} ≤ E                  (the window)
γ ≤ (E⁻¹)^{10}                       (the smallness)

The arithmetic core, in one paragraph

On ε ∈ (0,1/2] one has ε⁻¹ ≥ 2, hence ε^{-a} ≥ 2^a for every a ≥ 0 (two_rpow_le_rpow_neg). The proved Provider.Disorder.cstar_le_three_halves gives c⋆⁻¹ ≥ 2/3, so the window binder yields the two floors

K * c⋆⁻¹ ≤ E        whenever K ≤ 2^{Cms}        (the RELATIVE gate)
K ≤ E               whenever (3/2) K ≤ 2^{Cms}  (the ABSOLUTE gate)

and in particular 10 ≤ E as soon as Cms ≥ 4. The smallness binder then turns every E-floor into a γ-ceiling. For the corridor one uses the logarithmic form of the same window: ε^{-Cms} = exp(Cms |log ε|) and x + 1 ≤ exp x give Cms |log ε| ≤ (3/2) E, so the integer cutoff h := waveCutoff (2 Chom) ε = ⌈2 Chom |log ε|⌉ obeys h ≤ 3 Chom E / Cms + 1, which is ≤ 3E + 1 once the witness satisfies Chom ≤ Cms.

The 10^9 and where it may appear (development decision D4)

What §3 and §5 prove is strictly stronger and numeral free — the ε^2 form γ ≤ Chom⁻¹ E^{-2} ε^2 (development decision D2, the form the proved homogenizationStep_spec consumes) and the corridor γ h ≤ 1, both on a free real Chom and on the sole witness constraints 4 ≤ Cms, Chom ≤ Cms, Chom ≤ 2^{Cms}.

Those constraints are satisfiable for every real Chom: that is exists_parameterWeb_general (§8), which binds Chom freely. Consequently max (homogenizationStepConst d) 10^9 is a legitimate instantiation of that theorem, at which this module's own Chom-free dischargers (gamma_mul_waveCutoff_le_one, and chom_le_pow_mul_sq_of_window composed with gamma_le_gate_of_pow) deliver BOTH enlarged obligations — the corridor and the ε^2 gate at the enlarged constant. The numeral 10^9 therefore occurs in no statement of this file: it is a witness choice inside an existential and never a claim about .choose.

_root_ anchoring: prophylactic, measured

The three open _root_.… lines below are not load-bearing in this module. The anchoring is kept because the enclosing namespace Algsuperdiff.Section3.Provider.MultiscaleEstimate is a sibling of Algsuperdiff.Section3.Provider.Multiscale (Section 3.3, 77 files, live name collisions — development decision D5), so a future sibling declaration named Homogenization or MeasureTheory would silently capture the open. No claim of present load-bearing is made.

Sources

• ABK26, p.multiscale.estimate and its parameter conditions, the cutoff h := C|log ε|.

1. The window floor

The frozen root binds ε ∈ (0,1/2] and (c⋆)⁻¹ ε^{-Cms} ≤ E. Everything in §2-§5 is read off those two lines together with c⋆ ≤ 3/2.

theorem Algsuperdiff.Section3.Provider.MultiscaleEstimate.one_le_two_rpow {a : ℝ} (ha : 0 ≤ a) : 1 ≤ 2 ^ a

2^a ≤ 1 fails for a < 0; on a ≥ 0 the base-2 power is at least one.

theorem Algsuperdiff.Section3.Provider.MultiscaleEstimate.two_rpow_le_rpow_neg {epsilon a : ℝ} (heps0 : 0 < epsilon) (heps : epsilon ≤ 1 / 2) (ha : 0 ≤ a) : 2 ^ a ≤ epsilon ^ (-a)

The window's exponential floor. On ε ∈ (0,1/2] the negative power ε^{-a} dominates 2^a for every a ≥ 0.

theorem Algsuperdiff.Section3.Provider.MultiscaleEstimate.two_thirds_le_cstar_inv {d : ℕ} (M : ABKModel d) : 2 / 3 ≤ (Disorder.cstar M)⁻¹

The shell constant's reciprocal floor. From the proved Provider.Disorder.cstar_le_three_halves.

theorem Algsuperdiff.Section3.Provider.MultiscaleEstimate.two_thirds_mul_le_of_window {cstarInv epsilon Cms E : ℝ} (hcs : 2 / 3 ≤ cstarInv) (hpow : 0 ≤ epsilon ^ (-Cms)) (hwin : cstarInv * epsilon ^ (-Cms) ≤ E) : 2 / 3 * epsilon ^ (-Cms) ≤ E

The model-free window floor. The frozen window binder, with c⋆⁻¹ replaced by its absolute lower bound 2/3. Every later statement of §2-§5 takes this as its hypothesis, so it is stated once and proved once.

theorem Algsuperdiff.Section3.Provider.MultiscaleEstimate.two_thirds_mul_le_of_window' {d : ℕ} (M : ABKModel d) {epsilon Cms E : ℝ} (heps0 : 0 < epsilon) (hwin : (Disorder.cstar M)⁻¹ * epsilon ^ (-Cms) ≤ E) : 2 / 3 * epsilon ^ (-Cms) ≤ E

The model-level form of two_thirds_mul_le_of_window, at the frozen root's own window binder.

theorem Algsuperdiff.Section3.Provider.MultiscaleEstimate.ten_le_of_window {epsilon Cms E : ℝ} (heps0 : 0 < epsilon) (heps : epsilon ≤ 1 / 2) (hCms : 4 ≤ Cms) (hfloor : 2 / 3 * epsilon ^ (-Cms) ≤ E) : 10 ≤ E

The manuscript's E ≥ 15 is not used anywhere in this module.

theorem Algsuperdiff.Section3.Provider.MultiscaleEstimate.abs_log_le_of_window {epsilon Cms E : ℝ} (heps0 : 0 < epsilon) (heps : epsilon ≤ 1 / 2) (hfloor : 2 / 3 * epsilon ^ (-Cms) ≤ E) : Cms * |Real.log epsilon| ≤ 3 / 2 * E

The logarithmic form of the window. ε^{-Cms} = exp(Cms |log ε|) and x + 1 ≤ exp x turn the window binder into a linear bound on |log ε|. This is the step the corridor budget of §5 runs on; the private badEventMultiscaleGates performs it inline in Provider/BadEvents/BadEventMultiscaleConsumption.lean, as hExpScale and hLinearExp (header census, item 3).

2. The constant-E gates

(ii) (vi). Both are instances of one of two shapes, and both are absorbed by the root's own c⋆⁻¹ ε^{-Cms} witness at a witness-choice constraint on Cms.

theorem Algsuperdiff.Section3.Provider.MultiscaleEstimate.relative_gate_le_of_window {cstarInv epsilon Cms E K : ℝ} (heps0 : 0 < epsilon) (heps : epsilon ≤ 1 / 2) (hCms : 0 ≤ Cms) (hcs : 0 ≤ cstarInv) (hK : K ≤ 2 ^ Cms) (hwin : cstarInv * epsilon ^ (-Cms) ≤ E) : K * cstarInv ≤ E

The relative gate. A demand of the shape K c⋆⁻¹ ≤ E — the shape of p.homogenization.step's 15 c⋆⁻¹ ≤ E and of l.shom.continuity's Cshom c⋆⁻¹ ≤ E — is discharged by the window as soon as the chosen witness satisfies K ≤ 2^{Cms}. No bound on c⋆ is needed on this branch.

theorem Algsuperdiff.Section3.Provider.MultiscaleEstimate.absolute_gate_le_of_window {epsilon Cms E K : ℝ} (heps0 : 0 < epsilon) (heps : epsilon ≤ 1 / 2) (hCms : 0 ≤ Cms) (hK : 3 / 2 * K ≤ 2 ^ Cms) (hfloor : 2 / 3 * epsilon ^ (-Cms) ≤ E) : K ≤ E

The absolute gate. A demand of the shape K ≤ E with K a constant of the model-free part of the argument — the shape of the coarse-graining gate exp(Ccg/(1/7)) ≤ E — is discharged by the window together with c⋆ ≤ 3/2, at the witness-choice constraint (3/2) K ≤ 2^{Cms}.

theorem Algsuperdiff.Section3.Provider.MultiscaleEstimate.fifteen_mul_cstar_inv_le_of_window {d : ℕ} (M : ABKModel d) {epsilon Cms E : ℝ} (heps0 : 0 < epsilon) (heps : epsilon ≤ 1 / 2) (hCms : 4 ≤ Cms) (hwin : (Disorder.cstar M)⁻¹ * epsilon ^ (-Cms) ≤ E) : 15 * (Disorder.cstar M)⁻¹ ≤ E

** (vi): 15 c⋆⁻¹ ≤ E.**

The honest route is 2^{Cms} ≥ 15, i.e. Cms ≥ 4: the demand is relative to c⋆⁻¹, exactly like the root's own window, so it needs no bound on c⋆ whatsoever. That route proves a different statement (10 ≤ E, delivered separately as ten_le_of_window) and does not by itself give 15 c⋆⁻¹ ≤ E when c⋆ is small; the 2^{Cms} ≥ 15 route does, uniformly in the model, and is the one taken.

theorem Algsuperdiff.Section3.Provider.MultiscaleEstimate.coarseGrainingGate_le_of_window {d : ℕ} (M : ABKModel d) {epsilon Cms E Ccg : ℝ} (heps0 : 0 < epsilon) (heps : epsilon ≤ 1 / 2) (hCms : 0 ≤ Cms) (hK : 3 / 2 * Real.exp (Ccg / (1 / 7)) ≤ 2 ^ Cms) (hwin : (Disorder.cstar M)⁻¹ * epsilon ^ (-Cms) ≤ E) : max (Real.exp (Ccg / (1 / 7))) (Disorder.cstar M)⁻¹ ≤ E

** (ii), first gate: exp(Ccg/(1/7)) ≤ E.**

The coarse-graining gate of the frozen coarse_ellipticity_bounds at σ = 1/7, in the max spelling the proved exists_crude_bound consumes. Its second entry c⋆⁻¹ ≤ E is free from the window at Cms ≥ 0; the first is the absolute gate at the witness-choice constraint (3/2) exp(7 Ccg) ≤ 2^{Cms}.

theorem Algsuperdiff.Section3.Provider.MultiscaleEstimate.shomGate_le_of_window {d : ℕ} (M : ABKModel d) {epsilon Cms E Cshom : ℝ} (heps0 : 0 < epsilon) (heps : epsilon ≤ 1 / 2) (hCms : 0 ≤ Cms) (hK : Cshom ≤ 2 ^ Cms) (hwin : (Disorder.cstar M)⁻¹ * epsilon ^ (-Cms) ≤ E) : Cshom * (Disorder.cstar M)⁻¹ ≤ E

** (ii), second gate: Cshom c⋆⁻¹ ≤ E.**

The gauge-conversion gate of l.shom.continuity, at the witness-choice constraint Cshom ≤ 2^{Cms}.

3. The γ-ceilings

Every E-floor of §2 becomes a γ-ceiling through the root's own second scalar binder γ ≤ (E⁻¹)^{10}.

theorem Algsuperdiff.Section3.Provider.MultiscaleEstimate.chom_le_pow_mul_sq_of_window {epsilon Cms E Chom : ℝ} (heps0 : 0 < epsilon) (heps : epsilon ≤ 1 / 2) (hCms : 4 ≤ Cms) (hChom : Chom ≤ 2 ^ Cms) (hfloor : 2 / 3 * epsilon ^ (-Cms) ≤ E) : Chom ≤ E ^ 8 * epsilon ^ 2

The arithmetic core of the ε² smallness gate: the window forces Chom ≤ E^8 ε^2 at the witness-choice constraints 4 ≤ Cms, Chom ≤ 2^{Cms}.

The margin is enormous and entirely explicit: E^8 ε^2 ≥ (2/3)^8 2^{8Cms-2}, while the constraint only asks Chom ≤ 2^{Cms}, so the slack is the factor (2/3)^8 2^{7Cms-2} ≥ (256/6561)·2^{26} > 2.6·10^6 at Cms = 4.

theorem Algsuperdiff.Section3.Provider.MultiscaleEstimate.gamma_le_gate_of_pow {epsilon E Chom gamma : ℝ} (hChom0 : 0 < Chom) (hEpos : 0 < E) (hgate : Chom ≤ E ^ 8 * epsilon ^ 2) (hgamma : gamma ≤ E⁻¹ ^ 10) : gamma ≤ Chom⁻¹ * E⁻¹ ^ 2 * epsilon ^ 2

The ε² smallness gate in the consumer's spelling, over plain reals.

5. The corridor cutoff h := waveCutoff (2 Chom) ε

: the manuscript sets h := C|log ε|, which is not an integer, and the localization lemma needs h ∈ ℕ. The proved integer cutoff is waveCutoff C₀ ε = ⌈C₀ |log ε|⌉₊ (WaveSizesZeroth.lean); the development's instantiation is C₀ := 2 Chom, the doubling being the ε²-route cost of development decision D2.

theorem Algsuperdiff.Section3.Provider.MultiscaleEstimate.one_le_waveCutoff {C0 epsilon : ℝ} (hC0 : 0 < C0) (heps0 : 0 < epsilon) (heps : epsilon ≤ 1 / 2) : 1 ≤ waveCutoff C0 epsilon

1 ≤ h at the development's own cutoff. The one new binder of BadEventSummed.exists_badEventSup_isBigOWith_gammaOne, whose printed window had to exclude h = 0, is at the instantiation: ε ≤ 1/2 makes |log ε| > 0, so the ceiling is at least one.

theorem Algsuperdiff.Section3.Provider.MultiscaleEstimate.le_waveCutoff (C0 epsilon : ℝ) : C0 * |Real.log epsilon| ≤ ↑(waveCutoff C0 epsilon)

** (v): the corridor budget.** The integer cutoff is at least the printed real one, so h ≥ C₀ |log ε| — at the development's C₀ := 2 Chom this is exactly the corridor h ≥ 2 Chom |log ε| that the ε²-route endpoints of HomogenizationInput require.

theorem Algsuperdiff.Section3.Provider.MultiscaleEstimate.waveCutoff_le_add_one {C0 epsilon : ℝ} (hC0 : 0 ≤ C0) : ↑(waveCutoff C0 epsilon) ≤ C0 * |Real.log epsilon| + 1

The ceiling overshoot, in the form the consumers' H-budget binder (h : ℝ) ≤ H |log ε| + 1 asks for: at H := C₀ the binder is an equality of shapes.

theorem Algsuperdiff.Section3.Provider.MultiscaleEstimate.gamma_mul_waveCutoff_le_one {epsilon Cms E gamma Chom : ℝ} (heps0 : 0 < epsilon) (heps : epsilon ≤ 1 / 2) (hCms : 4 ≤ Cms) (hChom0 : 0 ≤ Chom) (hChomCms : Chom ≤ Cms) (hfloor : 2 / 3 * epsilon ^ (-Cms) ≤ E) (hgamma : gamma ≤ E⁻¹ ^ 10) : gamma * ↑(waveCutoff (2 * Chom) epsilon) ≤ 1

** (i): γ h ≤ 1.**

The printed window of l.localization.mathcalE and the collapse hypothesis of the proved AggregationRemainder both carry γ h ≤ 1; the aggregation record booked its discharge to this module. Route: the logarithmic window (abs_log_le_of_window) bounds |log ε| by (3/2) E / Cms, the ceiling costs one, and Chom ≤ Cms turns the result into h ≤ 3E + 1, which γ ≤ E^{-10} crushes at E ≥ 10 with nine orders of magnitude to spare.

The witness-choice constraint Chom ≤ Cms is the whole of what the corridor costs; exists_parameterWeb_general meets it, at a Chom, hence also at the enlarged max Chom 10^9.

theorem Algsuperdiff.Section3.Provider.MultiscaleEstimate.three_rpow_five_waveCutoff_le {C0 epsilon : ℝ} (hC0 : 0 ≤ C0) (heps0 : 0 < epsilon) (heps : epsilon ≤ 1 / 2) : 3 ^ (5 * ↑(waveCutoff C0 epsilon)) ≤ epsilon ^ (-(5 * C0 * Real.log 3 + 8))

** (vi): 3^{5h} ≤ ε^{-C} with C explicit.**

The absorption at the integer cutoff, in the exact rpow spelling `(3: ℝ) ^ (5

• (h: ℝ)) that the proved bad-event amplitudes carry (BadEventIngredients.lean, BadEventSummed.lean`). The output constant is

C(C₀) = 5 C₀ log 3 + 8 ,

explicit in the cutoff constant C₀, hence explicit in Chom at the development's C₀ := 2 Chom. The +8 is the ceiling overshoot: ⌈x⌉ < x + 1 leaves the factor 3^5 = 243, which ε ≤ 1/2 absorbs into ε^{-8} because 2^8 = 256 ≥ 243. The proved private twin at exponent 8 (three_pow_eight_cutoff_le in WaveSizesZeroth.lean) leaves its 6561 standing in front instead.

theorem Algsuperdiff.Section3.Provider.MultiscaleEstimate.window_of_le {cstarInv epsilon Cms Cms' E : ℝ} (heps0 : 0 < epsilon) (heps1 : epsilon ≤ 1) (hcs : 0 ≤ cstarInv) (hle : Cms ≤ Cms') (hwin : cstarInv * epsilon ^ (-Cms') ≤ E) : cstarInv * epsilon ^ (-Cms) ≤ E

The window binder transfers to any larger witness. If the window holds at Cms' and Cms ≤ Cms', it holds at Cms. This is the direction the enlargement needs: assuming the strong hypothesis at max Cms 1, one may still apply the root at Cms.

7. The almost-everywhere to pointwise witness bridge

((iii))

Probability.IsTwoTermBigOWithWitnesses demands the domination `∀ ω, X ω ≤ Y ω

• Z ω` pointwise, while every Section 3 identification of an observable with an analytic quantity is only almost everywhere (the observables are measurable representatives).

The proved witness upgrade Provider.Tail.isTwoTermBigOWith_of_ae_le (Provider/Tail/TailSqrt.lean) delivers the existential IsTwoTermBigOWith and forgets the modified witnesses. The frozen multiscale conclusion is not of that shape: its second conjunct is an IsBigOWith clause on the same Y that the first conjunct names, so the upgrade must return witnesses whose relation to the given ones is known. The statement below returns exactly that — the modified pair is almost everywhere equal to the given pair — from which every tail of the original witnesses transfers by the proved Provider.Tail.isBigOWith_of_ae_eq. In particular the refinement clause survives the modification with no extra hypothesis.

The construction is the proved one (modify on the measurable null set where the inequality fails, sending the failure into the Z-slot); the two tail transfers Provider.Tail.isBigOWith_of_ae_eq. IsFiniteMeasure is NOT required.

theorem Algsuperdiff.Section3.Provider.MultiscaleEstimate.exists_witnesses_ae_eq_of_ae_le {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} {Ψ₁ Ψ₂ : ℝ → ℝ} {X Y Z : Ω → ℝ} {A₁ A₂ : ℝ} (hΨ₁ : Probability.IsAdmissibleTail Ψ₁) (hΨ₂ : Probability.IsAdmissibleTail Ψ₂) (hA₁ : 0 < A₁) (hA₂ : 0 < A₂) (hX : Measurable X) (hY : Measurable Y) (hZ : Measurable Z) (hle : ∀ᵐ (ω : Ω) ∂μ, X ω ≤ Y ω + Z ω) (hYt : HCPolySupport.IndependentSums.IsBigOWith μ Ψ₁ Y A₁) (hZt : HCPolySupport.IndependentSums.IsBigOWith μ Ψ₂ Z A₂) : ∃ (Y' : Ω → ℝ) (Z' : Ω → ℝ), Probability.IsTwoTermBigOWithWitnesses μ Ψ₁ Ψ₂ X Y' Z' A₁ A₂ ∧ Y' =ᵐ[μ] Y ∧ Z' =ᵐ[μ] Z

The witness upgrade with its witnesses named. See the section docstring.

8. Feasibility of the witness choice

Every constraint the web places on Cms is a constraint on the existential witness of the conclusion, chosen after the homogenization constant Chom is in hand (development decision D4).

exists_parameterWeb_general is the theorem with Chom a free binder, which is what makes the enlarged witness max Chom 10^9's addendum a genuine instantiation rather than a wish.

theorem Algsuperdiff.Section3.Provider.MultiscaleEstimate.two_rpow_log_div_log_two {K : ℝ} (hK : 0 < K) : 2 ^ (Real.log K / Real.log 2) = K

2 ^ (log K / log 2) = K for K > 0; the base-2 logarithm written out, so that §8's witness needs no Real.logb in its statement.

The proof below therefore the Mathlib lemma rather than re-deriving it, and this statement is retained only as the log/log spelling in which the witness of exists_parameterWeb_general is written. Any future base-2 site must consume Real.rpow_logb directly.

theorem Algsuperdiff.Section3.Provider.MultiscaleEstimate.exists_parameterWeb_general (Chom Cwin Ccg Cshom : ℝ) : ∃ (Cms : ℝ), 0 < Cms ∧ 1 ≤ Cms ∧ 4 ≤ Cms ∧ Chom ≤ Cms ∧ Cwin ≤ Cms ∧ 10 * Chom * Real.log 3 + 8 ≤ Cms ∧ Chom ≤ 2 ^ Cms ∧ 3 / 2 * Real.exp (Ccg / (1 / 7)) ≤ 2 ^ Cms ∧ Cshom ≤ 2 ^ Cms ∧ 15 ≤ 2 ^ Cms

The parameter web is feasible, at every Chom. For every real homogenization constant Chom, every window exponent Cwin that a consumer carries in its own existential, and every pair of development constants Ccg, Cshom, there is a witness Cms meeting all constraints the dischargers of §2-§6 impose at once:

• 4 ≤ Cms — the E ≥ 10 floor, the 15 ≤ 2^{Cms} gate and the ε² gate;
• Chom ≤ Cms — the corridor budget γ h ≤ 1 (gamma_mul_waveCutoff_le_one);
• Cwin ≤ Cms — the transfer of the root's window, through window_of_le, to a consumer that carries its OWN existential window constant.
• Chom ≤ 2^{Cms} — the ε² smallness gate;
• (3/2) exp(Ccg/(1/7)) ≤ 2^{Cms} — the coarse-graining gate;
• Cshom ≤ 2^{Cms} — the l.shom.continuity gauge gate;
• 15 ≤ 2^{Cms} — the 15 c⋆⁻¹ ≤ E of p.homogenization.step ( Frozen/Section3/HomogenizationStep.lean).

The witness is explicit: the max of 4, of Chom, of Cwin, of the absorption exponent, and of the base-2 logarithm of the largest multiplicative constant in play. Only numerals already printed in the constraints occur.