PeelingData

formal source

  71        determinesVar aRef K v
  72
  73/-- Peeling witness structure: a list of variables and constraints meeting the peeling conditions. -/
  74structure PeelingData {n : Nat} (inputs : InputSet n) (aRef : Assignment n) (φ : CNF n) (H : XORSystem n) where
  75  vars : List (Var n)
  76  constrs : List (Constraint n)
  77  nodup : vars.Nodup
  78  len_eq : vars.length = constrs.length
  79  cover : ∀ v : Var n, v ∈ inputs ↔ v ∈ vars
  80  step : ∀ k (hk : k < vars.length),
  81    let v := vars.get ⟨k, hk⟩
  82    let K := constrs.get ⟨k, by omega⟩
  83    mentionsVar K v = true ∧
  84    (∀ w, w ∈ vars.drop k.succ → mentionsVar K w = false) ∧
  85    determinesVar aRef K v
  86
  87/-- Peeling witness (Prop-level): there exists a peeling structure. -/
  88def PeelingWitness {n}
  89  (inputs : InputSet n) (aRef : Assignment n) (φ : CNF n) (H : XORSystem n) : Prop :=
  90  Nonempty (PeelingData inputs aRef φ H)
  91
  92/-- Forced-implication reachability (abstract): there is a directed arborescence
  93    of locally-determining constraints from OUTPUT to every input.
  94
  95    **Definition**: We define ForcedArborescence as equivalent to PeelingWitness.
  96    The peeling order (v₁, v₂, ..., vₙ) with determining constraints (K₁, K₂, ..., Kₙ)
  97    implicitly defines an arborescence where each variable's parent is determined
  98    by the constraint that determines it.
  99
 100    **Graph interpretation**: The arborescence edges are:
 101    - v → K_i for each variable v mentioned in K_i's "known" portion
 102    - K_i → v_i for the variable determined by K_i
 103
 104    This forms a directed tree rooted at OUTPUT reaching all input variables. -/