UpperCollarBandMeanTunedAbsorption

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

Terminal absorption for the tuned collar band-mean root and depth trace

This file folds the exact untranslated source root and every translated strict depth into one block pole, then absorbs the deterministic tuned cap decay into the frozen exceptional scale. The depth coefficient is the internal choice siteRateBase d / 64; its floor, Step-3 ceiling, and large-parameter threshold are all derived from the existing final gate.

No mathematical premise is added to the caller surface. This remains an internal Provider theorem and makes no source-node or development-status claim.

theorem Algsuperdiff.Section3.Provider.Multiscale.k0_fourthRoot_collapse {b t : ℝ} (hb0 : 0 ≤ b) (hb18 : 18 * b ≤ 1) (ht : 0 ≤ t) : 3 ^ (2 * b * t) * √√(Real.exp (-t) + 3 ^ (-(t / 2))) ≤ 2 * Real.exp (-(t / 72))

The fourth-root form of the k₀ density collapse. Applying the existing square-root collapse at slope 2 * b gives the exact fourth root needed by the collar band-mean interpolation.

noncomputable def Algsuperdiff.Section3.Provider.CoarseEllipticity.collarBandMeanTunedCapPrefactor (d : ℕ) : ℝ

The dimension-only prefactor left after normalizing both cap branches.

Equations

• Algsuperdiff.Section3.Provider.CoarseEllipticity.collarBandMeanTunedCapPrefactor d = 2 * √√(9 * 99 ^ d)

noncomputable def Algsuperdiff.Section3.Provider.CoarseEllipticity.collarBandMeanTunedDecayRate (d : ℕ) : ℝ

The positive decay rate produced by the source-compatible depth choice.

Equations

• Algsuperdiff.Section3.Provider.CoarseEllipticity.collarBandMeanTunedDecayRate d = Algsuperdiff.Section3.Provider.CoarseEllipticity.collarBandMeanDepthCoeff d / 72

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.collarBandMeanTunedCapPrefactor_nonneg (d : ℕ) : 0 ≤ collarBandMeanTunedCapPrefactor d

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.collarBandMeanTunedDecayRate_pos (d : ℕ) : 0 < collarBandMeanTunedDecayRate d

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.probeSharpCollarBandMeanCapQuarter_le_normalized {d : ℕ} (M : ABKModel d) (E : ℝ) (k₀ : ℕ) (hk₀ : ↑k₀ ≤ Percolation.siteRateBase d / 2 * (E⁻¹ ^ 2 * M.gamma⁻¹)) : probeSharpCollarBandMeanCapQuarter M E k₀ ≤ √√(9 * 99 ^ d) * √√(Real.exp (-↑k₀) + 3 ^ (-(↑k₀ / 2)))

The Step-3 ceiling turns the first density branch into the same normalized k₀ expression as the geometric branch.

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.collarBandMeanDepthCoeff_mul_invSq_gammaInv_le_depth {d : ℕ} (M : ABKModel d) (E : ℝ) : collarBandMeanDepthCoeff d * (E⁻¹ ^ 2 * M.gamma⁻¹) ≤ ↑(collarBandMeanDepth M E)

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.probeSharpCollarBandMeanTunedCapGrowth_le_exp {d : ℕ} (M : ABKModel d) {E : ℝ} (hE : 0 < E) (hlarge : collarBandMeanDepthThreshold d ≤ E⁻¹ ^ 2 * M.gamma⁻¹) : probeSharpCollarBandMeanCapQuarter M E (collarBandMeanDepth M E) * 3 ^ (2 * bfaProfileB * ↑(collarBandMeanDepth M E)) ≤ collarBandMeanTunedCapPrefactor d * Real.exp (-(collarBandMeanTunedDecayRate d * (E⁻¹ ^ 2 * M.gamma⁻¹)))

The complete tuned cap-growth factor decays at a positive dimension-dependent rate. The large-parameter premise is exactly the internally defined threshold that pays the depth floor and ceiling error.

noncomputable def Algsuperdiff.Section3.Provider.CoarseEllipticity.collarBandMeanTunedLayerSumPrefactor (d : ℕ) : ℝ

Dimension-only cost after summing the exact tuned Whitney profile.

Equations

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

noncomputable def Algsuperdiff.Section3.Provider.CoarseEllipticity.collarBandMeanTunedTracePrefactor (d : ℕ) : ℝ

Dimension-only finite-trace prefactor after pricing the exact hsep power.

