Coarse-graining support:

Support.Deterministic.CoarseCaccioppoli.SingleCubeToRaw.HarmonicFinal.InputSpecializations .NoteRawBridge.BoundarySplit

Imported from the Apache-2.0 CoarseGraining development at commit c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4.

theorem HCPolySupport.CoarseCaccioppoliBoundaryCanonicalHarmonicVectorNoteRawBridgeSplitAllRadii.of_constantFamily_bufferedSmallCubeCoefficientBoundsSplitAllRadii {d : ℕ} [NeZero d] (Q : TriadicCube d) (a : CoeffField d) (s t Clocal Calpha Ccross : ℝ) {lam Lam : ℝ} (u0 : AHarmonicFunction a (openCubeSet Q)) (hClocal : 0 ≤ Clocal) (_hCalpha : 0 ≤ Calpha) (hCcross : 0 ≤ Ccross) (hCsol_le : fullVectorPoincareCubeConstant Q ≤ Clocal) (hs : 0 < s) (ht : 0 < t) (hst : s + t < 1) (hEllCube : IsEllipticFieldOn lam Lam (cubeSet Q) a) (hrawcoeff : boundaryCaccioppoliSmallCubeCoefficientSplitAllRadii Q a s t Clocal Calpha Ccross) : CoarseCaccioppoliBoundaryCanonicalHarmonicVectorNoteRawBridgeSplitAllRadii Q a s t Calpha Ccross (coarseCaccioppoliHarmonicL2Sq Q a u0) fun (x : Vec d) => scalarVariationEnergyIntegrand a u0 x

All-radii boundary raw bridge for a constant harmonic family using the split buffered localized-energy summation.

This is the proof-producing bridge needed by the standard beta-dependent radius iteration. It is the all-radii version of CoarseCaccioppoliBoundaryCanonicalHarmonicVectorNoteRawBridgeSplit.of_smallCubeBoundsSplit.

theorem HCPolySupport.CoarseCaccioppoliBoundaryCanonicalHarmonicVectorNoteRawBridgeSplit.of_smallCubeBoundsSplit {d : ℕ} [NeZero d] (Q : TriadicCube d) (a : CoeffField d) (s t Clocal Calpha Ccross : ℝ) {lam Lam : ℝ} (u0 : AHarmonicFunction a (openCubeSet Q)) (hClocal : 0 ≤ Clocal) (_hCalpha : 0 ≤ Calpha) (hCcross : 0 ≤ Ccross) (hCsol_le : fullVectorPoincareCubeConstant Q ≤ Clocal) (hs : 0 < s) (ht : 0 < t) (hst : s + t < 1) (hEllCube : IsEllipticFieldOn lam Lam (cubeSet Q) a) (hrawcoeff : BoundaryCaccioppoliHarmonicVectorSmallCubeCoefficientSplit Q a s t Clocal Calpha Ccross) : CoarseCaccioppoliBoundaryCanonicalHarmonicVectorNoteRawBridgeSplit Q a s t Calpha Ccross (coarseCaccioppoliHarmonicL2Sq Q a u0) fun (x : Vec d) => scalarVariationEnergyIntegrand a u0 x

Boundary raw bridge for a constant harmonic family using the split buffered localized-energy summation.

This is the split-budget version of of_constantFamily_bufferedFaithfulWorkSmallCubeExactRawCoefficientBounds_of_closedCubeEllipticity: the explicit height and absorption coefficient use Calpha, while the cross branch uses Ccross.