BfaPerCube

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

p.bfA.multiscalebound per cube: the sup_L, and the Step-3 payload as an Orlicz split

ABK26 p.bfA.multiscalebound (statement) prints, for every n <= m-1 (e.slstar.multiscale),

  sup_{L in [m-1, infty) cap Z}  3^{-gamma(m-n)} shom_{m-1} |s^{-1}_{L,*}(cu_n)|
      <=  C + O_{Gamma_{(1-sigma)/2}}( exp(-c E^{-2} gamma^{-1}) ) .

This module provides the abstract supremum and Orlicz algebra used by a faithful local producer; it does not itself discharge the source-level per-cube estimate.

The four sub-deltas, and what this module does with each

1. The s_{L,*}^{-1} observable. The chain (ConclusionRoot.abs_blockVecDot_coarseBlockMatrix_originCube_le_payload_ae, the proved local branch at the concrete competitor) bounds the scalar quadratic form |<(p,q), bfA_L(cu_m)(p,q)>| at the framed loading, at the single cube cu_m. The per-cube display needs the operator norm |s^{-1}_{L,*}(z + cu_n)| = matrixNorm (sigmaStarInvCoarse ...) at every descendant. BfaObservableNorm.lean supplies the conditional quadratic-form-to-operator-norm implication. Producing its pure-loading premise simultaneously in the loading and transporting the conclusion to each translated descendant remain open analytic work.
2. The hsep tail conversion. This is available at the base case, in HsepReduction.three_rpow_gamma_hsep_le_two_add_orlicz (the replacement route; the printed middle expression is false). What is not proved is the rest of the Step-3 right-hand side: the collar power 3^{2b hsep} multiplying the improved exponential, and the sum of the two resulting lanes at one exponent.
3. The sup_{L >= m-1}. Sections 1 and 3 prove the abstract carrier equivalence: once a faithful per-cube bound is available for every L with an L-free right-hand side, the canonical majorant is that right-hand side, and the forall L reading implies the printed sSup bound. This algebra does not prove the per-cube source premise, so it closes no source node.
4. This module neither proves nor removes them.

What is NOT proved here

• The Step-3 payoff at a descendant is only almost-everywhere and conditional, and its random separation scale is local: at R it is evaluated at R.scale on the translated sample. BfaLocalLane.lean records that exact interface. The former root/pathwise specialization in this file was rejected because it replaced that obligation by one root random variable and a pointwise forall omega; it has been removed.
• The final numerical comparison "bfaLaneScale <= exp(-c E^{-2} gamma^{-1})" is not performed here. ProfileConstants.lean proves the sound elementary comparisons and now also instantiates the _of_gates local-grid lane from the frozen maximum and fifth-root bounds. This file alone neither selects the final profile constants nor closes the remaining analytic payoff.
• The collar. e.slstar.multiscale carries 3^{-gamma(m-n)} on its L, while the proved payload carrier cutoffSigmaStarInvBlockFamily does not. At n = m-1-k the collar is 3^{gamma(k+1)} on the right, i.e. k-dependent, and BlockPayload's Cdet and A slots are scalars. The only route is to absorb the collar into the exponent, rho -> rho - gamma, which is what the conditional arithmetic of ProfileClose.lean does (foldedBlockPole_le_of_window). PayloadSandwich.blockGridSup_const_mul gives that arithmetic the exact factorization it needs, but no theorem here supplies its analytic premise.

References

• ABK26, p.bfA.multiscalebound; e.slstar.multiscale; e.bL.multiscale; Step 3 and its conclusion (the deterministic conclusion, the hsep conversion, the b_L display).
• ABK26, e.hsep.tails, e.indc.O.sigma, l.maximums.Gamma.s / e.maxy.bound.
• Provider/Multiscale/HsepReduction.lean (sub-delta 2, proved at base), Provider/Multiscale/ConclusionArithmetic.lean (three_rpow_le_two_add_indicator), Provider/Percolation/MinimalScaleSeparation.lean (hsep, e.hsep.tails), Provider/Multiscale/WaveOscillations.lean (measurableSet_lt_hsep), Provider/CoarseEllipticity/PayloadSandwich.lean (the hLunif slot), Provider/CoarseEllipticity/BlockPayload.lean (the hblock / hblockO slots).

1. The printed sup_{L in [m-1,infty) cap Z}

