literal_unchanged_by_flip
A literal whose variable index differs from j evaluates to the same Boolean value under an assignment a and under the assignment obtained by flipping bit j in a. Researchers analyzing the J-cost Laplacian on the Boolean hypercube for CNF formulas cite this invariance when isolating the effect of a single bit flip on edge weights. The proof is a one-line wrapper that unfolds Literal.satisfiedBy and rewrites via the flipBit_other lemma.
claimLet $a$ be an assignment of $n$ Boolean variables and let $j$ be a variable index. For a literal $(i,b)$ with $i ≠ j$, the literal is satisfied by the assignment obtained from $a$ by flipping the $j$-th bit if and only if it is satisfied by $a$.
background
The module constructs the J-cost Laplacian for a CNF formula on $n$ variables as a weighted graph on the Boolean hypercube whose vertices are assignments (Fin $n$ → Bool). Edge weights are absolute differences in satJCost between Hamming-distance-1 neighbors. A literal is a pair (Fin $n$ × Bool) whose satisfaction predicate returns true precisely when the assignment matches the required polarity at the indicated index. The flipBit operation replaces the value at index $k$ while leaving all other indices unchanged. The upstream flipBit_other theorem states that flipBit a j i = a i whenever i ≠ j, which directly supplies the required equality after unfolding the satisfaction definition.
proof idea
The term-mode proof first unfolds Literal.satisfiedBy to expose the conditional expression involving a(lit.1) or its negation. It then applies the flipBit_other lemma to the literal index lit.1 under the hypothesis lit.1 ≠ j, replacing the flipped assignment value with the original and yielding syntactic equality.
why it matters in Recognition Science
The lemma isolates the effect of a bit flip to only those literals that mention the flipped variable, which is a prerequisite for showing that clause satisfaction (and therefore satJCost) changes only when the clause contains the variable. It is invoked directly by the downstream clause_unchanged_by_flip theorem. Within the J-cost Laplacian development this invariance supports the non-negativity and kernel properties of the quadratic form Q_J. The result sits inside the broader Recognition Science encoding of SAT instances but does not itself invoke the forcing chain or phi-ladder.
scope and limits
- Does not apply when the literal index equals j.
- Does not compute satJCost or edge weights.
- Does not extend to simultaneous flips of multiple bits.
- Does not depend on the structure of any particular CNF formula.
Lean usage
example {n : ℕ} (a : Assignment n) (j : Fin n) (lit : Fin n × Bool) (h : lit.1 ≠ j) : Literal.satisfiedBy lit (flipBit a j) = Literal.satisfiedBy lit a := literal_unchanged_by_flip a j lit hformal statement (Lean)
96theorem literal_unchanged_by_flip {n : ℕ} (a : Assignment n) (j : Fin n)
97 (lit : Fin n × Bool) (hlit : lit.1 ≠ j) :
98 Literal.satisfiedBy lit (flipBit a j) = Literal.satisfiedBy lit a := by
proof body
Term-mode proof.
99 unfold Literal.satisfiedBy
100 rw [flipBit_other a j lit.1 hlit]
101
102/-- A clause not containing variable j has the same satisfaction after flipping j. -/