constraintsOf
plain-language theorem explainer
constraintsOf assembles the full list of constraints for a CNF formula paired with an XOR system by wrapping each clause as a CNF-constraint and each XOR element as an XOR-constraint then concatenating the results. Researchers formalizing propagation-completeness for mixed SAT instances in Recognition Science cite this when stating the PC predicate. The definition is a direct one-line construction via list map and append.
Claim. Let $n$ be a natural number, let $φ$ be a CNF formula over $n$ variables, and let $H$ be an XOR system over the same variables. Then constraintsOf$(φ, H)$ is the list obtained by mapping each clause of $φ$ under the CNF-constraint constructor and each element of $H$ under the XOR-constraint constructor, followed by concatenation of the two lists.
background
Constraints are defined inductively as either CNF-clauses or XOR-checks. CNF packages a list of clauses, each a disjunction of literals over $n$ variables, while XORSystem abbreviates a list of XOR constraints. The module establishes propagation-completeness for SAT instances that mix CNF clauses and XOR checks. Upstream, the cost algebra supplies the shifted cost $H(x) = J(x) + 1$ satisfying the d'Alembert equation $H(xy) + H(x/y) = 2 H(x) H(y)$ derived from the recognition composition law.
proof idea
One-line definition that maps the clauses field of the CNF argument under the cnf constructor, maps the XORSystem argument under the xor constructor, and appends the resulting lists.
why it matters
This definition supplies the constraint list required by the propagation-completeness predicate PC and by the extraction helper extractFromPC. It therefore supports the formal statement of the PC condition inside the Complexity.SAT.PC module. In the Recognition Science setting the construction enables discrete analysis of constraint systems that ultimately tie back to the forcing chain steps T5 through T8 and the phi-ladder mass formula.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.