Native query ranks and the finite ExactTriangle chunks

The native scanner uses Nat.count on flat positions. The finite splitting construction uses Matrix.rankIn on pairs. These lemmas identify their counts and ranks through the existing row-major indexing; they introduce no alternative notion of a residue class or chunk.

Main results

• QuerySpec.card_residueClass: the native count is the finite class cardinality.
• QuerySpec.rank_residueClass: native prefix rank is the existing finite rank.
• QuerySpec.mem_chunkOf: consecutive native query slices are the existing chunks.
• QuerySpec.query_readback: every occupied native query slot names exactly one class member.
• QuerySpec.chunk_readback: each local chunk slot names its unique existing finite member.
• QuerySpec.before_eq_totalChunks: the native catalogue count is the existing finite count.

theorem Cslib.Algorithms.WordRAM.ExactTriangle.QuerySpec.card_residueClass {n p : ℕ} (wAB : Fin n → Fin n → ℤ) (hp : p ≠ 0) (R : ℕ → ℕ) (hR : ∀ (q : Fin n × Fin n), R (Matrix.pairIndex q) = ↑(ExactTriangle.resFin hp (wAB q.1 q.2))) (rho : Fin p) : (ExactTriangle.residueClass wAB p rho).card = Nat.count (fun (q : ℕ) => R q = ↑rho) (n * n)

The count emitted by the native class scanner equals the existing finite class size.

theorem Cslib.Algorithms.WordRAM.ExactTriangle.QuerySpec.before_eq_totalChunks {n p : ℕ} (wAB : Fin n → Fin n → ℤ) (hp : p ≠ 0) (R : ℕ → ℕ) (hR : ∀ (q : Fin n × Fin n), R (Matrix.pairIndex q) = ↑(ExactTriangle.resFin hp (wAB q.1 q.2))) (D : ℕ) : ChunkCatalogue.before (fun (rho : ℕ) => Nat.count (fun (q : ℕ) => R q = rho) (n * n)) (ExactTriangle.queryCap n D) p = ExactTriangle.totalChunks wAB D p

The concatenation controller's final counter is exactly the existing total chunk count. The native table uses Nat.count; card_residueClass identifies each summand.

theorem Cslib.Algorithms.WordRAM.ExactTriangle.QuerySpec.before_mul_numPieces {n p : ℕ} (wAB : Fin n → Fin n → ℤ) (hp : p ≠ 0) (R : ℕ → ℕ) (hR : ∀ (q : Fin n × Fin n), R (Matrix.pairIndex q) = ↑(ExactTriangle.resFin hp (wAB q.1 q.2))) (D g : ℕ) : ChunkCatalogue.before (fun (rho : ℕ) => Nat.count (fun (q : ℕ) => R q = rho) (n * n)) (ExactTriangle.queryCap n D) p * ExactTriangle.numPieces n D g = (ExactTriangle.instanceIndices wAB D g p).card

Iterating every actual catalogue entry over every piece creates exactly the existing finite instance set's cardinality. This is the multiplier used by the native matrix caller.

theorem Cslib.Algorithms.WordRAM.ExactTriangle.QuerySpec.rank_residueClass {n p : ℕ} (wAB : Fin n → Fin n → ℤ) (hp : p ≠ 0) (R : ℕ → ℕ) (hR : ∀ (q : Fin n × Fin n), R (Matrix.pairIndex q) = ↑(ExactTriangle.resFin hp (wAB q.1 q.2))) (rho : Fin p) (q : Fin n × Fin n) : Matrix.rankIn (ExactTriangle.residueClass wAB p rho) q = Nat.count (fun (j : ℕ) => R j = ↑rho) (Matrix.pairIndex q)

Prefix rank agrees with the existing row-major rank used to split query chunks.

