flipBit
plain-language theorem explainer
The flipBit operation inverts the Boolean value at a specified position k within an n-variable assignment. Analysts of the J-cost Laplacian on SAT instances cite this when building the hypercube graph and its edge weights. The definition is realized by a conditional functional update that negates only the target bit.
Claim. Let $a :$ Fin $n$ $→$ Bool be an assignment and $k :$ Fin $n$. Then flipBit$(a,k)$ is the assignment $a'$ defined by $a'(j) = !a(j)$ if $j=k$ and $a'(j)=a(j)$ otherwise.
background
The module equips the Boolean hypercube with a graph whose vertices are assignments, i.e., functions from Fin n to Bool as defined upstream in RSatEncoding: an assignment is a Boolean function on variables. Edges connect assignments differing by one bit, with weights given by the absolute difference in satJCost after the flip. The local setting is the quadratic form Q_J that sums these weighted squared differences over all assignments and flips.
proof idea
The definition is given directly by the lambda that returns the negation of the assignment value at index k and the original value at every other index. No lemmas are applied; it is a primitive functional constructor.
why it matters
This supplies the neighbor map used to define jcostEdgeWeight as the absolute cost difference after a flip and to generate the inductive CostConnected relation on positive-weight paths. It therefore underpins the non-negativity of the Laplacian quadratic form and the fact that constants lie in its kernel. In the Recognition framework the construction sits inside the SAT encoding layer that connects to the J-uniqueness and Recognition Composition Law.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.