Lax489179.HypothesisProperties
Negations and algorithm conventions for the four hypotheses
concepts/Lax489179/HypothesisProperties.lean · lax-489179
No public endorsements yet.
Loading review…
Sign in with ORCIDConcept map
Evidence
This concept declares 8 statements. Each proof establishes one of them relative to its assumptions.
1st statement not_apsp proven
2nd statement not_eth proven
3rd statement not_seth proven
4th statement not_three_sum proven
5th statement randomized_apsp proven
6th statement randomized_eth proven
7th statement randomized_seth proven
8th statement randomized_three_sum proven
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
| 1 | import Lax489179.ETH |
| 2 | import Lax489179.SETH |
| 3 | import Lax489179.APSPHypothesis |
| 4 | import Lax489179.ThreeSUMHypothesis |
| 5 | |
| 6 | /-! |
| 7 | --- |
| 8 | title: Negations and algorithm conventions for the four hypotheses |
| 9 | type: lemma |
| 10 | --- |
| 11 | Negating ETH allows a separate 3-SAT algorithm for each positive |
| 12 | exponent. Negating SETH gives one positive exponent improvement that |
| 13 | works for every fixed clause width, with the algorithm allowed to |
| 14 | depend on the width. Negating the 3-SUM Hypothesis gives a truly |
| 15 | subquadratic solver. Negating the APSP assumption gives, for each |
| 16 | fixed weight exponent, some truly subcubic solver; its improvement |
| 17 | may depend on that weight exponent. |
| 18 | |
| 19 | For each hypothesis, its randomized version implies its deterministic |
| 20 | version. These are logical consequences of the specified algorithm |
| 21 | classes; all four hypotheses themselves remain explicit premises. |
| 22 | -/ |
| 23 | |
| 24 | namespace Lax489179.HypothesisProperties |
| 25 | |
| 26 | axiom not_eth (mode : Algorithms.Mode) : |
| 27 | ¬ ETH.Hypothesis mode ↔ ∀ a : ℝ, 0 < a → SATTime.Solvable mode 3 a |
| 28 | |
| 29 | axiom not_seth (mode : Algorithms.Mode) : |
| 30 | ¬ SETH.Hypothesis mode ↔ ∃ ε : ℝ, 0 < ε ∧ ε < 1 ∧ |
| 31 | ∀ k : ℕ, 3 ≤ k → SATTime.Solvable mode k (1 - ε) |
| 32 | |
| 33 | axiom not_three_sum (mode : Algorithms.Mode) : |
| 34 | ¬ ThreeSUMHypothesis.Hypothesis mode ↔ ∃ ε : ℝ, 0 < ε ∧ |
| 35 | WordTime.Solvable mode ThreeSUM.problem (2 - ε) |
| 36 | |
| 37 | axiom not_apsp (mode : Algorithms.Mode) : |
| 38 | ¬ APSPHypothesis.Hypothesis mode ↔ ∀ c : ℕ, 0 < c → |
| 39 | ∃ ε : ℝ, 0 < ε ∧ WordTime.Solvable mode (WeightedAPSP.problem c) (3 - ε) |
| 40 | |
| 41 | axiom randomized_eth : ETH.Randomized → ETH.Deterministic |
| 42 | |
| 43 | axiom randomized_seth : SETH.Randomized → SETH.Deterministic |
| 44 | |
| 45 | axiom randomized_three_sum : ThreeSUMHypothesis.Randomized → ThreeSUMHypothesis.Deterministic |
| 46 | |
| 47 | axiom randomized_apsp : APSPHypothesis.Randomized → APSPHypothesis.Deterministic |
| 48 | |
| 49 | end Lax489179.HypothesisProperties |
| 50 |
Used by
none
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