Koszul flattenings of paired clusters: proof internals #

Proofs behind Complexitylib.Algebraic.LinearAlgebra.Tensor.Diagonal.Paired.

Block-triangular minors. card_mul_card_le_rank_of_det_blocks_ne_zero_of_lt: the block-diagonal certificate Matrix.card_mul_card_le_rank_of_det_blocks_ne_zero with the entries between blocks required to vanish in one direction only, for an injective order v on the blocks. The minor is block triangular (Matrix.BlockTriangular.det).
Several clusters on one slice space. choose_mul_card_le_rank_of_sum_shifts: for clusters o b (b : κ) identified slicewise, so that the tensor is ∑ b, weightedShifts (o b) (g b), and blocks q : Q of cluster c q and shift w q, the rows (σ I, w q + ∑_{σ I} o (c q)) and columns (I, w q + ∑_I o (c q)) give a minor of rank (2p+1).choose p * card Q once the entries from later blocks to earlier ones vanish. The diagonal block of q is the single-cluster block of o (c q): another cluster b would need o b t = o (c q) t (hinj).
Centers. choose_mul_card_le_rank_of_centers: the same with the shifts w q written through centers x q. If the sums ∑_K o b stay within F of |K| rr b and the offsets within G of rr b, the columns of block q lie within F of x q and its rows within F of x q + rr (c q); an entry from row block q to column block q' through cluster b then forces |x q + rr (c q) - x q' - rr b| ≤ 2F + G, unless q and q' lie in cluster b, where the shift is preserved.
Two tiles. choose_mul_le_rank_pair: for a positive cluster with median r and a negative cluster with median -s (diameters at most L), with z = r + s and the margin μ = (p + 1) L, the blocks are the centers in the four tiles P1 = [μ, s - μ), P2 = [z + μ, min (z + s) (m - r) - μ) (positive) and N2 = [z + s + μ, min (2z) m - μ), N1 = [s + μ, z - μ) (negative), ordered P1 < P2 < N2 < N1. A positive column at x meets rows near x + r and x - s, a negative one rows near x - s and x + r: the only cross entries go from P2 to P1 and from N1 to N2. The tiles have widths s, min s (m - r - z), min r (m - s - z), r, each less 2μ.
The Landsberg–Michałek tensor. The paired projection of weightedLMTensor k is the sum of the two cluster tensors; the bound Φ combines the paired bound with the single-cluster bounds n - r - p L and n - s - p L.

theorem Algebraic.Tensor3.Internal.Paired.card_mul_card_le_rank_of_det_blocks_ne_zero_of_lt {K : Type u_1} [Field K] {m : Type u_2} {n : Type u_3} [Fintype n] {ι : Type u_4} {β : Type u_5} {γ : Type u_6} [Fintype ι] [DecidableEq ι] [Fintype β] [DecidableEq β] [LinearOrder γ] (A : Matrix m n K) (f : ι → β → m) (g : ι → β → n) (v : β → γ) (hv : Function.Injective v) (hoff : ∀ (i i' : ι) (b b' : β), v b' < v b → A (f i b) (g i' b') = 0) (hdet : ∀ (b : β), (A.submatrix (fun (x : ι) => f x b) fun (x : ι) => g x b).det ≠ 0) :

Fintype.card ι * Fintype.card β ≤ A.rank

Block-triangular minors. Choose, for each block b : β, rows f i b and columns g i b of A. If every entry from a block b to a block b' with v b' < v b vanishes, for an injective v into a linear order, and every block is nonsingular, then card ι * card β ≤ rank A.