Draft — mutable and not usable as a dependency; its citation marks the draft state.

Lax489179.ThreeSUMHypothesis

The 3-SUM Hypothesis

concepts/Lax489179/ThreeSUMHypothesis.lean · lax-489179

definition

Loading review…

Sign in with ORCID

Community review

Flags

Each flag is tied to a public ORCID identity and explains why this concept may be incorrect.

No flags have been submitted.

    Community review

    Flag this concept

    State precisely what appears incorrect. This explanation will be public under your ORCID name.

    No source line selected.

    Concept map

    Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A

    Definition

    The integer 3-SUM Hypothesis excludes an O(n2ε)O(n^{2-\varepsilon}) word-RAM algorithm for every constant ε>0\varepsilon>0, on arrays of nn distinct integers in [n3,n3][-n^3,n^3]. Words have O(logn)O(\log n) bits.

    DeterministicDeterministic uses deterministic algorithms; RandomizedRandomized also excludes randomized algorithms with two-sided error at most 1/31/3 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

    1import Lax489179.ThreeSUM
    2
    3/-!
    4---
    5title: The 3-SUM Hypothesis
    6type: definition
    7---
    8The integer 3-SUM Hypothesis excludes an O(n2ε)O(n^{2-\varepsilon})
    9word-RAM algorithm for every constant ε>0\varepsilon>0, on arrays of
    10nn distinct integers in [n3,n3][-n^3,n^3]. Words have O(logn)O(\log n) bits.
    11
    12`Deterministic` uses deterministic algorithms;
    13`Randomized` also excludes randomized algorithms with
    14two-sided error at most 1/31/3 and a worst-case time bound. The latter
    15is the randomized convention supplied by this submission. We do not
    16identify it here with an expected-time or a zero-error formulation.
    17
    18These are propositions. The bound concerns a fixed improvement in the
    19exponent; it permits savings by logarithmic or other subpolynomial factors.
    20-/
    21
    22namespace Lax489179.ThreeSUMHypothesis
    23
    24def Hypothesis (mode : Algorithms.Mode) : Prop :=
    25 ∀ ε : ℝ, 0 < ε → ¬ WordTime.Solvable mode ThreeSUM.problem (2 - ε)
    26
    27def Deterministic : Prop := Hypothesis .deterministic
    28
    29def Randomized : Prop := Hypothesis .randomized
    30
    31end Lax489179.ThreeSUMHypothesis
    32

    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…