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

Lax489179.HypothesisProperties

Negations and algorithm conventions for the four hypotheses

concepts/Lax489179/HypothesisProperties.lean · lax-489179

proven

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

    Evidence

    This concept declares 8 statements. Each proof establishes one of them relative to its assumptions.

    Lemma

    Negating ETH allows a separate 3-SAT algorithm for each positive exponent. Negating SETH gives one positive exponent improvement that works for every fixed clause width, with the algorithm allowed to depend on the width. Negating the 3-SUM Hypothesis gives a truly subquadratic solver. Negating the APSP assumption gives, for each fixed weight exponent, some truly subcubic solver; its improvement may depend on that weight exponent.

    For each hypothesis, its randomized version implies its deterministic version. These are logical consequences of the specified algorithm classes; all four hypotheses themselves remain explicit premises.

    Lean source view on GitHub

    1import Lax489179.ETH
    2import Lax489179.SETH
    3import Lax489179.APSPHypothesis
    4import Lax489179.ThreeSUMHypothesis
    5
    6/-!
    7---
    8title: Negations and algorithm conventions for the four hypotheses
    9type: lemma
    10---
    11Negating ETH allows a separate 3-SAT algorithm for each positive
    12exponent. Negating SETH gives one positive exponent improvement that
    13works for every fixed clause width, with the algorithm allowed to
    14depend on the width. Negating the 3-SUM Hypothesis gives a truly
    15subquadratic solver. Negating the APSP assumption gives, for each
    16fixed weight exponent, some truly subcubic solver; its improvement
    17may depend on that weight exponent.
    18
    19For each hypothesis, its randomized version implies its deterministic
    20version. These are logical consequences of the specified algorithm
    21classes; all four hypotheses themselves remain explicit premises.
    22-/
    23
    24namespace Lax489179.HypothesisProperties
    25
    26axiom not_eth (mode : Algorithms.Mode) :
    27 ¬ ETH.Hypothesis mode ↔ ∀ a : ℝ, 0 < a → SATTime.Solvable mode 3 a
    28
    29axiom not_seth (mode : Algorithms.Mode) :
    30 ¬ SETH.Hypothesis mode ↔ ∃ ε : ℝ, 0 < ε ∧ ε < 1
    31 ∀ k : ℕ, 3 ≤ k → SATTime.Solvable mode k (1 - ε)
    32
    33axiom not_three_sum (mode : Algorithms.Mode) :
    34 ¬ ThreeSUMHypothesis.Hypothesis mode ↔ ∃ ε : ℝ, 0 < ε ∧
    35 WordTime.Solvable mode ThreeSUM.problem (2 - ε)
    36
    37axiom not_apsp (mode : Algorithms.Mode) :
    38 ¬ APSPHypothesis.Hypothesis mode ↔ ∀ c : ℕ, 0 < c →
    39 ∃ ε : ℝ, 0 < ε ∧ WordTime.Solvable mode (WeightedAPSP.problem c) (3 - ε)
    40
    41axiom randomized_eth : ETH.RandomizedETH.Deterministic
    42
    43axiom randomized_seth : SETH.RandomizedSETH.Deterministic
    44
    45axiom randomized_three_sum : ThreeSUMHypothesis.RandomizedThreeSUMHypothesis.Deterministic
    46
    47axiom randomized_apsp : APSPHypothesis.RandomizedAPSPHypothesis.Deterministic
    48
    49end Lax489179.HypothesisProperties
    50
    Show ProofShow ProofShow ProofShow ProofShow ProofShow ProofShow ProofShow Proof

    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…