containsVar
plain-language theorem explainer
This definition determines whether a given variable index appears in the literals of a CNF clause, independent of polarity. Researchers constructing the J-cost Laplacian for SAT instances cite it when proving flip-invariance of clause satisfaction and computing variable degrees. The implementation is a direct one-line application of List.any to the clause's literals list.
Claim. For a clause $c$ over $n$ variables whose literals form a list $L$ of pairs (index, polarity) and for an index $j$, the predicate returns true if and only if there exists a pair in $L$ whose first component equals $j$.
background
The module equips CNF formulas with a weighted graph on the Boolean hypercube whose edges receive weights equal to the absolute change in satJCost under a single bit flip. A Clause n is a list of at most three literals, each a pair consisting of a variable index in Fin n and a Boolean polarity. The predicate identifies whether flipping index $j$ can affect the satisfaction status of clause $c$ and is therefore required for the quadratic form $Q_J$ and its kernel analysis. It depends on the Clause structure defined in RSatEncoding, which encodes a simplified 3-SAT representation, and on the J-cost structures imported from PhiForcingDerived.
proof idea
The definition is realized as a one-line wrapper that applies the any combinator to the literals list of the clause and tests equality of the first component against the supplied index $j$.
why it matters
It is invoked by clause_unchanged_by_flip, which states that a clause lacking variable $j$ retains the same satisfaction value after the flip, and by varDegree, which counts the clauses containing each variable. These two results supply the local combinatorial infrastructure for the J-cost Laplacian quadratic form, shown elsewhere to be positive semi-definite with constants in the kernel. The construction sits inside the Recognition Science treatment of complexity that derives spectral properties from the phi-forcing chain and the eight-tick octave.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.