theorem Cslib.Algorithms.WordRAM.ExactTriangle.QuerySpec.mem_chunkOf {n p : ℕ} (wAB : Fin n → Fin n → ℤ) (hp : p ≠ 0) (R : ℕ → ℕ) (hR : ∀ (q : Fin n × Fin n), R (Matrix.pairIndex q) = ↑(ExactTriangle.resFin hp (wAB q.1 q.2))) (D : ℕ) (rho : Fin p) (j : ℕ) (q : Fin n × Fin n) : q ∈ ExactTriangle.chunkOf wAB D p rho j ↔ R (Matrix.pairIndex q) = ↑rho ∧ Nat.count (fun (k : ℕ) => R k = ↑rho) (Matrix.pairIndex q) / ExactTriangle.queryCap n D = j

Dividing the actual prefix rank by the query capacity gives precisely chunkOf.

theorem Cslib.Algorithms.WordRAM.ExactTriangle.QuerySpec.query_readback {n p : ℕ} (wAB : Fin n → Fin n → ℤ) (hp : p ≠ 0) (R : ℕ → ℕ) (hR : ∀ (q : Fin n × Fin n), R (Matrix.pairIndex q) = ↑(ExactTriangle.resFin hp (wAB q.1 q.2))) (rho : Fin p) (mem : ℕ → ℕ) (base : ℕ) (hread : ∀ q < n * n, R q = ↑rho → mem (base + 2 * Nat.count (fun (j : ℕ) => R j = ↑rho) q) = q / n ∧ mem (base + 2 * Nat.count (fun (j : ℕ) => R j = ↑rho) q + 1) = q % n) (k : ℕ) (hk : k < (ExactTriangle.residueClass wAB p rho).card) : ∃! q : Fin n × Fin n, q ∈ ExactTriangle.residueClass wAB p rho ∧ Matrix.rankIn (ExactTriangle.residueClass wAB p rho) q = k ∧ mem (base + 2 * k) = ↑q.1 ∧ mem (base + 2 * k + 1) = ↑q.2

Every occupied native query slot names exactly one member of the existing residue class. The readback premise is precisely the rank-indexed conclusion of Classes.exec; in particular, this rules out unspecified or duplicate pairs below the computed count.

theorem Cslib.Algorithms.WordRAM.ExactTriangle.QuerySpec.chunk_readback {n p : ℕ} (wAB : Fin n → Fin n → ℤ) (hp : p ≠ 0) (R : ℕ → ℕ) (hR : ∀ (q : Fin n × Fin n), R (Matrix.pairIndex q) = ↑(ExactTriangle.resFin hp (wAB q.1 q.2))) (D : ℕ) (rho : Fin p) (mem : ℕ → ℕ) (base : ℕ) (hread : ∀ q < n * n, R q = ↑rho → mem (base + 2 * Nat.count (fun (j : ℕ) => R j = ↑rho) q) = q / n ∧ mem (base + 2 * Nat.count (fun (j : ℕ) => R j = ↑rho) q + 1) = q % n) (hcap : 0 < ExactTriangle.queryCap n D) (k : ℕ) (hk : k < Matrix.numChunks (ExactTriangle.residueClass wAB p rho) (ExactTriangle.queryCap n D)) (r : ℕ) (hr : r < min (ExactTriangle.queryCap n D) ((ExactTriangle.residueClass wAB p rho).card - k * ExactTriangle.queryCap n D)) : ∃! q : Fin n × Fin n, q ∈ ExactTriangle.chunkOf wAB D p rho k ∧ Matrix.rankIn (ExactTriangle.residueClass wAB p rho) q = k * ExactTriangle.queryCap n D + r ∧ mem (base + 2 * (k * ExactTriangle.queryCap n D + r)) = ↑q.1 ∧ mem (base + 2 * (k * ExactTriangle.queryCap n D + r) + 1) = ↑q.2

Every occupied position of a native chunk names exactly one member of the existing finite chunk. The local position is translated to its actual global class rank; the scanner's readback premise is unchanged, so no list or ordering certificate is assumed.