HomSpineRepChain #

Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.

Theorem B, §4.5, Step 3c: the chain endpoint with NO representative binder #

What this module is #

HomSpineRepLimit produces a continuous representative from the negative-order gauge alone. This module wires that producer into the two places the chain assumed one:

HasContinuousRepresentative — the residue predicate — is now a THEOREM under the gauge (hasContinuousRepresentative_of_uniformBoxGauge);
the finite-p L^∞ conversion — whose three binders hgc, hgw, hzero carried the representative and its face vanishing — is restated with those three binders GONE and the conclusion at the a.e.-defined w itself.

The face vanishing hzero is not lost: it is the derived faceZero_of_continuousRepresentative, applied to the representative this module produces. The only new hypothesis is hWzero (w vanishes off the open cube), which the H¹₀ zero extension supplies and which the frame already carries.

The shape of the endpoint #

  3^{-m}|w x| ≤ 96 d² · liftGeomFactor (s + d/p) · A     for a.e. x ∈ □_m

— the same display as the conversion theorem, with g replaced by w. The two agree a.e., so the restricted a.e. statement transfers verbatim; the consumer (clause (C3)) reads |u - v| on the open cube, where w IS u - v.

References #

ABK26, Theorem B Step 3.

1. The residue, discharged #

source

theorem Algsuperdiff.Section4.Provider.Homogenization.hasContinuousRepresentative_of_uniformBoxGauge {d : ℕ} {m : ℤ} {s A : ℝ} {w : HCPolySupport.Vec d → ℝ} {G : HCPolySupport.Vec d → HCPolySupport.Vec d} (hw : HCPolySupport.HasWeakGradientOn Set.univ w G) (hwI : MeasureTheory.Integrable w MeasureTheory.volume) (hwc : HasCompactSupport w) (hGI : ∀ (i : Fin d), MeasureTheory.Integrable (fun (y : HCPolySupport.Vec d) => G y i) MeasureTheory.volume) (hgauge : UniformBoxGaugeBound m s A G) (hs0 : 0 < s) (hs2 : s ≤ 1 / 2) :

HasContinuousRepresentative w

the residue, as a theorem.

HasContinuousRepresentative w — the ONE irreducible frame item of the §4.5 spine — holds under the translate-uniform negative gauge on ∇w together with the integrability and compact support the H¹₀ zero extension already supplies. This is HomSpineRepLimit.exists_continuous_ae_eq_of_uniformBoxGauge read in the vocabulary of HomSpineFrameData.