StepSevenCaccFinalInterior #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
1. The interior geometry #
The concentric Caccioppoli core is the cube two scales down. At the
Dirichlet-patch centre x = 0 the lemma's core □_Q ∩ (x + □_{Q.scale-2}) is
□_{j-2} — the set the §4.4 volume step passes to.
The Dirichlet-patch binder at the concentric centre, discharged: the patch
0 + □_{j-1} sits inside □_j.
The window IS the cube on the interior branch. For z ∈ □_{m-1} and j ≤ m-1 the truncation is inert: U_j = (z+□_j) ∩ □_m = z + □_j.
2. The display's own gradient scalar #
ν^{1/2}‖∇u‖_{L²(V)}, the left-hand side of e.gradient.with.shom and
the Caccioppoli's core energy, as ONE named scalar: for the §4.4 family
𝐚_{L,k} = ν I + 𝐤 with 𝐤 antisymmetric the symmetric coefficient energy IS
ν ⨍|∇u|².
Equations
- Algsuperdiff.Section4.Provider.Regularity.stepSevenNuGradNorm nu V G = √(nu * HCPolySupport.volumeAverage V fun (x : HCPolySupport.Vec d) => HCPolySupport.vecNormSq (G x))
Instances For
The named scalar IS the root display's own left-hand side.
RootAssemblyConditional.RootLatticeDisplay writes the same quantity as √ν · ‖ |∇u| ‖_{L²(V)} with the pointwise Euclidean norm inside; the two agree
exactly.
The named scalar in the ratio spelling's volume step uses.
3. The gradCore identification #
** residue, the gradCore identification.**
The Caccioppoli's left-hand side, read at the concentric patch centre in the
translated frame, IS the display's ν^{1/2}‖∇u‖_{L²(U_{j-2})} on the §4.4
window: the ν-identification removes the coefficient and the translation
transport moves the frame, both without constants. v is the transported
solution (v = u(·+z), ∇v = ∇u(·+z) — the builder's own two clauses).
4. The oscLo match #
** residue, the cube-versus-window oscLo match.**
5. hvol with the mass monotonicity discharged #
The gradient square of an H¹(□_m) function is integrable on every subset of
□_m.
's mass comparison, discharged. (b)'s integral monotonicity I_S ≤ I_T on
nested windows is not an estimate: the integrand is a square and u ∈ H¹(□_m).
hvol at the §4.4 carriers ((b)), unconditional.
ν^{1/2}‖∇u‖_{L²(U_{n+1})} ≤ 3^{(d/2)(n'-n)} · ν^{1/2}‖∇u‖_{L²(U_{n'-2})} .
The volume-factor producer with its one caller-side input — the mass comparison
— discharged from u ∈ H¹(□_m). The side condition n+1 ≤ n'-2 is free at
the Step-7a selection.
6. The hcacc slot at the §4.4 interior carriers #
The hcacc slot on the interior branch.
l.coarse.grained.Caccioppoli.RHS at the §4.4 exponent pin, in the energy-norm
shape StepSevenCaccGradient.stepSevenGradientWithShom consumes, with every
scalar read on the §4.4 windows:
ν^{1/2}‖∇u‖_{L²(U_{n'-2})}
≤ Ccacc · ( √λ_{1/8,1} · 3^{-n'}‖u - (u)_{U_{n'}}‖_{L²(U_{n'})} )
+ Ccacc · dataM ,
Ccacc = √(caccioppoliWithRHSPrefactor C □_{n'} 𝐚 (1/4) (1/8)) ,
dataM = √(F · λ_{1/8,1}^{-1}) · [𝐠]_{B^{1/4}(□_{n'})} .
Conditional on NOTHING beyond the pinned lemma's own equation and forcing
binders and the printed interior gate z ∈ □_{m-1}: the Dirichlet patch is
discharged at the concentric centre, the window/cube and frame identifications
are the exact equalities of §§1--4, and the ∇h summand of the printed display
is absent exactly because the gate is the printed indicator's own condition (
residue).
** residue, the Gagliardo ↔ ForceBesovRegularity bridge, at the Step-7c
interior carriers.**
The §4.4 forcing datum is carried on □_m as the manuscript's 𝐠 ∈ H^{1/4}
(MemLp for the normalized cube measure and for the Gagliardo product measure
— literally the two MemLp binders the Step-6 interior endpoint carries), while
l.coarse.grained.Caccioppoli.RHS asks for CoarseGraining's
ForceBesovRegularity
at the good-scale cube in the translated frame. No new analysis, and no
constant.
8. The transported solution of the good-scale cube #
StepSevenGradForcedSolution.isForcedEquation_fluxCorrected_of_subset
re-derived with the flux-correction parameters (scale, cube) left free
instead of pinned to the solution cube's own (k, □_k). The freedom is what
lets the clause-(B) producer
(StepSevenLambdaEndpoint.ae_stepSevenLambdaSlots, which caps the family (k, □_k) on the cube □_{k-1}) and the good-scale Caccioppoli (whose cube is
□_{n'}) speak about one family: take (mf, Qf) = (n'+1, □_{n'+1}). A
re-derivation, not a new statement.
The Caccioppoli's solution object, built from t.regularity's own
Dirichlet datum on the interior branch.
At z ∈ □_{m-1} and n' ≤ m-1 the translate z + □_{n'} sits inside □_m,
so the transport applies at the lattice centre z itself — no clamp, no off-grid
centre. The flux pair (mf, Qf) is free, so the caller may take the pair the
clause-(B) caps are stated at. The two frame identities the hcacc producer
consumes are the proved untranslate clauses.