`consistent`

definition

show as: view math explainer →

module: IndisputableMonolith.Complexity.SAT.Backprop
domain: Complexity
line: 109 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Complexity.SAT.Backprop on GitHub at line 109.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

used by

formal source

 106  ∀ v, (s.assign v).isSome = true
 107
 108/-- Predicate: state is consistent with φ ∧ H (semantic notion). -/
 109def consistent {n} (s : BPState n) (φ : CNF n) (H : XORSystem n) : Prop :=
 110  ∃ a : Assignment n, (∀ v, s.assign v = some (a v)) ∧
 111    evalCNF a φ = true ∧ satisfiesSystem a H
 112
 113/-- Compatibility: a partial assignment agrees with a total assignment on known bits. -/
 114def compatible {n} (σ : PartialAssignment n) (a : Assignment n) : Prop :=
 115  ∀ v, σ v = some (a v) ∨ σ v = none
 116
 117/-- If σ is compatible with a and we set v to (a v), the result is still compatible. -/
 118lemma compatible_setVar {n} (σ : PartialAssignment n) (a : Assignment n) (v : Var n)
 119    (hcompat : compatible σ a) :
 120    compatible (setVar σ v (a v)) a := by
 121  intro w
 122  by_cases hwv : w = v
 123  · subst hwv
 124    left
 125    simp [setVar_same]
 126  · rw [setVar_ne σ v w (a v) hwv]
 127    exact hcompat w
 128
 129/-!
 130## Semantic Correctness for XOR Propagation
 131
 132The xorMissing function produces the correct value for a satisfying assignment.
 133This is now a **proved theorem**, not an axiom.
 134-/
 135
 136-- Helper lemmas for xorMissing_correct proof
 137private lemma not_isSome_eq_isNone' {α : Type*} (o : Option α) : (!o.isSome) = o.isNone := by
 138  cases o <;> rfl
 139

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.