ConclusionData

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

Local providers for three named data of the p.bfA.multiscalebound conclusion

Provider/Multiscale/ConclusionKtot.lean and Provider/Multiscale/ConclusionSeam3.lean land the two remaining analytic inputs of the concluding assembly and leave exactly three data open, named in their own docstrings: the descendant-weight bound Cw, the transported wave gauge bound Swave, and the seam-3 shell envelope hA. This module proves local Provider results for two of those A antecedents and replaces the third by the strongest statement its own route supports. It does not close the source conclusion or any fraction of it.

1. The local Cw = 3 result

On 𝒲(□_m,k) one has □.scale = m − k − h_k and simplexScale m h k = m − (k+1) − h_{k+1}, so

multiscaleDescendantWeight □ (simplexScale m h k) (1/4)
    = 3^{2·(1/4)·(1 + h_{k+1} − h_k)} = 3^{(1 + h_{k+1} − h_k)/2} .

multiscaleDescendantWeight_eq_of_mem_whitneyLayer is this identity. The gap step of e.hn.gap ((the label line — the development convention, restored), h_{k+1} ≤ h_k + 1) is proved for the Whitney sequence as Whitney.whitneyScaleSeq_succ_le (b ≤ 1/8), so the exponent is at most 1 and the weight at most 3^1 = 3, uniformly over the layers and over the cubes of a layer. ConclusionKtot's docstring records that e.SW.def's hstep binder carried by Provider/Whitney/SimplexPartition.lean is the opposite inequality h_k ≤ h_{k+1} + 1 and therefore does not discharge this; the gap lemma used here is a different, proved statement about the sequence itself, read in the same direction. multiscaleDescendantWeight_whitneyScaleSeq_le_three is literally the hCw binder of ConclusionKtot.goodCellForm_le_ktotConst_mul_layerQuantity_ae at Cw := 3, and goodCellForm_le_ktotConst_three_mul_layerQuantity_ae is that consumer with the datum discharged --- so the fit is machine-checked, not asserted.

2. The local hA envelope

streamIncrementLpMassScale M p n m depends on n only through min{γ^{-1/2}, (m−n)^{1/2}} inside streamPointScale, which is ANTITONE in n: a deeper shell index can only enlarge the e.kmn.bounds scale, and the growth saturates at the γ-entry. streamPointScale_le_of_le and streamIncrementLpMassScale_le_of_le record this, and seamLayerScale_le_of_le is the resulting envelope over h ≤ H in the exact shape of the hA binder of ConclusionSeam3.measureReal_upperTailEvent_seamLayerObject_hsep_le: the common scale is the proved deterministic-index scale read at the D index h = H, so it is not a new constant and carries no new hypothesis. measureReal_upperTailEvent_seamLayerObject_hsep_envelope_le is the seam-3 conclusion with that datum discharged; it has no interface datum left.

3. Swave (no constant; an honest layer envelope only)

ConclusionKtot prices the transported gauge Stream.cubeSupBound inside ONE layer at Γ₂, at the scale

