InputSet
plain-language theorem explainer
InputSet n denotes the finite collection of designated input variables for an n-variable SAT instance. Researchers formalizing propagation-completeness or constructing peeling orders cite it when quantifying over nonempty subsets U in the PC predicate. The declaration is a direct abbreviation that renames Finset (Fin n) to mark the domain of the forcing relation.
Claim. $InputSet(n) := Finset(Var(n))$, where $Var(n)$ is the set of $n$ variable indices.
background
The module models constraints as CNF clauses or XOR checks. Variables are indexed by Fin n, and InputSet n collects the designated inputs as a Finset. This collection supplies the domain for the PC predicate, which asserts that every nonempty U subset of the inputs contains a variable v uniquely determined by some constraint K that mentions only v inside U.
proof idea
The declaration is an abbreviation that directly aliases Finset (Var n). No lemmas or tactics are invoked; the name simply clarifies the role of the input set inside PC, ForcedArborescence, and the inductive peeling constructions.
why it matters
InputSet supplies the input domain for PC and therefore for ForcedArborescence (defined as PeelingWitness) and the inductive buildPeelingResult. It anchors the equivalence between propagation-completeness and forced arborescences, supporting the reduction of SAT instances to structures compatible with the Recognition forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.