High-contrast homogenization: Geometry.BlockBridge

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

The bridge between the two block dialects

A doubled block matrix is carried in two equivalent ways. The structural carrier BlockMat d records the four d × d corners separately and comes with its own multiplication, transpose, inverse, dilation, reflection, quadratic-form order BlockMatLoewnerLE, and positivity predicate BlockPosDef. The flattened carrier FullBlockMat d = Matrix (BlockCoord d) (BlockCoord d) ℝ is a genuine matrix ring over the doubled index type, so it carries mathlib's multiplication, inverse, Loewner order, PosDef, and square root; the canonical block geometry of e.scale.selection.canonical.metric is developed there.

This file shows that the flattening map toFullBlockMat identifies the two: it is a ring isomorphism onto FullBlockMat d sending each structural operation to its matrix counterpart, and — on symmetric data — it identifies BlockMatLoewnerLE with the Loewner order and BlockPosDef with PosDef.

Symmetry is needed for one direction only. A Loewner inequality between flattened matrices always implies the corresponding inequality of quadratic forms; the converse needs the difference to be Hermitian, which for real data is exactly the symmetry of the two blocks. This asymmetry is recorded in the two one-directional lemmas, and blockMatLoewnerLE_iff_le assumes symmetry of both arguments.

The final section transports the primal-adjoint involution H^♯ = R H^{-1} R, formed with the swap matrix R of s.scale.selection. The structural blockSharp and the flattened fullBlockSharp correspond under the bridge with no hypotheses at all, so its rules — involution, order reversal, homogeneity of degree minus one — become available in the structural dialect by transport.

Structure transport

toFullBlockMat is the map that assembles the four corners into one matrix over the doubled index type; it is mathlib's Matrix.fromBlocks.

theorem HCPolySupport.HighContrast.toFullBlockMat_eq_fromBlocks {d : ℕ} (A : BlockMat d) : toFullBlockMat A = Matrix.fromBlocks A.upperLeft A.upperRight A.lowerLeft A.lowerRight

The flattening map is Matrix.fromBlocks on the four corners.

theorem HCPolySupport.HighContrast.toFullBlockMat_injective {d : ℕ} : Function.Injective toFullBlockMat

The flattening map is injective; ofFullBlockMat is its inverse.

theorem HCPolySupport.HighContrast.toFullBlockMat_blockMatMul {d : ℕ} (A B : BlockMat d) : toFullBlockMat (Book.Ch02.blockMatMul A B) = toFullBlockMat A * toFullBlockMat B

Flattening turns the structural product into the matrix product.

theorem HCPolySupport.HighContrast.toFullBlockMat_blockDiag {d : ℕ} (A B : Mat d) : toFullBlockMat (Book.Ch02.blockDiag A B) = Matrix.fromBlocks A 0 0 B

Flattening turns the structural block diagonal into Matrix.fromBlocks.

theorem HCPolySupport.HighContrast.toFullBlockMat_blockIdentity {d : ℕ} : toFullBlockMat (Book.Ch02.blockIdentity d) = 1

Flattening turns the structural identity into the matrix identity.

theorem HCPolySupport.HighContrast.toFullBlockMat_blockMatTranspose {d : ℕ} (A : BlockMat d) : toFullBlockMat (Book.Ch02.blockMatTranspose A) = Matrix.transpose (toFullBlockMat A)

Flattening turns the structural transpose into the matrix transpose.

theorem HCPolySupport.HighContrast.toFullBlockMat_blockMatTranspose_conj {d : ℕ} (A : BlockMat d) : toFullBlockMat (Book.Ch02.blockMatTranspose A) = Matrix.conjTranspose (toFullBlockMat A)

Over the reals the structural transpose is the conjugate transpose of the flattened matrix.

theorem HCPolySupport.HighContrast.toFullBlockMat_blockMatInv {d : ℕ} (A : BlockMat d) : toFullBlockMat (Book.Ch02.blockMatInv A) = (toFullBlockMat A)⁻¹

Flattening turns the structural inverse into the matrix inverse. The structural inverse is defined by flattening, inverting and unflattening, so this is the round trip.

theorem HCPolySupport.HighContrast.toFullBlockMat_blockScale {d : ℕ} (c : ℝ) (A : BlockMat d) : toFullBlockMat (blockScale c A) = c • toFullBlockMat A

Flattening turns the structural dilation into the scalar action.

theorem HCPolySupport.HighContrast.toFullBlockMat_blockR {d : ℕ} : toFullBlockMat (Book.Ch02.blockR d) = fullBlockRefl d

Flattening turns the structural reflection matrix R into fullBlockRefl.

theorem HCPolySupport.HighContrast.toFullBlockMat_blockG {d : ℕ} (h : Mat d) : toFullBlockMat (Book.Ch02.blockG h) = fullBlockShear h

Flattening turns the structural shear G_h into fullBlockShear.

theorem HCPolySupport.HighContrast.toFullBlockMat_blockReflect {d : ℕ} (A : BlockMat d) : toFullBlockMat (blockReflect A) = fullBlockRefl d * toFullBlockMat A * fullBlockRefl d

Flattening turns the structural corner swap into conjugation by R.

Symmetry and the quadratic form

theorem HCPolySupport.HighContrast.blockMatEntry_eq_toFullBlockMat {d : ℕ} (A : BlockMat d) (α β : BlockCoord d) : blockMatEntry A α β = toFullBlockMat A α β