e.slstar.multiscale prints a supremum over the cutoff ray on the L of an L-free right-hand side. The proved consumers instead take the forall L form (hLunif plus hblock). The two lemmas below prove that this is not a weakening: the forall L form implies the printed sSup bound (raySup_le_of_forall), and conversely the elements of the ray are dominated by the sSup as soon as the ray is bounded above at all (le_raySup), which the forall L form itself supplies. Nothing anywhere in this file introduces an unbounded supremum: Lean's sSup of an unbounded set is a junk value, and the only direction used downstream is the one that needs no boundedness.

2. The two per-cube payload families

3. The sup_L collapse: hLunif and hblock from one forall L bound

hLunif asks for an L-free family Xc dominating the per-cube datum at every cutoff index; hblock asks that same Xc to obey |Xc| <= Cdet + U. The source supplies both at once, because the right-hand side it prints is already L-free: take Xc to BE that right-hand side. hblock then becomes abs_of_nonneg and the entire content is the forall L bound.

4. Measurability of the hsep-driven observables

Every lane below is a fixed function of the integer hsep, so a single measurability statement covers all of them. Percolation.MinimalScaleSeparation leaves this to the consumer and WaveOscillations.measurableSet_lt_hsep supplies the only input needed.

theorem Algsuperdiff.Section3.Provider.Multiscale.measurable_comp_hsep {d : ℕ} (M : ABKModel d) (m : ℤ) (E b : ℝ) (g : ℕ → ℝ) : Measurable fun (omega : Cutoff.CutoffSample d) => g (Percolation.hsep M m E b omega)

Any postcomposition of hsep is measurable: ℕ is countable.

5. The Step-3 payload as a constant plus one Orlicz lane

The Step-3 conclusion, in its replacement shape, is Cpre * (3^{gamma hsep} (1 + 3^{2b hsep} eps)). Expanding, this is Cpre * 3^{gamma hsep} + Cpre eps * 3^{(gamma+2b) hsep}. The first summand is the truncated prefactor, handled by HsepReduction; the second is a pure power of 3^{hsep}, handled by the e.powerofGammasigma power rule. The free indicator exponent is fixed so that both lanes land at one exponent, and that exponent is the manuscript's relabelled sigma.

noncomputable def Algsuperdiff.Section3.Provider.Multiscale.bfaPower (gam b : ℝ) : ℝ

The power p = (gamma + 2b)/b: the exponent to which e.hsep.tails (which controls 3^{b hsep}) must be raised to control 3^{(gamma+2b) hsep}.

Equations

• Algsuperdiff.Section3.Provider.Multiscale.bfaPower gam b = (gam + 2 * b) / b

noncomputable def Algsuperdiff.Section3.Provider.Multiscale.bfaSigmaTwo (sigma gam b : ℝ) : ℝ

The choice of e.indc.O.sigma's free exponent, the unique one making the two lanes coincide.

Equations

• Algsuperdiff.Section3.Provider.Multiscale.bfaSigmaTwo sigma gam b = (1 - sigma) / (Algsuperdiff.Section3.Provider.Multiscale.bfaPower gam b - 1)

noncomputable def Algsuperdiff.Section3.Provider.Multiscale.bfaTau (sigma gam b : ℝ) : ℝ

The common exponent of the two lanes, tau = (1-sigma) b / (gamma + 2b).

Equations

• Algsuperdiff.Section3.Provider.Multiscale.bfaTau sigma gam b = (1 - sigma) / Algsuperdiff.Section3.Provider.Multiscale.bfaPower gam b

theorem Algsuperdiff.Section3.Provider.Multiscale.one_lt_bfaPower {gam b : ℝ} (hgam : 0 < gam) (hb : 0 < b) : 1 < bfaPower gam b

theorem Algsuperdiff.Section3.Provider.Multiscale.two_le_bfaPower {gam b : ℝ} (hgam : 0 ≤ gam) (hb : 0 < b) : 2 ≤ bfaPower gam b

p >= 2 always, so the relabelling genuinely weakens the exponent.

theorem Algsuperdiff.Section3.Provider.Multiscale.bfaPower_pos {gam b : ℝ} (hgam : 0 < gam) (hb : 0 < b) : 0 < bfaPower gam b

theorem Algsuperdiff.Section3.Provider.Multiscale.bfaSigmaTwo_pos {sigma gam b : ℝ} (hsigma : sigma < 1) (hgam : 0 < gam) (hb : 0 < b) : 0 < bfaSigmaTwo sigma gam b

