High-contrast homogenization: Entry.Analysis.ReferenceComparison

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

Reference block comparison

These are deterministic bounds for the block carriers and reference constants. The source statements are near e.reference.aspect.ratio and e.two.grid.whitney.source, p.initial.fixed.grid.scale and p.global.selection. The source argument is Lemma l.bfE.bounds of the companion paper HC. The swap, shear and Schur algebra these bounds run on is HCPoly/Entry/Analysis/BlockSwapReflection.lean.

Reference order remains an explicit premise; this module does not derive it from the dagger. Schur factorization identifies the inverse flux block, giving 1 ≤ refContrast E. An attained skew minimizer gives refContrast E ≤ aspectRatio E and strictly positive reference constants. For the comparison, positive block quadratic forms give domination by twice the scalar diagonal bounds after a skew shear. Inversion and reflection then give a 4 * aspectRatio E bound, which implies the exported, literal 6 * aspectRatio E bound. This is the direct route: the sharper HC excess estimate e.grok with coefficient 1 + 6 * (refContrast E - 1) is not delivered.

The determinant is the ordinary determinant of the full 2d matrix. Its comparison with the reciprocal determinant first bounds its square and therefore gives the printed exponent d. The weaker exponent 2 * d is recorded separately. No probability law, quantitative ellipticity constant, or annealed premise enters these bounds.

theorem HCPolySupport.HighContrast.Analysis.lambdaRef_pos {d : ℕ} [NeZero d] {E : BlockMat d} (hsymm : IsSymmetricBlockMat E) (hpos : Book.Ch02.BlockPosDef E) : 0 < lambdaRef E

The reference lower ellipticity constant is strictly positive.

theorem HCPolySupport.HighContrast.Analysis.bigLambdaRef_pos {d : ℕ} [NeZero d] {E : BlockMat d} (hsymm : IsSymmetricBlockMat E) (hpos : Book.Ch02.BlockPosDef E) : 0 < bigLambdaRef E

The attained reference upper ellipticity constant is strictly positive.

theorem HCPolySupport.HighContrast.Analysis.refContrast_le_aspectRatio {d : ℕ} [NeZero d] {E : BlockMat d} (hsymm : IsSymmetricBlockMat E) (hpos : Book.Ch02.BlockPosDef E) : refContrast E ≤ aspectRatio E

Minimizing the intrinsic contrast is bounded by the product of the two reference norms.

theorem HCPolySupport.HighContrast.Analysis.schurSigma_le_corrected {d : ℕ} {E : BlockMat d} (hs : IsSymmetricBlockMat E) (hp : Book.Ch02.BlockPosDef E) (h : Mat d) : schurSigma E ≤ skewCorrectedForm E h

The Schur complement is dominated in the Loewner order by every skew-corrected form: schurSigma E ≤ skewCorrectedForm E h for an arbitrary skew correction h.

theorem HCPolySupport.HighContrast.Analysis.one_le_refContrast {d : ℕ} [NeZero d] {E : BlockMat d} (hsymm : IsSymmetricBlockMat E) (hpos : Book.Ch02.BlockPosDef E) (horder : BlockMatLoewnerLE (ofFullBlockMat (toFullBlockMat (blockSwap d) * (toFullBlockMat E)⁻¹ * toFullBlockMat (blockSwap d))) E) : 1 ≤ refContrast E

Reference order forces the attained intrinsic contrast to be at least one.

theorem HCPolySupport.HighContrast.Analysis.one_le_aspectRatio {d : ℕ} [NeZero d] {E : BlockMat d} (hsymm : IsSymmetricBlockMat E) (hpos : Book.Ch02.BlockPosDef E) (horder : BlockMatLoewnerLE (ofFullBlockMat (toFullBlockMat (blockSwap d) * (toFullBlockMat E)⁻¹ * toFullBlockMat (blockSwap d))) E) : 1 ≤ aspectRatio E

The printed aspect ratio lower bound, under reference order.

theorem HCPolySupport.HighContrast.Analysis.aspectRatio_pos_and_three_le {d : ℕ} [NeZero d] {E : BlockMat d} (hsymm : IsSymmetricBlockMat E) (hpos : Book.Ch02.BlockPosDef E) (horder : BlockMatLoewnerLE (ofFullBlockMat (toFullBlockMat (blockSwap d) * (toFullBlockMat E)⁻¹ * toFullBlockMat (blockSwap d))) E) : 0 < aspectRatio E ∧ 3 ≤ 2 + aspectRatio E

Positivity and the lower bound for the logarithmic argument used downstream.

theorem HCPolySupport.HighContrast.Analysis.refBlock_le_six_aspectRatio_smul_swapConj {d : ℕ} [NeZero d] {E : BlockMat d} (hsymm : IsSymmetricBlockMat E) (hpos : Book.Ch02.BlockPosDef E) (horder : BlockMatLoewnerLE (ofFullBlockMat (toFullBlockMat (blockSwap d) * (toFullBlockMat E)⁻¹ * toFullBlockMat (blockSwap d))) E) : BlockMatLoewnerLE E (blockScale (6 * aspectRatio E) (ofFullBlockMat (toFullBlockMat (blockSwap d) * (toFullBlockMat E)⁻¹ * toFullBlockMat (blockSwap d))))

The printed factor-six comparison. The proof uses diagonal domination after an attained skew shear, directly; the sharper HC excess estimate e.grok is not asserted here.