polynomial_time_3sat_algorithm_hypothesis
plain-language theorem explainer
This definition encodes the hypothesis that a polynomial-time algorithm exists for deciding 3-SAT on n variables, returning a satisfying assignment when one exists and none otherwise. It would be cited in attempts to prove P=NP via geometric isolation and backpropagation in SAT encodings. The definition is a direct Prop statement with no derivation or lemmas applied.
Claim. For natural number $n$, the proposition that if the program target condition holds then there exists a map from CNF formulas on $n$ variables to optional assignments such that the map returns a satisfying assignment for every satisfiable formula and returns none for every unsatisfiable formula.
background
CNF formulas are structures consisting of lists of clauses over $n$ variables. An assignment is a function from the $n$ variables to booleans. The predicate Satisfiable asserts existence of an assignment making evalCNF true, where evalCNF returns true precisely when every clause evaluates to true under the assignment. The module builds fully-determined backpropagation states from total assignments and imports CNF semantics along with isolation and small-bias constructions. Upstream results supply the literal satisfaction check and the definition of Satisfiable as existence of a satisfying assignment.
proof idea
This is a direct definition of the hypothesis proposition. The body states the required existence of the algorithm together with the two universal correctness conditions; no lemmas, tactics, or reductions are used.
why it matters
The hypothesis is the assumption in the downstream theorem polynomial_time_3sat_algorithm. Documentation explicitly marks the claim as falsified because deterministic isolation fails to yield a polynomial family, propagation completeness does not hold for expander-Tseitin formulas, and the argument relativizes, contradicting the Baker-Gill-Solovay oracle separation. It attempts to link geometric methods to polynomial-time SAT solving but supplies no connection to the Recognition Science forcing chain or phi-ladder.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.