Native row-major residue-class queries

The program scans a square residue matrix and writes the row and column of each entry equal to the runtime query residue. Its output order is the row-major order used by the existing finite chunk construction. Prefix ranks use Mathlib's Nat.count.

This directly adapts the query-class construction in the pinned Theorem 17 class builder. The per-class scan is charged explicitly; composing all residue classes multiplies its bound by the modulus. No class-membership or query-list table is supplied to the program.

Main definitions

• QueryScan.program: the fixed twelve-register query scan.

Main results

• QueryScan.exec: actual scan execution, exact ranks and the output-prefix frame.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ExactTriangle.QueryScan.src : Fin 12

Square residue input pointer.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ExactTriangle.QueryScan.dst : Fin 12

Output pointer for consecutive row/column pairs.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ExactTriangle.QueryScan.size : Fin 12

Matrix side.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ExactTriangle.QueryScan.residue : Fin 12

Selected residue.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ExactTriangle.QueryScan.idx : Fin 12

Flat input cursor.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ExactTriangle.QueryScan.area : Fin 12

Input area.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ExactTriangle.QueryScan.count : Fin 12

Number of emitted pairs.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ExactTriangle.QueryScan.addr : Fin 12

Address temporary.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ExactTriangle.QueryScan.key : Fin 12

Loaded residue.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ExactTriangle.QueryScan.one : Fin 12

Constant one.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ExactTriangle.QueryScan.row : Fin 12

Output row.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ExactTriangle.QueryScan.col : Fin 12

Output column.

def Cslib.Algorithms.WordRAM.ExactTriangle.QueryScan.body : WordRAM.Code WordRAM.Basis.standard 12

Every successful match computes both coordinates and stores their two words.

def Cslib.Algorithms.WordRAM.ExactTriangle.QueryScan.program : WordRAM.Code WordRAM.Basis.standard 12

Constants, counters and matrix area are initialized by actual instructions.

theorem Cslib.Algorithms.WordRAM.ExactTriangle.QueryScan.program_fixed : program.size ≤ 32 ∧ ¬program.ReadsWidth

The query scanner has a fixed instruction graph and no physical-width reads.

theorem Cslib.Algorithms.WordRAM.ExactTriangle.QueryScan.exec {w : ℕ} (x : WordRAM.Data 12) (R : ℕ → ℕ) (h1 : WordRAM.Fits w 1) (hinput : ∀ i < x.regs size * x.regs size, x.mem (x.regs src + i) = R i) (hsrc : WordRAM.Fits w (x.regs src + x.regs size * x.regs size)) (hdst : WordRAM.Fits w (x.regs dst + 2 * (x.regs size * x.regs size))) (hdisj : x.regs src + x.regs size * x.regs size ≤ x.regs dst) : ∃ (y : WordRAM.Data 12), WordRAM.ExecWithin w program x y (14 * (x.regs size * x.regs size) + 6) ∧ y.regs idx = x.regs size * x.regs size ∧ y.regs count = Nat.count (fun (j : ℕ) => R j = x.regs residue) (x.regs size * x.regs size) ∧ (∀ (i : Fin 12), ↑i < 4 → y.regs i = x.regs i) ∧ (∀ q < x.regs size * x.regs size, R q = x.regs residue → y.mem (x.regs dst + 2 * Nat.count (fun (j : ℕ) => R j = x.regs residue) q) = q / x.regs size ∧ y.mem (x.regs dst + 2 * Nat.count (fun (j : ℕ) => R j = x.regs residue) q + 1) = q % x.regs size) ∧ ∀ (a : ℕ), ¬(x.regs dst ≤ a ∧ a < x.regs dst + 2 * y.regs count) → y.mem a = x.mem a

Scan an actual residue matrix, preserving the input and all cells outside the emitted pair prefix. Each selected flat position is stored at its exact row-major rank, counted by Nat.count. The final halt is excluded from the 14n²+6 instruction bound.