Summing the native ExactTriangle preparation costs

The initialized preparation program computes the catalogue and writes every instance's record and two matrices within 690n²Dg charged instructions, including halt, in the source's admissible parameter regime. The bound uses the existing finite instance count. Prime selection and solving the prepared instances belong to the outer ExactTriangle host.

Main results

• PreparationBounds.matrix_writing_total_le: both native matrix writers over all actual instances, including an explicit per-instance overhead.
• PreparationBounds.residue_class_parameter_time_le: signed residues, class scans and parameter arithmetic fit the preparation scale in the source's admitted regime.
• PreparationBounds.catalogue_time_le: descriptor enumeration, including empty-class costs.
• PreparationBounds.timeBound_le: the complete budget summed over the existing actual finite instance indices.
• PreparationBounds.runs_input: actual initialized execution with the complete output contract and the 690n²Dg bound.

theorem Cslib.Algorithms.WordRAM.ExactTriangle.PreparationBounds.matrix_writing_total_le {n D g p : ℕ} (wAB : Fin n → Fin n → ℤ) (c : ℕ) (hD : 16 ≤ D) (hDn : D ≤ n) (hg : 1 ≤ g) (hp : p ∈ D.sqrtPrimeWindow) : ∑ _ι ∈ ExactTriangle.instanceIndices wAB D g p, (2 * (20 * (n * D) + 6) + c) ≤ (208 + 4 * c) * (n * n) * D * g

Sum the two 20nD+6 matrix-writer bounds over the existing actual instance set. An explicit additional c instructions per instance accounts for caller overhead separately.

theorem Cslib.Algorithms.WordRAM.ExactTriangle.PreparationBounds.residue_class_parameter_time_le {n D g p : ℕ} (hD : 1 ≤ D) (hDn : D ≤ n) (hg : 1 ≤ g) (hp : p ≤ D) : 69 * (n * n) + p * (14 * (n * n) + 14) + 30 + (5 * ExactTriangle.sOf D + 5 * ExactTriangle.queryCap n D + 27) ≤ 164 * (n * n) * D * g

The exact signed-residue/class prefix bound and the parameter-kernel bound are charged separately. Their sum is at most a fixed multiple of n² D g when p ≤ D; the prime-window caller supplies that inequality. This includes all per-class scan overhead.

theorem Cslib.Algorithms.WordRAM.ExactTriangle.PreparationBounds.catalogue_time_le {n D g p : ℕ} (hD : 1 ≤ D) (hDn : D ≤ n) (hg : 1 ≤ g) (hp : p ≤ D) : p * (17 * (n * n) + 20) + 9 ≤ 46 * (n * n) * D * g

The actual concatenation loop scans all p class counts, but writes only their actual chunks. Its conservative charged bound still lies on the n² D g preparation scale.

theorem Cslib.Algorithms.WordRAM.ExactTriangle.PreparationBounds.prefix_time_le {n D g p : ℕ} (hD : 1 ≤ D) (hDn : D ≤ n) (hg : 1 ≤ g) (hp : p ≤ D) : Catalogue.cost n D p ≤ 229 * (n * n) * D * g

The complete prefix cost includes both argument-delivery stages in addition to residue, class, parameter and descriptor enumeration.

theorem Cslib.Algorithms.WordRAM.ExactTriangle.PreparationBounds.timeBound_le {n D g p : ℕ} (wAB : Fin n → Fin n → ℤ) (hD : 16 ≤ D) (hDn : D ≤ n) (hg : 1 ≤ g) (hp : p ∈ D.sqrtPrimeWindow) : Instances.timeBound n D p (ExactTriangle.totalChunks wAB D p) (ExactTriangle.numPieces n D g) ≤ 690 * (n * n) * D * g

Substitute the existing actual chunk and piece counts into the native budget. The 690n²Dg bound includes all catalogue work, selection, record stores, both matrix calls, argument delivery, loop control and halt. runs_input applies this bound to actual execution.

theorem Cslib.Algorithms.WordRAM.ExactTriangle.PreparationBounds.computed_timeBound_le {n D g p : ℕ} (values : List ℤ) (hD : 16 ≤ D) (hDn : D ≤ n) (hg : 1 ≤ g) (hp : p ∈ D.sqrtPrimeWindow) : have C := fun (rho : ℕ) => Nat.count (fun (q : ℕ) => (values.getD q 0 % ↑p).toNat = rho) (n * n); Instances.timeBound n D p (ChunkCatalogue.before C (ExactTriangle.queryCap n D) p) (ExactTriangle.numPieces n D g) ≤ 690 * (n * n) * D * g

The native count in the initialized theorem is the existing finite chunk count. Thus its actual charged execution budget, not an assumed matrix-write contract, has the preparation bound in the source's admissible regime.

theorem Cslib.Algorithms.WordRAM.ExactTriangle.PreparationBounds.runs_input {n D g p A W : ℕ} (values : List ℤ) (hlen : values.length = 3 * (n * n)) (hD : 16 ≤ D) (hDn : D ≤ n) (hg : 1 ≤ g) (hp : p ∈ D.sqrtPrimeWindow) (hv : ∀ z ∈ values, z.natAbs ≤ A) (hw : PreparationInput.width n D g p A ≤ W) : ∃ (y : WordRAM.Data 64), ∃ t ≤ 690 * (n * n) * D * g, WordRAM.Runs W PreparationInput.flatProgram (WordRAM.State.init (PreparationInput.input n D g p values)) { pc := Instances.program.size, data := y } (t - 1) ∧ WordRAM.Executes W PreparationInput.flatProgram (WordRAM.State.init (PreparationInput.input n D g p values)) (y.regs Instances.output) t ∧ Instances.Output n D g p (fun (q : ℕ) => values.getD q 0) (WordRAM.Data.init (PreparationInput.input n D g p values)) y ∧ WordRAM.InputFits W (PreparationInput.input n D g p values) ∧ WordRAM.Data.Bounded W y

The entire real initialized preparation, including halt, costs at most 690n²Dg under the existing finite splitting hypotheses. All output assertions refer to its same pre-halt state. The supplied prime has not been chosen by this component.