HomSpineTopScale #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
htop: the printed Step-2 top-scale datum #
What this file supplies #
HomSpineEnergySlot.energySlot_of_regularityDisplay carries exactly one
content-bearing hypothesis, htop:
3^{(1-α)X} · T.toReal ≤ recutEnergyFactor M Y m ω · energyBracket σ_m 3^{m/2} K_g K_h^∞ K_h
where T is the Theorem-C bracket. That bracket is (verbatim from
anomalous_regularity) the sum of THREE terms: the top-scale energy
√ν‖∇u‖_{L²(□_m)} and the two printed data terms √(σ_m⁻¹)3^{m/2}K_g,
√σ_m 3^{m/2}K_h. This file
- identifies the FIRST term with the left-hand side of the print's
the energy-from-data display (
ofReal_sqrtNu_mul_gradAverage— an identity: theℝ≥0∞eLpNormcarrier of the root against the REALnormalizedSetAveragecarrier ofHomStepTwoEnergy, via thevolumeAverage_eq_toReal_lintegraland theH¹integrability of|∇u|²); - absorbs the two data terms into
energyBracket— the printed bracket's own summands, at no cost, since√σ_m K_h^∞ ≥ 0(regularityDataBracket_toReal_le); - produces
htopfrom the printed top-scale energy bound (htop_of_topScaleEnergy), with the3^{(1-α)X}factor and the constant parked in the FREE slotYofrecutEnergyFactor, which is where the printedEthmB(m)carries3^{(1-α)X_m(α)}; - EXECUTES the print's own derivation of the top-scale energy bound
(
topScaleEnergy_of_stepTwoA) from the LANDEDHomStepTwoEnergy.exists_sqrt_nu_mul_gradL2_le(= the coarse-graining right-hand side + the display bounding theΛ's by the𝓔's) and TWO named bridges; - closes the INDEX bridge unconditionally in the enlarged-
Yreading (htop_of_stepTwoA_enlargedY): the two honest error indices of the two-index display are carried byYitself.
The two named bridges (nothing else is assumed) #
StepTwoDataBridge— the already-named component input:CoarseGraining's note-normalized Besov data quantities at the indextare below the printed3^{m/2}-normalized Hölder data, at the constant(1 - 3^{2t-1})^{-1/2}recorded in that correction. It needst < 1/2STRICTLY; att = 1/2theC^{0,1/2}data leg is infinite.StepTwoIndexBridge— the honest composition of the print's own inputs carries TWO error indices,t/2andt, where the printed display quotes the single1/4. Collapsing them onto1/4needs an order monotonicity of𝓔_{·,∞,2}in the UNAVAILABLE direction (theHomSeamRepin.parentTruncatedTwo_le_of_order_lebounds the HIGHER order by the LOWER one, andt/2 < 1/4for every admissiblet).htop_of_stepTwoA_enlargedYtherefore does NOT use this bridge: it enlargesYby(1 + 𝓔sup_{t/2})(1 + 𝓔sup_t), which is exactly the print's Step-1 Hölder budget applied to two more factors. The bridge is kept as a namedPropso the narrow reading (the printed single index) remains statable.
1. The top-scale carrier identity #
The gradient square of an H¹(□_m) function is integrable on the cube.
THE TOP-SCALE CARRIER IDENTITY.
The Theorem-C bracket's first term — an ℝ≥0∞ eLpNorm against the
normalized volume measure — IS the real quantity
√ν · ‖∇u‖_{L²(□_m)} that the energy-from-data display of HomStepTwoEnergy bounds.
No estimate is spent: the only steps are the real/ℝ≥0∞ average bridge and
the H¹ integrability of |∇u|².
2. The bracket, and its two data terms against energyBracket #
The Theorem-C bracket, transcribed verbatim from
anomalous_regularity: the top-scale energy plus the two printed data
terms.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The bracket is a single ENNReal.ofReal of the printed real sum.
The two data terms are inside energyBracket.
The bracket's real value is the top-scale energy plus a quantity below the
printed introduction's energy display bracket; the only slack is the √σ_m K_h^∞ summand, which the printed bracket carries and the Theorem-C one does
not.
3. htop, produced #
htop, PRODUCED.
The binder energySlot_of_regularityDisplay consumes, at the Theorem-C
bracket, from the printed top-scale energy bound. The 3^{(1-α)X} factor and
the Step-2 constant are parked in the FREE slot Y of recutEnergyFactor —
the slot the printed EthmB(m) uses for exactly that factor — together with
any extra random factor Y₀ the honest Step-2 display needs; Y₀ = 1 is the
printed reading.
4. The two named bridges of the print's Step-2 chain #
THE DATA-LEG BRIDGE (the already-named component
input). CoarseGraining's note-normalized Besov data quantities at the index t are below
the printed 3^{m/2}-normalized Hölder data of the manuscript. The correction records
the constant (1 - 3^{2t-1})^{-1/2} and the STRICT requirement t < 1/2.
THIS IS AN INPUT. It is never proved in this repository.
Equations
- One or more equations did not get rendered due to their size.
Instances For
THE INDEX BRIDGE.
The honest composition of the print's own Step-2 inputs carries TWO error
indices, t/2 on the g leg and t on the ∇h leg; the printed display
quotes the single 1/4. This Prop is the collapse onto a common factor W.
At W:= (1 + 𝓔sup_{1/4}) the collapse is exactly what the print asserts and is
NOT available (see the module docstring); htop_of_stepTwoA_enlargedY avoids it
by carrying W = (1 + 𝓔sup_{t/2})(1 + 𝓔sup_t)(1 + 𝓔sup_{1/4}) instead, at
Kidx = 1.
Equations
- One or more equations did not get rendered due to their size.
Instances For
5. The print's Step-2 chain, executed #
STEP 2, EXECUTED.
The print's own derivation, on the carriers: the LANDED
exists_sqrt_nu_mul_gradL2_le (= the coarse-graining right-hand side + the
display bounding the Λ's by the 𝓔's), the data-leg bridge and the index
bridge compose into the printed top-scale energy bound at the explicit constant
C_step (t^{-3/2} + t^{-1/2}) √(2d) · K_idx · C_data.
Nothing else is used; the t-powers and the √(2d) are CoarseGraining's own
and stay displayed .
6. The index bridge, CLOSED at the enlarged Y #
The enlargement of the printed Y slot.
EthmB(m)'s Y slot carries 3^{(1-α)X_m(α)}; the honest two-index Step-2
display asks it to carry, in addition, the two sup_{L ≥ m} error factors at
the display's OWN indices t/2 and t. That is exactly two more factors for
the print's Step-1 Hölder budget, and no new object: the factors are the
public observable at two more orders.
Equations
- One or more equations did not get rendered due to their size.
Instances For
THE INDEX BRIDGE, CLOSED — at the enlarged Y and at K_idx = 1.
No order monotonicity of 𝓔_{·,∞,2} is used: each honest index is carried by
its OWN factor of stepTwoEnlargedY, and le_fluxCorrectedTwoScaleError ObservableSup supplies the sup_{L ≥ m} step. The two hrep hypotheses are
the standard a.e. carrier identification
(Support.fluxCorrectedError_ae_eq_representative), not new content.
7. htop, with the index bridge discharged #
htop, PRODUCED FROM THE PRINT'S OWN STEP-2 CHAIN.
Sections 5 and 6 composed into section 3: the binder
energySlot_of_regularityDisplay consumes, at the Theorem-C bracket, from
- the LANDED the coarse-graining right-hand side + the display bounding the
Λ's by the𝓔's composition (exists_sqrt_nu_mul_gradL2_le), - the ONE named data-leg input
StepTwoDataBridge, - the standard a.e. carrier identification
hrep1/hrep2, and - three a.e. finiteness cuts.
NO order monotonicity of 𝓔_{·,∞,2} is used: the printed Y slot is enlarged
by stepTwoEnlargedY, which is the two honest indices of the two-index display
carried where the print carries 3^{(1-α)X_m(α)}.