theorem Algsuperdiff.Section3.Provider.Multiscale.bfaTau_pos {sigma gam b : ℝ} (hsigma : sigma < 1) (hgam : 0 < gam) (hb : 0 < b) : 0 < bfaTau sigma gam b

theorem Algsuperdiff.Section3.Provider.Multiscale.prodSigma_bfaSigmaTwo_eq_bfaTau {sigma gam b : ℝ} (hsigma : sigma < 1) (hgam : 0 < gam) (hb : 0 < b) : (1 - sigma) * bfaSigmaTwo sigma gam b / (1 - sigma + bfaSigmaTwo sigma gam b) = bfaTau sigma gam b

** +: the two lanes coincide.** With sigma_2 chosen as bfaSigmaTwo, e.multGammasig's product exponent (1-sigma) sigma_2/((1-sigma)+sigma_2) equals the power lane's (1-sigma)/p.

noncomputable def Algsuperdiff.Section3.Provider.Multiscale.slstarCollapseTerm {d : ℕ} (M : ABKModel d) (m : ℤ) (E b gam : ℝ) (omega : Cutoff.CutoffSample d) : ℝ

The truncated prefactor, 3^{gamma hsep} 1_{gamma hsep > 3^{-4}}.

Equations

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

noncomputable def Algsuperdiff.Section3.Provider.Multiscale.slstarPowerTerm {d : ℕ} (M : ABKModel d) (m : ℤ) (E b gam : ℝ) (omega : Cutoff.CutoffSample d) : ℝ

The collar power 3^{(gamma+2b) hsep} carried by the improved exponential.

Equations

• Algsuperdiff.Section3.Provider.Multiscale.slstarPowerTerm M m E b gam omega = 3 ^ ((gam + 2 * b) * ↑(Algsuperdiff.Section3.Provider.Percolation.hsep M m E b omega))

noncomputable def Algsuperdiff.Section3.Provider.Multiscale.bfaLane {d : ℕ} (M : ABKModel d) (m : ℤ) (E b gam Cpre eps : ℝ) (omega : Cutoff.CutoffSample d) : ℝ

The Orlicz lane of e.slstar.multiscale: the whole random part of the Step-3 right-hand side.

Equations

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

theorem Algsuperdiff.Section3.Provider.Multiscale.slstarCollapseTerm_nonneg {d : ℕ} (M : ABKModel d) (m : ℤ) (E b gam : ℝ) (omega : Cutoff.CutoffSample d) : 0 ≤ slstarCollapseTerm M m E b gam omega

theorem Algsuperdiff.Section3.Provider.Multiscale.slstarPowerTerm_nonneg {d : ℕ} (M : ABKModel d) (m : ℤ) (E b gam : ℝ) (omega : Cutoff.CutoffSample d) : 0 ≤ slstarPowerTerm M m E b gam omega

theorem Algsuperdiff.Section3.Provider.Multiscale.bfaLane_nonneg {d : ℕ} (M : ABKModel d) (m : ℤ) {E b gam Cpre eps : ℝ} (hCpre : 0 ≤ Cpre) (heps : 0 ≤ eps) (omega : Cutoff.CutoffSample d) : 0 ≤ bfaLane M m E b gam Cpre eps omega

theorem Algsuperdiff.Section3.Provider.Multiscale.measurable_bfaLane {d : ℕ} (M : ABKModel d) (m : ℤ) (E b gam Cpre eps : ℝ) : Measurable (bfaLane M m E b gam Cpre eps)

theorem Algsuperdiff.Section3.Provider.Multiscale.step3Payload_le_two_mul_add_bfaLane {d : ℕ} (M : ABKModel d) (m : ℤ) {E b gam Cpre eps : ℝ} (hgam : 0 ≤ gam) (hCpre : 0 ≤ Cpre) (omega : Cutoff.CutoffSample d) : Cpre * (3 ^ (gam * ↑(Percolation.hsep M m E b omega)) * (1 + 3 ^ (2 * b * ↑(Percolation.hsep M m E b omega)) * eps)) ≤ 2 * Cpre + bfaLane M m E b gam Cpre eps omega

The Step-3 payload split into a constant and the lane (the replacement deterministic step, times the collar power).

