InputSet
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 in Recognition Science
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.
scope and limits
- Does not distinguish inputs from outputs.
- Does not encode any reference assignment or constraint collection.
- Does not impose bounds on problem size n.
- Does not reference phi, K, or other Recognition constants.
formal statement (Lean)
55abbrev InputSet (n : Nat) := Finset (Var n)
proof body
Definition body.
56
57/-- Propagation-Completeness condition (PC):
58 For every nonempty U ⊆ inputs, there exists a constraint K and v ∈ U such that
59 (i) K mentions v, (ii) K mentions no other element of U, and (iii) K determines v
60 with respect to the unique reference assignment `aRef`. -/