flipBit_flipBit
plain-language theorem explainer
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.
Claim. Let $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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.