 151/-- **PROVED**: Build the peeling order via Finset induction.
 152    At each step, PC gives constraint K and variable v ∈ U that K uniquely determines.
 153    Recursively peel U \ {v} to get (vs, cs), then return (v :: vs, K :: cs). -/
 154noncomputable def buildPeelingResult {n : Nat} (inputs : InputSet n) (aRef : Assignment n)
 155    (φ : CNF n) (H : XORSystem n) (hPC : PC inputs aRef φ H)
 156    (U : Finset (Var n)) (hU : U ⊆ inputs) :
 157    PeelingResult inputs aRef φ H U := by
 158  induction' hcard : U.card with k ih generalizing U
 159  · -- Base case: U is empty
 160    exact {
 161      vars := []
 162      constrs := []
 163      len_eq := rfl
 164      nodup := List.nodup_nil
 165      cover := by intro v; simp; rw [Finset.card_eq_zero.mp hcard]; exact Finset.not_mem_empty v
 166      step := by intro k hk; simp at hk
 167    }
 168  · -- Inductive case: U is nonempty
 169    have hne : U.Nonempty := Finset.card_pos.mp (by omega)
 170    let ⟨⟨K, v⟩, _, hvmem, hment, honly, hdet⟩ := extractFromPC inputs aRef φ H hPC U hU hne
 171    let U' := U.erase v
 172    have hU' : U' ⊆ inputs := fun w hw => hU (Finset.mem_erase.mp hw).2
 173    have hcard' : U'.card = k := by rw [Finset.card_erase_of_mem hvmem]; omega
 174    let rec_result := ih U' hU' hcard'
 175    exact {
 176      vars := v :: rec_result.vars
 177      constrs := K :: rec_result.constrs
 178      len_eq := by simp only [List.length_cons, rec_result.len_eq]
 179      nodup := by
 180        refine List.Nodup.cons ?_ rec_result.nodup
 181        intro hv_in_vs
 182        have hv_in_U' := (rec_result.cover v).mp hv_in_vs
 183        exact (Finset.not_mem_erase v U) hv_in_U'
 184      cover := by

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.