module module

`IndisputableMonolith.Complexity.SAT.Completeness`

show as: view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

depends on (6)

Lean names referenced from this declaration's body.

IndisputableMonolith.Complexity.SAT.Backprop module_import
IndisputableMonolith.Complexity.SAT.CNF module_import
IndisputableMonolith.Complexity.SAT.Isolation module_import
IndisputableMonolith.Complexity.SAT.PC module_import
IndisputableMonolith.Complexity.SAT.SmallBias module_import
IndisputableMonolith.Complexity.SAT.XOR module_import

declarations in this module (15)

def completeStateFrom L14
lemma complete_completeStateFrom L18
lemma consistent_completeStateFrom L24
structure PropagationGraph L58
inductive Reachable L63
def AllReachable L68
structure IsolationInvariant L82
def BackpropCompleteUnderInvariant L91
theorem determined_values_correct L101
def geometric_isolation_enables_propagation_hypothesis L143
theorem geometric_isolation_enables_propagation_thm L146
def polynomial_time_3sat_algorithm_hypothesis L179
theorem polynomial_time_3sat_algorithm L185
theorem backprop_succeeds_of_unique L195
theorem backprop_succeeds_from_PC L208