HomSpineSupFormRethread #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
The Step-3c re-thread at the sup-form clause #
The measurement this file records #
Which consumers of the clause actually need the ℓ^p-over-depths
aggregate, and which only need the print's sup?
Answer: NONE of them needs the ℓ^p aggregate. The Step-3c chain
the descendant bound
→ the translate-uniform box gauge
→ { the continuous representative, the `L^∞` endpoint }
→ clause (C3)
touches its ℓ^p-over-depths gauge hypothesis on □_m at
exactly ONE place — the outer-index collapse, which throws
the sum away and keeps a single depth term. Everything after that point is a
statement about the per-depth quantities: the descendant bound ‖(G)_R‖ ≤ A·3^{(s+d/p)m}·3^{-(s+d/p)·scale R}, the box gauge, the translate-uniform
carrier, and the L^∞ lift, whose own depth summation is the INDEPENDENT
geometric factor liftGeomFactor (s + d/p) at the FIXED gap 1 - (s + d/p) ≥ 1/2.
So the whole leg re-threads verbatim at the sup-form clause of
HomSpineSupFormClause, with identical constants: the theorems below are
the same, with the ℓ^p-over-depths gauge bound replaced by
NegBesovSupGaugeBound … A, and the endpoint constant 96 d² · liftGeomFactor (s + d/p) is unchanged. In particular the ℓ^p aggregation on the clause's
left-hand side was pure overshoot: it was forced by the PRODUCER
(CoarseGraining's negative Besov seminorm is an ℓ^p depth tsum), never by
a consumer.
The per-cell sharpening #
At the print's own per-cell carrier (forced by the far-band
result for depth-global tests) the re-thread is not merely constant-preserving,
it is strictly better: the datum IS the per-cell descendant bound, so the order
shift s ↦ s + d/p — the price of reading one cell out of an ℓ^p mean over
3^{jd} cells — disappears, the guard becomes s ≤ 1/2, the endpoint constant
becomes 96 d² · liftGeomFactor s (≤ 3 on that range), and p leaves the
lifting leg entirely.
What this file does not prove #
The sup-form clause itself. HomSpineSupFormClause states the exact
interface (NegativeBesovGridSmoothDualConverseAtDepth — the single-depth
grid/smooth-dual comparison, plus
ofReal_negBesovSupPartialNorm_le_of_depthConverse); the single-depth dual
test family is supplied by that interface and is consumed here as a named
input only. The energy
slot is unchanged, so the ℓ^p energy factor coarseGrainingGeomFactor p (s/4) (the D3 site) survives this re-cut; see HomSpineSupFormClause §5.
1. The descendant bound, from one depth at a time #
The printed descendant bound from the SUP-form gauge.
The finite-p descendant bound with the ℓ^p hypothesis
replaced by the sup-form one. The proof never used more: it applied
the outer-index collapse and discarded the sum.
the translate-uniform carrier from the SUP-form gauge, at the constant.
The residue, from the sup-form gauge.
2. The L^∞ endpoint at the sup-form gauge #
THE CONVERSION THEOREM AT THE PRINT'S OWN AGGREGATION.
The finite-p L^∞ conversion with the ℓ^p-over-depths
hypothesis replaced by the sup over depths, at the SAME constant
96 d² · liftGeomFactor (s + d/p).
3. Clause (C3) from the sup-form clause #
CLAUSE (C3), FROM THE SUP-FORM MULTISCALE CLAUSE.
The printed Step-3c clause re-threaded at
CoarseGrainingSupMultiscale: the printed Step-3c leg, with the print's own
p = ∞ depth aggregation on the left-hand side of the clause, and with the
identical output constant 96 d² · liftGeomFactor (s + d/p) · C_w.
The energy slot, the level condition hlevel, and the frame hypotheses are
carried over verbatim — none of them mentions the depth aggregation.