extractFromPC
extractFromPC selects one constraint-variable pair satisfying the unique-mention and determination properties inside the propagation-completeness condition for any nonempty input subset. Researchers studying SAT propagation completeness and inductive peeling constructions cite this helper when building ordered extraction sequences. The definition applies the PC hypothesis to U and uses two choice steps to package the witness into the dependent subtype.
claimGiven an input set $I$, reference assignment $a$, CNF formula $φ$, and XOR system $H$ satisfying propagation completeness, for any nonempty $U ⊆ I$ the function returns a pair $(K, v)$ where $K$ belongs to the combined constraint set, $v ∈ U$, $K$ mentions $v$ but no other element of $U$, and $K$ determines the value of $v$ under $a$.
background
Constraints are an inductive type whose constructors are CNF clauses or XOR constraints. InputSet is an abbreviation for the Finset of designated input variables. The PC predicate asserts that every nonempty $U ⊆ I$ admits a constraint $K$ from the system together with $v ∈ U$ such that $K$ mentions only $v$ inside $U$ and determines $v$ relative to the reference assignment.
proof idea
Apply the PC hypothesis to the supplied $U$ to obtain an existential statement, then use choose to select the constraint $K$ and the variable $v$ from the nested witnesses, finally constructing the subtype element with the collected properties.
why it matters in Recognition Science
The helper is called inside buildPeelingResult to support Finset induction that assembles the complete peeling sequence of variables and constraints. It thereby enables formal statements about propagation-complete encodings in the SAT complexity layer of the Recognition Science development.
scope and limits
- Does not establish that any given encoding satisfies the PC condition.
- Does not supply a computable procedure for locating the pair.
- Applies only to nonempty subsets contained in the declared inputs.
- Does not treat the empty-set case or variables outside the input set.
Lean usage
have p := extractFromPC inputs aRef φ H hPC U hU hneformal statement (Lean)
122noncomputable def extractFromPC {n : Nat} (inputs : InputSet n) (aRef : Assignment n)
123 (φ : CNF n) (H : XORSystem n) (hPC : PC inputs aRef φ H)
124 (U : Finset (Var n)) (hU : U ⊆ inputs) (hne : U.Nonempty) :
125 { p : Constraint n × Var n //
126 p.1 ∈ constraintsOf φ H ∧
127 p.2 ∈ U ∧
128 mentionsVar p.1 p.2 = true ∧
129 (∀ w ∈ U, w ≠ p.2 → mentionsVar p.1 w = false) ∧
130 determinesVar aRef p.1 p.2 } := by
proof body
Definition body.
131 have h := hPC U hU hne
132 choose K hK using h
133 choose v hv using hK.2
134 exact ⟨(K, v), hK.1, hv.1, hv.2.1, hv.2.2.1, hv.2.2.2⟩
135
136/-- Bundled result type for peeling construction. -/