polynomial_time_3sat_algorithm
The declaration shows that under the named hypothesis for parameter n, every ProgramTarget of size n admits a map from CNF formulas to optional assignments that returns a satisfying assignment exactly when one exists. Complexity researchers working on SAT decision procedures inside the Recognition Science model would cite this when establishing efficient solvability. The proof is a direct one-line application of the hypothesis with no additional steps.
claimAssuming the hypothesis that a polynomial-time 3SAT algorithm exists for $n$ variables, for any program target of size $n$ there exists a function $alg$ from CNF formulas over $n$ variables to optional assignments such that $alg$ returns a satisfying assignment for every satisfiable formula and returns none for every unsatisfiable formula.
background
The module constructs fully-determined backpropagation states from total assignments. CNF formulas are structures consisting of lists of clauses over $n$ variables, with evaluation defined by checking that every clause holds under a given assignment. Satisfiability is the existence of at least one assignment making the entire conjunction true. Upstream results supply the cellular-automaton step operation that applies a local rule to each cell and the basic definition of an assignment as a map from variables to booleans.
proof idea
The proof is a one-line wrapper that applies the hypothesis polynomial_time_3sat_algorithm_hypothesis directly to the given ProgramTarget.
why it matters in Recognition Science
The result supplies the existence claim for a polynomial-time 3SAT solver that the SAT completeness module requires. It closes the semantic existence argument for backpropagation under unique XOR solutions without depending on a concrete cellular-automaton step system. No downstream theorems are recorded, indicating the declaration functions as a terminal interface for the polynomial-time claim in the complexity domain.
scope and limits
- Does not prove the hypothesis itself.
- Does not exhibit an explicit algorithm or runtime bound.
- Does not handle reductions from other NP-complete problems.
- Does not address concrete 3SAT instances or clause densities.
formal statement (Lean)
185theorem polynomial_time_3sat_algorithm (n : Nat)
186 (h : polynomial_time_3sat_algorithm_hypothesis n) :
187 ProgramTarget n →
188 ∃ (alg : CNF n → Option (Assignment n)),
189 (∀ φ, Satisfiable φ → ∃ x, alg φ = some x ∧ evalCNF x φ = true) ∧
190 (∀ φ, ¬Satisfiable φ → alg φ = none) :=
proof body
Term-mode proof.
191 h
192
193/-- Backpropagation succeeds when there is a unique solution under XOR constraints.
194This is a semantic existence result that does not rely on a specific step system. -/