Applying the adapter to the actual native producer

The record, source pointers, original zero/one matrices and ordered coordinate occurrences are derived from Instances.Output and the existing native readback theorems. The initialized client obtains that output from the actual producer execution, not from an algorithm oracle. Prime selection, global parameters and the outer ExactTriangle host are separate components.

def Cslib.Algorithms.WordRAM.ExactTriangle.RecordProduct.producerBank (i : Fin 64) : Fin 320

The unchanged complete producer occupies the original low register bank.

def Cslib.Algorithms.WordRAM.ExactTriangle.RecordProduct.matrixArgs (n D g p rho piece : ℕ) : WriteMatrices.Args

Existing native writer arguments, with pointer fields omitted from the value-only view.

def Cslib.Algorithms.WordRAM.ExactTriangle.RecordProduct.leftMatrix (m n g p : ℕ) (values : ℕ → ℤ) (idx : ExactTriangle.InstanceIndex p) : Matrix (Fin n) (Fin (MatrixMultiplication.Schonhage.D m)) ℤ

Exact raw left adjacency matrix written by the actual producer.

def Cslib.Algorithms.WordRAM.ExactTriangle.RecordProduct.rightMatrix (m n g p : ℕ) (values : ℕ → ℤ) (idx : ExactTriangle.InstanceIndex p) : Matrix (Fin (MatrixMultiplication.Schonhage.D m)) (Fin n) ℤ

Exact raw right adjacency matrix, in its actual D×n storage order.

theorem Cslib.Algorithms.WordRAM.ExactTriangle.RecordProduct.entry_le_one (side : Bool) (A : WriteMatrices.Args) (R : ℕ → ℕ) (a : ℕ) : WriteMatrices.entry side A R a ≤ 1

Both native writer value functions are raw zero/one words at every index.

theorem Cslib.Algorithms.WordRAM.ExactTriangle.RecordProduct.matrices_zero_one (m n g p : ℕ) (values : ℕ → ℤ) (idx : ExactTriangle.InstanceIndex p) : (∀ (a : Fin n) (k : Fin (MatrixMultiplication.Schonhage.D m)), 0 ≤ leftMatrix m n g p values idx a k ∧ leftMatrix m n g p values idx a k ≤ 1) ∧ ∀ (k : Fin (MatrixMultiplication.Schonhage.D m)) (a : Fin n), 0 ≤ rightMatrix m n g p values idx k a ∧ rightMatrix m n g p values idx k a ≤ 1

The readback matrices satisfy the raw callee's original-entry hypotheses.

def Cslib.Algorithms.WordRAM.ExactTriangle.RecordProduct.recordOrdinal (n D g p : ℕ) (values : ℕ → ℤ) (idx : ExactTriangle.InstanceIndex p) : ℕ

The actual computed ordinal of an existing finite class/chunk/piece. This is a value specification for the caller's selection register, not a table supplied to the adapter.

def Cslib.Algorithms.WordRAM.ExactTriangle.RecordProduct.recordQueryCount (n D p : ℕ) (values : ℕ → ℤ) (idx : ExactTriangle.InstanceIndex p) : ℕ

Actual descriptor occurrence count, rather than an assumed sparse set size.

theorem Cslib.Algorithms.WordRAM.ExactTriangle.RecordProduct.recordQueryCount_pos {n D g p : ℕ} (values : ℕ → ℤ) (hp : p ≠ 0) (hD : 1 ≤ D) (hDn : D ≤ n) (idx : ExactTriangle.InstanceIndex p) (hidx : idx ∈ ExactTriangle.instanceIndices (fun (a b : Fin n) => values (Matrix.pairIndex (a, b))) D g p) : 0 < recordQueryCount n D p values idx

Every occupied finite instance has a nonempty actual descriptor query slice.

def Cslib.Algorithms.WordRAM.ExactTriangle.RecordProduct.recordQueries (n D p : ℕ) (idx : ExactTriangle.InstanceIndex p) : ℕ

Actual query pointer into the protected producer catalogue.

theorem Cslib.Algorithms.WordRAM.ExactTriangle.RecordProduct.exec_of_output {W m n g p : ℕ} (values : ℕ → ℤ) (initial : WordRAM.Data 64) (x : WordRAM.Data 320) (h : Instances.Output n (MatrixMultiplication.Schonhage.D m) g p values initial (WordRAM.Data.comap producerBank x)) (hD : 16 ≤ MatrixMultiplication.Schonhage.D m) (hg : 1 ≤ g) (hp : p ≠ 0) (hN : MatrixMultiplication.Schonhage.D m ^ 18 ≤ n) (hheaderD : initial.mem 1 = MatrixMultiplication.Schonhage.D m) (hheaderN : initial.mem 3 = n) (idx : ExactTriangle.InstanceIndex p) (hidx : idx ∈ ExactTriangle.instanceIndices (fun (a b : Fin n) => values (Matrix.pairIndex (a, b))) (MatrixMultiplication.Schonhage.D m) g p) (hi : x.regs Reg.ordinal = recordOrdinal n (MatrixMultiplication.Schonhage.D m) g p values idx) (hfit : WordRAM.Fits W (2 * x.regs 42 + 4 * MatrixMultiplication.Schonhage.CallableProduct.windowSize n (recordQueryCount n (MatrixMultiplication.Schonhage.D m) p values idx) + 1024)) : have hn := ⋯; have qs := decodedQueries hn x.mem (recordQueries n (MatrixMultiplication.Schonhage.D m) p idx) (recordQueryCount n (MatrixMultiplication.Schonhage.D m) p values idx); ∃ (y : WordRAM.Data 320), WordRAM.ExecWithin W program x y (timeBound qs) ∧ y.regs Reg.result = x.regs 42 + MatrixMultiplication.Schonhage.QueriedProduct.outputBase (19 * m) m n qs.length ∧ (∀ (j : Fin qs.length), y.mem (x.regs 42 + (MatrixMultiplication.Schonhage.QueriedProduct.outputBase (19 * m) m n qs.length + ↑j)) = WordRAM.Signed.encode ((leftMatrix m n g p values idx * rightMatrix m n g p values idx) (qs.get j).1 (qs.get j).2)) ∧ (∀ (a : ℕ), a < x.regs 42 ∨ x.regs 42 + MatrixMultiplication.Schonhage.CallableProduct.windowSize n qs.length ≤ a → y.mem a = x.mem a) ∧ (∀ (j : Fin 320), ↑j < 65 → y.regs j = x.regs j) ∧ qs.length * 2 ^ m ≤ n ^ 2

Full adapter execution over a genuine producer output. Every descriptor and source-span premise of exec is derived here from the actual output; none remains an independent caller certificate. A following initialized client obtains this output by executing the producer.