ConclusionAssemblyFinal #

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

The concluding assembly of `p.bfA.multiscalebound` #

ConclusionCompetitor.toReal_tsum_simplexPartition_cutoff_two_leg_le_payload is the Step-3 payload at the two cell functionals goodCellForm, collarCellForm. Four groups of binders were still the caller's when it proved: the good leg (hgood), the collar leg (hcol), the four mass data (hmassgood, hmasscol, hMass, hBadMass, hBadDens) and the parameter window. ConclusionKtotEnvelope supplies the local hgood antecedent. This module reduces hcol to the two explicit slope-envelope inputs below, discharges the F input, instantiates the mass data using the proved local CollarMass route, and runs the composition. Its remaining G input is local to this module's theorem and is discharged by the later ConclusionCompose/ConclusionRoot route.

1. The collar leg #

ConclusionCompetitor.collarCellForm_le_stepOneLayerMajorant_ae prices one collar cell by 4 Cgrad² 3^{2b(k+h_k)} times the Step-1 majorant M, and ConclusionKtot.stepOneLayerMajorant_le_ktotConst_mul prices M by ktotConst . 3^{2γ(k+h_k)}. Composing them (collarCellForm_le_ktotConst_mul_layerScale_ae) and feeding the layer envelope of ConclusionData through ConclusionKtotEnvelope's absorption (collarCellForm_le_collarEnvelopeConst_mul_layerQuantity_ae) gives the layer-free constant collarEnvelopeConst at the exponent

2b + 2γ + ε   (γ = M.gamma, ε the absorption exponent),

i.e. the collar leg's honest per-cell growth is 3^{(2b+2γ+ε)(k+h_k)}, NOT 3^{2b(k+h_k)}. This module's theorem still exposes hGv, the G-leg envelope at (∇·D̂_q)(𝔰), and applies it at Gv := competitorDivergence in the downstream binder-drop composition. Thus hGv is an explicit premise of this local theorem, not a currently open project obligation and not evidence that this module closes a source node.

2. Why the payload's `b` is not the geometry's `b` #

The payload's hcol slot is Ccol . 3^{2b . layerQuantity b hs k₀ n}. Section 1 produces 3^{(2b+2γ+ε)(k+h_k)}. The manuscript's own Step 3 also multiplies e.bounds.on.slopes.when.bad by e.good.simplex.consequence, so the extra 3^{γ(k+h_k)} is genuinely there and is NOT an artefact of this repository; ConclusionAssembly.layerContrib simply carries the collar leg at the bare 3^{2b(k+h_k)}, i.e. it expects the caller to have already absorbed the Step-1 growth into its own b.

The absorption is legitimate because toReal_tsum_simplexPartition_..._payload binds hn and (b, hs, k₀) independently: nothing there forces hn = whitneyScaleSeq b hs k₀. So the assembly runs at

hn := whitneyScale M m E b k₀ ω = whitneyScaleSeq b h_hat_sep k₀   (the geometry),
payload parameters := (β, h_hat_sep + k₀, kp)   with   2b + 2γ + ε ≤ 2β ,

and layerQuantity_le_of_le supplies layerQuantity b h_hat_sep k₀ n ≤ layerQuantity β (h_hat_sep+k₀) kp n (the ceiling ⌈b(1-b)^{-1}n⌉ is monotone in b, and the offsets are ordered). Both legs then fit their slots: the good leg because its exponent γ is nonnegative and the layer quantity only grew; the collar leg because 2b+2γ+ε ≤ 2β and the layer quantity only grew.

3. The mass data #

hMass/hmassgood are LayerMass.sum_cubeMassRatio_whitneyLayer_le at Cmass = 6d (assemblyMass). For the bad sequence the module takes the feasible route CollarMass records:

Bad j := min ( collarMassCap ,  6d . 3^{-j} ) ,
collarMassCap := 9 . 99^d ( exp(-c(d) E^{-2} γ^{-1}) + 3^{-(h_hat_sep+k₀)/2} )

(assemblyBad). The min's right branch is hBadMass and is available because collarLayer ⊆ 𝒲(□_m,n); the left branch is CollarMass.sum_cubeMassRatio_collarLayer_le_layerQuantity read at layerQuantity b h_hat_sep k₀ n ≥ h_hat_sep + k₀ (sum_cubeMassRatio_collarLayer_le_assemblyBad). hBadDens is then the T Bad j ≤ ε at ε := collarMassCap --- the whole 3^{-(j+h_j)/2} decay is spent inside the constant, which is exactly what ConclusionAssembly.layerContrib_le consumes anyway (its only use of hBadDens is through k₀ ≤ layerQuantity, i.e. through the constant). The (hs, k₀) shift that CollarMass leaves to its consumer is therefore implemented here as the payload offset hs := h_hat_sep + k₀, and the 9.99^d dimensional factor is paid once, inside ε, by the single arithmetic gate

