Barrier

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 Family2import ParityCircuit34/- Phase 6, Priority 1b: the barrier side of the three bypasses.  Written by Claude5   (10 October 2026).  Lean 4.26.0, core/Std only.67   EXTERNAL INPUT.  `ParityNotAC0` is the classical worst-case statement (Furst–Saxe–8   Sipser, Ajtai, Håstad): for each depth d and polynomial size c·m^k, for all large m,9   no formula of depth ≤ d and size ≤ c·m^k reading m inputs computes parity.  It is a10   theorem PARAMETER, never an axiom; Classical.lean derives it from the negligible11   correlation form of Håstad (2014), Corollary 3.2, with the convention adapters.1213   PROVED HERE.14   * extraction_enc: the parity extraction of phase 4 needs the selector's behaviour only15     on the encoded boards (2, b₁, …, b_m), B = 2.16   * barrier_core / barrier_fam / barrier_net: under ParityNotAC0 no AC0 formula family17     and no fixed-scale network family (fixed W, constant layers, polynomial widths)18     computes, on every encoded board, a map that plays a winning move there.19   * The COMPLETE multi-head map (rollouts executed by the compiled policy networks, then20     the compiled readout) and the COMPLETE recurrent map (2N+2 threshold-controller21     updates from the initial state) equal decisionMove on every board of width B; hence22     neither is computed by a single-frame AC0 family or network family, even on the23     two-bit encoding family.24   * Why this does not contradict the two-frame AC0 map: on a promised pair (Q, Game.encode y)25     the predecessor Q already carries the parity locally (promised_pred_parity), the26     two-frame network indeed outputs (0, parity y) there, and no AC0 family can produce27     such a promised predecessor from y (no_ac0_predecessor). -/2829namespace NimAudit30namespace Barrier3132open Game Rollout Prob Attain Recurrent AC0 AC0.Circ CorrBridge AttainCircuit Bridge SelectCircuit33  BinReadout Controller ControllerBits PriorityEncoder ThresholdNet ThresholdInst FiniteNet WholeGame34  Family ParityCircuit3536/-- CLASSICAL WORST-CASE PARITY HARDNESS, family form (EXTERNAL HYPOTHESIS). -/37def ParityNotAC0 : Prop := ∀ d c k : Nat, ∃ m0 : Nat, ∀ m, m0 ≤ m → ParityHard d (c * m ^ k) m3839/-! ## Extraction from the encoded boards only -/4041/-- The selector plays a zero-restoring legal move on every encoded board with m bits. -/42def EncWin (S : BCirc) (m : Nat) : Prop :=43  ∀ y : List Bool, y.length = m → ∃ i v x, binMove S (m + 1) (Game.encode y) = some (i, v) ∧44    (Game.encode y)[i]? = some x ∧ v < x ∧ nimSum ((Game.encode y).set i v) = 04546/-- EXTRACTION ON THE ENCODING FAMILY: same formula, depth, size and inputs as phase 4,47    but assuming correct play only on the encoded boards. -/48theorem extraction_enc {S : BCirc} {m r d s : Nat} (hb : BBound S (m + 1) 2 r d s) (hS : EncWin S m) :49    (∀ y : List Bool, y.length = m → eval (vfun y) (parityFormula S m) = par y) ∧50    depth (parityFormula S m) ≤ d ∧ size (parityFormula S m) ≤ s ∧51    maxInput (parityFormula S m) ≤ m := by52  have hval1 : getC S.val 1 ∈ S.val := getC_mem (by rw [hb.val_len]; decide)53  refine ⟨?_, ?_, ?_, ?_⟩54  · intro y hy55    unfold parityFormula56    rw [eval_subst]57    have hz : (fun j => eval (vfun y) (parSubst m j)) = boardBits 2 (Game.encode y) := by58      funext j; exact parSubst_eval hy j59    rw [hz]60    obtain ⟨i, v, x, hmove, hx, hlt, hz0⟩ := hS y hy61    obtain ⟨_, hvp⟩ := winning_move_on_encode y hx hlt hz062    unfold binMove binReadoutOf at hmove63    split at hmove64    · split at hmove65      · simp only [Option.some.injEq, Prod.mk.injEq] at hmove66        obtain ⟨_, hvdef⟩ := hmove67        rw [hvp] at hvdef68        have hl : (S.val.map (eval (boardBits 2 (Game.encode y)))).length = 2 := by simp [hb.val_len]69        have := low_bit_of_two hl hvdef70        rw [eval_getC, this, par_eq_parity]71      · cases hmove72    · cases hmove73  · unfold parityFormula74    rw [depth_subst_leaf _ (parSubst_leaf m)]75    exact hb.depth_val _ hval176  · unfold parityFormula77    rw [size_subst_leaf _ (parSubst_leaf m)]78    exact hb.size_val _ hval179  · exact maxInput_subst_le _ m (parSubst_max m) _8081/-- BARRIER, CORE FORM: under ParityNotAC0, no family of binary selectors with BBound of82    fixed depth d and size s m ≤ c·m^k plays winning moves on all encoded boards. -/83theorem barrier_core (hard : ParityNotAC0) (S : Nat → BCirc) (r s : Nat → Nat) (d c k : Nat)84    (hb : ∀ m, 1 ≤ m → BBound (S m) (m + 1) 2 (r m) d (s m))85    (hs : ∀ m, 1 ≤ m → s m ≤ c * m ^ k)86    (hwin : ∀ m, 1 ≤ m → EncWin (S m) m) : False := by87  obtain ⟨m0, hm0⟩ := hard d c k88  have hm : 1 ≤ m0 + 1 := by omega89  obtain ⟨heval, hd, hsz, hmx⟩ := extraction_enc (hb (m0 + 1) hm) (hwin (m0 + 1) hm)90  obtain ⟨y, hy, hne⟩ := hm0 (m0 + 1) (by omega) _ hd (Nat.le_trans hsz (hs _ hm)) hmx91  exact hne (heval y (mem_bitvecs_length hy))9293/-! ## From AC0 family certificates to BBound -/9495theorem size_le_tsize {c : Circ} {cs : List Circ} (h : c ∈ cs) : size c ≤ tsize cs := by96  unfold tsize97  induction cs with98  | nil => cases h99  | cons a cs ih =>100    simp only [List.map_cons, List.sum_cons]101    rcases List.mem_cons.mp h with rfl | h'102    · omega103    · have := ih h'; omega104105theorem bbound_of_forms {S : BCirc} {N B r d s : Nat} (hidx : S.idx.length = r) (hval : S.val.length = B)106    (hw : N ≤ 2 ^ r) (hd : ∀ c ∈ bForms S, depth c ≤ d) (hm : ∀ c ∈ bForms S, maxInput c ≤ B * N)107    (hs : tsize (bForms S) ≤ s) : BBound S N B r d s := by108  have hsz : ∀ c ∈ bForms S, size c ≤ s := fun c hc => Nat.le_trans (size_le_tsize hc) hs109  have m0 : S.valid ∈ bForms S := by simp [bForms]110  have mi : ∀ c ∈ S.idx, c ∈ bForms S := fun c hc => by simp [bForms, hc]111  have mv : ∀ c ∈ S.val, c ∈ bForms S := fun c hc => by simp [bForms, hc]112  exact ⟨hidx, hval, hw, hd _ m0, fun c hc => hd c (mi c hc), fun c hc => hd c (mv c hc), hsz _ m0,113    fun c hc => hsz c (mi c hc), fun c hc => hsz c (mv c hc), hm _ m0, fun c hc => hm c (mi c hc),114    fun c hc => hm c (mv c hc)⟩115116theorem bbound_mono {S : BCirc} {N B r d s d' s' : Nat} (h : BBound S N B r d s) (hd : d ≤ d') (hs : s ≤ s') :117    BBound S N B r d' s' :=118  ⟨h.idx_len, h.val_len, h.width, Nat.le_trans h.depth_valid hd, fun c hc => Nat.le_trans (h.depth_idx c hc) hd,119    fun c hc => Nat.le_trans (h.depth_val c hc) hd, Nat.le_trans h.size_valid hs,120    fun c hc => Nat.le_trans (h.size_idx c hc) hs, fun c hc => Nat.le_trans (h.size_val c hc) hs,121    h.max_valid, h.max_idx, h.max_val⟩122123/-- The encoding family: m parity bits, m + 1 heaps of 2 bits, input length 2(m+1). -/124def encAdm : Nat → Prop := fun m => 1 ≤ m125def encLen : Nat → Nat := fun m => 2 * (m + 1)126127theorem enc_poly {c k m : Nat} (hm : 1 ≤ m) : c * encLen m ^ k ≤ c * 4 ^ k * m ^ k := by128  have h1 : encLen m ≤ 4 * m := by unfold encLen; omega129  have := Nat.pow_le_pow_left h1 k130  rw [Nat.mul_pow] at this131  have := Nat.mul_le_mul_left c this132  rw [Nat.mul_assoc]; exact this133134/-- BARRIER FOR AC0 FORMULA FAMILIES on the encoding family. -/135theorem barrier_fam (hard : ParityNotAC0) (S : Nat → BCirc) (r : Nat → Nat) (d : Nat)136    (hfam : AC0Fam encAdm encLen (fun m => bForms (S m)) d)137    (hidx : ∀ m, 1 ≤ m → (S m).idx.length = r m ∧ (S m).val.length = 2 ∧ m + 1 ≤ 2 ^ r m)138    (hwin : ∀ m, 1 ≤ m → EncWin (S m) m) : False := by139  obtain ⟨c, k, hsz⟩ := hfam.size_poly140  apply barrier_core hard S r (fun m => c * encLen m ^ k) d (c * 4 ^ k) k _ (fun m hm => enc_poly hm) hwin141  intro m hm142  exact bbound_of_forms (hidx m hm).1 (hidx m hm).2.1 (hidx m hm).2.2 (hfam.depth_le m hm)143    (fun c' hc => hfam.reads m hm c' hc) (hsz m hm)144145/-! ## Maps that win on the encoding family -/146147/-- A move map plays a zero-restoring legal move on every encoded board. -/148def WinsOnEnc (F : List Nat → Option (Nat × Nat)) : Prop :=149  ∀ y : List Bool, ∃ i v x, F (Game.encode y) = some (i, v) ∧ (Game.encode y)[i]? = some x ∧ v < x ∧150    nimSum ((Game.encode y).set i v) = 0151152theorem decisionMove_winsOnEnc : WinsOnEnc decisionMove := by153  intro y154  obtain ⟨i, v, hd, hz⟩ := (decision_correct (Game.encode y)).2.2 (nimSum_encode_ne y)155  obtain ⟨x, hx, hlt, _⟩ := (decision_correct (Game.encode y)).2.1 i v hd156  exact ⟨i, v, x, hd, hx, hlt, hz⟩157158theorem winsOnEnc_congr {F G : List Nat → Option (Nat × Nat)} (h : ∀ y, F (Game.encode y) = G (Game.encode y))159    (hG : WinsOnEnc G) : WinsOnEnc F := by160  intro y; obtain ⟨i, v, x, h1, h2⟩ := hG y; exact ⟨i, v, x, by rw [h y, h1], h2⟩161162/-- BARRIER FOR A MAP (formula families): if F wins on the encoding family, no AC0163    family of binary selectors computes F there. -/164theorem barrier_map (hard : ParityNotAC0) (F : List Nat → Option (Nat × Nat)) (hF : WinsOnEnc F)165    (S : Nat → BCirc) (r : Nat → Nat) (d : Nat)166    (hfam : AC0Fam encAdm encLen (fun m => bForms (S m)) d)167    (hidx : ∀ m, 1 ≤ m → (S m).idx.length = r m ∧ (S m).val.length = 2 ∧ m + 1 ≤ 2 ^ r m)168    (hcomp : ∀ m, 1 ≤ m → ∀ y : List Bool, y.length = m → binMove (S m) (m + 1) (Game.encode y) = F (Game.encode y)) :169    False := by170  apply barrier_fam hard S r d hfam hidx171  intro m hm y hy172  obtain ⟨i, v, x, h1, h2⟩ := hF y173  exact ⟨i, v, x, by rw [hcomp m hm y hy, h1], h2⟩174175/-! ## Network families -/176177theorem binMove_netBCirc {W N r : Nat} (ls : List Layer) (hv : NetValid W ls) {P : List Nat}178    (hP : P.length = N) : binMove (netBCirc W 2 N r ls) N P = netBinSem ls N r 2 (boardBits 2 P) := by179  unfold binMove180  rw [netReadout_eq (fun _ => ls) (fun _ => hv) hP false]181  rfl182183/-- BARRIER FOR FIXED-SCALE NETWORK FAMILIES: under ParityNotAC0 no family of W-valid184    networks with at most L layers (W, L fixed) and polynomial widths/fan-ins, decoded as185    (valid, r index bits, 2 value bits), computes on all encoded boards a map that wins186    there.  (The network-to-AC0 compilation is applied to the same networks.) -/187theorem barrier_net (hard : ParityNotAC0) (F : List Nat → Option (Nat × Nat)) (hF : WinsOnEnc F)188    (net : Nat → List Layer) (r : Nat → Nat) (W L : Nat)189    (hnet : NetFam encAdm encLen net W L) (hr : ∀ m, 1 ≤ m → m + 1 ≤ 2 ^ r m)190    (hcomp : ∀ m, 1 ≤ m → ∀ y : List Bool, y.length = m →191      netBinSem (net m) (m + 1) (r m) 2 (boardBits 2 (Game.encode y)) = F (Game.encode y)) : False := by192  obtain ⟨c, k, hbd⟩ := hnet.bounded193  let s : Nat → Nat := fun m => 2 * ((2 * W + 3) ^ L * (c * encLen m ^ k + 1) ^ (W * L))194  have hpoly : PolyIn encAdm (fun m => m) s :=195    polyE (fun m hm => hm) (fun _ m => m) (fun _ _ _ => Nat.le_refl _)196      (2 * (PE.c (2 * W + 3) ^ L * (PE.c c * (2 * (vB + 1)) ^ k + 1) ^ (W * L))) s (fun _ => rfl)197  obtain ⟨c', k', hs⟩ := hpoly198  apply barrier_core hard (fun m => netBCirc W 2 (m + 1) (r m) (net m)) r s (3 * L) c' k' _ hs199  · intro m hm y hy200    obtain ⟨i, v, x, h1, h2⟩ := hF y201    refine ⟨i, v, x, ?_, h2⟩202    rw [binMove_netBCirc (net m) (hnet.valid m hm) (by rw [length_encode, hy]), hcomp m hm y hy, h1]203  · intro m hm204    have hb := netBCirc_BBound (B := 2) (N := m + 1) (r := r m) (net m) (hnet.valid m hm) (hbd m hm) (hr m hm)205    have hl := hnet.layers m hm206    refine bbound_mono hb (Nat.mul_le_mul_left 3 hl) ?_207    have e1 : (2 * W + 3) ^ (net m).length ≤ (2 * W + 3) ^ L := Nat.pow_le_pow_right (by omega) hl208    have e2 : (c * encLen m ^ k + 1) ^ (W * (net m).length) ≤ (c * encLen m ^ k + 1) ^ (W * L) :=209      Nat.pow_le_pow_right (by omega) (Nat.mul_le_mul_left W hl)210    have := Nat.mul_le_mul e1 e2211    show 2 * ((2 * W + 3) ^ (net m).length * (c * encLen m ^ k + 1) ^ (W * (net m).length)) ≤ s m212    simp only [s]; omega213214/-! ## The complete multi-head and recurrent decision maps -/215216/-- The COMPLETE multi-head decision map: B rollouts executed by the compiled policy217    networks (sequential), their outcome parities, then the compiled readout network. -/218def mhMove (B : Nat) (P : List Nat) : Option (Nat × Nat) :=219  netBinSem (mhNet B P.length (rIdx P.length)) P.length (rIdx P.length) B220    (obsIn B P.length P (fun j => rollOut B j P))221222theorem mhMove_eq {B : Nat} {P : List Nat} (hw : Width B P) : mhMove B P = decisionMove P := by223  have ho : (fun j => rollOut B j P) = outcomes P := by funext j; exact rollOut_eq hw224  unfold mhMove; rw [ho]225  exact mhNet_correct (rIdx_width _) rfl hw226227/-- The COMPLETE recurrent decision map: 2N + 2 threshold-controller updates from the228    initial state on rows, SEP, rows, SEP. -/229def recMove (B : Nat) (P : List Nat) : Option (Nat × Nat) :=230  (WholeGame.decide B (rIdx P.length) (sbits B (rIdx P.length) cinit) P).2231232theorem cinit_fits (B N : Nat) : Fits B N cinit :=233  ⟨Nat.two_pow_pos B, Nat.two_pow_pos B, Nat.two_pow_pos B, Nat.zero_le _, by simp [cinit], by simp [cinit]⟩234235theorem recMove_eq {B : Nat} {P : List Nat} (hw : Width B P) : recMove B P = decisionMove P := by236  unfold recMove237  rw [(decide_spec (rIdx_counter P.length) cinit_idle (cinit_fits B P.length) rfl hw).1]238239theorem width2_encode (y : List Bool) : Width 2 (Game.encode y) := encode_width y240241theorem mhMove_winsOnEnc : WinsOnEnc (mhMove 2) :=242  winsOnEnc_congr (fun y => mhMove_eq (width2_encode y)) decisionMove_winsOnEnc243244theorem recMove_winsOnEnc : WinsOnEnc (recMove 2) :=245  winsOnEnc_congr (fun y => recMove_eq (width2_encode y)) decisionMove_winsOnEnc246247/-- MULTI-HEAD BARRIER: under ParityNotAC0 the complete multi-head decision map is not248    computed by any single-frame AC0 formula family, even on the two-bit encoding family. -/249theorem no_ac0_mh (hard : ParityNotAC0) (S : Nat → BCirc) (r : Nat → Nat) (d : Nat)250    (hfam : AC0Fam encAdm encLen (fun m => bForms (S m)) d)251    (hidx : ∀ m, 1 ≤ m → (S m).idx.length = r m ∧ (S m).val.length = 2 ∧ m + 1 ≤ 2 ^ r m)252    (hcomp : ∀ m, 1 ≤ m → ∀ y : List Bool, y.length = m → binMove (S m) (m + 1) (Game.encode y) = mhMove 2 (Game.encode y)) :253    False :=254  barrier_map hard _ mhMove_winsOnEnc S r d hfam hidx hcomp255256/-- RECURRENT BARRIER (formula families). -/257theorem no_ac0_rec (hard : ParityNotAC0) (S : Nat → BCirc) (r : Nat → Nat) (d : Nat)258    (hfam : AC0Fam encAdm encLen (fun m => bForms (S m)) d)259    (hidx : ∀ m, 1 ≤ m → (S m).idx.length = r m ∧ (S m).val.length = 2 ∧ m + 1 ≤ 2 ^ r m)260    (hcomp : ∀ m, 1 ≤ m → ∀ y : List Bool, y.length = m → binMove (S m) (m + 1) (Game.encode y) = recMove 2 (Game.encode y)) :261    False :=262  barrier_map hard _ recMove_winsOnEnc S r d hfam hidx hcomp263264/-- Network forms of both barriers. -/265theorem no_net_mh (hard : ParityNotAC0) (net : Nat → List Layer) (r : Nat → Nat) (W L : Nat)266    (hnet : NetFam encAdm encLen net W L) (hr : ∀ m, 1 ≤ m → m + 1 ≤ 2 ^ r m)267    (hcomp : ∀ m, 1 ≤ m → ∀ y : List Bool, y.length = m →268      netBinSem (net m) (m + 1) (r m) 2 (boardBits 2 (Game.encode y)) = mhMove 2 (Game.encode y)) : False :=269  barrier_net hard _ mhMove_winsOnEnc net r W L hnet hr hcomp270271theorem no_net_rec (hard : ParityNotAC0) (net : Nat → List Layer) (r : Nat → Nat) (W L : Nat)272    (hnet : NetFam encAdm encLen net W L) (hr : ∀ m, 1 ≤ m → m + 1 ≤ 2 ^ r m)273    (hcomp : ∀ m, 1 ≤ m → ∀ y : List Bool, y.length = m →274      netBinSem (net m) (m + 1) (r m) 2 (boardBits 2 (Game.encode y)) = recMove 2 (Game.encode y)) : False :=275  barrier_net hard _ recMove_winsOnEnc net r W L hnet hr hcomp276277/-- "On all boards" corollary: agreement on all width-2 boards implies agreement on the278    encoded boards, so the barrier applies a fortiori. -/279theorem no_ac0_mh_allBoards (hard : ParityNotAC0) (S : Nat → BCirc) (r : Nat → Nat) (d : Nat)280    (hfam : AC0Fam encAdm encLen (fun m => bForms (S m)) d)281    (hidx : ∀ m, 1 ≤ m → (S m).idx.length = r m ∧ (S m).val.length = 2 ∧ m + 1 ≤ 2 ^ r m)282    (hcomp : ∀ m, 1 ≤ m → ∀ P : List Nat, P.length = m + 1 → Width 2 P → binMove (S m) (m + 1) P = mhMove 2 P) :283    False :=284  no_ac0_mh hard S r d hfam hidx (fun m hm y hy => hcomp m hm _ (by rw [length_encode, hy]) (width2_encode y))285286theorem no_ac0_rec_allBoards (hard : ParityNotAC0) (S : Nat → BCirc) (r : Nat → Nat) (d : Nat)287    (hfam : AC0Fam encAdm encLen (fun m => bForms (S m)) d)288    (hidx : ∀ m, 1 ≤ m → (S m).idx.length = r m ∧ (S m).val.length = 2 ∧ m + 1 ≤ 2 ^ r m)289    (hcomp : ∀ m, 1 ≤ m → ∀ P : List Nat, P.length = m + 1 → Width 2 P → binMove (S m) (m + 1) P = recMove 2 P) :290    False :=291  no_ac0_rec hard S r d hfam hidx (fun m hm y hy => hcomp m hm _ (by rw [length_encode, hy]) (width2_encode y))292293/-! ## Why the promised two-frame map is not a counterexample -/294295/-- OR over heaps of the low bit of Q_i ⊕ P_i (a depth-4 local test on a pair). -/296def lowXorOr (Q P : List Nat) : Bool :=297  (List.range P.length).any (fun i => ((Q.getD i 0) ^^^ (P.getD i 0)).testBit 0)298299theorem move_split {Q P : List Nat} (h : Move Q P) :300    ∃ pre x post z, Q = pre ++ x :: post ∧ P = pre ++ z :: post ∧ z < x := by301  obtain ⟨pre, x, post, z, h1, h2, h3⟩ := h; exact ⟨pre, x, post, z, h1, h2, h3⟩302303theorem getD_split' (pre post : List Nat) (x i : Nat) :304    (pre ++ x :: post).getD i 0 = if i = pre.length then x else (pre ++ 0 :: post).getD i 0 := by305  by_cases hi : i = pre.length306  · subst hi; simp307  · rw [if_neg hi]308    simp only [List.getD_eq_getElem?_getD]309    rcases Nat.lt_or_ge i pre.length with h | h310    · rw [List.getElem?_append_left h, List.getElem?_append_left h]311    · rw [List.getElem?_append_right h, List.getElem?_append_right h]312      have : i - pre.length ≠ 0 := by omega313      obtain ⟨k, hk⟩ : ∃ k, i - pre.length = k + 1 := ⟨i - pre.length - 1, by omega⟩314      rw [hk]; simp315316/-- PROMISED PREDECESSORS REVEAL PARITY LOCALLY: if nim(Q) = 0 and Q → Game.encode y is a317    legal move, then the pair-local test lowXorOr Q (Game.encode y) equals parity y. -/318theorem promised_pred_parity (y : List Bool) {Q : List Nat} (h0 : nimSum Q = 0) (hm : Move Q (Game.encode y)) :319    lowXorOr Q (Game.encode y) = parity y := by320  obtain ⟨pre, x, post, z, hQ, hP, _⟩ := move_split hm321  have hd : x ^^^ z = 2 ^^^ (parity y).toNat := by322    have e := one_heap_difference pre post x z323    rw [← hQ, ← hP, h0, Nat.zero_xor, nimSum_encode] at e324    exact e.symm325  have hlow : (x ^^^ z).testBit 0 = parity y := by326    rw [hd]; cases parity y <;> decide327  have hlen : (Game.encode y).length = pre.length + 1 + post.length := by rw [hP]; simp; omega328  unfold lowXorOr329  apply Bool.eq_iff_iff.mpr330  rw [List.any_eq_true]331  constructor332  · rintro ⟨i, _, hi⟩333    rw [hQ, hP, getD_split', getD_split' pre post z] at hi334    by_cases hc : i = pre.length335    · rw [if_pos hc, if_pos hc, hlow] at hi; exact hi336    · rw [if_neg hc, if_neg hc, Nat.xor_self] at hi; simp at hi337  · intro hpar338    refine ⟨pre.length, List.mem_range.mpr (by omega), ?_⟩339    rw [hQ, hP, getD_split', getD_split' pre post z, if_pos rfl, if_pos rfl, hlow, hpar]340341/-- The local test as a formula over the predecessor's formulas G (bit wire 2i+1 is the342    low bit of heap i in the two-bit layout) and the inputs y. -/343def lowEnc (i : Nat) : Circ := if i = 0 then const false else input (i - 1)344345def predParity (G : List Circ) (m : Nat) : Circ :=346  or ((List.range (m + 1)).map (fun i => xor2 (getC G (2 * i + 1)) (lowEnc i)))347348theorem lowEnc_eval {y : List Bool} {i : Nat} (hi : i < y.length + 1) :349    eval (vfun y) (lowEnc i) = ((Game.encode y).getD i 0).testBit 0 := by350  unfold lowEnc Game.encode351  by_cases h0 : i = 0352  · subst h0; simp353  · rw [if_neg h0]354    obtain ⟨k, rfl⟩ : ∃ k, i = k + 1 := ⟨i - 1, by omega⟩355    simp only [eval_input, Nat.add_sub_cancel, List.getD_cons_succ, vfun]356    have hk : k < y.length := by omega357    rw [List.getD_eq_getElem?_getD, List.getD_eq_getElem?_getD (l := List.map Bool.toNat y), List.getElem?_map,358      List.getElem?_eq_getElem hk]359    cases y[k] <;> simp360361/-- NO AC0 FAMILY PRODUCES PROMISED PREDECESSORS: under ParityNotAC0 there is no AC0362    family G m (input: the m bits y; outputs: the 2(m+1) bits of a board Q) such that, for363    every y, Q is a predecessor of Game.encode y with nim(Q) = 0 reached by a legal move.  The364    two-frame selector is AC0 only because this promised frame is SUPPLIED. -/365theorem no_ac0_predecessor (hard : ParityNotAC0) (G : Nat → List Circ) (d : Nat)366    (hfam : AC0Fam encAdm (fun m => m) G d)367    (hpred : ∀ m, 1 ≤ m → ∀ y : List Bool, y.length = m → ∃ Q : List Nat, Q.length = m + 1 ∧368      nimSum Q = 0 ∧ Move Q (Game.encode y) ∧ ∀ w, w < 2 * (m + 1) → eval (vfun y) (getC (G m) w) = boardBits 2 Q w) :369    False := by370  have hp : ∀ m, encAdm m → 1 ≤ m := fun m hm => hm371  have hT : PolyIn encAdm (fun m => m) (fun m => tsize (G m)) := hfam.size_poly372  have hP : PolyIn encAdm (fun m => m) (fun m => (m + 1) * (2 * (tsize (G m) + 1) + 7) + 1) :=373    polyIn_add hp (polyIn_mul (polyIn_add hp (polyIn_leaf (fun _ _ => Nat.le_refl _)) (polyIn_const _ _ 1))374      (polyIn_add hp (polyIn_mul (polyIn_const _ _ 2) (polyIn_add hp hT (polyIn_const _ _ 1))) (polyIn_const _ _ 7)))375      (polyIn_const _ _ 1)376  obtain ⟨c, k, hsz⟩ := hP377  obtain ⟨m0, hm0⟩ := hard (d + 4) c k378  have hm : 1 ≤ m0 + 1 := by omega379  -- the parity formula computes parity on every y of length m0 + 1380  have heval : ∀ y : List Bool, y.length = m0 + 1 → eval (vfun y) (predParity (G (m0 + 1)) (m0 + 1)) = par y := by381    intro y hy382    obtain ⟨Q, hQl, h0, hmv, hbits⟩ := hpred (m0 + 1) hm y hy383    rw [par_eq_parity, ← promised_pred_parity y h0 hmv]384    unfold predParity lowXorOr385    simp only [eval_or, List.any_map, length_encode, hy]386    apply any_congr_mem387    intro i hi388    have hi' := List.mem_range.mp hi389    simp only [Function.comp_apply, eval_xor2]390    have hw := hbits (2 * i + 1) (by omega)391    rw [hw, lowEnc_eval (by omega)]392    unfold boardBits393    rw [hQl, if_pos (by omega)]394    have e1 : (2 * i + 1) / 2 = i := by omega395    have e2 : 2 - 1 - (2 * i + 1) % 2 = 0 := by omega396    rw [e1, e2, Nat.testBit_xor]397  -- resources of the parity formula398  have hget : ∀ w, depth (getC (G (m0 + 1)) w) ≤ d ∧ maxInput (getC (G (m0 + 1)) w) ≤ m0 + 1 ∧399      size (getC (G (m0 + 1)) w) ≤ tsize (G (m0 + 1)) + 1 := by400    intro w; unfold getC; rw [List.getD_eq_getElem?_getD]401    cases h : (G (m0 + 1))[w]? with402    | none => simp403    | some c' =>404      have hmem := List.mem_of_getElem? h405      exact ⟨hfam.depth_le _ hm c' hmem, hfam.reads _ hm c' hmem, Nat.le_succ_of_le (size_le_tsize hmem)⟩406  have hlow : ∀ i, i ≤ m0 + 1 → depth (lowEnc i) = 0 ∧ size (lowEnc i) = 1 ∧ maxInput (lowEnc i) ≤ m0 + 1 := by407    intro i hi; unfold lowEnc; split <;> simp <;> omega408  have hx : ∀ i, i ≤ m0 + 1 → depth (xor2 (getC (G (m0 + 1)) (2 * i + 1)) (lowEnc i)) ≤ d + 3 ∧409      size (xor2 (getC (G (m0 + 1)) (2 * i + 1)) (lowEnc i)) ≤ 2 * (tsize (G (m0 + 1)) + 1) + 7 ∧410      maxInput (xor2 (getC (G (m0 + 1)) (2 * i + 1)) (lowEnc i)) ≤ m0 + 1 := by411    intro i hi412    obtain ⟨a1, a2, a3⟩ := hget (2 * i + 1)413    obtain ⟨b1, b2, b3⟩ := hlow i hi414    simp only [xor2, depth_or, depth_and, depth_not, size_or, size_and, size_not, maxInput_or, maxInput_and,415      maxInput_not, List.map_cons, List.map_nil, List.sum_cons, List.sum_nil, b1, b2]416    simp only [listMax, List.foldr]417    refine ⟨by omega, by omega, by omega⟩418  have hd : depth (predParity (G (m0 + 1)) (m0 + 1)) ≤ d + 4 := by419    unfold predParity420    apply depth_or_le; intro c' hc'421    obtain ⟨i, hi, rfl⟩ := List.mem_map.mp hc'422    exact (hx i (by have := List.mem_range.mp hi; omega)).1423  have hmx : maxInput (predParity (G (m0 + 1)) (m0 + 1)) ≤ m0 + 1 := by424    unfold predParity425    apply ControllerBits.maxInput_or_le; intro c' hc'426    obtain ⟨i, hi, rfl⟩ := List.mem_map.mp hc'427    exact (hx i (by have := List.mem_range.mp hi; omega)).2.2428  have hs : size (predParity (G (m0 + 1)) (m0 + 1)) ≤ c * (m0 + 1) ^ k := by429    unfold predParity430    rw [size_or]431    have h1 := sum_le_len_mul (cs := (List.range (m0 + 1 + 1)).map432      (fun i => xor2 (getC (G (m0 + 1)) (2 * i + 1)) (lowEnc i))) (S := 2 * (tsize (G (m0 + 1)) + 1) + 7)433      (fun c' hc' => by434        obtain ⟨i, hi, rfl⟩ := List.mem_map.mp hc'435        exact (hx i (by have := List.mem_range.mp hi; omega)).2.1)436    rw [List.length_map, List.length_range] at h1437    have h2 := hsz (m0 + 1) hm438    dsimp only at h2439    omega440  obtain ⟨y, hy, hne⟩ := hm0 (m0 + 1) (by omega) _ hd hs hmx441  exact hne (heval y (mem_bitvecs_length hy))442443/-- On a promised pair (Q, Game.encode y) the two-frame network outputs heap 0 and the parity444    of y: the two-frame AC0 map does compute parity there, from the supplied frame Q. -/445theorem twoFrame_on_encoding (y : List Bool) {Q : List Nat} (hQ : Q.length = y.length + 1) (hw : Width 2 Q)446    (h0 : nimSum Q = 0) (hm : Move Q (Game.encode y)) :447    netBinSem (restN (2, y.length + 1)) (y.length + 1) (rIdx (y.length + 1)) 2448      (LocalRestore.tf 2 (y.length + 1) Q (Game.encode y)) = some (0, (parity y).toNat) := by449  obtain ⟨i, v, _, h2, _, h4, h5⟩ := rest_semantics (B := 2) hQ (by rw [length_encode]) hw (width2_encode y) h0 hm450  have hred := unique_zero_move y _ h4 h5451  cases i with452  | zero =>453    have := congrArg List.head? hred454    simp [Game.encode, reduced] at this455    rw [this] at h2; exact h2456  | succ k =>457    exfalso458    have := congrArg List.head? hred459    simp [Game.encode, reduced] at this460    have h2le := Bool.toNat_le (parity y)461    omega462463/-! ## Axiom audit -/464465#print axioms extraction_enc466#print axioms barrier_core467#print axioms size_le_tsize468#print axioms bbound_of_forms469#print axioms bbound_mono470#print axioms enc_poly471#print axioms barrier_fam472#print axioms decisionMove_winsOnEnc473#print axioms winsOnEnc_congr474#print axioms barrier_map475#print axioms binMove_netBCirc476#print axioms barrier_net477#print axioms mhMove_eq478#print axioms cinit_fits479#print axioms recMove_eq480#print axioms width2_encode481#print axioms mhMove_winsOnEnc482#print axioms recMove_winsOnEnc483#print axioms no_ac0_mh484#print axioms no_ac0_rec485#print axioms no_net_mh486#print axioms no_net_rec487#print axioms no_ac0_mh_allBoards488#print axioms no_ac0_rec_allBoards489#print axioms move_split490#print axioms getD_split'491#print axioms promised_pred_parity492#print axioms lowEnc_eval493#print axioms no_ac0_predecessor494#print axioms twoFrame_on_encoding495496