IndisputableMonolith.Complexity.SAT.Completeness
This module constructs a fully-determined backpropagation state from any total assignment to the variables of a SAT instance. Researchers developing polynomial-time 3SAT algorithms or propagation-based solvers in the Recognition framework would cite the state-completion functions. It assembles imported CNF, XOR, and isolation structures to define complete states and verify their consistency and reachability properties.
claimGiven a total assignment $σ : Fin n → {0,1}$, the map completeStateFrom(σ) produces a backpropagation state in which every variable receives a definite Boolean value, satisfying the isolation invariant and propagation-graph reachability.
background
The module works inside the SAT setting where instances are built from CNF clauses or XOR parity checks over variables indexed by Fin n. Partial assignments appear as maps to Option Bool, with none marking undetermined entries. Isolation supplies XOR families that geometrically separate variable influences, while Backprop tracks determined values under propagation. The module uses these imported definitions to lift a total assignment into a fully fixed state.
proof idea
This is a definition module, no proofs.
why it matters in Recognition Science
The module supplies the state-completion mechanism required by the polynomial_time_3sat_algorithm_hypothesis. It closes the passage from arbitrary total assignments to fully determined, consistent backpropagation states, enabling the completeness claim under the geometric isolation invariant.
scope and limits
- Does not prove NP-completeness of 3SAT.
- Does not exhibit an explicit polynomial-time algorithm.
- Does not handle unsatisfiable instances.
- Does not bound the number of propagation steps.
depends on (6)
declarations in this module (15)
-
def
completeStateFrom -
lemma
complete_completeStateFrom -
lemma
consistent_completeStateFrom -
structure
PropagationGraph -
inductive
Reachable -
def
AllReachable -
structure
IsolationInvariant -
def
BackpropCompleteUnderInvariant -
theorem
determined_values_correct -
def
geometric_isolation_enables_propagation_hypothesis -
theorem
geometric_isolation_enables_propagation_thm -
def
polynomial_time_3sat_algorithm_hypothesis -
theorem
polynomial_time_3sat_algorithm -
theorem
backprop_succeeds_of_unique -
theorem
backprop_succeeds_from_PC