The actual first prepared record exists

The fixed initialized composition selects ordinal zero. An original vertex pair belongs to one existing residue class, so that class has a chunk and the vertex set has a piece. The native ordinal characterization then supplies the unique existing finite index of the first record. No nonempty catalogue or index certificate is an extra runtime input.

theorem Cslib.Algorithms.WordRAM.ExactTriangle.RecordProduct.first_index {n D g p : ℕ} (values : ℕ → ℤ) (hD : 16 ≤ D) (hDn : D ≤ n) (hg : 1 ≤ g) (hp : p ≠ 0) : ∃ idx ∈ ExactTriangle.instanceIndices (fun (a b : Fin n) => values (Matrix.pairIndex (a, b))) D g p, recordOrdinal n D g p values idx = 0

Under the real producer geometry, ordinal zero always names an existing finite instance.