Modular meaning of the native instance matrices

The active middle positions use the ordinary flattening vertex * p + label. The left and right zero/one entries test exactly the two modular adjacency relations of lopInstance. The remaining positions are zero. All residues here are Euclidean natural residues of signed weights, as produced by the existing native signed-residue kernel.

Main results

• MatrixSpec.left_entry: left adjacency is label ≡ weight + rho.
• MatrixSpec.right_entry: right adjacency is label ≡ -weight.
• MatrixSpec.left_padding, MatrixSpec.right_padding: padded middle positions are zero.
• MatrixSpec.left_lopInstance, MatrixSpec.right_lopInstance: raw matrix ones are exactly the corresponding edges of the existing finite lopsided instance.

theorem Cslib.Algorithms.WordRAM.ExactTriangle.MatrixSpec.left_entry (A : WriteMatrices.Args) (R : ℕ → ℕ) (a : Fin A.n) (v : Fin A.length) (label : Fin A.p) (hpad : A.length * A.p ≤ A.D) (w : ℤ) (hR : R (↑a * A.n + A.first + ↑v) = w.natMod ↑A.p) : WriteMatrices.entry false A R (↑a * A.D + (↑v * A.p + ↑label)) = if ↑↑label ≡ w + ↑A.rho [ZMOD ↑A.p] then 1 else 0

The native left matrix has exactly the intended modular adjacency at every active middle vertex. Pointers do not enter this semantic assertion.

theorem Cslib.Algorithms.WordRAM.ExactTriangle.MatrixSpec.right_entry (A : WriteMatrices.Args) (R : ℕ → ℕ) (b : Fin A.n) (v : Fin A.length) (label : Fin A.p) (w : ℤ) (hR : R (↑b * A.n + A.first + ↑v) = w.natMod ↑A.p) : WriteMatrices.entry true A R ((↑v * A.p + ↑label) * A.n + ↑b) = if ↑↑label ≡ -w [ZMOD ↑A.p] then 1 else 0

The right matrix uses the negated B–C weight and the transposed residue lookup.

theorem Cslib.Algorithms.WordRAM.ExactTriangle.MatrixSpec.left_padding (A : WriteMatrices.Args) (R : ℕ → ℕ) (a : Fin A.n) (middle : Fin A.D) (hpad : A.length ≤ ↑middle / A.p) : WriteMatrices.entry false A R (↑a * A.D + ↑middle) = 0

A padded middle column is zero even if its input residue would otherwise match.

theorem Cslib.Algorithms.WordRAM.ExactTriangle.MatrixSpec.right_padding (A : WriteMatrices.Args) (R : ℕ → ℕ) (b : Fin A.n) (middle : Fin A.D) (hpad : A.length ≤ ↑middle / A.p) : WriteMatrices.entry true A R (↑middle * A.n + ↑b) = 0

A padded middle row of the right matrix is zero.

theorem Cslib.Algorithms.WordRAM.ExactTriangle.MatrixSpec.left_lopInstance (A : WriteMatrices.Args) (R : ℕ → ℕ) (wAB wBC wAC : Fin A.n → Fin A.n → ℤ) (g chunk k : ℕ) (rho : Fin A.p) (hrho : A.rho = ↑rho) (a c : Fin A.n) (v : Fin A.length) (label : Fin A.p) (hpiece : c ∈ ExactTriangle.piece A.n A.D g k) (hvertex : A.first + ↑v = ↑c) (hpad : A.length * A.p ≤ A.D) (hR : ∀ (a c : Fin A.n), R (↑a * A.n + ↑c) = (wAC a c).natMod ↑A.p) : WriteMatrices.entry false A R (↑a * A.D + (↑v * A.p + ↑label)) = 1 ↔ (ExactTriangle.lopInstance wAB wBC wAC A.D g A.p (rho, chunk, k)).adjA a (⟨c, hpiece⟩, label)

Active left cells are precisely the adjacency of the existing finite lopsided instance. The source-array equation relates original weights to their actual Euclidean residues, and the local-to-original vertex equation identifies the selected piece coordinate.

theorem Cslib.Algorithms.WordRAM.ExactTriangle.MatrixSpec.right_lopInstance (A : WriteMatrices.Args) (R : ℕ → ℕ) (wAB wBC wAC : Fin A.n → Fin A.n → ℤ) (g chunk k : ℕ) (rho : Fin A.p) (b c : Fin A.n) (v : Fin A.length) (label : Fin A.p) (hpiece : c ∈ ExactTriangle.piece A.n A.D g k) (hvertex : A.first + ↑v = ↑c) (hR : ∀ (b c : Fin A.n), R (↑b * A.n + ↑c) = (wBC b c).natMod ↑A.p) : WriteMatrices.entry true A R ((↑v * A.p + ↑label) * A.n + ↑b) = 1 ↔ (ExactTriangle.lopInstance wAB wBC wAC A.D g A.p (rho, chunk, k)).adjB (⟨c, hpiece⟩, label) b

Active right cells are precisely the adjacency of the same finite lopsided instance; the stored right matrix uses its original B–C row and local middle vertex.