High-contrast homogenization: Provider.Quenched.SmallContrastRecenteredCertificates #
Imported from the Apache-2.0 HighContrastHomogenization development at commit
7a13dbcd8d6609264a713373f5c69ceeac870472.
The recentered certificates, all at one block #
hsharp and hrec were being produced at different blocks:
the Dagger gives blockSharp E ≤ E at E, while
canonicalShear_recentered_eq_zero gives vanishing shear only at the recentered
E' := Response.skewBlockCongr (canonicalShear E) E. The isotropic squared-base
weak-value bound takes one block, so one of them had to move.
The Dagger moves, and the law-side API already moves it.
coarseEllipticityDagger_recenteredLaw (HCPoly.Provider.Quenched.SmallContrastSkewDagger)
transports the Dagger to
CoarseEllipticityDagger (recenteredLaw P hg) gexp (Response.skewBlockCongr g E) Ψ K
(recenteredSource S hg)
for any skew g. At g := canonicalShear E its block is exactly E'. So
hsharp at E' follows from blockMatLoewnerLE_blockSharp_reference applied
to the transported Dagger, and's missing commutation lemma is not
needed at all: nothing about blockSharp under congruence has to be proved,
because the hypothesis that produces it travels instead.
The account then runs at the recentered law throughout and is carried back by the invariances.
The four isotropy certificates, all at the recentered block. The Dagger travels with the law; the shear vanishes; the canonical metric — and hence the adapted geometry — is unchanged.