Lax489179.ThreeSUM

The integer 3-SUM problem

concepts/Lax489179/ThreeSUM.lean · lax-489179

definition

Loading review…

Concept map

Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A

Definition

The input is an array of $n$ distinct integers in $[-n^3,n^3]$ . It is a yes-instance if three distinct entries sum to zero. The order of the array is arbitrary. The machine must output exactly one word: one for yes and zero for no. The raw input is the list of signed integer codes; lax-67 supplies its length through the input interface.

The cubic universe is the standard integer 3-SUM convention. Arithmetic in the specification is over $\mathbb Z$ , so the sum test is exact and has no modular overflow. Machine arithmetic remains bounded-word arithmetic as specified in $WordPrograms$ .

Lean source view on GitHub

1	import Lax489179.WordTime
2	import Lax489179.IntegerEncoding
3
4	/-!
5	---
6	title: The integer 3-SUM problem
7	type: definition
8	---
9	The input is an array of $n$ distinct integers in $[-n^3,n^3]$ .
10	It is a yes-instance if three distinct entries sum to zero. The
11	order of the array is arbitrary. The machine must output exactly
12	one word: one for yes and zero for no. The raw input is the list of
13	signed integer codes; lax-67 supplies its length through the input interface.
14
15	The cubic universe is the standard integer 3-SUM convention. Arithmetic
16	in the specification is over $\mathbb Z$ , so the sum test is exact and
17	has no modular overflow. Machine arithmetic remains bounded-word
18	arithmetic as specified in `WordPrograms`.
19	-/
20
21	namespace Lax489179.ThreeSUM
22
23	def HasZeroSum (input : List ℤ) : Prop :=
24	∃ i j k : Fin input.length,
25	i < j ∧ j < k ∧ input[i] + input[j] + input[k] = 0
26
27	def Valid (input : List ℤ) : Prop :=
28	input.Nodup ∧ ∀ z ∈ input, z.natAbs ≤ input.length ^ 3
29
30	def Correct (input : List ℤ) (output : List ℕ) : Prop :=
31	(output = [1] ∧ HasZeroSum input) ∨ (output = [0] ∧ ¬ HasZeroSum input)
32
33	def problem : WordTime.Problem where
34	Input := List ℤ
35	size := List.length
36	encode := List.map IntegerEncoding.encodeInt
37	valid := Valid
38	correct := Correct
39
40	end Lax489179.ThreeSUM
41

Builds on

Used by

From Mathlib

none

Community review

Discussion

Ask a question or add context. Endorsements and structured flags are kept in the review panel above; your ORCID profile must share a public name.

0 comments

Loading discussion…

Lax Lean Archive

The integer 3-SUM problem

Flags

Flag this concept