Example 1Pairing strategy: a constant-depth mirror selector wins as second player on paired boards

209/-- PAIRING STRATEGY (weak mastery for the second player): from every paired board of210    width B, the reply rule computed by the local binary mirror circuit wins against every211    legal opponent. -/212theorem pairing_wins {B : Nat} : ∀ P : List Nat, Paired P → Width B P → SecondWins (pairSel B) P := by213  intro P214  induction P using (measure List.sum).wf.induction with215  | h P ih =>216    intro hp hw217    have key : ∀ Q, Move P Q → ∃ i y, pairSel B Q = some (Q.set (partner i) y) ∧218        Paired (Q.set (partner i) y) ∧ Move Q (Q.set (partner i) y) := by219      intro Q hm220      obtain ⟨i, y, _, hsel, hpair, hmv⟩ := pairR_correct hp hw hm221      refine ⟨i, y, ?_, hpair, hmv⟩222      unfold pairSel223      rw [pairBin, encode_correct _ Q.length _ (by simp [pairR]) (rIdx_width _), hsel]; rfl224    refine SecondWins.intro P (fun Q hm => ?_) (fun Q R hm hR => ?_) (fun Q R hm hR => ?_)225    · obtain ⟨i, y, h1, _⟩ := key Q hm; rw [h1]; rfl226    · obtain ⟨i, y, h1, _, h3⟩ := key Q hm; rw [h1] at hR; cases hR; exact h3227    · obtain ⟨i, y, h1, h2, h3⟩ := key Q hm228      rw [h1] at hR; cases hR229      have e1 := move_sum_lt hm; have e2 := move_sum_lt h3230      exact ih _ (by show (Q.set (partner i) y).sum < P.sum; omega) h2 (width_move (width_move hw hm) h3)

155/-- MIRROR CIRCUIT CORRECTNESS: after a legal move from a paired board, the selector156    outputs (partner of the changed heap, new value). -/157theorem pairR_correct {B : Nat} {P Q : List Nat} (hp : Paired P) (hw : Width B P) (hm : Move P Q) :158    ∃ i y, Q = P.set i y ∧ selReadout (pairR B Q.length) (boardBits B Q) = some (partner i, y) ∧159      Paired (Q.set (partner i) y) ∧ Move Q (Q.set (partner i) y) := by160  obtain ⟨i, y, hi, hQ, hy, hQl, hflag, hpair, hmv⟩ := paired_move hp hm161  refine ⟨i, y, hQ, ?_, hpair, hmv⟩162  have hN : Q.length % 2 = 0 := by rw [hQl]; exact hp.1163  have hwQ : Width B Q := width_move hw (by164    obtain ⟨pre, x, post, z, h1, h2, h3⟩ := hm; exact ⟨pre, x, post, z, h1, h2, h3⟩)165  have hj : partner i < Q.length := by rw [hQl]; exact partner_lt hi hp.1166  have hfl : ∀ k, k < Q.length → eval (boardBits B Q) (flagC B k) = decide (k = partner i) := by167    intro k hk; rw [flagC_eval rfl hwQ hN hk]; exact decide_eq_decide.mpr (hflag k hk)168  unfold selReadout pairR169  simp only170  have hvalid : eval (boardBits B Q) (or ((List.range Q.length).map (flagC B))) = true := by171    rw [eval_or, List.any_eq_true]172    exact ⟨flagC B (partner i), List.mem_map.mpr ⟨_, List.mem_range.mpr hj, rfl⟩, by rw [hfl _ hj]; simp⟩173  rw [if_pos hvalid]174  have hft : firstTrue (((List.range Q.length).map (flagC B)).map (eval (boardBits B Q))) = some (partner i) := by175    rw [firstTrue_some_iff]176    simp only [List.map_map, List.length_map, List.length_range]177    refine ⟨hj, ?_, fun i' hi' => ?_⟩178    · rw [List.getD_eq_getElem?_getD, List.getElem?_map, List.getElem?_range hj]179      simp [hfl _ hj]180    · rw [List.getD_eq_getElem?_getD, List.getElem?_map, List.getElem?_range (by omega)]181      simp [hfl _ (by omega : i' < Q.length)]; omega182  rw [hft]183  simp only [Option.some.injEq, Prod.mk.injEq, true_and]184  -- the value bits are the bits of heap i (the flagged heap's partner)185  have hval : ((List.range B).map (fun p => or ((List.range Q.length).map186      (fun k => and [flagC B k, heapC B (partner k) p])))).map (eval (boardBits B Q)) =187      (List.range B).map (fun p => boardBits B Q (B * i + p)) := by188    simp only [List.map_map]189    apply List.map_congr_left190    intro p hp191    simp only [Function.comp_apply, eval_or, List.any_map]192    apply Bool.eq_iff_iff.mpr193    rw [List.any_eq_true]194    constructor195    · rintro ⟨k, hk, he⟩196      have hk' := List.mem_range.mp hk197      simp only [Function.comp_apply, eval_and, List.all_cons, List.all_nil, Bool.and_true, Bool.and_eq_true,198        hfl k hk', decide_eq_true_eq, heapC, eval_input] at he199      obtain ⟨rfl, h2⟩ := he200      rw [partner_partner] at h2; exact h2201    · intro h202      refine ⟨partner i, List.mem_range.mpr hj, ?_⟩203      simp only [Function.comp_apply, eval_and, List.all_cons, List.all_nil, Bool.and_true, hfl _ hj, decide_true,204        Bool.true_and, heapC, eval_input, partner_partner]205      exact h206  rw [hval, toNatBE_heap rfl hwQ (by omega)]207  rw [hQ, getD_set_eq' P y hi]

353/-- The binary mirror selector is a constant-depth (≤ 10), polynomial-size formula family354    reading only the B·N board bits. -/355theorem pairBin_bound (B N r : Nat) (hr : N ≤ 2 ^ r) (hN : N % 2 = 0) :356    BinBound (pairBin B N r) N B r 10 (4 * ((N + 2) * (N * (2 * pairF B + 1) + 1 + 2)) ^ 3) (B * N) :=357  encode_bound (pairR B N) (by simp [pairR]) (by simp [pairR]) hr358    (fun c hc => ⟨(pairR_res B N c hc).1, (pairR_res B N c hc).2, pairR_reads B N hN c hc⟩)

690theorem pairing_net_weak :691    WeakMasteryFam (fun B P => Paired P ∧ Width B P) .second (fun B => ofSel (pairNetSel B)) := by692  intro B693  show WeakMastery _ _ (ofSel (pairNetSel B))694  rw [pairNetSel_eq]; exact pairing_weak B

673/-- For the first role the paired family is losing, so weak mastery there is vacuous. -/674theorem pairing_first_vacuous (B : Nat) (σ : Strat) : WeakMastery (fun P => Paired P ∧ Width B P) .first σ :=675  weakMastery_vacuous (fun P0 hF hw => (roleWinnable_first P0).1 hw (paired_lose hF.1 hF.2).2) σ