Bypass

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 RolloutExec23/- Phase 6, Priority 1c: the paper's Proposition prop:bypass-interfaces, the barrier side,4   and the recurrent-history caveat.  Written by Claude (10 October 2026).5   Lean 4.26.0, core/Std only.67   Each bypass is stated as: (a) family certificates for its SHALLOW COMPONENT (formula8   family and threshold-network family, the same objects as in (b)); (b) the component's9   semantics on its declared domain; (c) the complete strategy against every legal10   opponent, with its protocol and time/count bounds.  Polynomial size and constant depth11   are claims about ONE component evaluation; they never bound the number of sequential12   evaluations.1314   WHICH HYPOTHESIS OF THE SINGLE-FRAME BARRIER EACH BYPASS RELAXES.15   (i)   two-frame restoration keeps one shallow evaluation per decision but changes the16         INPUT: a promised pair (nim(Q) = 0, legal Q → Q'), not a single arbitrary board.17         The circuit reads only the 2BN bits of the two frames; no global nim-sum enters.18   (ii)  multi-head keeps every component shallow but performs B SEQUENTIAL rollouts19         (Σ_j (L_j + 1) clocked policy steps, unbounded in N) before the readout.20   (iii) recurrence keeps one update shallow but performs 2N + 2 SEQUENTIAL updates.21   Under ParityNotAC0 the complete board-to-move maps of (ii) and (iii) are not AC022   families (bypass_barriers); (i) is not a counterexample because the promised frame23   carries the parity and cannot itself be produced by an AC0 family. -/2425namespace NimAudit26namespace Bypass2728open Game Rollout Prob Attain Recurrent AC0 AC0.Circ CorrBridge AttainCircuit Bridge SelectCircuit29  BinReadout Controller ControllerBits PriorityEncoder ThresholdNet ThresholdInst FiniteNet WholeGame30  Family Barrier RolloutExec3132/-! ## (i) Two-frame restoration -/3334/-- The restoration circuit's input is exactly the two frames (Q at wires < BN, Q' after). -/35theorem tf_frames (B N : Nat) (Q Q' : List Nat) (j : Nat) :36    LocalRestore.tf B N Q Q' j = if j < B * N then boardBits B Q j else boardBits B Q' (j - B * N) := rfl3738theorem bypass_twoFrame :39    AC0Fam restAdm restLen (fun i => bForms (restS i)) 20 ∧40    NetFam restAdm restLen restN 1 42 ∧41    (∀ (B N : Nat) (Q Q' : List Nat), Q.length = N → Q'.length = N → Width B Q → Width B Q' →42      nimSum Q = 0 → Move Q Q' →43      ∃ i v, netBinSem (restN (B, N)) N (rIdx N) B (LocalRestore.tf B N Q Q') = some (i, v) ∧44        Move Q' (Q'.set i v) ∧ nimSum (Q'.set i v) = 0 ∧ restore Q Q' = some (Q'.set i v)) ∧45    (∀ (B : Nat) (Q : List Nat), Width B Q → nimSum Q = 0 → TwoFrameWins (restReply B) Q ∧ Lose Q) := by46  refine ⟨rest_ac0, rest_net, fun B N Q Q' hQ hQ' hw hw' h0 hm => ?_, fun B Q hw h0 =>47    ⟨twoFrame_wins Q hw h0, twoFrame_lose hw h0⟩⟩48  obtain ⟨i, v, _, h2, h3, h4, h5⟩ := rest_semantics hQ hQ' hw hw' h0 hm49  exact ⟨i, v, h2, h4, h5, h3⟩5051/-- The two-frame strategy uses exactly the certified network on the two frames. -/52theorem restReply_uses_restN (B : Nat) (Q Q' : List Nat) :53    restReply B Q Q' = applyM Q' (netBinSem (restN (B, Q'.length)) Q'.length (rIdx Q'.length) B54      (LocalRestore.tf B Q'.length Q Q')) := rfl5556/-! ## (ii) Multi-head rollouts with finite-register execution -/5758theorem bypass_multiHead :59    AC0Fam polAdm polLen (fun i => bForms (polS i)) 17 ∧ NetFam polAdm polLen polN 1 36 ∧60    AC0Fam polAdm stepLen stepF 28 ∧ NetFam polAdm stepLen stepN 1 58 ∧61    AC0Fam mhAdm mhLen (fun i => bForms (mhS i)) 19 ∧ NetFam mhAdm mhLen mhN 1 40 ∧62    (∀ (B : Nat) (P : List Nat), Width B P →63      mhExec B P = decisionMove P ∧ (nimSum P ≠ 0 → Wins (mhExecSel B) P) ∧64      (∀ j, outBit B j P = rolloutWinner j P ∧ polEvals B j P = rolloutMoves j P + 1) ∧65      ((List.range B).map (fun j => polEvals B j P)).sum = totalRolloutMoves B P + B ∧66      totalRolloutMoves B P ≤ B * P.sum ∧ B * P.sum ≤ B * (P.length * (2 ^ B - 1)) ∧67      totalRolloutMoves B P + B ≤ B * clockBound B P.length) := by68  refine ⟨pol_ac0, pol_net, step_ac0, step_net, mh_ac0, mh_net, fun B P hw => ?_⟩69  obtain ⟨_, h2, h3⟩ := mhSelect_cost hw70  obtain ⟨e1, e2, e3⟩ := mhExec_evals hw71  exact ⟨mhExec_eq hw, mhExec_wins hw, fun j => ⟨outBit_eq hw, e1 j⟩, e2, h2, h3, e3⟩7273/-! ## (iii) Persistent recurrence with replay -/7475theorem bypass_recurrent :76    AC0Fam ctrlAdm ctrlLen ctrlF 8 ∧ NetFam ctrlAdm ctrlLen ctrlN 1 18 ∧77    (∀ (B N : Nat) (v : Nat → Bool) (t : Tok), tstep B (rIdx N) v t = bstep B (rIdx N) v t) ∧78    (∀ (B N : Nat) (v : Nat → Bool) (P : List Nat), P.length = N → Width B P → nimSum P ≠ 0 →79      (tstep B (rIdx N) v Tok.reset).1 = sbits B (rIdx N) cinit ∧ ReplayWins B (rIdx N) cinit P) ∧80    (∀ (B N : Nat) (P : List Nat), P.length = N →81      (dtoks P).length = 2 * N + 2 ∧ (Tok.reset :: dtoks P).length = 2 * N + 3 ∧82      stateWidth B (rIdx N) = 7 + 5 * B + 3 * N.log2 ∧ inWidth B (rIdx N) = stateWidth B (rIdx N) + (2 + B)) := by83  refine ⟨ctrl_ac0, ctrl_net, fun B N v t => tstep_eq _ _ v t, fun B N v P hP hw h0 =>84    replay_game (rIdx_counter N) v hP hw h0, fun B N P hP => ?_⟩85  obtain ⟨a, b, c⟩ := replay_counts B N P hP86  exact ⟨a, b, c, (ctrl_widths B N).1⟩8788/-- PROPOSITION prop:bypass-interfaces (all three parts): for each bypass the formula89    family AND the {0,1}-weight threshold-network family (W = 1) of its shallow components,90    and the complete strategy with its protocol and count bounds. -/91theorem prop_bypass_interfaces :92    (AC0Fam restAdm restLen (fun i => bForms (restS i)) 20 ∧ NetFam restAdm restLen restN 1 42 ∧93      ∀ (B : Nat) (Q : List Nat), Width B Q → nimSum Q = 0 → TwoFrameWins (restReply B) Q) ∧94    (AC0Fam polAdm polLen (fun i => bForms (polS i)) 17 ∧ NetFam polAdm polLen polN 1 36 ∧95      AC0Fam polAdm stepLen stepF 28 ∧ NetFam polAdm stepLen stepN 1 58 ∧96      AC0Fam mhAdm mhLen (fun i => bForms (mhS i)) 19 ∧ NetFam mhAdm mhLen mhN 1 40 ∧97      ∀ (B : Nat) (P : List Nat), Width B P → nimSum P ≠ 0 →98        Wins (mhExecSel B) P ∧ totalRolloutMoves B P ≤ B * (P.length * (2 ^ B - 1)) ∧99        ((List.range B).map (fun j => polEvals B j P)).sum = totalRolloutMoves B P + B) ∧100    (AC0Fam ctrlAdm ctrlLen ctrlF 8 ∧ NetFam ctrlAdm ctrlLen ctrlN 1 18 ∧101      ∀ (B N : Nat) (v : Nat → Bool) (P : List Nat), P.length = N → Width B P → nimSum P ≠ 0 →102        (tstep B (rIdx N) v Tok.reset).1 = sbits B (rIdx N) cinit ∧ ReplayWins B (rIdx N) cinit P ∧103        (dtoks P).length = 2 * N + 2 ∧ stateWidth B (rIdx N) = 7 + 5 * B + 3 * N.log2) := by104  obtain ⟨t1, t2, _, t4⟩ := bypass_twoFrame105  obtain ⟨m1, m2, m3, m4, m5, m6, m7⟩ := bypass_multiHead106  obtain ⟨r1, r2, _, r4, r5⟩ := bypass_recurrent107  refine ⟨⟨t1, t2, fun B Q hw h0 => (t4 B Q hw h0).1⟩, ⟨m1, m2, m3, m4, m5, m6, fun B P hw h0 => ?_⟩,108    ⟨r1, r2, fun B N v P hP hw h0 => ⟨(r4 B N v P hP hw h0).1, (r4 B N v P hP hw h0).2, (r5 B N P hP).1,109      (r5 B N P hP).2.2.1⟩⟩⟩110  obtain ⟨_, hwin, _, h4, h5, h6, _⟩ := m7 B P hw111  exact ⟨hwin h0, Nat.le_trans h5 h6, h4⟩112113/-! ## The barrier side -/114115theorem mhExec_winsOnEnc : WinsOnEnc (mhExec 2) :=116  winsOnEnc_congr (fun y => mhExec_eq (width2_encode y)) decisionMove_winsOnEnc117118/-- ALL-BOARDS FORMS for the executed multi-head map and for network families: a family119    agreeing with mhExec 2 (resp. recMove 2) on every width-2 board of m+1 heaps agrees on120    the encoding family, so the barriers apply. -/121theorem no_ac0_mhExec_allBoards (hard : ParityNotAC0) (S : Nat → BCirc) (r : Nat → Nat) (d : Nat)122    (hfam : AC0Fam encAdm encLen (fun m => bForms (S m)) d)123    (hidx : ∀ m, 1 ≤ m → (S m).idx.length = r m ∧ (S m).val.length = 2 ∧ m + 1 ≤ 2 ^ r m)124    (hcomp : ∀ m, 1 ≤ m → ∀ P : List Nat, P.length = m + 1 → Width 2 P →125      ParityCircuit.binMove (S m) (m + 1) P = mhExec 2 P) : False :=126  no_ac0_mh_allBoards hard S r d hfam hidx (fun m hm P hP hw => (hcomp m hm P hP hw).trans (mhExec_eq_mhMove hw))127128theorem no_net_mhExec_allBoards (hard : ParityNotAC0) (net : Nat → List Layer) (r : Nat → Nat) (W L : Nat)129    (hnet : NetFam encAdm encLen net W L) (hr : ∀ m, 1 ≤ m → m + 1 ≤ 2 ^ r m)130    (hcomp : ∀ m, 1 ≤ m → ∀ P : List Nat, P.length = m + 1 → Width 2 P →131      netBinSem (net m) (m + 1) (r m) 2 (boardBits 2 P) = mhExec 2 P) : False :=132  no_net_mh hard net r W L hnet hr (fun m hm y hy => by133    rw [← mhExec_eq_mhMove (width2_encode y)]134    exact hcomp m hm _ (by rw [ParityCircuit.length_encode, hy]) (width2_encode y))135136theorem no_net_rec_allBoards (hard : ParityNotAC0) (net : Nat → List Layer) (r : Nat → Nat) (W L : Nat)137    (hnet : NetFam encAdm encLen net W L) (hr : ∀ m, 1 ≤ m → m + 1 ≤ 2 ^ r m)138    (hcomp : ∀ m, 1 ≤ m → ∀ P : List Nat, P.length = m + 1 → Width 2 P →139      netBinSem (net m) (m + 1) (r m) 2 (boardBits 2 P) = recMove 2 P) : False :=140  no_net_rec hard net r W L hnet hr (fun m hm y hy =>141    hcomp m hm _ (by rw [ParityCircuit.length_encode, hy]) (width2_encode y))142143/-- BYPASS BARRIERS.  Under ParityNotAC0:144    (a) the complete finite-register multi-head map mhExec and the complete recurrent map145        recMove are not computed by any AC0 formula family on the encoding family;146    (b) nor by any fixed-scale network family (fixed W, constant layers, polynomial size);147    (c) the promised two-frame map does compute parity on promised pairs, but no AC0148        family produces the promised predecessor from the single frame. -/149theorem bypass_barriers (hard : ParityNotAC0) :150    (∀ (S : Nat → BCirc) (r : Nat → Nat) (d : Nat), AC0Fam encAdm encLen (fun m => bForms (S m)) d →151      (∀ m, 1 ≤ m → (S m).idx.length = r m ∧ (S m).val.length = 2 ∧ m + 1 ≤ 2 ^ r m) →152      ¬ (∀ m, 1 ≤ m → ∀ y : List Bool, y.length = m → ParityCircuit.binMove (S m) (m + 1) (Game.encode y) = mhExec 2 (Game.encode y))) ∧153    (∀ (S : Nat → BCirc) (r : Nat → Nat) (d : Nat), AC0Fam encAdm encLen (fun m => bForms (S m)) d →154      (∀ m, 1 ≤ m → (S m).idx.length = r m ∧ (S m).val.length = 2 ∧ m + 1 ≤ 2 ^ r m) →155      ¬ (∀ m, 1 ≤ m → ∀ y : List Bool, y.length = m → ParityCircuit.binMove (S m) (m + 1) (Game.encode y) = recMove 2 (Game.encode y))) ∧156    (∀ (net : Nat → List Layer) (r : Nat → Nat) (W L : Nat), NetFam encAdm encLen net W L →157      (∀ m, 1 ≤ m → m + 1 ≤ 2 ^ r m) →158      ¬ (∀ m, 1 ≤ m → ∀ y : List Bool, y.length = m →159        netBinSem (net m) (m + 1) (r m) 2 (boardBits 2 (Game.encode y)) = mhExec 2 (Game.encode y))) ∧160    (∀ (net : Nat → List Layer) (r : Nat → Nat) (W L : Nat), NetFam encAdm encLen net W L →161      (∀ m, 1 ≤ m → m + 1 ≤ 2 ^ r m) →162      ¬ (∀ m, 1 ≤ m → ∀ y : List Bool, y.length = m →163        netBinSem (net m) (m + 1) (r m) 2 (boardBits 2 (Game.encode y)) = recMove 2 (Game.encode y))) ∧164    (∀ (G : Nat → List Circ) (d : Nat), AC0Fam encAdm (fun m => m) G d →165      ¬ (∀ m, 1 ≤ m → ∀ y : List Bool, y.length = m → ∃ Q : List Nat, Q.length = m + 1 ∧166        nimSum Q = 0 ∧ Move Q (Game.encode y) ∧167        ∀ w, w < 2 * (m + 1) → eval (vfun y) (getC (G m) w) = boardBits 2 Q w)) := by168  refine ⟨fun S r d hf hi hc => barrier_map hard _ mhExec_winsOnEnc S r d hf hi hc,169    fun S r d hf hi hc => no_ac0_rec hard S r d hf hi hc,170    fun net r W L hn hr hc => barrier_net hard _ mhExec_winsOnEnc net r W L hn hr hc,171    fun net r W L hn hr hc => no_net_rec hard net r W L hn hr hc,172    fun G d hf hp => no_ac0_predecessor hard G d hf hp⟩173174/-- On every promised pair over the encoding family the certified two-frame network175    outputs (0, parity y): the parity is read off the supplied predecessor. -/176theorem twoFrame_promised_parity (y : List Bool) {Q : List Nat} (hQ : Q.length = y.length + 1)177    (hw : Width 2 Q) (h0 : nimSum Q = 0) (hm : Move Q (Game.encode y)) :178    netBinSem (restN (2, y.length + 1)) (y.length + 1) (rIdx (y.length + 1)) 2179      (LocalRestore.tf 2 (y.length + 1) Q (Game.encode y)) = some (0, (parity y).toNat) ∧180    lowXorOr Q (Game.encode y) = parity y :=181  ⟨twoFrame_on_encoding y hQ hw h0 hm, promised_pred_parity y h0 hm⟩182183/-! ## Recurrent history caveat -/184185theorem one_transition_diff {Q Q' : List Nat} (hm : Move Q Q') :186    ∃ pre x post z, Q = pre ++ x :: post ∧ Q' = pre ++ z :: post ∧ z < x ∧ nimSum Q ^^^ nimSum Q' = x ^^^ z := by187  obtain ⟨pre, x, post, z, h1, h2, h3⟩ := move_split hm188  refine ⟨pre, x, post, z, h1, h2, h3, ?_⟩189  rw [h1, h2]; exact one_heap_difference pre post x z190191/-- The controller's outputs on two consecutively supplied boards: the second summary's192    difference is nim(Q) ⊕ nim(Q'). -/193theorem ctrlOuts_two (v : Bool) (q : Nat) (Q Q' : List Nat) (rest : List (List Nat)) :194    (ctrlOuts v q (Q :: Q' :: rest))[2]? = some (COut.summary (nimSum Q') (some (nimSum Q ^^^ nimSum Q'))) := by195  simp [ctrlOuts]196197/-- ONE-LEGAL-TRANSITION FORM: when consecutive supplied boards differ by one legal move,198    the threshold controller reports exactly that heap's XOR difference. -/199theorem diff_of_transition {B N : Nat} {Q Q' : List Nat} (hN : N < 2 ^ rIdx N) (hQ : Q.length = N)200    (hQ' : Q'.length = N) (hw : Width B Q) (hw' : Width B Q') (hm : Move Q Q') :201    ∃ pre x post z, Q = pre ++ x :: post ∧ Q' = pre ++ z :: post ∧202      (trun B (rIdx N) (sbits B (rIdx N) cinit) (stream [Q, Q'])).2[2]? =203        some (COut.summary (nimSum Q') (some (x ^^^ z))) := by204  obtain ⟨pre, x, post, z, h1, h2, _, h4⟩ := one_transition_diff hm205  refine ⟨pre, x, post, z, h1, h2, ?_⟩206  rw [trun_stream hN [Q, Q'] (by207    intro P hP; simp only [List.mem_cons, List.mem_nil_iff, or_false] at hP208    rcases hP with rfl | rfl209    · exact ⟨hQ, hw⟩210    · exact ⟨hQ', hw'⟩), ctrlOuts_two, h4]211212/-- POST-MOVE BOARD SUPPLIED: if the protocol also supplies the player's own post-move213    board R (nim(R) = 0) before the opponent's board P', the reported difference at P'214    is the opponent's one-heap delta x ⊕ z, which equals nim(P') (the restoration target). -/215theorem diff_with_postMove {B N : Nat} {P0 R P' : List Nat} (hN : N < 2 ^ rIdx N)216    (h0 : P0.length = N ∧ Width B P0) (h1 : R.length = N ∧ Width B R) (h2 : P'.length = N ∧ Width B P')217    (hz : nimSum R = 0) (hm : Move R P') :218    ∃ pre x post z, R = pre ++ x :: post ∧ P' = pre ++ z :: post ∧219      (trun B (rIdx N) (sbits B (rIdx N) cinit) (stream [P0, R, P'])).2[4]? =220        some (COut.summary (nimSum P') (some (x ^^^ z))) ∧ x ^^^ z = nimSum P' := by221  obtain ⟨pre, x, post, z, e1, e2, _, e4⟩ := one_transition_diff hm222  refine ⟨pre, x, post, z, e1, e2, ?_, by rw [← e4, hz, Nat.zero_xor]⟩223  rw [trun_stream hN [P0, R, P'] (by224    intro P hP; simp only [List.mem_cons, List.mem_nil_iff, or_false] at hP225    rcases hP with rfl | rfl | rfl226    · exact h0227    · exact h1228    · exact h2), ← e4]229  simp [ctrlOuts]230231/-- DECISION-TIME BOARDS ONLY: the reported difference spans two moves and is in general232    NOT the opponent's delta.  Concretely: P0 = [1,2] (player to move), the player moves to233    R = [1,1] (nim 0), the opponent moves to P1 = [0,1] (delta 1); supplying only P0 and P1,234    the threshold controller reports difference 2. -/235theorem diff_decision_only :236    Move [1, 2] [1, 1] ∧ nimSum [1, 1] = 0 ∧ Move [1, 1] [0, 1] ∧ (1 ^^^ 0 : Nat) = 1 ∧237    (trun 2 (rIdx 2) (sbits 2 (rIdx 2) cinit) (stream [[1, 2], [0, 1]])).2[2]? =238      some (COut.summary 1 (some 2)) := by239  refine ⟨⟨[1], 2, [], 1, rfl, rfl, by decide⟩, by decide, ⟨[], 1, [1], 0, rfl, rfl, by decide⟩, by decide, ?_⟩240  rw [trun_stream (rIdx_counter 2) _ (by241    intro P hP; simp only [List.mem_cons, List.mem_nil_iff, or_false] at hP242    rcases hP with rfl | rfl243    · exact ⟨rfl, by intro x hx; simp at hx; omega⟩244    · exact ⟨rfl, by intro x hx; simp at hx; omega⟩), ctrlOuts_two]245  rfl246247/-- The replay strategy's MOVE does not depend on the stored history: from any idle248    fitting state it equals decisionMove of the current board (recomputed by the scan). -/249theorem replay_move_current {B r N : Nat} (hN : N < 2 ^ r) {s : CState} (hs : Idle s) (hf : Fits B N s)250    {P : List Nat} (hP : P.length = N) (hw : Width B P) :251    (WholeGame.decide B r (sbits B r s) P).2 = decisionMove P :=252  by rw [(decide_spec hN hs hf hP hw).1]253254/-! ## Axiom audit -/255256#print axioms tf_frames257#print axioms bypass_twoFrame258#print axioms restReply_uses_restN259#print axioms bypass_multiHead260#print axioms bypass_recurrent261#print axioms prop_bypass_interfaces262#print axioms mhExec_winsOnEnc263#print axioms no_ac0_mhExec_allBoards264#print axioms no_net_mhExec_allBoards265#print axioms no_net_rec_allBoards266#print axioms bypass_barriers267#print axioms twoFrame_promised_parity268#print axioms one_transition_diff269#print axioms ctrlOuts_two270#print axioms diff_of_transition271#print axioms diff_with_postMove272#print axioms diff_decision_only273#print axioms replay_move_current274275