flipBit_flipBit
Double application of the single-bit flip on a Boolean assignment over n variables recovers the original assignment. Researchers encoding SAT instances as weighted hypercube graphs cite it to establish symmetry of edge weights. The argument reduces equality to pointwise checks via extensionality and resolves the index match by substitution.
claimLet $a$ be a Boolean assignment on $n$ variables and $k$ a variable index. Applying the operation that inverts the $k$-th bit twice yields the original assignment.
background
The J-Cost Laplacian module equips the Boolean hypercube with vertices given by assignments (maps from Fin n to Bool) and edges between assignments differing in exactly one coordinate. Edge weights are absolute differences of satJCost values under a CNF formula. The flip operation, defined pointwise by inverting the value at a chosen index while leaving all others fixed, generates the neighbors of any vertex.
proof idea
Functional extensionality reduces the claim to equality at every index j. The definition of the flip is unfolded and a case split is performed on whether j equals the chosen index k. The matching case substitutes and cancels the double negation; the non-matching case is immediate by reflexivity.
why it matters in Recognition Science
The result is invoked directly in the proof of jcostEdgeWeight_symm to replace the twice-flipped assignment and obtain symmetry of the absolute-difference weights. This symmetry is required for the quadratic form of the J-cost Laplacian to be well-defined and for the subsequent nonnegativity and kernel statements listed in the module documentation.
scope and limits
- Does not address flips at distinct indices.
- Does not depend on any CNF formula or J-cost evaluation.
- Applies only to finite n and indices in Fin n.
- Does not extend to continuous or probabilistic assignments.
Lean usage
rw [flipBit_flipBit]formal statement (Lean)
40theorem flipBit_flipBit {n : ℕ} (a : Assignment n) (k : Fin n) :
41 flipBit (flipBit a k) k = a := by
proof body
Term-mode proof.
42 funext j; simp only [flipBit]
43 split_ifs with h
44 · subst h; simp
45 · rfl
46