Exact native frontend from initialized signed input

The header is the unsigned length; payload cell one starts the canonical signed encoding. The parameter program computes the magnitude and explicit radix bit count. The radix program preserves full multiplicities; the complete descriptor program enumerates the existing inputs.

Main results

• exec_input: complete initialized-input execution, exact descriptors and full multiplicities.
• construct_preserves_parameters: computed parameters remain available to the traversal caller.

Execution uses a positive logarithmic physical width and fixed code per exponent.

theorem Cslib.Algorithms.WordRAM.ThreeSum.Frontend.parameterRegisters_injective : Function.Injective parameterRegisters

theorem Cslib.Algorithms.WordRAM.ThreeSum.Frontend.radixRegisters_injective : Function.Injective radixRegisters

theorem Cslib.Algorithms.WordRAM.ThreeSum.Frontend.arrayRegisters_injective : Function.Injective arrayRegisters

theorem Cslib.Algorithms.WordRAM.ThreeSum.Frontend.construct_preserves_parameters (i : Fin 24) : WordRAM.Code.Preserves (parameterRegisters i) construct

Parameter outputs remain available to the parent traversal without recomputation.

theorem Cslib.Algorithms.WordRAM.ThreeSum.Frontend.exec_input {κ w : ℕ} (input : List ℤ) (hw : width κ input.length ≤ w) (hvalues : ∀ z ∈ input, |z| ≤ ↑((input.length + 2) ^ κ)) : ∃ (y : WordRAM.Data 128) (rs : List (ℕ × ℕ)), WordRAM.ExecWithin w (program κ) (WordRAM.Data.init (List.map WordRAM.Signed.encode input)) y (cost κ input.length - 1) ∧ Output (layout κ input.length) ((input.length + 2) ^ κ) rs y.mem ∧ y.regs descriptorBase = (layout κ input.length).descriptors ∧ y.regs descriptorCount = (layout κ input.length).count ∧ y.regs heapEnd = (layout κ input.length).endpoint ∧ (List.map Prod.fst rs).Nodup ∧ List.Pairwise (fun (x1 x2 : ℕ) => x1 < x2) (List.map Prod.fst rs) ∧ (∀ (k : ℕ), k ∈ List.map Prod.fst rs ↔ k ∈ List.map WordRAM.Signed.encode input) ∧ (∀ p ∈ rs, 0 < p.2 ∧ List.count p.1 (List.map WordRAM.Signed.encode input) = p.2) ∧ WordRAM.Block.HoldsList (1 + 2 * input.length) (List.map Prod.fst rs) y.mem ∧ WordRAM.Block.HoldsList (1 + 3 * input.length) (List.map Prod.snd rs) y.mem ∧ ChanHe.Parameters.Output input.length ((input.length + 2) ^ κ) (WordRAM.Data.comap parameterRegisters y) ∧ WordRAM.Modifies { base := 1, length := (layout κ input.length).endpoint - 1 }.footprint (WordRAM.Data.init (List.map WordRAM.Signed.encode input)).mem y.mem

Complete initialized-input native construction, with no supplied algorithm or fit advice.