StepSevenCaccBoundaryLattice #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
The Step-7c display off the printed interior gate, at the lattice frame #
What is produced, and why the frame matters #
StepSevenCaccFinalInterior produces hcacc and
StepSevenCaccFinalDisplay produces e.gradient.with.shom under the printed
indicator's own gate z ∈ □_{m-1} together with n' ≤ m-1. Those two
hypotheses are used in exactly ONE way in the whole interior chain: through
EdFinalInputs.image_add_subset_openCubeSet_of_mem_inner, i.e. only to know
(GATE) z + □_{n'} ⊆ □_m .
This module re-proves the same two theorems with (GATE) itself as the
hypothesis. Nothing else changes: the frame stays at the printed lattice centre
z, so the coefficient family stays 𝐚_{L,mf}[Q_f](z + ·) and the hlambda
slot is discharged by the same clause-(B) record on □_{n'+1} that the interior
branch uses, with no off-grid transport and no re-gate. hosc is likewise
unmoved: the oscillation window is U_{n'}, not U_{n'+1}.
(GATE) is strictly weaker than the printed pair: for n' ≤ m-1 and z ∈ □_{m-1} one has |z_i| + ½·3^{n'} < ½·3^{m-1} + ½·3^{m-1} = 3^{m-1} ≤ ½·3^m,
so the interior branch is the special case. The centres it adds are genuine
boundary centres (z ∉ □_{m-1}) whenever ½·3^{n'} ≤ |z_i| ≤ ½·3^m − ½·3^{n'}
for some coordinate — an ℓ^∞-shell of width ½·3^m − ½·3^{n'} − ½·3^{m-1}.
What is not produced #
The centres with z + □_{n'} ⊄ □_m are not covered. Reaching them requires
moving the Caccioppoli's outer cube off the printed lattice centre (the clamp
of StepSevenCaccBoundary), and then the coefficient family is read at an
off-lattice translate, where the proved clause-(B) producer
(StepSevenLambdaGoodEvent.ae_stepSevenLambdaCaps, whose null set is indexed
by the countable family of triadic lattice points) supplies no record.
References #
- ABK26,
e.gradient.with.shom; Step 7a;l.coarse.grained.Caccioppoli.RHS.
1. The gate and its two immediate consequences #
2. The three identifications, at the gate #
The gradCore identification at the gate.
StepSevenCaccFinalInterior.sqrt_localizedCoeffEnergyValue_core_eq_nuGradNorm
with the printed pair replaced by the gate at scale j - 2.
The oscLo match at the gate.
StepSevenCaccFinalInterior.normalizedL2On_openCubeSet_sub_eq_truncatedWindow
with the printed pair replaced by the gate.
The Caccioppoli's solution object at the gate, built from t.regularity's
own Dirichlet datum and still framed at the printed lattice centre z.
3. The hcacc slot at the gate #
** gap 2 (hcacc) at the gate z + □_{n'} ⊆ □_m.**
StepSevenCaccFinalInterior.exists_stepSevenCaccHcacc_interior V — same
constant, same windows, same frame, same coefficient family — with the printed
pair z ∈ □_{m-1}, n' ≤ m-1 replaced by the single weaker gate.
4. e.gradient.with.shom at the gate #
e.gradient.with.shom at the gate, with hvol and hcacc discharged.
StepSevenCaccFinalDisplay.exists_stepSevenGradientWithShom_interior at the
weaker geometric hypothesis. Every carrier, every constant and every remaining
slot is unchanged — in particular hlambda is still asked at the family
𝐚_{L,mf}[Q_f](z + ·) framed at the printed lattice centre, and hosc is still
asked on U_{n'}.
e.gradient.with.shom at the gate, with hlambda wired in.
The derived-slot table's row 2 at the parent cube □_{n'+1}, at the same frame
the interior branch uses, so the record is the same conclusion of
StepSevenLambdaGoodEvent.ae_stepSevenLambdaCaps at the printed lattice
centre. The only surviving analytic input is hosc.