Lax489179.ThreeSUMHypothesis
The 3-SUM Hypothesis
concepts/Lax489179/ThreeSUMHypothesis.lean · lax-489179
No public endorsements yet.
Loading review…
Sign in with ORCIDConcept map
Definition
The integer 3-SUM Hypothesis excludes an word-RAM algorithm for every constant , on arrays of distinct integers in . Words have bits.
uses deterministic algorithms; also excludes randomized algorithms with two-sided error at most and a worst-case time bound. The latter is the randomized convention supplied by this submission. We do not identify it here with an expected-time or a zero-error formulation.
These are propositions. The bound concerns a fixed improvement in the exponent; it permits savings by logarithmic or other subpolynomial factors.
Lean source view on GitHub
| 1 | import Lax489179.ThreeSUM |
| 2 | |
| 3 | /-! |
| 4 | --- |
| 5 | title: The 3-SUM Hypothesis |
| 6 | type: definition |
| 7 | --- |
| 8 | The integer 3-SUM Hypothesis excludes an |
| 9 | word-RAM algorithm for every constant , on arrays of |
| 10 | distinct integers in . Words have bits. |
| 11 | |
| 12 | `Deterministic` uses deterministic algorithms; |
| 13 | `Randomized` also excludes randomized algorithms with |
| 14 | two-sided error at most and a worst-case time bound. The latter |
| 15 | is the randomized convention supplied by this submission. We do not |
| 16 | identify it here with an expected-time or a zero-error formulation. |
| 17 | |
| 18 | These are propositions. The bound concerns a fixed improvement in the |
| 19 | exponent; it permits savings by logarithmic or other subpolynomial factors. |
| 20 | -/ |
| 21 | |
| 22 | namespace Lax489179.ThreeSUMHypothesis |
| 23 | |
| 24 | def Hypothesis (mode : Algorithms.Mode) : Prop := |
| 25 | ∀ ε : ℝ, 0 < ε → ¬ WordTime.Solvable mode ThreeSUM.problem (2 - ε) |
| 26 | |
| 27 | def Deterministic : Prop := Hypothesis .deterministic |
| 28 | |
| 29 | def Randomized : Prop := Hypothesis .randomized |
| 30 | |
| 31 | end Lax489179.ThreeSUMHypothesis |
| 32 |
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