constraintsOf
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.
claimLet $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 in Recognition Science
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.
scope and limits
- Does not verify satisfiability of the assembled constraints.
- Does not enforce or check the propagation-completeness condition.
- Does not reference an input set or reference assignment.
- Does not compute J-cost, defect distance, or phi-ladder rung values.
formal statement (Lean)
51def constraintsOf {n} (φ : CNF n) (H : XORSystem n) : List (Constraint n) :=
proof body
Definition body.
52 (φ.clauses.map Constraint.cnf) ++ (H.map Constraint.xor)
53
54/-- Set of input variables (as a finset) for PC property articulation. -/