ConclusionKtotEnvelope

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

The Ktot pricing at the honest layer envelope

cubeSupBound □ □.scale L ω  ≤  (1+k)^{1/2} ρ_k A t ,
ρ_k = (3 max{1, log #𝒲(□_m,k)})^{1/2} ,   A = whitneyWaveCubeScale M L ,

on a set of outer measure at least 1 − 2 e^{−t²} (one_sub_le_measureReal_forall_cubeSupBound_le), while ConclusionKtot.goodCellForm_le_ktotConst_mul_layerQuantity_ae consumes a single real Swave. That module's "What is not proved" paragraph names the exact three-step local instantiation; this module performs it.

1. The logarithm of the proved layer-mass count

LayerMass.card_whitneyLayer_le is #𝒲(□_m,k) ≤ 2d (3^{d−1})^{k−1}(3^d)^{1+h_k}. Collapsing 2d ≤ 3^d (two_mul_le_three_pow, all d) puts it in the single power form #𝒲(□_m,k) ≤ 3^{d(2+k+h_k)} (card_whitneyLayer_le_pow), so

3 max{1, log #𝒲(□_m,k)}  ≤  whitneyLayerLogConst d . (1 + k + h_k) ,
whitneyLayerLogConst d = 3 (1 + 2 d log 3) ,

which is three_mul_max_one_log_card_whitneyLayer_le, and therefore ρ_k² ≤ C(d)(1 + k + h_k) (whitneyWaveLayerPenalty_sq_le). The route is the one already used for the covering family in Provider/Stream/LargeCubeLinfty.lean (three_mul_max_one_log_card_subcubeShifts_le, constant largeCubeLogConst); the empty layer k = 0 is covered because log 0 = 0 there.

2. The absorption, over abstract reals

The amplification (1+k) ρ_k² is polynomial while the payload of ConclusionCompetitor.toReal_tsum_simplexPartition_cutoff_two_leg_le_payload is geometric in k + h_k, so a polynomial-vs-exponential trade discharges this local pricing mismatch at an arbitrarily small exponent loss. The core is stated over abstract reals with the exponential kept as an atom A:

0 < c , 0 ≤ s , (1 + c s)² ≤ A   ⟹   (1 + s)² ≤ (1 + c⁻¹)² A ,

sq_one_add_le_mul, whose only content is 1 + s ≤ (1+c⁻¹)(1+cs) (one_add_le_mul). The atom is supplied once, at c = ε log 3 / 2, by sq_one_add_le_three_rpow ((1 + u)² ≤ (e^u)² = 3^{εs}), giving

(1+x)(1+x+y)  ≤  layerAbsorptionConst ε . 3^{ε(x+y)} ,
layerAbsorptionConst ε = (1 + 2 (ε log 3)^{-1})² ,

for all x, y ≥ 0 (one_add_mul_le_layerAbsorptionConst_mul). The constant is the honest one produced by that route; nothing here optimizes it.

3. The good leg at the raised exponent

Feeding the envelope Sc k = whitneyWaveLayerScale M m h k L . t makes the layer constant k-dependent through Sup² only, and steps 1--2 price exactly that dependence:

max{osc_m, Sc k}²  ≤  ktotEnvelopeSup M m L ε t² . 3^{ε(k+h_k)} ,
ktotEnvelopeSup M m L ε t
    = (osc_m² + C(d) C_ε (whitneyWaveCubeScale M L)² t²)^{1/2} ,

(sq_max_oscThreshold_whitneyWaveLayerScale_le), and ktotConst is affine in Sup² with nonnegative coefficients (ktotConst_le_mul), so the whole layer constant is at most ktotConst(ktotEnvelopeSup) . 3^{ε(k+h_k)} and the payload exponent rises from 2γ to 2γ + ε. goodCellForm_le_ktotEnvelopeConst_mul_layerQuantity_ae is the conclusion in the exact hgood binder body of ConclusionCompetitor.toReal_tsum_simplexPartition_cutoff_two_leg_le_payload at

Ktot := ktotConst M m i 3 (ktotEnvelopeSup M m L ε t) p q ,
γ    := 2 M.gamma + ε ,

and one_sub_le_measureReal_goodCellForm_le_ktotEnvelopeConst_mul discharges its envelope antecedent against ConclusionData's aggregation: the hgood body holds on a set of outer measure at least 1 − 2 (Γ₂ t)^{-1}.

The payload's remaining data at this Ktot are already proved elsewhere: hγ0: 0 ≤ 2 M.gamma + ε is immediate from M.shellPrefix.gamma_pos and ε > 0, and hK : 0 ≤ Ktot is ConclusionKtot.ktotConst_nonneg hd M m i (0 ≤ 3) _ p q. Neither is restated here, because nothing here invokes the payload.

Conditional consumer gate (audit-28 A2- pattern)

The payload's own window is hγ : 4 γ ≤ 1 − b (the layer-series summability condition of ConclusionAssembly, carried unchanged by LayerUniform.toReal_tsum_simplexPartition_two_leg_le_payload and by ConclusionCompetitor.toReal_tsum_simplexPartition_cutoff_two_leg_le_payload). At the instantiation above it reads

8 M.gamma + 4 ε  ≤  1 − b ,

which is NOT implied by the standing γ ≤ 1/4 gate and is NOT a binder of anything below (nothing here invokes the payload). It is the composer's gate, recorded here exactly as ConclusionKtot records its own 8 M.gamma ≤ 1 − b tightening: the factor 2 is the price of the squared-gauge pricing and the 4 ε is the price of this module's absorption. Both have wide room under the induction's own admissibility M.gamma ≤ E^{-5}, and ε is free, so the composer chooses ε after b; no statement below assumes any relation between ε, b and M.gamma.

What is not proved

• No constant Swave, and no claim that one exists: ConclusionData's analysis is unchanged and nothing here re-opens it. The envelope is carried as an antecedent of the almost-sure statements below; it is never replaced by a constant.
• The concluding assembly is NOT run. Nothing below invokes the concluding payload of ConclusionRoot; the parameter window above is recorded, not discharged, and the collar leg, the mass data and the hBadDens datum are untouched.
• No 3^{−3k/4} per-layer weight (blocks it, and the amplification is paid by the union bound of ConclusionData and by this module's ε, never by a layer weight).
• The constants are not optimized. whitneyLayerLogConst d = 3(1+2d log 3) and layerAbsorptionConst ε = (1 + 2(ε log 3)^{-1})² are the honest outputs of the two routes above; the manuscript's own C(d), C_ε are not claimed to be these.
• No new probabilistic input. The only almost-sure statement consumed is the base pricing ConclusionCompetitor.goodCellForm_le_stepOneLayerMajorant_ae; the layer envelope itself is carried as an antecedent rather than discharged here. No independence and no measurability of the good event is used or needed.

Main definitions

• Algsuperdiff.Section3.Provider.Multiscale.whitneyLayerLogConst
• Algsuperdiff.Section3.Provider.Multiscale.layerAbsorptionConst
• Algsuperdiff.Section3.Provider.Multiscale.ktotEnvelopeSup

Main results

• Algsuperdiff.Section3.Provider.Multiscale.three_mul_max_one_log_card_whitneyLayer_le
• Algsuperdiff.Section3.Provider.Multiscale.whitneyWaveLayerPenalty_sq_le
• Algsuperdiff.Section3.Provider.Multiscale.one_add_mul_le_layerAbsorptionConst_mul
• Algsuperdiff.Section3.Provider.Multiscale.sq_max_oscThreshold_whitneyWaveLayerScale_le
• Algsuperdiff.Section3.Provider.Multiscale.goodCellForm_le_ktotConst_mul_layerScale_ae
• Algsuperdiff.Section3.Provider.Multiscale. goodCellForm_le_ktotEnvelopeConst_mul_layerQuantity_ae

References

• ABK26, p.bfA.multiscalebound Step 1 (majorant) and Step 3; e.hn.def and e.hn.gap (label-line convention; the inequality prints on the following line; the printed reference is garbled); the Whitney layers; e.km.kn.Linfty; l.maximums.Gamma.s.
• Provider/Multiscale/ConclusionData.lean (the envelope and its aggregation), Provider/Multiscale/ConclusionKtot.lean (the pricing and ktotConst), Provider/Multiscale/LayerMass.lean (the layer count), Provider/Multiscale/ConclusionCompetitor.lean (the hgood consumer), Provider/Stream/LargeCubeLinfty.lean (the covering-count precedent).

Step 1: the logarithm of the proved layer count

theorem Algsuperdiff.Section3.Provider.Multiscale.two_mul_le_three_pow (d : ℕ) : 2 * d ≤ 3 ^ d

2 d ≤ 3^d, for every d.

theorem Algsuperdiff.Section3.Provider.Multiscale.card_whitneyLayer_le_pow {d : ℕ} (m : ℤ) (hn : ℕ → ℕ) (k : ℕ) : (Whitney.whitneyLayer m hn k).card ≤ 3 ^ (d * (2 + k + hn k))

The proved layer count in single-power form. LayerMass.card_whitneyLayer_le with 2d ≤ 3^d, 3^{d−1} ≤ 3^d and k − 1 ≤ k.

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

The log-cardinality constant of a Whitney layer, 3(1 + 2 d log 3).

Equations

• Algsuperdiff.Section3.Provider.Multiscale.whitneyLayerLogConst d = 3 * (1 + 2 * ↑d * Real.log 3)

theorem Algsuperdiff.Section3.Provider.Multiscale.whitneyLayerLogConst_pos (d : ℕ) : 0 < whitneyLayerLogConst d

theorem Algsuperdiff.Section3.Provider.Multiscale.three_mul_max_one_log_card_whitneyLayer_le {d : ℕ} (m : ℤ) (hn : ℕ → ℕ) (k : ℕ) : 3 * max 1 (Real.log ↑(Whitney.whitneyLayer m hn k).card) ≤ whitneyLayerLogConst d * (1 + ↑k + ↑(hn k))

Step (i). The l.maximums.Gamma.s penalty base of the layer 𝒲(□_m,k) is at most C(d) (1 + k + h_k). Layer 0 is empty and log 0 = 0, so the bound is trivial there.

theorem Algsuperdiff.Section3.Provider.Multiscale.whitneyWaveLayerPenalty_sq_le {d : ℕ} (m : ℤ) (hn : ℕ → ℕ) (k : ℕ) : whitneyWaveLayerPenalty d m hn k ^ 2 ≤ whitneyLayerLogConst d * (1 + ↑k + ↑(hn k))

Step (i), squared. ρ_k² ≤ C(d)(1 + k + h_k) for the finset-sup Orlicz penalty ρ_k = whitneyWaveLayerPenalty d m h k.

Step 2: the absorption, over abstract reals

theorem Algsuperdiff.Section3.Provider.Multiscale.one_add_le_mul (c s : ℝ) (hc : 0 < c) (hs : 0 ≤ s) : 1 + s ≤ (1 + c⁻¹) * (1 + c * s)

The absorption core, degree one. 1 + s ≤ (1 + c⁻¹)(1 + c s).

theorem Algsuperdiff.Section3.Provider.Multiscale.sq_one_add_le_mul {c s A : ℝ} (hc : 0 < c) (hs : 0 ≤ s) (hA : (1 + c * s) ^ 2 ≤ A) : (1 + s) ^ 2 ≤ (1 + c⁻¹) ^ 2 * A

The absorption core, squared, with the exponential kept as an ATOM. No rpow, no exp: only the abstract inequality (1 + c s)² ≤ A enters.

theorem Algsuperdiff.Section3.Provider.Multiscale.sq_one_add_le_three_rpow {eps s : ℝ} (heps : 0 < eps) (hs : 0 ≤ s) : (1 + eps * Real.log 3 / 2 * s) ^ 2 ≤ 3 ^ (eps * s)

The atom, supplied once. (1 + (ε log 3 / 2) s)² ≤ 3^{ε s} for s ≥ 0: the square of 1 + u ≤ e^u at u = ε s log 3 / 2.

noncomputable def Algsuperdiff.Section3.Provider.Multiscale.layerAbsorptionConst (eps : ℝ) : ℝ

The absorption constant C_ε = (1 + 2(ε log 3)^{-1})².

Equations

• Algsuperdiff.Section3.Provider.Multiscale.layerAbsorptionConst eps = (1 + (eps * Real.log 3 / 2)⁻¹) ^ 2

theorem Algsuperdiff.Section3.Provider.Multiscale.layerAbsorptionConst_nonneg (eps : ℝ) : 0 ≤ layerAbsorptionConst eps

theorem Algsuperdiff.Section3.Provider.Multiscale.one_add_mul_le_layerAbsorptionConst_mul {eps x y : ℝ} (heps : 0 < eps) (hx : 0 ≤ x) (hy : 0 ≤ y) : (1 + x) * (1 + x + y) ≤ layerAbsorptionConst eps * 3 ^ (eps * (x + y))

Step (ii). (1+x)(1+x+y) ≤ C_ε 3^{ε(x+y)} for every ε > 0 and every x, y ≥ 0: polynomial against exponential, at the honest C_ε.

Step 3: the layer envelope, priced into the exponent

theorem Algsuperdiff.Section3.Provider.Multiscale.whitneyWaveCubeScale_nonneg {d : ℕ} (hd : 2 ≤ d) (M : ABKModel d) (L : ℤ) : 0 ≤ whitneyWaveCubeScale M L

theorem Algsuperdiff.Section3.Provider.Multiscale.whitneyWaveLayerScale_nonneg {d : ℕ} (hd : 2 ≤ d) (M : ABKModel d) (m : ℤ) (hn : ℕ → ℕ) (k : ℕ) (L : ℤ) : 0 ≤ whitneyWaveLayerScale M m hn k L

noncomputable def Algsuperdiff.Section3.Provider.Multiscale.ktotEnvelopeSup {d : ℕ} (M : ABKModel d) (m L : ℤ) (eps t : ℝ) : ℝ

The layer-free gauge bound the raised-exponent pricing runs at. The root oscillation threshold and the whole layer envelope, combined in one constant: Sup₀² = osc_m² + C(d) C_ε A² t².

Equations

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

theorem Algsuperdiff.Section3.Provider.Multiscale.sq_ktotEnvelopeSup {d : ℕ} (M : ABKModel d) (m L : ℤ) (eps t : ℝ) : ktotEnvelopeSup M m L eps t ^ 2 = BadEvents.oscThreshold M m ^ 2 + whitneyLayerLogConst d * layerAbsorptionConst eps * whitneyWaveCubeScale M L ^ 2 * t ^ 2

theorem Algsuperdiff.Section3.Provider.Multiscale.sq_max_oscThreshold_whitneyWaveLayerScale_le {d : ℕ} (M : ABKModel d) (m : ℤ) (hn : ℕ → ℕ) (k : ℕ) (L : ℤ) {eps t : ℝ} (heps : 0 < eps) : max (BadEvents.oscThreshold M m) (whitneyWaveLayerScale M m hn k L * t) ^ 2 ≤ ktotEnvelopeSup M m L eps t ^ 2 * 3 ^ (eps * (↑k + ↑(hn k)))

Steps (i) and (ii), composed on the proved envelope. The squared gauge bound the layer-k pricing sees is the layer-free Sup₀² times exactly one factor 3^{ε(k+h_k)}.

theorem Algsuperdiff.Section3.Provider.Multiscale.ktotConst_le_mul {d : ℕ} (hd : 2 ≤ d) (M : ABKModel d) (m i : ℤ) {Cw : ℝ} (hCw : 0 ≤ Cw) {S1 S2 Eatom : ℝ} (hE : 1 ≤ Eatom) (hsq : S1 ^ 2 ≤ S2 ^ 2 * Eatom) (p q : HCPolySupport.Vec d) : ktotConst M m i Cw S1 p q ≤ ktotConst M m i Cw S2 p q * Eatom

The layer constant at a dominated gauge. If the layer's own squared gauge bound is at most S2² times an atom Eatom ≥ 1, then the layer constant is at most the layer-free one times that atom.

The good leg at the layer envelope

theorem Algsuperdiff.Section3.Provider.Multiscale.goodCellForm_le_ktotConst_mul_layerScale_ae {d : ℕ} (hd : 2 ≤ d) (M : ABKModel d) {m0 : ℤ} {E : { E : ℝ // 1 ≤ E }} (hS : Frozen.Section3.inductionState M m0 E) (m : ℤ) (hn : ℕ → ℕ) {i : ℤ} (hmi : m - 1 ≤ i) (hi : i ≤ m0) {L : ℤ} (hmL : m ≤ L) (p q : HCPolySupport.Vec d) {Cw : ℝ} {Sc : ℕ → ℝ} (hSc0 : ∀ (n : ℕ), 0 ≤ Sc n) : ∀ᵐ (omega : Cutoff.CutoffSample d) ∂↑(Cutoff.cutoffSampleLaw M), (∀ (n : ℕ), ∀ Q ∈ Whitney.whitneyLayer m hn n, HCPolySupport.Book.Ch02.multiscaleDescendantWeight Q (Whitney.simplexScale m hn n) (1 / 4) ≤ Cw) → (∀ (n : ℕ), ∀ Q ∈ Whitney.whitneyLayer m hn n, Stream.cubeSupBound Q Q.scale L ↑omega ≤ Sc n) → ∀ (n : ℕ), ∀ Q ∈ Whitney.whitneyLayer m hn n, ∀ T ∈ Whitney.whitneySimplexCells m hn n Q, goodCellForm M m hn L omega ((√↑(Annealed.sigmaBar M i))⁻¹ • p) (√↑(Annealed.sigmaBar M i) • q) T ≤ ktotConst M m i Cw (max (BadEvents.oscThreshold M m) (Sc n)) p q * 3 ^ (2 * M.gamma * (↑n + ↑(hn n)))

The good leg priced against a layer-dependent gauge bound. ConclusionKtot.goodCellForm_le_ktotConst_mul_ae with its single real Swave replaced by a sequence Sc read at the cube's own layer. The proof is the consumed one: the pricing stepOneLayerMajorant_le_ktotConst_mul is per-cube, and a layer cube's gauge bound is used only at its own layer index.

theorem Algsuperdiff.Section3.Provider.Multiscale.goodCellForm_le_ktotEnvelopeConst_mul_layerQuantity_ae {d : ℕ} (hd : 2 ≤ d) (M : ABKModel d) {m0 : ℤ} {E : { E : ℝ // 1 ≤ E }} (hS : Frozen.Section3.inductionState M m0 E) (m : ℤ) {b : ℝ} (hb0 : 0 < b) (hb : b ≤ 1 / 8) (hs k₀ : ℕ) {i : ℤ} (hmi : m - 1 ≤ i) (hi : i ≤ m0) {L : ℤ} (hmL : m ≤ L) (p q : HCPolySupport.Vec d) {eps : ℝ} (heps : 0 < eps) {t : ℝ} (ht0 : 0 ≤ t) : ∀ᵐ (omega : Cutoff.CutoffSample d) ∂↑(Cutoff.cutoffSampleLaw M), (∀ (n : ℕ), ∀ Q ∈ Whitney.whitneyLayer m (Whitney.whitneyScaleSeq b hs k₀) n, Stream.cubeSupBound Q Q.scale L ↑omega ≤ whitneyWaveLayerScale M m (Whitney.whitneyScaleSeq b hs k₀) n L * t) → ∀ (n : ℕ), ∀ Q ∈ Whitney.whitneyLayer m (Whitney.whitneyScaleSeq b hs k₀) n, ∀ T ∈ Whitney.whitneySimplexCells m (Whitney.whitneyScaleSeq b hs k₀) n Q, goodCellForm M m (Whitney.whitneyScaleSeq b hs k₀) L omega ((√↑(Annealed.sigmaBar M i))⁻¹ • p) (√↑(Annealed.sigmaBar M i) • q) T ≤ ktotConst M m i 3 (ktotEnvelopeSup M m L eps t) p q * 3 ^ ((2 * M.gamma + eps) * layerQuantity b hs k₀ n)

Step (iii): the hgood binder body at the raised exponent 2γ + ε. The good leg, at the honest layer envelope of ConclusionData and at the descendant weight Cw := 3, is bounded by a layer-free constant times 3^{(2γ+ε)(k+h_k)}. See the module docstring for the composer's gate 8 M.gamma + 4 ε ≤ 1 − b.