PeelingWitness

formal source

  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. -/
 105def ForcedArborescence {n}
 106  (inputs : InputSet n) (aRef : Assignment n) (φ : CNF n) (H : XORSystem n) : Prop :=
 107  PeelingWitness inputs aRef φ H  -- Arborescence IS the peeling structure
 108
 109/-- Forced arborescence witness: for this development we take it to be the same data
 110    as a peeling witness (a spanning, duplicate-free list of vars with matching constraints). -/
 111abbrev ForcedArborescenceWitness {n}
 112  (inputs : InputSet n) (aRef : Assignment n) (φ : CNF n) (H : XORSystem n) : Prop :=
 113  PeelingWitness inputs aRef φ H
 114
 115/-- Program goal (graph-theoretic equivalence to target):
 116    PC ↔ existence of a forced-implication arborescence (to be proven). -/
 117def programGoal_pc_iff_arborescence {n}
 118  (inputs : InputSet n) (aRef : Assignment n) (φ : CNF n) (H : XORSystem n) : Prop :=