Input-derived admission and charged adapter overhead

The actual producer supplies a polynomial bound for every pre-adapter word and address. Its existing wordBound determines a sufficient positive logarithmic physical width for the selected product's computed window. Adaptation is linear in nD+Q; this per-record statement does not sum an ExactTriangle solver or establish its aggregate subcubic bound.

def Cslib.Algorithms.WordRAM.ExactTriangle.RecordProduct.admissionWidth (n D g p A : ℕ) : ℕ

Original-input physical width covering the actual producer, every dirty producer word before normalization, and all relocated product addresses.

theorem Cslib.Algorithms.WordRAM.ExactTriangle.RecordProduct.admissionWidth_pos (n D g p A : ℕ) : 0 < admissionWidth n D g p A

Physical admission is positive, including parameter boundary cases.

theorem Cslib.Algorithms.WordRAM.ExactTriangle.RecordProduct.physical_fits {W n D g p A b Q : ℕ} (hb : b ≤ PreparationInput.wordBound n D g p A) (hQ : Q ≤ n ^ 2) (hW : admissionWidth n D g p A ≤ W) : WordRAM.Fits W (2 * b + 4 * MatrixMultiplication.Schonhage.CallableProduct.windowSize n Q + 1024)

Actual producer word/address bounds and the computed chunk size discharge the physical fit numerically; neither a window nor an intermediate arithmetic certificate is an input.

theorem Cslib.Algorithms.WordRAM.ExactTriangle.RecordProduct.admissionWidth_le_log {n D g p A κ : ℕ} (hn : 1 ≤ n) (hD : D ≤ n) (hg : g ≤ n) (hp : p ≤ n) (hA : A ≤ (n + 2) ^ κ) : admissionWidth n D g p A ≤ (257 * κ + 5906) * Nat.clog 2 (n + 2)

The final threshold is logarithmic in the original outer dimension under the producer's standard polynomial original-header/weight hypotheses. The constant is positive for every κ.

theorem Cslib.Algorithms.WordRAM.ExactTriangle.RecordProduct.timeBound_le {m n : ℕ} (qs : List (Fin n × Fin n)) (hN : MatrixMultiplication.Schonhage.D m ^ 18 ≤ n) : timeBound qs + 1 ≤ 3 * (MatrixMultiplication.Schonhage.QueriedProduct.timeBound ⋯ qs + 1) + 4096 * (n * MatrixMultiplication.Schonhage.D m + qs.length + 1)

All real descriptor/log/header/copy/invocation work is linear in original matrices and occurrences. This includes standalone halt, but not another execution of the producer.

theorem Cslib.Algorithms.WordRAM.ExactTriangle.RecordProduct.timeBound_le_twice_callable {m n : ℕ} (qs : List (Fin n × Fin n)) (hN : MatrixMultiplication.Schonhage.D m ^ 18 ≤ n) : timeBound qs + 1 ≤ 2 * (MatrixMultiplication.Schonhage.CallableProduct.timeBound qs + 3)

The actual callee envelope already dominates a second copy of this linear adaptation. This comparison reuses its established sparse bounds without a separate polylog oracle.

theorem Cslib.Algorithms.WordRAM.ExactTriangle.RecordProduct.thin_timeBound {m n : ℕ} (qs : List (Fin n × Fin n)) (hN : MatrixMultiplication.Schonhage.D m ^ 18 ≤ n) (hQ : qs.toFinset.card * 2 ^ m ≤ n ^ 2) : ↑(timeBound qs + 1) ≤ 524288 * ↑(19 * m + 1) * (65 * (↑(MatrixMultiplication.Schonhage.D m) ^ (-(1 / 18)) * ↑n ^ 2) + ↑qs.length)

Distinct-set sparsity retains the actual list-occurrence charge.

theorem Cslib.Algorithms.WordRAM.ExactTriangle.RecordProduct.thin_timeBound_sparse {m n : ℕ} (qs : List (Fin n × Fin n)) (hN : MatrixMultiplication.Schonhage.D m ^ 18 ≤ n) (hQ : qs.length * 2 ^ m ≤ n ^ 2) : ↑(timeBound qs + 1) ≤ 34603008 * ↑(19 * m + 1) * ↑n ^ 2 / ↑(MatrixMultiplication.Schonhage.D m) ^ (1 / 18)

Occurrence sparsity, which actual producer chunks supply, absorbs every occurrence charge. The bound includes the adapter's standalone halt; producer execution is charged separately.