High-contrast homogenization: Provider.PolynomialHomogenization.Root.RowSupply.DatumRowAggregation

Imported from the Apache-2.0 HighContrastHomogenization development at commit 7a13dbcd8d6609264a713373f5c69ceeac870472.

Datum-row aggregation over the enlarged-margin ruled carrier

The per-cell mismatch between the L² price and the fractional-energy weights is bounded because ruledCellScale_lt_two_mul_Rad bounds every selected Whitney scale by the sandwich radius.

Route

1. scale bound — physicalFullDualL2Constant d (whitneyCellCube system i) s = fullDualL2AmplitudeV2 d s * cubeScaleFactor (whitneyCellCube system i) ^ s, and cubeScaleFactor (whitneyCellCube system i) = 3 ^ system.scale i < 2 Rad, so every cell constant is under the uniform fullDualL2AmplitudeV2 d s * (2 Rad) ^ s;
2. disjoint-cell summation — the selected cells are pairwise disjoint, measurable, and exhaust U up to a null set, so ∑ᵢ ∫⁻_{cellᵢ} |∇h|² = ∫⁻_U |∇h|²;
3. volume-weight absorption — hsNormSq U s h.grad carries volume U ^ (-(2s)/d) · eVolumeAverage U |∇h|², so the average is recovered at the cost of volume U ^ ((2s)/d), a Rad-bounded factor that C₀ s rho Rad absorbs.

None of the three is an oscillation estimate.

theorem HCPolySupport.HighContrast.RowSupply.ruledCellScale_lt_two_mul_Rad {d : ℕ} [NeZero d] {U : Set (Vec d)} {rho Rad : ℝ} (hRad : 0 ≤ Rad) (system : EnlargedMarginRuledTriadicWhitneySystem U rho Rad) (hU : IsOpen U) (i : system.CellIndex) : 3 ^ system.scale i < 2 * Rad

Every selected enlarged-margin Whitney cell has scale bounded by twice the outer sandwich radius.

The uniform cell constant

The cube-average to lintegral bridge

The aggregation