ConclusionRoot #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
The [0,∞] root of the concluding assembly of p.bfA.multiscalebound #
ConclusionCompetitor records the join of the two as not performed, because
a toReal bound is vacuous unless the intermediate [0,∞] sum is finite.
This module performs the join.
1. What the module delivers #
tsum_..._le_ofReal_payload the [0,∞] twin of ConclusionCompetitor's payload
tsum_..._le_ofReal_payload_assembled_ae its assembled form, at a FREE competitor pair
abs_blockVecDot_..._le_payload_ae the local join at the concrete competitor
ofReal_abs_blockVecDot_le_tsum_superposed_ae the join's left half at the SUPERPOSED
competitor, with EXACTLY hF/hG open
abs_blockVecDot_..._le_payload_superposed its real-valued form
| (𝐀hom_i^{-1/2}(p,q)) . 𝐀_L(□_m) (𝐀hom_i^{-1/2}(p,q)) |
≤ layerSumConst β (2γ+ε) kp Ktot Ccol (6d)
. 3^{(2γ+ε)(h_hat_sep+k₀)} ( 1 + 3^{2β(h_hat_sep+k₀)} exp(-kp/36) )
2. The two open legs, and why they are packaged #
sum_of_a_decomp_cutoff carries eight affine A clauses. q + L²_sol,0(□_m).
Later files now prove the superposed potential and divergence trace statements;
the theorems below retain their original conditional interfaces.
At the concrete single-mesh competitor the four cell-constant clauses hbadF,
hoffF, hbadG, hoffG are theorems here
(kuhnSlope_competitorVertexData_eq_zero…, …_eq_of_mem_simplexPartition and
their competitorDivergence twins, all read off the proved
CompetitorVertexData / CollarLayerEnvelopeG clauses through
mem_simplexPartition_iff). What is NOT available at that competitor is
hFc/hGc: there is no proved global field whose cell constants are
kuhnSlope 𝔰 (competitorVertexData ℐ p) on ALL of SW(□_m) — that is exactly
what the cross-scale gluing rules out for the single-assignment presentation. hF
and hFc are therefore carried as ONE existential binder
∃ F, F − 𝐀hom^{-1/2}p ∈ L²_pot,0(□_m) ∧ F = Fc on every open cell of SW(□_m),
which is precisely e.hat.linear.1 for the concrete family, and likewise for
hG/hGc. So the theorem has TWO open legs and they are the affine chain's
own two open legs. Nothing else is assumed.
3. The superposition leg, and the finding that separates the two routes #
GlobalSuperposition.superposedCompetitor_decomp_clauses_badFamily discharges
all six cell-constant clauses at the superposed competitor ℓ̂_p = ℓ_p + Σ_𝒞 (ℓ̂_p^𝒞 − ℓ_p), including hFc/hGc, because that competitor comes with a global
field. ofReal_abs_blockVecDot_le_tsum_superposed_ae consumes it: at the
manuscript's own bad family and at any loads, with the window binder discharged
by badComponents_window_badFamily, the whole of sum_of_a_decomp_cutoff
reduces to hF and hG.
Off the collar and on bad cubes the two competitors agree (both are p resp.
0, by clauses 3 and 1 on each side). On a good cube the superposed cell
slope is a sum of per-component corrections read on per-component meshes; this
historical module neither identifies it with the single-mesh slope nor prices
it. The later SuperposedEnvelope.lean proves the summed active-component
estimate, including the dimension-only overlap bound, and the correct trace
providers land in SuperposedPotentialClosure.lean and
SuperposedDivergencePotential.lean.
4. Why hgood and hmasscol are not re-done here #
This module re-runs that same wiring only because the toReal conclusion
cannot be converted to the ofReal one after the fact; the wiring is
transcribed, not re-derived, and it is generalized in exactly two places: the
collar constant Cgrad is free (with 1 ≤ Cgrad) and the competitor pair
(Fv, Gv) is free (with the two collar-envelope binders). The proved local
F-leg and G-leg envelopes then instantiate it, so the G-leg input that is
explicit in ConclusionAssemblyFinal is discharged here at Gv:= ∇·D̂_q = competitorDivergence.
What is not proved #
- This module closes no node. Its historical public theorems retain
hF/hGor other payload data as conditional/A premises. Later providers discharge those premises at the correct superposed objects; that downstream progress is not credited to this file. - No local gradient or trace identification. Those statements are not
proved below; see
SuperposedPotentialClosure.leanandSuperposedDivergencePotential.leanfor the later route. - No local summed active-component estimate. See
SuperposedEnvelope.lean; the theorem below continues to expose the older collar-data interface. - No new probabilistic input, and no new constant: every constant below is
the one the proved inputs produce; nothing is optimized, and the only
measure-theoretic step is
filter_upwardson already-proved a.e. statements. - No
Ktotconstruction: the good leg's layer constant isConclusionKtotEnvelope's, unchanged, and the|b_L|branch of Step 2 is untouched.
Main results #
Algsuperdiff.Section3.Provider.Multiscale.payload_nonnegAlgsuperdiff.Section3.Provider.Multiscale.tsum_simplexPartition_cutoff_two_leg_le_ofReal_payloadAlgsuperdiff.Section3.Provider.Multiscale.tsum_simplexPartition_cutoff_two_leg_le_ofReal_payload_assembled_ae
References #
- ABK26,
p.bfA.multiscaleboundStep 3 (the payload display),e.sum-of-a-decomp,e.bounds.on.slopes.when.bad,l.piecewise.affine.approx(clauses 1 and 3), the false disjointness,e.hat.linear.1,e.hatdq,e.hat.D.bc,l.bad.cubes.density,e.hn.def, theb-window with label,e.SW.def, the Step-1 majorant. Provider/Multiscale/ConclusionCompetitor.lean(sum_of_a_decomp_cutoffand the two concrete cell functionals),Provider/Multiscale/ConclusionAssemblyFinal.lean(the assembled payload this module transcribes into[0,∞]),Provider/Multiscale/ConclusionFeasibility.lean(the parameter window),Provider/Multiscale/LayerMass.lean(tsum_simplexPartition_le_ofReal_payload),Provider/Affine/CollarLayerEnvelope.leanandProvider/Affine/CollarLayerEnvelopeG.lean(the two proved local envelopes),Provider/Affine/CompetitorVertexData.lean(clauses 1 and 3),Provider/Affine/GlobalSuperposition.lean(the six clauses at the superposed competitor and the window discharge).