mentionsVarClause
plain-language theorem explainer
mentionsVarClause determines whether a given variable index appears inside a CNF clause. Researchers formalizing SAT encodings or variable-dependency analysis in mixed constraint systems cite it when building higher-level mention predicates. The definition reduces the query to an existential scan over the clause's literals via the literal-level equality test.
Claim. Let $C$ be a clause (a list of literals over $n$ variables) and let $v$ be a variable index in $0..n-1$. Then $M(C,v)$ is true if and only if there exists a literal $l$ in $C$ such that the underlying variable of $l$ equals $v$.
background
A clause is a disjunction of literals; each literal is either a positive or negated variable index drawn from Fin n. Variables are simply the indices Fin n. The supporting literal predicate decides equality after discarding the sign bit. The module defines constraints as either CNF clauses or XOR checks, so this definition supplies the clause branch of any variable-mention query. Upstream the Clause structure records a list of at most three signed indices together with an explicit length bound.
proof idea
One-line wrapper that applies the any combinator to the literals list of the clause, feeding each literal to the mentionsVarLit test for the target variable.
why it matters
The definition is invoked by mentionsVar to cover the CNF case inside mixed constraints. It therefore supplies the variable-mention infrastructure required by the SAT encoding layer of the complexity module. The construction sits inside the broader formalization of constraint satisfaction problems that the Recognition framework uses to model computational structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.