Initialized native ExactTriangle preparation

The input supplies only four raw scalar headers and three signed weight arrays. One positive ceiling-logarithm threshold derived from these original parameters covers the signed residue calls and every arithmetic/address fit of the actual preparation program. The same fixed flat program executes at every larger physical width, with the complete output read from its actual pre-halt state and the final halt charged.

Main definitions

• PreparationInput.input: original unsigned headers and signed-encoded weights.
• PreparationInput.width: sufficient positive physical width from the original parameters.
• PreparationInput.flatProgram: fixed native code returning the output-record pointer.

Main results

• PreparationInput.exec_input: structured execution for composition, without the final halt.
• PreparationInput.runs_input: initialized execution, exact readback, fits and charged halt.
• PreparationInput.bounded_reachable: input-derived word and address bounds at every prefix.
• PreparationInput.width_le_log, PreparationInput.wordBound_le_pow: logarithmic physical width and polynomial words and address space when the scalar headers and weights are bounded.

def Cslib.Algorithms.WordRAM.ExactTriangle.PreparationInput.input (n D g p : ℕ) (values : List ℤ) : List ℕ

Actual raw (D,g,n,p) headers followed by the three signed matrix arrays.

def Cslib.Algorithms.WordRAM.ExactTriangle.PreparationInput.envelope (n D g p A : ℕ) : ℕ

Original-input numeric envelope; the preparation budget is an explicit polynomial.

def Cslib.Algorithms.WordRAM.ExactTriangle.PreparationInput.width (n D g p A : ℕ) : ℕ

Three extra bits supply both the asymmetric signed range and the native signed compiler's two-bit extension. This is a positive ceiling-logarithm bound in the original headers/weights.

def Cslib.Algorithms.WordRAM.ExactTriangle.PreparationInput.wordBound (n D g p A : ℕ) : ℕ

An explicit polynomial in the original numeric parameters bounds every word and address at every wider admitted width. It does not grow with the physical width chosen by the caller.

def Cslib.Algorithms.WordRAM.ExactTriangle.PreparationInput.flatProgram : WordRAM.Program WordRAM.Basis.standard 64

One fixed 64-register flat program, including the actual halt.

theorem Cslib.Algorithms.WordRAM.ExactTriangle.PreparationInput.flatProgram_fixed : List.length flatProgram ≤ 641 ∧ ¬flatProgram.ReadsWidth

The code length and width independence are uniform over all runtime inputs.

theorem Cslib.Algorithms.WordRAM.ExactTriangle.PreparationInput.input_word (n D g p : ℕ) (values : List ℤ) (q : ℕ) : (WordRAM.Data.init (input n D g p values)).mem (5 + q) = WordRAM.Signed.encode (values.getD q 0)

The concrete initialized payload is the original weight sequence, with no supplied table.

theorem Cslib.Algorithms.WordRAM.ExactTriangle.PreparationInput.width_le_log {n D g p A κ : ℕ} (hn : 1 ≤ n) (hD : D ≤ n) (hg : g ≤ n) (hp : p ≤ n) (hA : A ≤ (n + 2) ^ κ) : width n D g p A ≤ (κ + 18) * Nat.clog 2 (n + 2)

For polynomially bounded weights and size-bounded scalar headers, the physical threshold is explicitly logarithmic in the original outer dimension. The bound on g is stated because its raw input word must fit even when it does not change the resulting piece size.

theorem Cslib.Algorithms.WordRAM.ExactTriangle.PreparationInput.wordBound_le_pow {n D g p A κ : ℕ} (hn : 1 ≤ n) (hD : D ≤ n) (hg : g ≤ n) (hp : p ≤ n) (hA : A ≤ (n + 2) ^ κ) : wordBound n D g p A ≤ (n + 2) ^ (κ + 19)

The same original-size hypotheses turn the every-prefix word/support bound into a polynomial in the original outer dimension, independent of physical width.

theorem Cslib.Algorithms.WordRAM.ExactTriangle.PreparationInput.exec_input {n D g p A W : ℕ} (values : List ℤ) (hlen : values.length = 3 * (n * n)) (hD : 1 ≤ D) (hDn : D ≤ n) (hg : 1 ≤ g) (hp : 0 < p) (hv : ∀ z ∈ values, z.natAbs ≤ A) (hw : width n D g p A ≤ W) : have C := fun (rho : ℕ) => Nat.count (fun (q : ℕ) => (values.getD q 0 % ↑p).toNat = rho) (n * n); have K := ChunkCatalogue.before C (ExactTriangle.queryCap n D) p; ∃ (y : WordRAM.Data 64), WordRAM.ExecWithin W Instances.program (WordRAM.Data.init (input n D g p values)) y (Instances.timeBound n D p K (ExactTriangle.numPieces n D g) - 1) ∧ Instances.Output n D g p (fun (q : ℕ) => values.getD q 0) (WordRAM.Data.init (input n D g p values)) y ∧ WordRAM.InputFits W (input n D g p values) ∧ WordRAM.Data.Bounded W y

Structured initialized execution for real native caller composition. The budget excludes only the final halt; all existing original-input, width and exact readback hypotheses remain. This does not accept an execution, layout or intermediate-fit certificate.

theorem Cslib.Algorithms.WordRAM.ExactTriangle.PreparationInput.runs_input {n D g p A W : ℕ} (values : List ℤ) (hlen : values.length = 3 * (n * n)) (hD : 1 ≤ D) (hDn : D ≤ n) (hg : 1 ≤ g) (hp : 0 < p) (hv : ∀ z ∈ values, z.natAbs ≤ A) (hw : width n D g p A ≤ W) : have C := fun (rho : ℕ) => Nat.count (fun (q : ℕ) => (values.getD q 0 % ↑p).toNat = rho) (n * n); have K := ChunkCatalogue.before C (ExactTriangle.queryCap n D) p; ∃ (y : WordRAM.Data 64), ∃ t ≤ Instances.timeBound n D p K (ExactTriangle.numPieces n D g), WordRAM.Runs W flatProgram (WordRAM.State.init (input n D g p values)) { pc := Instances.program.size, data := y } (t - 1) ∧ WordRAM.Executes W flatProgram (WordRAM.State.init (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 (input n D g p values)) y ∧ WordRAM.InputFits W (input n D g p values) ∧ WordRAM.Data.Bounded W y

Complete initialized execution at every admitted physical width. The prefix witness and the output predicate use the same actual pre-halt memory, and the bound includes the halt.

theorem Cslib.Algorithms.WordRAM.ExactTriangle.PreparationInput.bounded_reachable {n D g p A W : ℕ} (values : List ℤ) (hlen : values.length = 3 * (n * n)) (hD : 1 ≤ D) (hDn : D ≤ n) (hg : 1 ≤ g) (hp : 0 < p) (hv : ∀ z ∈ values, z.natAbs ≤ A) (hw : width n D g p A ≤ W) (s : WordRAM.State 64) (steps : ℕ) (hr : WordRAM.Runs W flatProgram (WordRAM.State.init (input n D g p values)) s steps) : (∀ (i : Fin 64), s.data.regs i < wordBound n D g p A) ∧ (∀ (a : ℕ), s.data.mem a < wordBound n D g p A) ∧ ∀ (a : ℕ), wordBound n D g p A ≤ a → s.data.mem a = 0

All actual run prefixes, at every admitted physical width, have bounded words and zero memory beyond one original-input polynomial. Width independence identifies each such prefix with the smaller admitted run; the generic native memory-frame theorem supplies the support bound. No caller-provided invariant or execution certificate is used.