Equations

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

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.collarBandMeanTunedLayerSumPrefactor_nonneg {d : ℕ} (hd : 2 ≤ d) : 0 ≤ collarBandMeanTunedLayerSumPrefactor d

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.collarBandMeanTunedTracePrefactor_nonneg {d : ℕ} (hd : 2 ≤ d) : 0 ≤ collarBandMeanTunedTracePrefactor d

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.tsum_probeSharpCollarBandMeanTunedLayerScale_le_exp {d : ℕ} (hd : 2 ≤ d) (M : ABKModel d) {E : ℝ} (hE : 0 < E) (hlarge : collarBandMeanDepthThreshold d ≤ E⁻¹ ^ 2 * M.gamma⁻¹) : ∑' (n : ℕ), probeSharpCollarBandMeanTunedLayerScale M E n ≤ collarBandMeanTunedLayerSumPrefactor d * Real.exp (-(collarBandMeanTunedDecayRate d * (E⁻¹ ^ 2 * M.gamma⁻¹)))

The exact Whitney sum inherits the tuned exponential cap decay.

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.probeSharpCollarBandMeanTunedPowerScale_le_profileCube {d : ℕ} (M : ABKModel d) {sigma : ℝ} (hsigma0 : 0 < sigma) (hsigma : sigma ≤ 1 / 2) (hgammaB : M.gamma ≤ bfaProfileB) : probeSharpCollarBandMeanTunedPowerScale M sigma ≤ superposedFluxHsepConst ^ 3

The exact hsep-power scale is bounded by a universal cube once the auxiliary frozen gates imply gamma ≤ bfaProfileB.

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.probeSharpCollarBandMeanTunedTraceScale_le_exp {d : ℕ} (hd : 2 ≤ d) (M : ABKModel d) {E sigma : ℝ} (hE : 0 < E) (hsigma0 : 0 < sigma) (hsigma : sigma ≤ 1 / 2) (hgammaB : M.gamma ≤ bfaProfileB) (hlarge : collarBandMeanDepthThreshold d ≤ E⁻¹ ^ 2 * M.gamma⁻¹) : probeSharpCollarBandMeanTunedTraceScale d M E sigma ≤ collarBandMeanTunedTracePrefactor d * Real.exp (-(collarBandMeanTunedDecayRate d * (E⁻¹ ^ 2 * M.gamma⁻¹)))

The exact strict-row finite trace has a dimension-only prefactor times the tuned exponential decay.

noncomputable def Algsuperdiff.Section3.Provider.CoarseEllipticity.collarBandMeanTunedFrozenPrefactor (d : ℕ) : ℝ

Dimension-only prefactor in the terminal folded-pole gate.

Equations

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

noncomputable def Algsuperdiff.Section3.Provider.CoarseEllipticity.collarBandMeanTunedOutputConst (d : ℕ) : ℝ

Dimension-only threshold paying the depth floor, ceiling error, fixed prefactor, and reciprocal tuned decay rate.

Equations

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

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.collarBandMeanTunedFrozenPrefactor_nonneg {d : ℕ} (hd : 2 ≤ d) : 0 ≤ collarBandMeanTunedFrozenPrefactor d

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.collarBandMeanTunedOutputConst_pos {d : ℕ} (hd : 2 ≤ d) : 0 < collarBandMeanTunedOutputConst d

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.collarBandMeanDepthThreshold_le_outputConst (d : ℕ) : collarBandMeanDepthThreshold d ≤ collarBandMeanTunedOutputConst d

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.isBigOWith_upperProfileTarget_probeSharpFramedCollarBandMeanTunedTraceLane_frozenReserve {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 Cup : ℝ} (hsigma0 : 0 < sigma) (hsigma : sigma ≤ 1 / 2) (hmax : max (Real.exp (Cup / sigma)) (Disorder.cstar M)⁻¹ ≤ ↑E) (hEgamma : ↑E ≤ M.gamma ^ (-(1 / 5))) (hCup : max (profileAuxiliaryConst d) (collarBandMeanTunedOutputConst d) ≤ Cup) : have eps := Real.exp (-(Cup⁻¹ * ((↑E)⁻¹ ^ 2 * M.gamma⁻¹))); HCPolySupport.IndependentSums.IsBigOWith (↑(Cutoff.cutoffSampleLaw M)) (HCPolySupport.IndependentSums.gammaSigma (upperProfileTargetSigma sigma)) (probeSharpFramedCollarBandMeanTunedTraceLane M m R ↑E) (3 ^ (M.gamma * (↑k + 1)) * eps ^ 8)

Direct per-descendant collar band-mean trace at the eighth-power reserve.