HomSeamFluxLane #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
The §4.5 duality lane, RE-INSTANTIATED at the printed field ã_{L,m} #
Why this file exists #
The lane (HomSpineRecutSupport, HomSchauderSwap) is
pinned at the UNCUT cutoff field a_L, while the manuscript runs Step 3 and
Step 4 at the flux-corrected field ã_{L,m} = a_L - (k_L - k_m)_{□_m}.
HomSeamFluxCoefficient showed the a_L-sided seam bridge is not available;
the lane is therefore re-instantiated at ã, which is what this file does.
Nothing new is estimated. Every mathematical step of the lane is already GENERIC in the coefficient:
HomCGDischargeInstantiation.exists_printedCoarseGraining_of_dirichletPairquantifies overa: CoeffOn (cubeDomain □_m);HomCGFinalLegs.weakNegDualBounds_of_smoothDualDisplayis generic ina;HomCGCarrierRHS.localCoarseGrainingLpRHS_{toReal_le,ne_top}andHomCGCarrierEnergy.weightedLocalSymmetricEnergyLp_le_ofRealare generic ina;HomSpineRecutClose.integrableOn_{self,cross}Energyare generic ina;HomStepFourEnergy.energy_splitis generic in the fieldAand reads it only throughsymmPart A = ν·Id.
The only pinned bytes were the INSTANTIATIONS, and they are re-made here at
ã, using
HomSeamFluxCoefficient.isDirichletSolutionOn_fluxCorrected_of_cutoff to
transport the spine's Dirichlet binder.
The C∇u shift never materializes (the price of the re-instantiation) #
ã∇u = a_L∇u - C∇u with C = (k_L - k_m)_{□_m} constant and skew. The shift
would cost something only if some consumer needed the flux leg in its
a_L-form. None does:
- the two weak negative-norm slots are consumed ONLY by
HomStepFourEnergy.stepFourEnergyDisplay, against the Schauder gauge of∇v, andenergy_splitsupplies the identity at whichever field is used; - the identity's left-hand side is
⨍ ν|∇u|², produced fromsymmPart(ã) = ν·Id— the SAME function as ata_L(symmPart_fluxCorrectedCoeffOn_eq_nubelow); - the Step-4 payoff and the Step-3c payoff of
HomSpineFinalEndpoint's clause supplier are coefficient-FREE (⨍ ν|∇u|²,⨍ σ|∇v|²,|u - v|).
So the whole lane moves at constant 1, and the C∇u shift is invisible at
every slot. (Consistency check: ã solves the same Dirichlet problem, so the
testing identity gives ∫_{□_m} C∇u·(∇u - ∇v) = 0, and ∫ C∇u·∇u = 0 by
skewness — the two energy splits agree term by term.)
Scope #
Nothing here is a source-facing claim. All declarations are conditional APIs
or named helpers of this tree; the printed proposition the general
coarse-graining proposition enters exactly as it does in the lane, at the same
finite p and the same constant C(p,d).
THE ν-DROP IS BLIND TO THE FLUX CORRECTION. The subtracted matrix is
constant and skew, so the symmetric part of ã_{L,m} is the symmetric part of
a_L, namely ν Id. This is the single fact that makes the Step-4 energy
identity fire at the printed field with the printed left-hand side.
2. The printed display at ã_{L,m} #
THE PRINTED FINITE-p DISPLAY, AT THE PRINT'S OWN COEFFICIENT.
The printed display at the spine's own cutoff pair, with
the coefficient slot filled by the flux-corrected field instead of the uncut
a_L. The elliptic pair fed in is still the spine's own (the root's binder is
at a_L); the transport to ã is
isDirichletSolutionOn_fluxCorrected_of_cutoff, i.e. the printed display's own
sentence. The constant is the SAME C(p,d), produced before the model and
before the coefficient.
3. The two duality legs, generic in the coefficient #
The two Step-4 duality slots from the display, GENERIC in the coefficient.
The two endpoint-level duality slots of the display, with the
coefficient slot freed: the inner producer
HomCGFinalLegs.weakNegDualBounds_of_smoothDualDisplay never looks at the
field, and the two level transports are scalar arithmetic.
4. The two legs at ã_{L,m}, from the root's own binders #
THE TWO STEP-4 DUALITY SLOTS AT THE PRINT'S COEFFICIENT.
The two duality slots at the spine's own cutoff pair, re-instantiated at
ã_{L,m}. The inputs are unchanged in kind:
- the root's two
IsDirichletSolutionOnbinders — still stated ata_L, and transported toãbyisDirichletSolutionOn_fluxCorrected_of_cutoff; - the root's
C^{0,1/2}binder on𝐠; - the four slot dominations and the
S-slot comparison, now read atã; - the arithmetic side condition
hlevelDual.
The produced flux leg carries ã∇u - σ∇v, which is exactly what the printed
Step 4 pairs against the Schauder gauge of ∇v.
5. The produced constant at ã, NAMED #
The printed coarse-graining constant C(p,d) of the ã lane, named.
The sibling of the a_L lane's coarse-graining dual-bound constant: the re-cut
bundle refers to it in the slot condition C(p,d) ≤ Ccg.
Equations
- Algsuperdiff.Section4.Provider.Homogenization.cgDualBoundConstFlux d p = if h : 2 ≤ d ∧ 2 ≤ p.exponent then Classical.choose ⋯ else 0
Instances For
The Ccg domination is free at the canonical pin.
6. The Step-4 endpoint, generic in the field #
THE STEP-4 ENDPOINT, GENERIC IN THE COEFFICIENT FIELD.
The Step-4 energy endpoint with the cutoff field replaced by an
arbitrary field whose symmetric part is ν Id. The proof is unchanged:
HomStepFourEnergy.energy_split reads the field only through hsym, and
stepFourEnergyDisplay never sees it at all. The conclusion is
coefficient-FREE.
7. Clause (C4)'s payload at ã, at the s-free Schauder constant #
CLAUSE (C4)'s PAYLOAD, AT ã_{L,m} AND THE s-FREE CONSTANT.
HomSchauderSwap.stepFourEnergy_of_dualBounds_uniform with every occurrence of
the cutoff field replaced by the printed flux-corrected field. The conclusion
is byte-identical: it never mentions a coefficient.