Connection pairings and the edge-rank hypothesis

The hypothesis class of the main theorem — pairClose, the connection pairing, EdgeRankBounded and EdgeRankParameter — is defined in RS/Definitions.lean: ranks of infinite matrices are avoided by bounding the Module.rank of the range of the curried pairing.

This module proves the two facts about it: the bound weakens as the base grows (EdgeRankBounded.mono — the literature takes R ≥ 1 where the definition admits any natural number, and nothing is gained or lost), and the row-span reading agrees with the literature's supremum over finite submatrices (edgeRankBounded_iff_submatrixRank).

theorem RS.EdgeRankBounded.mono {f : ClosedFragment → ℂ} {R R' : ℕ} (hf : EdgeRankBounded f R) (hRR : R ≤ R') : EdgeRankBounded f R'

Edge-rank boundedness is monotone in the base.

def RS.SubmatrixRankBounded (f : ClosedFragment → ℂ) (t n : ℕ) : Prop

The rank condition as the literature states it, at arity t: every finite submatrix of the connection matrix — a finite set S of row fragments against a finite set T of column fragments — has rank at most n.

Equations

• RS.SubmatrixRankBounded f t n = ∀ (S T : Finset (RS.Fragment (Fin t))), (RS.submatrixOn (RS.connectionPairing f t) S T).rank ≤ n

theorem RS.edgeRankBounded_iff_submatrixRank (f : ClosedFragment → ℂ) (R : ℕ) : EdgeRankBounded f R ↔ ∀ (t : ℕ), SubmatrixRankBounded f t (R ^ t)

The two readings of the connection rank agree. Bounding the dimension of the row span of the connection pairing, as EdgeRankBounded does, is the same condition as bounding the ranks of all the finite submatrices of the connection matrix, which is how the rank of that infinite matrix is defined in the literature.