The structural entry function is the entry function of the flattened matrix.

theorem HCPolySupport.HighContrast.isSymm_toFullBlockMat {d : ℕ} {A : BlockMat d} (hA : IsSymmetricBlockMat A) : Matrix.IsSymm (toFullBlockMat A)

Structural symmetry is symmetry of the flattened matrix.

theorem HCPolySupport.HighContrast.isHermitian_toFullBlockMat {d : ℕ} {A : BlockMat d} (hA : IsSymmetricBlockMat A) : Matrix.IsHermitian (toFullBlockMat A)

Structural symmetry makes the flattened matrix Hermitian.

theorem HCPolySupport.HighContrast.blockVecDot_blockMatVecMul_eq_dotProduct {d : ℕ} (A : BlockMat d) (X : BlockVec d) : blockVecDot X (blockMatVecMul A X) = toFullBlockVec X ⬝ᵥ Matrix.mulVec (toFullBlockMat A) (toFullBlockVec X)

The structural quadratic form is the flattened quadratic form.

theorem HCPolySupport.HighContrast.toFullBlockVec_eq_zero_iff {d : ℕ} (X : BlockVec d) : toFullBlockVec X = 0 ↔ X = 0

Flattening a doubled vector detects vanishing.

Order transport

Only the passage from the quadratic-form order to the Loewner order needs symmetry, and it needs it on both arguments: the Loewner order is defined by positive semidefiniteness of the difference, and a real matrix is positive semidefinite only if it is symmetric.

theorem HCPolySupport.HighContrast.blockMatLoewnerLE_of_le {d : ℕ} {A B : BlockMat d} (h : toFullBlockMat A ≤ toFullBlockMat B) : BlockMatLoewnerLE A B

The Loewner order implies the quadratic-form order. No symmetry hypothesis is needed in this direction.

theorem HCPolySupport.HighContrast.posSemidef_toFullBlockMat_sub_of_blockMatLoewnerLE {d : ℕ} {A B : BlockMat d} (hA : IsSymmetricBlockMat A) (hB : IsSymmetricBlockMat B) (h : BlockMatLoewnerLE A B) : Matrix.PosSemidef (toFullBlockMat B - toFullBlockMat A)

The difference of two symmetric blocks is positive semidefinite as soon as the quadratic forms compare. This is the intermediate through which the order transport runs.

theorem HCPolySupport.HighContrast.le_of_blockMatLoewnerLE {d : ℕ} {A B : BlockMat d} (hA : IsSymmetricBlockMat A) (hB : IsSymmetricBlockMat B) (h : BlockMatLoewnerLE A B) : toFullBlockMat A ≤ toFullBlockMat B

The quadratic-form order implies the Loewner order, for symmetric blocks.

theorem HCPolySupport.HighContrast.blockMatLoewnerLE_iff_le {d : ℕ} {A B : BlockMat d} (hA : IsSymmetricBlockMat A) (hB : IsSymmetricBlockMat B) : BlockMatLoewnerLE A B ↔ toFullBlockMat A ≤ toFullBlockMat B

The two orders agree on symmetric blocks.

theorem HCPolySupport.HighContrast.blockPosDef_iff_posDef {d : ℕ} {A : BlockMat d} (hA : IsSymmetricBlockMat A) : Book.Ch02.BlockPosDef A ↔ Matrix.PosDef (toFullBlockMat A)

The two positivity predicates agree on symmetric blocks.

theorem HCPolySupport.HighContrast.posDef_toFullBlockMat {d : ℕ} {A : BlockMat d} (hA : IsSymmetricBlockMat A) (hpd : Book.Ch02.BlockPosDef A) : Matrix.PosDef (toFullBlockMat A)

Positive definiteness of a symmetric block transports to the flattened matrix.

The sharp involution

The structural sharp is the corner swap of the structural inverse; flattening turns the corner swap into conjugation by R and the structural inverse into the matrix inverse, so it agrees exactly with fullBlockSharp.

theorem HCPolySupport.HighContrast.toFullBlockMat_blockSharp {d : ℕ} (H : BlockMat d) : toFullBlockMat (blockSharp H) = fullBlockSharp (toFullBlockMat H)

The sharp map is the same on both carriers.

theorem HCPolySupport.HighContrast.blockSharp_blockSharp {d : ℕ} {H : BlockMat d} (hH : IsSymmetricBlockMat H) (hpd : Book.Ch02.BlockPosDef H) : blockSharp (blockSharp H) = H

The sharp map is an involution, in the structural dialect.

theorem HCPolySupport.HighContrast.blockMatLoewnerLE_blockSharp_of_le {d : ℕ} {H K : BlockMat d} (hH : IsSymmetricBlockMat H) (hK : IsSymmetricBlockMat K) (hHpd : Book.Ch02.BlockPosDef H) (hKpd : Book.Ch02.BlockPosDef K) (h : BlockMatLoewnerLE H K) : BlockMatLoewnerLE (blockSharp K) (blockSharp H)

The sharp map reverses the order, in the structural dialect.

theorem HCPolySupport.HighContrast.blockSharp_blockScale {d : ℕ} {H : BlockMat d} (hH : IsSymmetricBlockMat H) (hpd : Book.Ch02.BlockPosDef H) {c : ℝ} (hc : 0 < c) : blockSharp (blockScale c H) = blockScale c⁻¹ (blockSharp H)

The sharp map is homogeneous of degree minus one, in the structural dialect.