Exact ordinary 3SUM boundary verdicts

Inputs of lengths zero, one and two cannot contain three distinct positions, even when values repeat. The actual native controller returns false before preprocessing on precisely this branch. This is a final-verdict optimization, not an assertion about the instance catalogue.

Main results

• not_hasSolution_of_length_lt_three: the existing distinct-position predicate is false.
• exec_small: the actual finite controller executes the false branch in six instructions.

These boundary and native execution proofs are original.

theorem Cslib.Algorithms.WordRAM.ThreeSum.Decision.not_hasSolution_of_length_lt_three {n : ℕ} (x : Fin n → ℤ) (hn : n < 3) : ¬ThreeSum.HasSolution x

Three distinct input positions require at least three entries.

theorem Cslib.Algorithms.WordRAM.ThreeSum.Decision.exec_readLength {w : ℕ} (x : WordRAM.Data 16) (h3 : WordRAM.Fits w 3) : have y := (((x.set address 0).set inputLength (x.mem 0)).set three 3).set answer 0; WordRAM.ExecWithin w readLength x y 4

The length header and constants are read by actual native instructions.

theorem Cslib.Algorithms.WordRAM.ThreeSum.Decision.exec_small {κ w r : ℕ} (input : List ℤ) (c : Host.Callee r) (hn : input.length < 3) (h3 : WordRAM.Fits w 3) : ∃ (y : WordRAM.Data (registerCount r)), WordRAM.ExecWithin w (program κ c) (WordRAM.Data.init (List.map WordRAM.Signed.encode input)) y 6 ∧ y.regs (controllerRegisters r answer) = 0 ∧ ¬ThreeSum.HasSolution fun (i : Fin input.length) => input[i]

Every admitted empty, singleton or two-entry input follows the actual false-verdict path.