High-contrast homogenization: Provider.PolynomialHomogenization.Root.Corrector.GaugeSlopeResidue

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

The gauge identification reduced to one slope equality

The normalized-root pullback of the marked pair is a Liouville-class solution of the normalized affine coefficient, so reverse Liouville classification already identifies it with the reference family's joint local limit — at some slope, together with an additive constant. What is not supplied by any available ingredient is that the slope produced there is the pulled-back slope.

This module isolates exactly that. Everything else in the gauge identification of the corrector family is discharged: the elliptic representative, the Liouville input, the coefficient bridge, the value identity and the gradient identity. Two named inputs remain, one certificate-side and one analytic.

The normalized root is symmetric

theorem HCPolySupport.HighContrast.Root.matTranspose_normalizedRoot {d : ℕ} [NeZero d] {m : Mat d} (hm : Matrix.PosDef m) : matTranspose (Selection.normalizedRoot m) = Selection.normalizedRoot m

The normalized root of a positive-definite matrix is symmetric. (The same fact is proved privately upstream; it is restated here because the upstream copy is private.)

The tolerance of the reverse classification at the private exponents

The two named inputs

The reduction