theorem Algsuperdiff.Section3.Provider.Multiscale.isBigOWith_gammaSigma_slstarPowerTerm_of_gates {d : ℕ} (M : ABKModel d) {m : ℤ} {E sigma b gam : ℝ} (hd : 2 ≤ d) (hE : 1 ≤ E) (hS : Frozen.Section3.inductionState M (m - 1) ⟨E, hE⟩) (hsigma0 : 0 < sigma) (hsigma : sigma ≤ 1 / 2) (hb0 : 0 < b) (hb1 : b ≤ 1 / 8) (hEexp : Real.exp (Percolation.badClustersConst d / sigma) ≤ E) (hE4 : 4 ≤ E) (hunit : BadEvents.unitGate M) (hgamma20 : M.gamma ≤ 1 / 20) (hinvSq : E⁻¹ ^ 2 ≤ Disorder.cstar M) (hEb : Percolation.badClustersConst d / b ≤ E) (hgammaE : M.gamma ≤ E ^ (-5)) (hgam : 0 < gam) : HCPolySupport.IndependentSums.IsBigOWith (↑(Cutoff.cutoffSampleLaw M)) (HCPolySupport.IndependentSums.gammaSigma (bfaTau sigma gam b)) (slstarPowerTerm M m E b gam) (Percolation.hsepAmplitude sigma b ^ bfaPower gam b)

The collar power at Gamma_{(1-sigma)/p}'s power route: e.hsep.tails controls 3^{b hsep} at Gamma_{1-sigma} and amplitude hsepAmplitude sigma b; raising to p = (gamma+2b)/b gives the collar power.

noncomputable def Algsuperdiff.Section3.Provider.Multiscale.bfaLaneScale (sigma b gam Cpre eps : ℝ) : ℝ

The explicit scale of the Orlicz lane: e.multGammasig's constant times e.hsep.tails' amplitude times e.indc.O.sigma's exp(-c gamma^{-1})-sized scale, plus eps times the collar power's amplitude, all through the two-term l.Gamma.sigma.triangle.

Equations

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

theorem Algsuperdiff.Section3.Provider.Multiscale.bfaLaneScale_pos {sigma b gam Cpre eps : ℝ} (hCpre : 0 < Cpre) (heps : 0 < eps) : 0 < bfaLaneScale sigma b gam Cpre eps

The lane's scale is positive, as the consumers' hA slot requires.

theorem Algsuperdiff.Section3.Provider.Multiscale.isBigOWith_gammaSigma_bfaLane_of_gates {d : ℕ} (M : ABKModel d) {m : ℤ} {E sigma b gam Cpre eps : ℝ} (hd : 2 ≤ d) (hE : 1 ≤ E) (hS : Frozen.Section3.inductionState M (m - 1) ⟨E, hE⟩) (hsigma0 : 0 < sigma) (hsigma : sigma ≤ 1 / 2) (hb0 : 0 < b) (hb1 : b ≤ 1 / 8) (hEexp : Real.exp (Percolation.badClustersConst d / sigma) ≤ E) (hE4 : 4 ≤ E) (hunit : BadEvents.unitGate M) (hgamma20 : M.gamma ≤ 1 / 20) (hinvSq : E⁻¹ ^ 2 ≤ Disorder.cstar M) (hEb : Percolation.badClustersConst d / b ≤ E) (hgammaE : M.gamma ≤ E ^ (-5)) (hgam : 0 < gam) (hgammab : gam ≤ b) (hCpre : 0 < Cpre) (heps : 0 < eps) : HCPolySupport.IndependentSums.IsBigOWith (↑(Cutoff.cutoffSampleLaw M)) (HCPolySupport.IndependentSums.gammaSigma (bfaTau sigma gam b)) (bfaLane M m E b gam Cpre eps) (bfaLaneScale sigma b gam Cpre eps)

The Orlicz lane of e.slstar.multiscale, at one exponent and an explicit scale. Both lanes are put at bfaTau --- the truncated prefactor by the product rule at sigma_2, the collar power by the power rule --- and added by the two-term l.Gamma.sigma.triangle. By bfaTau_eq_half_one_sub_bfaSigmaPrime this exponent is the printed Gamma_{(1-sigma')/2} at the relabelled sigma'.

6. Generic composed-leg adapters

The following theorems conditionally adapt explicitly supplied descendant-indexed estimates to the proved payload consumers. They discharge only the abstract majorant plumbing; they neither establish the source per-cube estimate nor reduce O1/O2 to a root hpay. The faithful local, almost-everywhere shape needed to produce such data is recorded separately in BfaLocalLane.lean.