InputSet
plain-language theorem explainer
The finite collection of input variables for a problem of size n. Researchers working on SAT encodings and propagation completeness cite it when stating the PC predicate or building peeling orders. It is introduced as a direct type abbreviation with no proof content.
Claim. Let $n$ be a natural number. The input variable collection is the type of all finite subsets of the variable indices $0,1,…,n-1$.
background
The module defines constraints as either CNF clauses or XOR checks. Variables are indexed by the finite set of size n. The input collection supplies the domain over which the propagation-completeness predicate quantifies nonempty subsets. The PC predicate itself takes this collection together with a reference assignment and the two constraint systems.
proof idea
Direct abbreviation that aliases the finite-subset type constructor applied to the variable index type.
why it matters
The collection parametrizes the PC definition and all downstream constructions of peeling results and forced arborescence. It is referenced by the theorems that convert PC into an explicit peeling witness and by the equivalence that identifies forced arborescence with the peeling structure. This places the declaration inside the SAT layer that models forced implication reachability.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.