flipBit_ne
plain-language theorem explainer
The single-bit-flip map on Boolean assignments of length n yields a distinct assignment. Workers constructing the J-cost Laplacian on the hypercube graph cite it to guarantee that Hamming-distance-1 pairs are proper edges without self-loops. The short proof assumes functional equality, evaluates both sides at the flipped coordinate via congruence, and obtains an immediate contradiction after unfolding the definition.
Claim. Let $n$ be a natural number, let $a$ be a function from the finite set of $n$ indices to the Booleans, and let $k$ be an index in that set. The function obtained by negating the value of $a$ at coordinate $k$ differs from $a$.
background
The module defines a weighted graph on the Boolean hypercube whose vertices are all assignments (Fin n → Bool). Edges connect assignments at Hamming distance one, realized by the flipBit operation that inverts exactly one coordinate. Edge weights are absolute differences of satJCost values, so the Laplacian quadratic form is well-defined only when these pairs are distinct. The upstream flipBit definition supplies the concrete map: it returns the function that equals a everywhere except at k, where it returns the negation. Related cost definitions from MultiplicativeRecognizerL4 and ObserverForcing supply the J-cost values whose differences become the weights.
proof idea
Assume for contradiction that flipBit a k equals a as functions. Apply congruence to obtain equality of their values at index k. Unfold the definition of flipBit inside the resulting equation to reach ¬(a k) = a k, which is impossible for any Boolean value.
why it matters
The result ensures the hypercube graph underlying the J-cost Laplacian has no self-loops, so the quadratic form Q_J is well-defined on genuine edges. It is a prerequisite for the non-negativity and kernel properties listed in the module documentation. In the Recognition Science setting it supports the translation of SAT structure into a discrete Laplacian whose spectrum can be compared with the phi-ladder and Berry thresholds.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.