flipBit_other
plain-language theorem explainer
The lemma states that flipping the j-th bit of a Boolean assignment leaves the value at any other index i unchanged. Analysts of the J-cost Laplacian on SAT encodings cite this when establishing that literals independent of variable j preserve their satisfaction status under single-bit flips. The proof reduces directly by case analysis on the definition of the flip operation using the distinctness hypothesis.
Claim. For an assignment $a :$ Fin $n$ $→$ Bool and distinct indices $i,j$ in Fin $n$, the assignment obtained by flipping bit $j$ satisfies $(flipBit a j)(i) = a(i)$.
background
The JCostLaplacian module constructs a weighted graph on the Boolean hypercube whose vertices are assignments (Fin n → Bool) to n variables. Edges correspond to single bit flips with weights given by the absolute difference in satJCost. The flipBit operation inverts exactly one specified bit while leaving others fixed, as defined by the conditional expression that returns the negation only at the target index.
proof idea
The proof is a one-line term-mode simplification. It applies simp with the definition of flipBit and the hypothesis that i differs from j, which selects the unchanged branch in the conditional.
why it matters
This result supports the parent theorem literal_unchanged_by_flip, which in turn contributes to the analysis of the J-cost Laplacian quadratic form and its kernel. Within the Recognition Science framework it helps establish invariance properties under the eight-tick octave structure for complexity measures on Boolean formulas. It closes a basic scaffolding step in the complexity domain before addressing the PSD property of the Laplacian. The module notes one remaining sorry in summand extraction for the zero-form implication.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.