High-contrast homogenization: Provider.PolynomialHomogenization.Root.Dirichlet.PerGOrderGapAudit

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

The gap between the row order and twice the response order

The row order and the response order of the printed route are distinct affine functions of the exponent, and the geometric factor that closes every descendant sum in the certificate chain is read at their difference. The difference is strictly positive on the whole admissible window and degenerates only at its excluded right endpoint, where the geometric factor has no value.

The estimate below fixes that: the row order is strictly below twice the certificate order and strictly below twice the response-window order, at every admissible exponent, with the gaps computed exactly; and the geometric factor of the absorption prefactor is therefore positive.

The exact gaps

theorem HCPolySupport.HighContrast.RowSupply.two_mul_responseWindowOrder_sub_printRowOrder (g : ℝ) : 2 * responseWindowOrder g - Certificate.printRowOrder g = (1 - g) / 8

The gap between twice the response-window order and the row order is (1 - g) / 8.

The geometric factor of the absorption prefactor

theorem HCPolySupport.HighContrast.RowSupply.one_sub_rpow_neg_gap_pos_responseWindow {g : ℝ} (hg : g < 1) : 0 < 1 - 3 ^ (-(2 * responseWindowOrder g - Certificate.printRowOrder g))

The geometric factor that closes the descendant sums is positive exactly because the gap above is positive. This discharges the hypothesis of the prefactor estimate at the printed orders.