pith. machine review for the scientific record. sign in
def definition def or abbrev high

compatible

show as:
view Lean formalization →

A definition stating that a partial assignment σ over n variables is compatible with a total assignment a exactly when σ agrees with a on every decided variable. Researchers formalizing backpropagation soundness for SAT instances in complexity reductions would cite this predicate when proving preservation under propagation steps. It is introduced directly as a universal quantification over variables with a disjunction on the Option type.

claimLet $σ$ be a partial assignment and $a$ a total assignment over $n$ variables. Then $σ$ is compatible with $a$ if and only if for every variable $v$, either $σ(v) = some(a(v))$ or $σ(v) = none$.

background

PartialAssignment is the type of maps from variables to Option Bool, with none marking unknown values and some b marking determined bits. Assignment (from both RSatEncoding and the local CNF module) is the type of total maps from variables to Bool. The module develops backpropagation over CNF formulas augmented with XOR systems, using these types to track determined literals during search.

proof idea

This is a definition, not a derived theorem. It directly encodes the agreement condition as the predicate ∀ v, σ v = some (a v) ∨ σ v = none. No lemmas or tactics are applied; the body is the primitive predicate consumed by later soundness results.

why it matters in Recognition Science

The predicate is invoked in downstream lemmas including bp_step_sound (preservation of compatibility under a propagation step) and clauseUnit_correct (correctness of unit-clause inference under a satisfying assignment). It supplies the basic interface for partial information in the SAT backpropagation development, which in turn supports the PvsNPFromBIT certification and related complexity arguments within Recognition Science.

scope and limits

formal statement (Lean)

 114def compatible {n} (σ : PartialAssignment n) (a : Assignment n) : Prop :=

proof body

Definition body.

 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. -/

used by (40)

From the project-wide theorem graph. These declarations reference this one in their body.

… and 10 more

depends on (8)

Lean names referenced from this declaration's body.