Exact finite meaning of prepared native instances

The native catalogue enumerates the existing residue classes, chunks and pieces. These results identify its actual output count and per-instance records with that finite construction. Matrix meaning and padding reuse MatrixSpec and its existing writer-entry formulas.

The consumer extension connects these cells to finite adjacency, deriving piece coordinates and the padding bound.

Main results

• PreparationSpec.count_eq_card: the actual output counter is the finite instance cardinality.
• PreparationSpec.index_unique: unique existing finite coordinates for each output record.
• PreparationSpec.instance_readback: exact query slices and matrices at every finite index.

theorem Cslib.Algorithms.WordRAM.ExactTriangle.PreparationSpec.count_eq_card {n D g p : ℕ} (values : ℕ → ℤ) (wAB : Fin n → Fin n → ℤ) (hp : p ≠ 0) (hAB : ∀ (a b : Fin n), values (Matrix.pairIndex (a, b)) = wAB a b) {initial y : WordRAM.Data 64} (h : Instances.Output n D g p values initial y) : y.regs Instances.produced = (ExactTriangle.instanceIndices wAB D g p).card

The counter of an actual native output is exactly the existing finite instance count. The weight-array correspondence concerns only the original A–B input, not supplied classes.

theorem Cslib.Algorithms.WordRAM.ExactTriangle.PreparationSpec.index_unique {n D g p : ℕ} (values : ℕ → ℤ) (wAB : Fin n → Fin n → ℤ) (hp : p ≠ 0) (hAB : ∀ (a b : Fin n), values (Matrix.pairIndex (a, b)) = wAB a b) (hD : 16 ≤ D) (hDn : D ≤ n) (hg : 1 ≤ g) (i : ℕ) : have C := fun (rho : ℕ) => Nat.count (fun (q : ℕ) => (values q % ↑p).toNat = rho) (n * n); have H := ExactTriangle.numPieces n D g; i < ChunkCatalogue.before C (ExactTriangle.queryCap n D) p * H → ∃! idx : ExactTriangle.InstanceIndex p, idx ∈ ExactTriangle.instanceIndices wAB D g p ∧ i = (ChunkCatalogue.before C (ExactTriangle.queryCap n D) ↑idx.1 + idx.2.1) * H + idx.2.2

Every occupied native instance slot has exactly one existing finite class/chunk/piece index. This uses the standard dependent finite-sum enumeration and ordinary division/remainder; there is no second definition of a residue class or finite instance.

theorem Cslib.Algorithms.WordRAM.ExactTriangle.PreparationSpec.instance_readback {n D g p : ℕ} (values : ℕ → ℤ) (wAB : Fin n → Fin n → ℤ) (hp : p ≠ 0) (hAB : ∀ (a b : Fin n), values (Matrix.pairIndex (a, b)) = wAB a b) (hD : 16 ≤ D) (hDn : D ≤ n) (hg : 1 ≤ g) {initial y : WordRAM.Data 64} (h : Instances.Output n D g p values initial y) (idx : ExactTriangle.InstanceIndex p) (hidx : idx ∈ ExactTriangle.instanceIndices wAB D g p) : have N := n * n; have R := fun (q : ℕ) => (values q % ↑p).toNat; have C := fun (rho : ℕ) => Nat.count (fun (q : ℕ) => R q = rho) N; have H := ExactTriangle.numPieces n D g; have B := ExactTriangle.pieceSize D g; have K := ChunkCatalogue.before C (ExactTriangle.queryCap n D) p; have ord := ChunkCatalogue.before C (ExactTriangle.queryCap n D) ↑idx.1 + idx.2.1; have base := 5 + 6 * N + p + 2 * N * p + 3 * K + (ord * H + idx.2.2) * (6 + 2 * (n * D)); have A := { src := 5 + 5 * N, dst := base + 6, n := n, D := D, p := p, first := idx.2.2 * B, length := min B (n - idx.2.2 * B), rho := ↑idx.1 }; have A' := { src := 5 + 4 * N, dst := base + 6 + n * D, n := A.n, D := A.D, p := A.p, first := A.first, length := A.length, rho := A.rho }; { base := base, length := 6 }.Realizes y.mem ![↑idx.1, idx.2.2, 5 + 6 * N + p + 2 * ↑idx.1 * N + 2 * (idx.2.1 * ExactTriangle.queryCap n D), min (ExactTriangle.queryCap n D) ((ExactTriangle.residueClass wAB p idx.1).card - idx.2.1 * ExactTriangle.queryCap n D), base + 6, base + 6 + n * D] ∧ ({ base := A.dst, length := n * D }.Realizes y.mem fun (j : Fin { base := A.dst, length := n * D }.length) => WriteMatrices.entry false A (fun (q : ℕ) => R (2 * N + q)) ↑j) ∧ { base := A'.dst, length := n * D }.Realizes y.mem fun (j : Fin { base := A'.dst, length := n * D }.length) => WriteMatrices.entry true A' (fun (q : ℕ) => R (N + q)) ↑j

Each existing finite instance is stored at its computed native ordinal. Its six-word record contains the exact residue, piece, existing query-chunk pointer/cardinality and both matrix pointers. The matrix readback reuses the same entry formulas as MatrixSpec, including their modular adjacency and zero-padding results.