High-contrast homogenization: Provider.Response.RandomAdaptedResponseCompactInsertion

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

Compact pre-Young insertion at the Schur loads

The two carried compact estimates are specialized to the independently centered primal and adjoint responses and discharged by the calibrated defect, energy, hatted-row, and weak bounds.

theorem HCPolySupport.HighContrast.Response.is_skew_mat_response_skew {d : ℕ} (K : Mat d) : IsSkewMat (responseSkew K)

The skew coordinate of a Schur block is an admissible profile gauge.