ρ_k · A ,    ρ_k = (3 max{1, log #𝒲(□_m,k)})^{1/2} ,
A   = (3 max{1, log 7^d})^{1/2} · C_d · γ^{-1/2} · 3^{γL} ,

and asks for a single real Swave dominating the gauge on ALL layers at once. Two facts about the proved inputs bear on that request, and both are proved or computed here rather than asserted.

• The per-cube amplitude is layer-free. At n = □.scale the covering family of e.km.kn.Linfty has (subcubeShifts d n n).card = 7^d members at every scale (card_subcubeShifts_self; subcubeRadius n n = 3), and min{γ^{-1/2}, (L − □.scale)^{1/2}} ≤ γ^{-1/2} caps the only other scale-dependent factor. whitneyWaveCubeScale is the resulting layer-free amplitude and isBigOWith_gammaSigma_two_layerSup_cubeSupBound_whitneyWaveCubeScale is the layer maximum at it.
• The penalty ρ_k is NOT bounded in k. The layers are the literal infinite family (whitneyPartition is a Set, not a Finset); every layer k ≥ 1 is nonempty and #𝒲(□_m,k) grows with k, so the Γ₂ scales of the layer maxima are unbounded. This module therefore does NOT produce a constant Swave, and nothing below claims one exists.

What IS produced is the all-layer aggregation with the amplification the union bound actually pays. measureReal_exists_cubeSupBound_gt_le: for every t ≥ 1,

P[ ∃ k, ∃ □ ∈ 𝒲(□_m,k) :  the dominating gauge cubeSupBound (≥ ‖k_L − k_{□.scale}‖_{L^∞(□)}; audit
#29 F-11) > (1+k)^{1/2} ρ_k A t ]
      ≤ 2 e^{−t²} = 2 (Γ₂ t)^{-1} ,

because the k-th piece costs exp(−(1+k)t²) and the geometric series is at most 2 e^{−t²} for t ≥ 1 (exp 1 ≥ 2). Only monotonicity, finite subadditivity and continuity from below are used: no independence, no measurability of the union and no identification across samples (discipline is inherited unchanged, since every per-layer estimate is the proved one). one_sub_le_measureReal_forall_ cubeSupBound_le is the complementary reading, which is the hSwave binder of the good leg with its single constant replaced by the layer envelope whitneyWaveLayerScale M m h k L · t, on an event of probability at least 1 − 2 e^{−t²}.

The amplification is in k ((1+k)^{1/2} ρ_k, with ρ_k² = 3 max{1, log #𝒲(□_m,k)}), while the payload of ConclusionRoot.tsum_simplexPartition_cutoff_two_leg_le_ofReal_payload reads its two legs at the geometric weight 3^{γ · layerQuantity} in k + h_k; the remaining distance is therefore an arithmetic re-absorption, spelled out in "What is not proved".

What is not proved

• No constant Swave, and no claim that one exists. The obstruction above is an analysis of the proved scales, not a theorem: this module proves no lower bound on any layer maximum and asserts no divergence. What it does assert is that the route through the proved per-layer Γ₂ estimates cannot produce one, which is why the consumer's binder is the thing that must move.
• The good leg is NOT restated at the layer envelope. Feeding whitneyWaveLayerScale into stepOneLayerMajorant_le_ktotConst_mul makes the constant k-dependent through Sup², so the payload exponent must rise from 2γ to 2γ + ε. That needs (i) the logarithm of the already proved cardinality bound LayerMass.card_whitneyLayer_le (#𝒲(□_m,k) ≤ 2d·(3^{d−1})^{k−1}·(3^d)^{1+h_k}, giving ρ_k² ≤ C(d)·(1 + k + h_k)), (ii) the elementary (1+k)·(1+k+h_k) ≤ C_ε 3^{ε(k+h_k)}, and (iii) a restatement of the good leg at the raised exponent, with the parameter window 4(2γ+ε) ≤ 1 − b. None of the three is done in this module; all three are carried out in ConclusionKtotEnvelope.lean, whose endpoint is goodCellForm_le_ktotEnvelopeConst_mul_layerQuantity_ae.
• No monotonicity of streamIncrementLpMassScale in p, m or the cube, and no re-basing onto the cube-averaged L⁴ norm: only the shell-index direction is proved, which is all hA needs.

Main definitions

• Algsuperdiff.Section3.Provider.Multiscale.whitneyWaveCubeScale
• Algsuperdiff.Section3.Provider.Multiscale.whitneyWaveLayerPenalty
• Algsuperdiff.Section3.Provider.Multiscale.whitneyWaveLayerScale

Main results

• Algsuperdiff.Section3.Provider.Multiscale.multiscaleDescendantWeight_whitneyScaleSeq_le_three
• Algsuperdiff.Section3.Provider.Multiscale.card_subcubeShifts_self
• Algsuperdiff.Section3.Provider.Multiscale. isBigOWith_gammaSigma_two_layerSup_cubeSupBound_whitneyWaveCubeScale
• Algsuperdiff.Section3.Provider.Multiscale.measureReal_exists_cubeSupBound_gt_le

References

• ABK26, p.bfA.multiscalebound Step 1 (majorant) and Step 3; e.hn.def / e.hn.gap; e.SW.def; e.km.kn.Linfty; e.kmn.bounds; l.maximums.Gamma.s; e.hsep.tails.
• Provider/Multiscale/ConclusionKtot.lean and Provider/Multiscale/ConclusionSeam3.lean (the two consumers), Provider/Whitney/BadSetDefinitions.lean (the Whitney sequence and layers), Provider/Stream/IncrementLp.lean (the e.kmn.bounds scale), Provider/Stream/WaveTranslation.lean (the transported gauge).

Cw: the descendant weight along the Whitney layers

theorem Algsuperdiff.Section3.Provider.Multiscale.multiscaleDescendantWeight_eq_of_mem_whitneyLayer {d : ℕ} (m : ℤ) (hn : ℕ → ℕ) (n : ℕ) {Q : HCPolySupport.TriadicCube d} (hQ : Q ∈ Whitney.whitneyLayer m hn n) : HCPolySupport.Book.Ch02.multiscaleDescendantWeight Q (Whitney.simplexScale m hn n) (1 / 4) = 3 ^ ((1 + ↑(hn (n + 1)) - ↑(hn n)) / 2)

The descendant weight of a layer cube is 3^{(1 + h_{k+1} − h_k)/2}. On 𝒲(□_m,k) one has □.scale = m − k − h_k and the simplex scale is m − (k+1) − h_{k+1}, so the exponent of Ch02.multiscaleDescendantWeight □ (simplexScale m h k) (1/4) is 2·(1/4)·(1 + h_{k+1} − h_k).

theorem Algsuperdiff.Section3.Provider.Multiscale.multiscaleDescendantWeight_le_three_of_mem_whitneyLayer {d : ℕ} (m : ℤ) (hn : ℕ → ℕ) (n : ℕ) (hgap : hn (n + 1) ≤ hn n + 1) {Q : HCPolySupport.TriadicCube d} (hQ : Q ∈ Whitney.whitneyLayer m hn n) : HCPolySupport.Book.Ch02.multiscaleDescendantWeight Q (Whitney.simplexScale m hn n) (1 / 4) ≤ 3

The uniform bound Cw = 3. With the e.hn.gap step h_{k+1} ≤ h_k + 1 the exponent is at most 1, so the descendant weight of every layer cube is at most 3^{(1+1)/2} = 3.

theorem Algsuperdiff.Section3.Provider.Multiscale.multiscaleDescendantWeight_whitneyScaleSeq_le_three {d : ℕ} {b : ℝ} (hb0 : 0 < b) (hb : b ≤ 1 / 8) (hs k₀ : ℕ) (m : ℤ) (n : ℕ) (Q : HCPolySupport.TriadicCube d) : Q ∈ Whitney.whitneyLayer m (Whitney.whitneyScaleSeq b hs k₀) n → HCPolySupport.Book.Ch02.multiscaleDescendantWeight Q (Whitney.simplexScale m (Whitney.whitneyScaleSeq b hs k₀) n) (1 / 4) ≤ 3

Cw := 3, in the exact binder shape the good leg's descendant-weight hypothesis has (the hCw binder of ConclusionKtotEnvelope.goodCellForm_le_ktotConst_mul_layerScale_ae). The Whitney sequence h_k = ⌈b(1−b)⁻¹k⌉ + h_hat_sep + k₀ satisfies e.hn.gap for b ≤ 1/8 (whitneyScaleSeq_succ_le), so its descendant weights are bounded by 3 uniformly over the layers and over the cubes of each layer.

hA: the shell-index envelope of the seam-3 scales

Swave: the transported wave gauge, aggregated over all layers

theorem Algsuperdiff.Section3.Provider.Multiscale.card_subcubeShifts_self (d : ℕ) (n : ℤ) : (Stream.subcubeShifts d n n).card = 7 ^ d

The covering family of a cube at its OWN scale has 7^d members, at every scale: subcubeRadius n n = 3.

noncomputable def Algsuperdiff.Section3.Provider.Multiscale.whitneyWaveCubeScale {d : ℕ} (M : ABKModel d) (L : ℤ) : ℝ

The layer-free per-cube amplitude of the transported wave gauge. The amplitude of Stream.isBigOWith_gammaSigma_cubeSupBound_cutoffLaw at n = □.scale, with the covering count evaluated (7^d, independent of the scale) and the min capped by its γ-entry, so that nothing depends on the layer.

Equations

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

noncomputable def Algsuperdiff.Section3.Provider.Multiscale.whitneyWaveLayerPenalty (d : ℕ) (m : ℤ) (hn : ℕ → ℕ) (k : ℕ) : ℝ

The l.maximums.Gamma.s penalty of the layer 𝒲(□_m,k).

Equations

• Algsuperdiff.Section3.Provider.Multiscale.whitneyWaveLayerPenalty d m hn k = (3 * max 1 (Real.log ↑(Algsuperdiff.Section3.Provider.Whitney.whitneyLayer m hn k).card)) ^ 2⁻¹

noncomputable def Algsuperdiff.Section3.Provider.Multiscale.whitneyWaveLayerScale {d : ℕ} (M : ABKModel d) (m : ℤ) (hn : ℕ → ℕ) (k : ℕ) (L : ℤ) : ℝ

The honest layer envelope of the wave gauge. The Γ₂ scale of the layer-k maximum, amplified by (1+k)^{1/2}; the amplification is what makes the countable aggregation over the layers summable.

Equations

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

theorem Algsuperdiff.Section3.Provider.Multiscale.isBigOWith_gammaSigma_two_layerSup_cubeSupBound_whitneyWaveCubeScale {d : ℕ} (hd : 2 ≤ d) (M : ABKModel d) (m : ℤ) (hn : ℕ → ℕ) {n : ℕ} (hne : (Whitney.whitneyLayer m hn n).Nonempty) {L : ℤ} (hL : m - ↑n - ↑(hn n) < L) : HCPolySupport.IndependentSums.IsBigOWith (↑(Cutoff.cutoffSampleLaw M)) (HCPolySupport.IndependentSums.gammaSigma 2) (fun (omega : Cutoff.CutoffSample d) => (Whitney.whitneyLayer m hn n).sup' hne fun (Q : HCPolySupport.TriadicCube d) => Stream.cubeSupBound Q (m - ↑n - ↑(hn n)) L ↑omega) (whitneyWaveLayerPenalty d m hn n * whitneyWaveCubeScale M L)

The layer maximum of the transported gauge at the layer-free amplitude: the covering count is evaluated and the min is capped, so only the log-cardinality penalty of the layer remains k-dependent.

theorem Algsuperdiff.Section3.Provider.Multiscale.measureReal_exists_cubeSupBound_gt_le {d : ℕ} (hd : 2 ≤ d) (M : ABKModel d) (m : ℤ) (hn : ℕ → ℕ) {L : ℤ} (hmL : m ≤ L) {t : ℝ} (ht : 1 ≤ t) : (↑(Cutoff.cutoffSampleLaw M)).real {omega : Cutoff.CutoffSample d | ∃ (k : ℕ), ∃ Q ∈ Whitney.whitneyLayer m hn k, whitneyWaveLayerScale M m hn k L * t < Stream.cubeSupBound Q Q.scale L ↑omega} ≤ 2 * (HCPolySupport.IndependentSums.gammaSigma 2 t)⁻¹

The wave gauge over ALL layers, priced. For every t ≥ 1, the probability that SOME Whitney cube of SOME layer violates its own layer envelope at level t is at most 2 e^{-t²}:

P[ ∃ k, ∃ □ ∈ 𝒲(□_m,k),  the dominating gauge cubeSupBound (≥ ‖k_L − k_{□.scale}‖_{L^∞(□)}) >
(1+k)^{1/2} ρ_k A t ]
      ≤ 2 (Γ₂ t)^{-1} ,

with ρ_k = (3 max{1, log #𝒲(□_m,k)})^{1/2} the layer penalty of l.maximums.Gamma.s and A = whitneyWaveCubeScale M L the layer-free per-cube amplitude of e.km.kn.Linfty. The (1+k)^{1/2} amplification is exactly what makes the countable union over the layers summable: the k-th piece costs e^{-(1+k)t²} and the geometric series is bounded by 2 e^{-t²} for t ≥ 1. No independence and no measurability of the union is used: the estimate is a countable union bound over the proved per-layer maxima.