PeelingData
plain-language theorem explainer
PeelingData bundles ordered lists of variables and constraints that cover exactly the input set, remain duplicate-free, match in length, and satisfy a sequential determination property under a fixed reference assignment. Researchers formalizing propagation-completeness for hybrid CNF-XOR SAT instances would cite the structure when constructing implication chains. The declaration is a plain six-field structure whose predicates directly encode the required coverage and non-overlap conditions.
Claim. A record consisting of lists $vars$ and $constrs$ of equal length together with proofs that $vars$ is duplicate-free, that $vars$ equals the input set, and that for each index $k$ the constraint at position $k$ mentions the variable at $k$, mentions none of the later variables, and determines that variable under the reference assignment.
background
InputSet n abbreviates Finset (Var n) where Var n = Fin n. Constraint n is the inductive type whose constructors are cnf (a Clause n) and xor (an XORConstraint n). The module states that constraints are either CNF-clauses or XOR-checks. The PC condition in the InputSet doc-comment requires that every nonempty subset U of inputs admits a constraint K and variable v in U such that K mentions v, mentions no other element of U, and determines v with respect to aRef.
proof idea
The declaration is a structure definition. Its six fields are introduced directly: vars and constrs as lists, nodup asserting duplicate-freeness, len_eq asserting equal lengths, cover asserting exact coverage of the input set, and step asserting the three local conditions (mention, non-mention of later variables, and determination) at each position.
why it matters
PeelingData supplies the concrete carrier whose non-emptiness is asserted by the downstream PeelingWitness definition. It makes the abstract propagation-completeness condition stated in the InputSet doc-comment into a usable data type, supporting statements of forced-implication reachability. The structure therefore sits at the base of any formal argument that a given CNF-XOR system satisfies the PC property.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.