Actual producer chunks admit the native query copies

The class scanner's real coordinate stores and the existing finite chunk theorem derive in-range query words. Their original occurrence count is the descriptor's computed minimum. The power-of-four query-capacity bound supplies occurrence sparsity without assuming a sparse execution or replacing a list length by a set cardinality.

theorem Cslib.Algorithms.WordRAM.ExactTriangle.RecordProduct.queryCap_mul_two_pow_le (n m : ℕ) : ExactTriangle.queryCap n (MatrixMultiplication.Schonhage.D m) * 2 ^ m ≤ n ^ 2

The existing computed chunk capacity supplies the stronger occurrence bound at 4^m.

theorem Cslib.Algorithms.WordRAM.ExactTriangle.RecordProduct.output_query_coordinates {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 : 1 ≤ D) (hDn : D ≤ n) {initial y : WordRAM.Data 64} (h : Instances.Output n D g p values initial y) (rho : Fin p) (k : ℕ) (hk : k < Matrix.numChunks (ExactTriangle.residueClass wAB p rho) (ExactTriangle.queryCap n D)) : have q := 5 + 6 * (n * n) + p + 2 * ↑rho * (n * n) + 2 * (k * ExactTriangle.queryCap n D); have Q := min (ExactTriangle.queryCap n D) ((ExactTriangle.residueClass wAB p rho).card - k * ExactTriangle.queryCap n D); (∀ i < Q, y.mem (q + 2 * i) < n ∧ y.mem (q + 2 * i + 1) < n) ∧ ∀ i < Q, ∃! pair : Fin n × Fin n, pair ∈ ExactTriangle.chunkOf wAB D p rho k ∧ Matrix.rankIn (ExactTriangle.residueClass wAB p rho) pair = k * ExactTriangle.queryCap n D + i ∧ y.mem (q + 2 * i) = ↑pair.1 ∧ y.mem (q + 2 * i + 1) = ↑pair.2

The producer's actual scanner stores identify every local chunk occurrence with its unique existing finite pair. Thus neither coordinate range nor the query count is supplied as an independent adapter certificate.