9 . 99^d ( exp(-c(d) E^{-2} γ^{-1}) + 3^{-k₀/2} )  ≤  exp(-kp)          (GATE)

which is the binder hcap and is discharged in Provider/Multiscale/ConclusionFeasibility.lean.

4. What this local assembly delivers #

toReal_tsum_simplexPartition_cutoff_two_leg_le_payload_assembled_ae is, almost surely and on the scale-separation event, the Step-3 payload

( ∑'_{𝔰 ∈ SW(□_m)} ofReal(|𝔰|/|□_m| g_good 𝔰) + ofReal(|𝔰|/|□_m| g_col 𝔰) )^{ℝ}
  ≤ layerSumConst β (2γ+ε) kp Ktot Ccol (6d)
      . 3^{(2γ+ε)(h_hat_sep+k₀)} ( 1 + 3^{2β(h_hat_sep+k₀)} exp(-kp/36) )

at the concrete competitor (∇ℓ̂_p, G) and the concrete loads (σ_i^{-1/2}p, σ_i^{1/2}q), with Ktot, Ccol explicit and layer-free. The right-hand side is the manuscript's own first Step-3 display, which is written there at 3^{γ(h_hat_sep+k_0)}(1 + 3^{2b(h_hat_sep+k_0)}(...)) before the k_0 collapse.

This module itself does not perform the following three downstream steps:

discharge of its local hGv premise (now performed downstream using CollarLayerEnvelopeG);
the eight affine A clauses of ConclusionCompetitor.sum_of_a_decomp_cutoff (l.piecewise.affine.approx), which are what turn this payload into a bound on |(p,q).𝐀_L(□_m)(p,q)| --- this module does NOT invoke sum_of_a_decomp_cutoff (the later superposed route supplies these clauses);
the real-valued join of sum_of_a_decomp_cutoff with the payload, i.e. the finiteness of the intermediate [0,∞] sum (performed in ConclusionRoot).

What is not proved #

No local proof of the G-leg: the theorem below keeps it as a hypothesis; the downstream repository supplies it as described above.
No affine A discharge, no glued competitor, no H¹ statement.
No claim that Ccol is the manuscript's C: collarEnvelopeConst is the honest output of the route above (4 Cgrad² ktotConst), nothing is optimized.
No new probabilistic input: the only measure-theoretic steps are ae_all_iff over the countable h_hat_sep-values and the a.e. statements already proved.

Main definitions #

Main results #

Algsuperdiff.Section3.Provider.Multiscale.layerQuantity_le_of_le
Algsuperdiff.Section3.Provider.Multiscale.collarCellForm_le_ktotConst_mul_layerScale_ae
Algsuperdiff.Section3.Provider.Multiscale. collarCellForm_le_collarEnvelopeConst_mul_layerQuantity_ae
Algsuperdiff.Section3.Provider.Multiscale.sum_cubeMassRatio_collarLayer_le_assemblyBad

References #

ABK26, p.bfA.multiscalebound Step 3 (the payload display), e.bounds.on.slopes.when.bad, e.sum-of-a-decomp, e.good.simplex.consequence, l.bad.cubes.density, e.hn.def, e.hn.gap, l.piecewise.affine.approx, r.gradient.bound.simplified.
Provider/Multiscale/ConclusionCompetitor.lean (the payload and the two cell functionals), Provider/Multiscale/ConclusionKtotEnvelope.lean (the good leg), Provider/Multiscale/CollarMass.lean (the collar mass), Provider/Multiscale/LayerMass.lean (the layer mass), Provider/Affine/CollarLayerEnvelope.lean (the F-leg envelope).

ConclusionAssemblyFinal #

The concluding assembly of p.bfA.multiscalebound #

1. The collar leg #

2. Why the payload's b is not the geometry's b #

3. The mass data #

4. What this local assembly delivers #

What is not proved #

Main definitions #

Main results #

References #

The layer quantity is monotone in the parameter and in the offset #

The collar leg, priced against a layer-dependent gauge bound #

The collar leg at the layer envelope #

The four mass data #

The concluding assembly #

The concluding assembly of `p.bfA.multiscalebound` #

2. Why the payload's `b` is not the geometry's `b` #