ParityCircuit

Comment and keyword shading is a reading aid only. It is not a verification marker; the evidence is the build record on the Build page.

1import BinaryReadout23/- Phase 4, Priority 2c: the concrete parity reduction.  Written by Claude4   (10 October 2026).  Lean 4.26.0, core/Std only.56   Replaces the phase-2 generic closure/hardness packaging by an explicit circuit7   composition.  A binary move selector (BCirc, B = 2 bits per heap, N = m+1 heaps)8   that plays a winning move on every winning 2-bit board yields, by LEAF9   SUBSTITUTION (two-bit heap encoding of (2, b_1, ..., b_m)), a formula of the SAME10   depth and size, reading only the m parity inputs, that computes b_1 XOR ... XOR b_m.11   Hence the classical statement "no formula of depth ≤ d and size ≤ s computes parity12   of m bits" (ParityHard) rules out such selectors.  ParityHard itself follows from13   the correlation premise with error ε < 1/2, so the single remaining assumption is14   the classical AC0 parity theorem. -/1516namespace NimAudit17namespace ParityCircuit1819open Prob AC0 AC0.Circ Game Bridge Rollout CorrBridge BinReadout2021attribute [local simp] Rat.add_zero Rat.zero_add2223/-- The move of a binary selector (no observed bit). -/24def binMove (S : BCirc) (N : Nat) (P : List Nat) : Option (Nat × Nat) :=25  binReadoutOf 2 N (fun _ => S) P false2627/-- Strong mastery on 2-bit boards with N heaps: from every winning position the28    selector outputs a legal move to a losing position. -/29def StrongMastery (S : BCirc) (N : Nat) : Prop :=30  ∀ P : List Nat, P.length = N → Width 2 P → Win P →31    ∃ i v x, binMove S N P = some (i, v) ∧ P[i]? = some x ∧ v < x ∧ Lose (P.set i v)3233theorem par_eq_parity : ∀ y : List Bool, par y = parity y34  | [] => rfl35  | b :: y => by simp [par, parity, par_eq_parity y]3637theorem length_encode (bs : List Bool) : (encode bs).length = bs.length + 1 := by38  simp [encode]3940theorem encode_width (bs : List Bool) : Width 2 (encode bs) := by41  intro x hx42  simp only [encode, List.mem_cons, List.mem_map] at hx43  rcases hx with rfl | ⟨b, _, rfl⟩44  · decide45  · have := Bool.toNat_le b; omega4647/-- A winning move from (2, b_1, ..., b_m) is (index 0, new value parity). -/48theorem winning_move_on_encode (bs : List Bool) {i v x : Nat} (hx : (encode bs)[i]? = some x)49    (hv : v < x) (hz : nimSum ((encode bs).set i v) = 0) : i = 0 ∧ v = (parity bs).toNat := by50  have hred := unique_zero_move bs _ (set_move hx hv) hz51  cases i with52  | zero =>53    refine ⟨rfl, ?_⟩54    have := congrArg List.head? hred55    simp [encode, reduced] at this56    exact this57  | succ i =>58    exfalso59    have := congrArg List.head? hred60    simp [encode, reduced] at this61    have := Bool.toNat_le (parity bs)62    omega6364/-- Two big-endian bits encoding 0 or 1: the high bit is 0 and the low bit is the value. -/65theorem low_bit_of_two {l : List Bool} (hl : l.length = 2) {p : Bool} (h : toNatBE l = p.toNat) :66    l.getD 1 false = p := by67  match l, hl with68  | [a, c], _ =>69    simp only [toNatBE, List.length_cons, List.length_nil] at h70    cases a <;> cases c <;> cases p <;> simp_all7172/-- Leaf substitution realising the two-bit encoding of (2, y_1, ..., y_m). -/73def parSubst (m : Nat) : Nat → Circ := fun j =>74  if j = 0 then const true75  else if j < 2 * (m + 1) then (if j % 2 = 1 ∧ 2 ≤ j then input (j / 2 - 1) else const false)76  else const false7778theorem parSubst_leaf (m j : Nat) : IsLeaf (parSubst m j) := by79  unfold parSubst; split80  · simp [IsLeaf]81  · split82    · split <;> simp [IsLeaf]83    · simp [IsLeaf]8485theorem parSubst_eval {m : Nat} {y : List Bool} (hy : y.length = m) (j : Nat) :86    eval (vfun y) (parSubst m j) = boardBits 2 (encode y) j := by87  unfold parSubst boardBits88  rw [length_encode, hy]89  by_cases h0 : j = 090  · subst h0; simp [encode]; decide91  · simp only [h0, if_false]92    by_cases hj : j < 2 * (m + 1)93    · simp only [hj, if_true, show j < 2 * (m + 1) from hj]94      have hpos : 1 ≤ j / 2 ∨ j = 1 := by omega95      rcases hpos with hpos | h196      · have hget : (encode y).getD (j / 2) 0 = (y.getD (j / 2 - 1) false).toNat := by97          simp only [encode, List.getD_eq_getElem?_getD]98          rw [show j / 2 = (j / 2 - 1) + 1 by omega, List.getElem?_cons_succ, List.getElem?_map]99          have : j / 2 - 1 < y.length := by rw [hy]; omega100          simp [List.getElem?_eq_getElem this]101        rw [hget]102        rcases Nat.mod_two_eq_zero_or_one j with hm | hm103        · have : ¬ (j % 2 = 1 ∧ 2 ≤ j) := by omega104          simp only [this, if_false, eval_const]105          first | rw [show 2 - 1 - j % 2 = 1 by omega] | skip106          cases y.getD (j / 2 - 1) false <;> rfl107        · have : j % 2 = 1 ∧ 2 ≤ j := ⟨hm, by omega⟩108          simp only [this, and_self, if_true, eval_input, vfun]109          first | rw [show 2 - 1 - j % 2 = 0 by omega] | skip110          cases y.getD (j / 2 - 1) false <;> rfl111      · subst h1; simp [encode]112    · simp [hj]113114theorem parSubst_max (m j : Nat) : maxInput (parSubst m j) ≤ m := by115  unfold parSubst; split116  · simp117  · split118    · split119      · simp; omega120      · simp121    · simp122123/-- The parity formula extracted from a selector: the low value bit, restricted to124    the encoded boards. -/125def parityFormula (S : BCirc) (m : Nat) : Circ := subst (parSubst m) (getC S.val 1)126127/-- EXTRACTION THEOREM.  If a binary selector with BBound (depth ≤ d, size ≤ s,128    2 value bits) has strong mastery on 2-bit boards with m+1 heaps, then129    parityFormula S m computes parity of every y ∈ {0,1}^m, has depth ≤ d and size130    ≤ s, and reads only the m parity inputs. -/131theorem extraction {S : BCirc} {m r d s : Nat} (hb : BBound S (m + 1) 2 r d s)132    (hS : StrongMastery S (m + 1)) :133    (∀ y : List Bool, y.length = m → eval (vfun y) (parityFormula S m) = par y) ∧134    depth (parityFormula S m) ≤ d ∧ size (parityFormula S m) ≤ s ∧135    maxInput (parityFormula S m) ≤ m := by136  have hval1 : getC S.val 1 ∈ S.val := getC_mem (by rw [hb.val_len]; decide)137  refine ⟨?_, ?_, ?_, ?_⟩138  · intro y hy139    unfold parityFormula140    rw [eval_subst]141    have hz : (fun j => eval (vfun y) (parSubst m j)) = boardBits 2 (encode y) := by142      funext j; exact parSubst_eval hy j143    rw [hz]144    have hW : Win (encode y) := (win_iff _).2 (nimSum_encode_ne y)145    obtain ⟨i, v, x, hmove, hx, hlt, hlose⟩ :=146      hS (encode y) (by rw [length_encode, hy]) (encode_width y) hW147    have hz0 := (lose_iff _).1 hlose148    obtain ⟨_, hvp⟩ := winning_move_on_encode y hx hlt hz0149    -- read the value bits off the selector's output150    unfold binMove binReadoutOf at hmove151    split at hmove152    · split at hmove153      · simp only [Option.some.injEq, Prod.mk.injEq] at hmove154        obtain ⟨_, hvdef⟩ := hmove155        rw [hvp] at hvdef156        have hl : (S.val.map (eval (boardBits 2 (encode y)))).length = 2 := by simp [hb.val_len]157        have := low_bit_of_two hl hvdef158        rw [eval_getC, this, par_eq_parity]159      · cases hmove160    · cases hmove161  · unfold parityFormula162    rw [depth_subst_leaf _ (parSubst_leaf m)]163    exact hb.depth_val _ hval1164  · unfold parityFormula165    rw [size_subst_leaf _ (parSubst_leaf m)]166    exact hb.size_val _ hval1167  · exact maxInput_subst_le _ m (parSubst_max m) _168169/-- The CLASSICAL HARDNESS STATEMENT for given depth, size and input length: no170    formula of depth ≤ d and size ≤ s reading m inputs computes parity of m bits. -/171def ParityHard (d s m : Nat) : Prop :=172  ∀ C : Circ, depth C ≤ d → size C ≤ s → maxInput C ≤ m →173    ∃ y ∈ bitvecs m, eval (vfun y) C ≠ par y174175/-- SINGLE-FRAME BARRIER (circuit form).  Under ParityHard d s m, no binary selector176    with BBound (depth ≤ d, size ≤ s) has strong mastery on 2-bit boards with m+1177    heaps. -/178theorem no_small_strong_master {S : BCirc} {m r d s : Nat} (hb : BBound S (m + 1) 2 r d s)179    (hard : ParityHard d s m) : ¬ StrongMastery S (m + 1) := by180  intro hS181  obtain ⟨heval, hd, hs, hm⟩ := extraction hb hS182  obtain ⟨y, hy, hne⟩ := hard _ hd hs hm183  exact hne (heval y (mem_bitvecs_length hy))184185/-! ## The correlation premise implies hardness -/186187theorem rsum_odd (n : Nat) :188    rsum (bitvecs (n + 1)) (fun y => if par y then (1 : Rat) else 0) = (2 : Rat) ^ n := by189  have hsplit : ∀ k, rsum (bitvecs k) (fun y => if par y then (1 : Rat) else 0) +190      rsum (bitvecs k) (fun y => if par y then (0 : Rat) else 1) = (2 : Rat) ^ k := by191    intro k192    rw [← rsum_add, ← count_bitvecs k]193    apply rsum_congr; intro y _; cases par y <;> simp194  rw [rsum_bitvecs_succ]195  have e1 : rsum (bitvecs n) (fun v => if par (false :: v) then (1 : Rat) else 0) =196      rsum (bitvecs n) (fun y => if par y then (1 : Rat) else 0) := by197    apply rsum_congr; intro v _; simp [par]198  have e2 : rsum (bitvecs n) (fun v => if par (true :: v) then (1 : Rat) else 0) =199      rsum (bitvecs n) (fun y => if par y then (0 : Rat) else 1) := by200    apply rsum_congr; intro v _; cases h : par v <;> simp [par, h]201  rw [e1, e2, hsplit]202203/-- A formula computing parity on m ≥ 1 inputs has correlation −1/2 with parity204    (in the premise's 0/1-indicator convention); so the premise with ε < 1/2205    implies ParityHard. -/206theorem hard_of_premise {d s m : Nat} {ε : Rat} (hm : 1 ≤ m) (hε : ε < 1 / 2)207    (h : ParityCorrPremise d s m ε) : ParityHard d s m := by208  intro C hd hs hmx209  by_cases hall : ∀ y ∈ bitvecs m, eval (vfun y) C = par y210  · exfalso211    obtain ⟨k1, _⟩ := h C hd hs hmx212    have e : rsum (bitvecs m) (fun y => ind (eval (vfun y) C) * sgn (par y)) =213        (-1) * rsum (bitvecs m) (fun y => if par y then (1 : Rat) else 0) := by214      rw [← rsum_mul_left]215      apply rsum_congr; intro y hy216      rw [hall y hy]; unfold ind sgn; cases par y <;> simp <;> grind217    obtain ⟨n, rfl⟩ : ∃ n, m = n + 1 := ⟨m - 1, by omega⟩218    rw [e, rsum_odd, Rat.pow_succ] at k1219    have hp := two_pow_pos' n220    have hp' : (2 : Rat) ^ n ≠ 0 := Rat.ne_of_gt hp221    have : (-1) * (2 : Rat) ^ n / ((2 : Rat) ^ n * 2) = -(1 / 2) := by grind222    rw [this] at k1223    grind224  · -- some y disagrees225    apply Classical.byContradiction226    intro hno227    apply hall228    intro y hy229    by_cases hq : eval (vfun y) C = par y230    · exact hq231    · exact absurd ⟨y, hy, hq⟩ hno232233/-- SINGLE-FRAME BARRIER UNDER THE CORRELATION PREMISE: if the classical parity-234    correlation premise holds at depth d, size s, input length m ≥ 1 with ε < 1/2,235    no binary selector with BBound (d, s) has strong mastery on 2-bit boards with236    m + 1 heaps. -/237theorem no_strong_master_of_premise {S : BCirc} {m r d s : Nat} {ε : Rat}238    (hb : BBound S (m + 1) 2 r d s) (hm : 1 ≤ m) (hε : ε < 1 / 2)239    (h : ParityCorrPremise d s m ε) : ¬ StrongMastery S (m + 1) :=240  no_small_strong_master hb (hard_of_premise hm hε h)241242243/-! ## Axiom audit -/244245#print axioms par_eq_parity246#print axioms length_encode247#print axioms encode_width248#print axioms winning_move_on_encode249#print axioms low_bit_of_two250#print axioms parSubst_leaf251#print axioms parSubst_eval252#print axioms parSubst_max253#print axioms extraction254#print axioms no_small_strong_master255#print axioms rsum_odd256#print axioms hard_of_premise257#print axioms no_strong_master_of_premise258end ParityCircuit259end NimAudit