Step3BlockSplit #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
Step 3 at the block response maximum: the split applied, both legs supplied #
Nothing here imports that file, and nothing here claims the anchor.
What this module does #
Step3HSlot.exists_responseJ_step3_recentered supplies the field leg of
the primal/adjoint split e.bfJ.general, proved here as
Annular.normalizedBlockResponseMax_isotropicComparator_le at constant 1: an
e-free bound on J(3^j v + □_j, σ_m^{-1/2} e, σ_m^{1/2} e; ã_{L,m}). The
split also needs the transpose leg, at ã_{L,m}ᵗ.
The transpose leg is supplied here by ONE per-cube specialization of the proved
lattice-level negation calculus of Annular/TransposeDischarge.lean: at the
negated sample Nω = −ω the coefficient field transposes,
ã_{L,m}(Nω)(x) = ã_{L,m}(ω)(x)ᵗ (`subConstCutoffField_negateCutoffSample`)
This is the author's (J3) symmetry route, exactly as §4.1 discharges its
hpret/huglyt slots at the lattice level; nothing new is assumed, and NO
probabilistic input enters: the statements below are pointwise in ω. (The
law-level invariance Cutoff.map_negateCutoffSample_cutoffSampleLaw is what a
later expectation step uses to make the Nω leg cost nothing; it is not used,
and not needed, here.)
Combining the two legs with the proved split, and rewriting the left-hand side
through the family bridge of FamilyBridge.lean, bounds the Step-1 endpoint's
per-cube object Ch02.normalizedBlockResponseMax R (a_L − (k_L−k_m)_{□_m}) σ_m Id by the sum of Step 3's display at ω and at Nω.
Annular.scalarResponseMax_le_normalizedBlockResponseMax runs the W WAY for
this purpose (it bounds the scalar maximum by the block maximum); the split
above is the only proved route from scalar J-displays to the block maximum.
Deviations, all inherited #
Every deviation of Step3HSlot.lean is inherited verbatim -- in particular the
ruled gapped gauge s = 2γ (exponents 2s/(1−4γ) and 4γ/(1−4γ), λ-slots
at unitCubeLambda (2γ); A9 direction warning: the display can never be read
back at gauge γ) and the unit-cube gauges of the Section 2.4 anchor. The s ≤ 1/4 and γ ≤ 1/8 binders are free at §4.5's own ranges. Nothing new is
introduced here: step3Display is a name for the right-hand side of
exists_responseJ_step3_recentered, at the cube R = ⟨R.scale, R.index⟩ and
the recentering index m.
Main results #
responseJ_subConstFlux_transpose_eq_negate— the per-cube negation identity: the transposed response atωis the field response atNω.normalizedBlockResponseMax_subConstFlux_le_of_bounds— the proved split with its transpose leg pre-rewritten: two hypotheses (atωand atNω) bound the block maximum byJf + Jt.exists_normalizedBlockResponseMax_step3_split— the two legs discharged by Step 3's display, with the left-hand side at the endpoint's carrier family.
References #
- ABK26,
l.bounds.mathcal.E.aL, (Step 3);e.bfJ.general; (the transposed annulus maximum).
The per-cube negation identity #
ã_{L,m} at Nω is ã_{L,m}ᵗ at ω, at one cube. The a.e. field
identity behind the transpose leg; the proved field identity
Annular.subConstCutoffField_negateCutoffSample read through the definitional
coeffOn-characterization of the hand-built family.
The per-cube transpose leg. The transposed response functional at ω is
the untransposed response functional at the negated sample Nω, at every cube and
at every pair of loads.
The split, with the transpose leg pre-rewritten #
The proved primal/adjoint split, at the development carrier, with the transpose leg read at the negated sample.
Annular.normalizedBlockResponseMax_isotropicComparator_le (e.bfJ.general,
constant 1) asks for a bound on the field response and a bound on the
transposed field response. By the per-cube negation identity the second is a
bound on the field response at Nω; so both hypotheses below are displays,
which is exactly what Step3HSlot.lean produces.
Step 3's display, named #
The recentered skew shell perturbation of Step 3: h = k_L − k_{j−2} − (k_L − k_m)_{□_m} at the cube R, with the recentering constant folded into the
unit-cube perturbation. A spelling abbreviation for the object appearing in
Step3HSlot.exists_responseJ_step3_recentered.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Step 3's display, named. The right-hand side of
Step3HSlot.exists_responseJ_step3_recentered at the cube R: the three
printed summands of e.apply.sensitivity.J.aL, in the anchor's unit-cube
gauges and at the ruled gapped gauge s = 2γ. It does not mention e.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The two legs discharged #
The constant is the Section 2.4 anchor's own, taken from
Step3HSlot.exists_responseJ_step3_recentered; the field leg is that theorem
at ω, the transpose leg is that theorem at Nω composed with the per-cube
negation identity, and the left-hand side is moved to the endpoint's carrier by
the family bridge FamilyBridge.normalizedBlockResponseMax_fluxCorrected_eq.
Pointwise in ω: no event, no probability, no stationarity, no z-collapse.