SharpFramedAfterBandOrlicz

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

Orlicz split for the actual framed after-band square

This file applies the upper-profile separation split to the literal after-band-square summand in one sharp Whitney layer. It treats only the normalized inner good-mass branch, before multiplication by probeMeanGoodWaveConst M * vecNormSq p. The collar contribution, wave head, band mean, deep-band tail, and wave tail are all excluded. The explicit rare scale is retained without a uniform exponential weakening.

The final two lane facts use the bounded product A directly at the explicit witnesses ordinaryLane = 2 * X and rareLane = R * X; no choice witness is introduced.

The declarations below are internal Provider helpers.

Literal carriers

noncomputable def Algsuperdiff.Section3.Provider.Multiscale.probeSharpAfterBandDescendantOffset {d : ℕ} (M : ABKModel d) (E : ℝ) (k n : ℕ) : ℝ

The deterministic depth removed from the descendant frame.

Equations

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

noncomputable def Algsuperdiff.Section3.Provider.Multiscale.probeSharpAfterBandGoodMassCoeff (d n : ℕ) : ℝ

The coefficient of the normalized good-mass after-band square before the random frame is applied.

Equations

• Algsuperdiff.Section3.Provider.Multiscale.probeSharpAfterBandGoodMassCoeff d n = 5 * ↑d ^ 2 * √(Algsuperdiff.Section3.Provider.Multiscale.probeSharpLayerMassEnvelope d n)

noncomputable def Algsuperdiff.Section3.Provider.Multiscale.probeSharpAfterBandHsepFactor {d : ℕ} (M : ABKModel d) (root : ℤ) (E : ℝ) (omega : Cutoff.CutoffSample d) : ℝ

The 3^{gamma hsep} factor singled out for the split.

Equations

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

noncomputable def Algsuperdiff.Section3.Provider.Multiscale.probeSharpAfterBandHsepResidual {d : ℕ} (M : ABKModel d) (root : ℤ) (E : ℝ) (omega : Cutoff.CutoffSample d) : ℝ

The truncated random residual in the split.

Equations

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

noncomputable def Algsuperdiff.Section3.Provider.Multiscale.probeSharpAfterBandBaseGoodMassScale {d : ℕ} (M : ABKModel d) (root m : ℤ) (E : ℝ) (k n : ℕ) : ℝ

The exact Gamma_1 scale of the unframed factor.

Equations

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

noncomputable def Algsuperdiff.Section3.Provider.Multiscale.probeSharpAfterBandRareGoodMassScale {d : ℕ} (M : ABKModel d) (root m : ℤ) (E sigma : ℝ) (k n : ℕ) : ℝ

Exact rare-lane scale. In particular the full hsep residual amplitude is visible and has not been replaced by a uniform exponential envelope.

Equations

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

theorem Algsuperdiff.Section3.Provider.Multiscale.probeSharpAfterBandGoodMassCoeff_nonneg (d n : ℕ) : 0 ≤ probeSharpAfterBandGoodMassCoeff d n

theorem Algsuperdiff.Section3.Provider.Multiscale.probeSharpAfterBandHsepResidual_nonneg {d : ℕ} (M : ABKModel d) (root : ℤ) (E : ℝ) (omega : Cutoff.CutoffSample d) : 0 ≤ probeSharpAfterBandHsepResidual M root E omega

theorem Algsuperdiff.Section3.Provider.Multiscale.measurable_probeSharpAfterBandHsepResidual {d : ℕ} (M : ABKModel d) (root : ℤ) (E : ℝ) : Measurable (probeSharpAfterBandHsepResidual M root E)

theorem Algsuperdiff.Section3.Provider.Multiscale.probeSharpAfterBandBaseGoodMassScale_nonneg {d : ℕ} (M : ABKModel d) (root m : ℤ) (E : ℝ) (k n : ℕ) : 0 ≤ probeSharpAfterBandBaseGoodMassScale M root m E k n

Descendant identities and the exact Gamma_1 input

theorem Algsuperdiff.Section3.Provider.Multiscale.probeSharpAfterBandBaseGoodMassScale_eq_profileHalf {d : ℕ} (M : ABKModel d) {m : ℤ} {k : ℕ} {R : HCPolySupport.TriadicCube d} (hR : R ∈ HCPolySupport.descendantsAtScale (HCPolySupport.originCube d m) (m - 1 - ↑k)) (E : ℝ) (n : ℕ) : probeSharpAfterBandBaseGoodMassScale M R.scale m E k n = 5 * ↑d ^ 2 * waveSharpUpperConst d ^ 2 * √(probeSharpLayerMassEnvelope d n) * min 1 (M.gamma * (1 + ↑k + ↑n + ↑(bfaAfterBandLayerCeil n))) * 3 ^ (M.gamma * (2 + ↑k + ↑n + ↑(bfaAfterBandLayerCeil n) + ↑(CoarseEllipticity.waveBandDepth 1 E M.gamma)))

Exact descendant normalization of the unframed Gamma_1 scale.

theorem Algsuperdiff.Section3.Provider.Multiscale.two_mul_probeSharpAfterBandBaseGoodMassScale_eq_ordinary {d : ℕ} (M : ABKModel d) {m : ℤ} {k : ℕ} {R : HCPolySupport.TriadicCube d} (hR : R ∈ HCPolySupport.descendantsAtScale (HCPolySupport.originCube d m) (m - 1 - ↑k)) (E : ℝ) (n : ℕ) : 2 * probeSharpAfterBandBaseGoodMassScale M R.scale m E k n = probeSharpAfterBandOrdinaryGoodMassLayer M E k n

The deterministic lane scale returned by the generic split is exactly the verified ordinary layer scale.

Exact upper-profile hsep input

theorem Algsuperdiff.Section3.Provider.Multiscale.probeSharpAfterBandHsep_split_of_profileAuxiliaryMaxGate {d : ℕ} (M : ABKModel d) {m : ℤ} {k : ℕ} {R : HCPolySupport.TriadicCube d} (hR : R ∈ HCPolySupport.descendantsAtScale (HCPolySupport.originCube d m) (m - 1 - ↑k)) {E : { E : ℝ // 1 ≤ E }} (hS : Frozen.Section3.inductionState M (m - 1) E) {sigma : ℝ} (hsigma0 : 0 < sigma) (hsigma : sigma ≤ 1 / 2) (hmax : max (Real.exp (CoarseEllipticity.profileAuxiliaryConst d / sigma)) (Disorder.cstar M)⁻¹ ≤ ↑E) (hEgamma : ↑E ≤ M.gamma ^ (-(1 / 5))) : (∀ (omega : Cutoff.CutoffSample d), probeSharpAfterBandHsepFactor M R.scale (↑E) omega ≤ 2 + probeSharpAfterBandHsepResidual M R.scale (↑E) omega) ∧ HCPolySupport.IndependentSums.IsBigOWith (↑(Cutoff.cutoffSampleLaw M)) (HCPolySupport.IndependentSums.gammaSigma (CoarseEllipticity.upperProfileHsepTau sigma)) (probeSharpAfterBandHsepResidual M R.scale ↑E) (HCPolySupport.Book.Ch04.gammaProductConst (CoarseEllipticity.upperProfileBaseSigma sigma) (CoarseEllipticity.upperProfileHsepAuxSigma sigma) * Percolation.hsepAmplitude (CoarseEllipticity.upperProfileSigma sigma) CoarseEllipticity.bfaProfileB * truncationIndicatorScale CoarseEllipticity.bfaProfileB (CoarseEllipticity.upperProfileSigma sigma) (CoarseEllipticity.upperProfileHsepAuxSigma sigma) (Percolation.hsepAmplitude (CoarseEllipticity.upperProfileSigma sigma) CoarseEllipticity.bfaProfileB) ⌊(81 * M.gamma)⁻¹⌋₊)

The frozen profile gates instantiate HsepReduction at the upper-profile exponents. The residual scale is kept in its exact closed form.

Explicit ordinary and rare lanes