NimAttain

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 NimProbability23/- Phase 3, target A: attainability.  Written by Claude (10 October 2026).4   Lean 4.26.0, core/Std only.  Imports the unchanged phase 1-2 files.56   For B ≥ 2 and any nonzero B-bit functional ell(sigma) = <w, sigma>, an explicit7   readout (cancel a guessed nim-sum a_b at the first eligible heap, else subtract8   1 from the first nonzero heap, halt only on terminal boards) has conditional9   success10     * at least 2/(2^B-1) for ANY nonzero fibre representatives a_0, a_1, and11     * exactly 2/(2^B-1) when a_b is the least nonzero value in its fibre.12   The paper's B = 2, pi_0 example (a_0 = 2, a_1 = 1) is the least-representative13   case, so its success is exactly 2/3 for every N ≥ 1.1415   This file proves the finite combinatorics only; it says nothing about circuit16   complexity of the readout (that belongs to targets C/D). -/1718namespace NimAudit19namespace Attain2021open Game Rollout Prob2223attribute [local simp] Rat.add_zero Rat.zero_add Rat.zero_mul Rat.mul_zero Rat.one_mul2425/-! ## The readout -/2627/-- First index i with x_i XOR t < x_i, with the new value x_i XOR t. -/28def cancelIdx (t : Nat) : List Nat → Option (Nat × Nat)29  | [] => none30  | x :: rest =>31    if x ^^^ t < x then some (0, x ^^^ t) else (cancelIdx t rest).map (fun p => (p.1 + 1, p.2))3233/-- First nonzero index i with new value x_i - 1. -/34def decIdx : List Nat → Option (Nat × Nat)35  | [] => none36  | x :: rest => if 0 < x then some (0, x - 1) else (decIdx rest).map (fun p => (p.1 + 1, p.2))3738/-- Attainability readout with guesses a_0 (observed bit false) and a_1 (true). -/39def attainF (a0 a1 : Nat) : Readout := fun P b =>40  match cancelIdx (if b then a1 else a0) P with41  | some m => some m42  | none => decIdx P4344theorem cancelIdx_some {t : Nat} {P : List Nat} {i v : Nat} (h : cancelIdx t P = some (i, v)) :45    ∃ x, P[i]? = some x ∧ v = x ^^^ t ∧ v < x := by46  induction P generalizing i v with47  | nil => simp [cancelIdx] at h48  | cons x rest ih =>49    by_cases hx : x ^^^ t < x50    · simp only [cancelIdx, hx, if_true, Option.some.injEq, Prod.mk.injEq] at h51      obtain ⟨rfl, rfl⟩ := h52      exact ⟨x, rfl, rfl, hx⟩53    · simp only [cancelIdx, hx, if_false] at h54      cases hr : cancelIdx t rest with55      | none => simp [hr] at h56      | some p =>57        obtain ⟨i', v'⟩ := p58        simp only [hr, Option.map_some, Option.some.injEq, Prod.mk.injEq] at h59        obtain ⟨rfl, rfl⟩ := h60        obtain ⟨y, hy, rfl, hlt⟩ := ih hr61        exact ⟨y, by simpa using hy, rfl, hlt⟩6263theorem cancelIdx_none {t : Nat} {P : List Nat} (h : cancelIdx t P = none) :64    ∀ x ∈ P, ¬ x ^^^ t < x := by65  induction P with66  | nil => simp67  | cons x rest ih =>68    by_cases hx : x ^^^ t < x69    · simp [cancelIdx, hx] at h70    · simp only [cancelIdx, hx, if_false] at h71      cases hr : cancelIdx t rest with72      | some p => simp [hr] at h73      | none =>74        intro y hy75        rcases List.mem_cons.mp hy with rfl | hy76        · exact hx77        · exact ih hr y hy7879theorem decIdx_some {P : List Nat} {i v : Nat} (h : decIdx P = some (i, v)) :80    ∃ x, P[i]? = some x ∧ v = x - 1 ∧ 0 < x := by81  induction P generalizing i v with82  | nil => simp [decIdx] at h83  | cons x rest ih =>84    by_cases hx : 0 < x85    · simp only [decIdx, hx, if_true, Option.some.injEq, Prod.mk.injEq] at h86      obtain ⟨rfl, rfl⟩ := h87      exact ⟨x, rfl, rfl, hx⟩88    · simp only [decIdx, hx, if_false] at h89      cases hr : decIdx rest with90      | none => simp [hr] at h91      | some p =>92        obtain ⟨i', v'⟩ := p93        simp only [hr, Option.map_some, Option.some.injEq, Prod.mk.injEq] at h94        obtain ⟨rfl, rfl⟩ := h95        obtain ⟨y, hy, rfl, hlt⟩ := ih hr96        exact ⟨y, by simpa using hy, rfl, hlt⟩9798theorem decIdx_none {P : List Nat} (h : decIdx P = none) : Terminal P := by99  induction P with100  | nil => intro x hx; simp at hx101  | cons x rest ih =>102    by_cases hx : 0 < x103    · simp [decIdx, hx] at h104    · simp only [decIdx, hx, if_false] at h105      cases hr : decIdx rest with106      | some p => simp [hr] at h107      | none =>108        intro y hy109        rcases List.mem_cons.mp hy with rfl | hy110        · omega111        · exact ih hr y hy112113theorem decIdx_terminal {P : List Nat} (h : Terminal P) : decIdx P = none := by114  induction P with115  | nil => rfl116  | cons x rest ih =>117    have hx : x = 0 := h x (by simp)118    subst hx119    simp [decIdx, ih (fun y hy => h y (List.mem_cons_of_mem _ hy))]120121theorem cancelIdx_terminal {t : Nat} {P : List Nat} (h : Terminal P) : cancelIdx t P = none := by122  induction P with123  | nil => rfl124  | cons x rest ih =>125    have hx : x = 0 := h x (by simp)126    subst hx127    simp [cancelIdx, ih (fun y hy => h y (List.mem_cons_of_mem _ hy))]128129/-- Every output of the readout is a legal move (index in range, value strictly smaller). -/130theorem attainF_legal {a0 a1 : Nat} {P : List Nat} {b : Bool} {i v : Nat}131    (h : attainF a0 a1 P b = some (i, v)) : ∃ x, P[i]? = some x ∧ v < x := by132  unfold attainF at h133  split at h134  · next m hm =>135    cases h136    obtain ⟨x, hx, rfl, hlt⟩ := cancelIdx_some hm137    exact ⟨x, hx, hlt⟩138  · obtain ⟨x, hx, rfl, hlt⟩ := decIdx_some h139    exact ⟨x, hx, by omega⟩140141theorem attainF_move {a0 a1 : Nat} {P : List Nat} {b : Bool} {i v : Nat}142    (h : attainF a0 a1 P b = some (i, v)) : Move P (P.set i v) := by143  obtain ⟨x, hx, hlt⟩ := attainF_legal h144  exact set_move hx hlt145146/-- The readout halts exactly on terminal boards. -/147theorem attainF_none_iff (a0 a1 : Nat) (P : List Nat) (b : Bool) :148    attainF a0 a1 P b = none ↔ Terminal P := by149  constructor150  · intro h151    unfold attainF at h152    split at h153    · cases h154    · exact decIdx_none h155  · intro ht156    unfold attainF157    rw [cancelIdx_terminal ht, decIdx_terminal ht]158159theorem gval_attainF_cancel {a0 a1 : Nat} {P : List Nat} {b : Bool} {i v : Nat}160    (hc : cancelIdx (if b then a1 else a0) P = some (i, v)) :161    gval (attainF a0 a1) b P = (if b then a1 else a0) := by162  obtain ⟨x, hx, rfl, hlt⟩ := cancelIdx_some hc163  have hF : attainF a0 a1 P b = some (i, x ^^^ (if b then a1 else a0)) := by164    unfold attainF; rw [hc]165  unfold gval166  rw [hF]167  simp only [hx, hlt, if_true]168  exact xor_cancel_left x _169170/-- SUCCESS WHEN THE GUESS IS RIGHT: if sigma(P) = a_b ≠ 0 the readout wins. -/171theorem attain_success {a0 a1 : Nat} {P : List Nat} {b : Bool}172    (hs : nimSum P = (if b then a1 else a0)) (h0 : nimSum P ≠ 0) :173    successB (attainF a0 a1) b P = true := by174  rw [success_iff_gval h0]175  obtain ⟨pre, x, post, hp, hlt, _⟩ := exists_decreasing_heap P h0176  cases hc : cancelIdx (if b then a1 else a0) P with177  | none =>178    exact absurd (hs ▸ hlt) (cancelIdx_none hc x (by rw [hp]; simp))179  | some m =>180    obtain ⟨i, v⟩ := m181    rw [gval_attainF_cancel hc, hs]182183/-! ## Lower bound 2/(2^B - 1) for any fibre representatives -/184185theorem rsum_nonneg_ite {α : Type} (l : List α) (p : α → Prop) [DecidablePred p] :186    (0 : Rat) ≤ rsum l (fun x => if p x then 1 else 0) := by187  have := rsum_le (l := l) (f := fun _ => (0 : Rat)) (g := fun x => if p x then 1 else 0)188    (by intro x _; show (0 : Rat) ≤ if p x then 1 else 0; split <;> grind)189  rw [rsum_zero] at this190  exact this191192/-- (counting form) #success ≥ #{sigma = a_0} + #{sigma = a_1} = 2 q^N. -/193theorem attain_count_lower {B N w a0 a1 : Nat} (ha0 : a0 ≠ 0) (ha1 : a1 ≠ 0)194    (hd0 : dotB B w a0 = false) (hd1 : dotB B w a1 = true)195    (hl0 : a0 < 2 ^ B) (hl1 : a1 < 2 ^ B) :196    2 * ((2 ^ B : Nat) : Rat) ^ N ≤ succCount B (N + 1) (attainF a0 a1) w := by197  have hne : a0 ≠ a1 := by intro e; rw [e, hd1] at hd0; cases hd0198  have hle : rsum (boards (2 ^ B) (N + 1))199      (fun P => (if nimSum P = a0 then 1 else 0) + (if nimSum P = a1 then 1 else 0)) ≤200      succCount B (N + 1) (attainF a0 a1) w := by201    unfold succCount202    apply rsum_le203    intro P _204    by_cases h0 : nimSum P = a0205    · have hs : successB (attainF a0 a1) (dotB B w (nimSum P)) P = true := by206        apply attain_success207        · rw [h0, hd0]; simp208        · rw [h0]; exact ha0209      rw [h0] at hs210      simp [h0, hne, hs, ha0]211      exact Rat.le_refl212    · by_cases h1 : nimSum P = a1213      · have hs : successB (attainF a0 a1) (dotB B w (nimSum P)) P = true := by214          apply attain_success215          · rw [h1, hd1]; simp216          · rw [h1]; exact ha1217        rw [h1] at hs218        simp [h1, hs, ha1, Ne.symm hne]219        exact Rat.le_refl220      · simp only [h0, h1, if_false, Rat.add_zero]221        split <;> grind222  rw [rsum_add, sigma_uniform B N a0 hl0, sigma_uniform B N a1 hl1] at hle223  grind224225theorem nonzeroCount_eq' (B N : Nat) :226    nonzeroCount B (N + 1) = (((2 ^ B : Nat) : Rat) - 1) * ((2 ^ B : Nat) : Rat) ^ N := by227  rw [nonzeroCount_eq]228  unfold T229  rw [Rat.pow_succ]230  grind231232theorem qpow_pos (B N : Nat) : (0 : Rat) < ((2 ^ B : Nat) : Rat) ^ N := by233  rw [← Rat.natCast_pow]; exact Rat.natCast_pos.mpr (Nat.pow_pos (Nat.two_pow_pos B))234235theorem q_ge_two {B : Nat} (hB : 1 ≤ B) : (2 : Rat) ≤ ((2 ^ B : Nat) : Rat) := by236  have hqge : 2 ≤ 2 ^ B := by237    have := Nat.pow_le_pow_right (show 0 < 2 by decide) hB; simpa using this238  have := Rat.natCast_le_natCast.mpr hqge; simpa using this239240/-- LOWER BOUND: for B ≥ 1 and any nonzero fibre representatives a_0, a_1,241    Pr[legal winning move | sigma ≠ 0] ≥ 2/(2^B - 1). -/242theorem attain_lower {B N w a0 a1 : Nat} (hB : 1 ≤ B) (ha0 : a0 ≠ 0) (ha1 : a1 ≠ 0)243    (hd0 : dotB B w a0 = false) (hd1 : dotB B w a1 = true)244    (hl0 : a0 < 2 ^ B) (hl1 : a1 < 2 ^ B) :245    2 / (((2 ^ B : Nat) : Rat) - 1) ≤246      succCount B (N + 1) (attainF a0 a1) w / nonzeroCount B (N + 1) := by247  have hc := attain_count_lower (N := N) ha0 ha1 hd0 hd1 hl0 hl1248  rw [nonzeroCount_eq']249  have ht := qpow_pos B N250  have hq2 := q_ge_two hB251  generalize succCount B (N + 1) (attainF a0 a1) w = S at *252  generalize ((2 ^ B : Nat) : Rat) ^ N = t at *253  generalize ((2 ^ B : Nat) : Rat) = q at *254  have h1 : (0 : Rat) < q - 1 := by grind255  have hZ : 0 < (q - 1) * t := Rat.mul_pos h1 ht256  have hZ' : (q - 1) * t ≠ 0 := Rat.ne_of_gt hZ257  have hq1 : q - 1 ≠ 0 := Rat.ne_of_gt h1258  -- 2/(q-1) * Z = 2 t ≤ S, so 2/(q-1) ≤ S/Z259  apply Rat.le_of_mul_le_mul_right _ hZ260  have e1 : 2 / (q - 1) * ((q - 1) * t) = 2 * t := by grind261  have e2 : S / ((q - 1) * t) * ((q - 1) * t) = S := by grind262  rw [e1, e2]263  exact hc264265/-! ## Least fibre representatives and exact equality -/266267/-- Least n' < n with p n' (if any). -/268def findLeast (p : Nat → Bool) : Nat → Option Nat269  | 0 => none270  | n + 1 =>271    match findLeast p n with272    | some a => some a273    | none => if p n then some n else none274275theorem findLeast_some {p : Nat → Bool} {n a : Nat} (h : findLeast p n = some a) :276    p a = true ∧ a < n ∧ ∀ c < a, p c = false := by277  induction n generalizing a with278  | zero => simp [findLeast] at h279  | succ n ih =>280    unfold findLeast at h281    split at h282    · next a' ha' =>283      cases h284      obtain ⟨h1, h2, h3⟩ := ih ha'285      exact ⟨h1, by omega, h3⟩286    · next hnone =>287      by_cases hp : p n = true288      · simp only [hp, if_true, Option.some.injEq] at h289        subst h290        refine ⟨hp, by omega, ?_⟩291        intro c hc292        have key : ∀ m, findLeast p m = none → ∀ c < m, p c = false := by293          intro m294          induction m with295          | zero => intro _ c hc; omega296          | succ m ihm =>297            intro hm c hc298            unfold findLeast at hm299            split at hm300            · cases hm301            · next hm' =>302              by_cases hpm : p m = true303              · simp [hpm] at hm304              · by_cases hcm : c = m305                · subst hcm; simpa using hpm306                · exact ihm hm' c (by omega)307        exact key n hnone c hc308      · simp [hp] at h309310theorem findLeast_isSome {p : Nat → Bool} {n c : Nat} (hc : c < n) (hp : p c = true) :311    ∃ a, findLeast p n = some a := by312  induction n with313  | zero => omega314  | succ n ih =>315    unfold findLeast316    cases hf : findLeast p n with317    | some a => exact ⟨a, rfl⟩318    | none =>319      by_cases hcn : c = n320      · subst hcn; exact ⟨c, by simp [hp]⟩321      · obtain ⟨a, ha⟩ := ih (by omega)322        rw [hf] at ha; cases ha323324/-- The fibre predicate: nonzero with ell(a) = b. -/325def inFibre (B w : Nat) (b : Bool) (a : Nat) : Bool := a != 0 && dotB B w a == b326327/-- Least nonzero B-bit value in the fibre ell = b (0 if none). -/328def fibreRep (B w : Nat) (b : Bool) : Nat := (findLeast (inFibre B w b) (2 ^ B)).getD 0329330theorem dotB_comm (B u v : Nat) : dotB B u v = dotB B v u := by331  induction B with332  | zero => rfl333  | succ B ih => simp only [dotB, ih, Bool.and_comm]334335theorem dotB_two_pow_right (B j v : Nat) : dotB B v (2 ^ j) = (decide (j < B) && v.testBit j) := by336  rw [dotB_comm, dotB_two_pow]337338/-- Both fibres of a nonzero functional on F_2^B (B ≥ 2) contain a nonzero vector. -/339theorem fibre_nonempty {B w : Nat} (hB : 2 ≤ B) (hw0 : w ≠ 0) (hw : w < 2 ^ B) (b : Bool) :340    ∃ c, c < 2 ^ B ∧ inFibre B w b c = true := by341  obtain ⟨i, hi⟩ := Nat.exists_testBit_of_ne_zero hw0342  have hiB : i < B := by343    rcases Nat.lt_or_ge i B with hlt | hge344    · exact hlt345    exfalso346    have := Nat.testBit_lt_two_pow347      (Nat.lt_of_lt_of_le hw (Nat.pow_le_pow_right (by decide) (by omega)) : w < 2 ^ i)348    rw [this] at hi; cases hi349  have hpi : 2 ^ i < 2 ^ B := Nat.pow_lt_pow_right (by decide) hiB350  cases b with351  | true =>352    refine ⟨2 ^ i, hpi, ?_⟩353    simp [inFibre, dotB_two_pow_right, hiB, hi, Nat.ne_of_gt (Nat.two_pow_pos i)]354  | false =>355    let k := if i = 0 then 1 else 0356    have hkB : k < B := by simp only [k]; split <;> omega357    have hki : k ≠ i := by simp only [k]; split <;> omega358    have hpk : 2 ^ k < 2 ^ B := Nat.pow_lt_pow_right (by decide) hkB359    cases hwk : w.testBit k with360    | false =>361      refine ⟨2 ^ k, hpk, ?_⟩362      simp [inFibre, dotB_two_pow_right, hkB, hwk, Nat.ne_of_gt (Nat.two_pow_pos k)]363    | true =>364      refine ⟨2 ^ i ^^^ 2 ^ k, Nat.xor_lt_two_pow hpi hpk, ?_⟩365      have hne : 2 ^ i ^^^ 2 ^ k ≠ 0 := by366        intro h367        have e := congrArg (fun z => z.testBit i) (xor_eq_zero_imp h)368        simp only [Nat.testBit_two_pow, decide_true] at e369        exact hki (of_decide_eq_true e.symm)370      simp only [inFibre, dotB_xor_right, dotB_two_pow_right, hiB, hkB, hi, hwk,371        decide_true, Bool.true_and]372      simp [hne]373374theorem fibreRep_spec {B w : Nat} (hB : 2 ≤ B) (hw0 : w ≠ 0) (hw : w < 2 ^ B) (b : Bool) :375    fibreRep B w b ≠ 0 ∧ fibreRep B w b < 2 ^ B ∧ dotB B w (fibreRep B w b) = b ∧376      ∀ c, c < fibreRep B w b → c ≠ 0 → dotB B w c ≠ b := by377  obtain ⟨c, hc, hpc⟩ := fibre_nonempty hB hw0 hw b378  obtain ⟨a, ha⟩ := findLeast_isSome hc hpc379  obtain ⟨h1, h2, h3⟩ := findLeast_some ha380  have hrep : fibreRep B w b = a := by simp [fibreRep, ha]381  rw [hrep]382  simp only [inFibre, Bool.and_eq_true, bne_iff_ne, ne_eq, beq_iff_eq] at h1383  refine ⟨h1.1, h2, h1.2, ?_⟩384  intro c' hc' hc0 hd385  have := h3 c' hc'386  simp [inFibre, hc0, hd] at this387388/-- x XOR (x - 1) is a low mask 2^s - 1, for x > 0. -/389theorem xor_pred_mask (x : Nat) (hx : 0 < x) : ∃ s, x ^^^ (x - 1) = 2 ^ s - 1 := by390  induction x using Nat.strongRecOn with391  | ind x ih =>392    rcases Nat.mod_two_eq_zero_or_one x with hev | hod393    · -- x = 2y with y > 0394      have hy : 0 < x / 2 := by omega395      obtain ⟨s, hs⟩ := ih (x / 2) (by omega) hy396      refine ⟨s + 1, ?_⟩397      have key : x ^^^ (x - 1) = 2 * ((x / 2) ^^^ (x / 2 - 1)) + 1 := by398        apply Nat.eq_of_testBit_eq399        intro i400        cases i with401        | zero =>402          rw [Nat.testBit_xor, Nat.testBit_zero, Nat.testBit_zero, Nat.testBit_zero]403          have h1 : (x - 1) % 2 = 1 := by omega404          have h2 : (2 * ((x / 2) ^^^ (x / 2 - 1)) + 1) % 2 = 1 := by omega405          simp [hev, h1, h2]406        | succ i =>407          rw [Nat.testBit_xor, ← Nat.testBit_div_two x i, ← Nat.testBit_div_two (x - 1) i,408            ← Nat.testBit_div_two (2 * ((x / 2) ^^^ (x / 2 - 1)) + 1) i]409          have e1 : (x - 1) / 2 = x / 2 - 1 := by omega410          have e2 : (2 * ((x / 2) ^^^ (x / 2 - 1)) + 1) / 2 = (x / 2) ^^^ (x / 2 - 1) := by omega411          rw [e1, e2, Nat.testBit_xor]412      rw [key, hs, Nat.pow_succ]413      have := Nat.two_pow_pos s414      omega415    · refine ⟨1, ?_⟩416      apply Nat.eq_of_testBit_eq417      intro i418      cases i with419      | zero =>420        rw [Nat.testBit_xor, Nat.testBit_zero, Nat.testBit_zero]421        have h1 : (x - 1) % 2 = 0 := by omega422        simp [hod, h1]423      | succ i =>424        rw [Nat.testBit_xor, ← Nat.testBit_div_two x i, ← Nat.testBit_div_two (x - 1) i]425        have e1 : (x - 1) / 2 = x / 2 := by omega426        rw [e1, Bool.xor_self]427        exact (Nat.testBit_lt_two_pow (Nat.one_lt_two_pow (by omega) : (2 ^ 1 - 1) < 2 ^ (i + 1))).symm428429/-- NO ADDITIONAL SUCCESS for least representatives: if sigma ≠ 0 and sigma differs430    from the guess a_{ell(sigma)}, the readout's move does not win. -/431theorem attain_no_extra {B w : Nat} (hB : 2 ≤ B) (hw0 : w ≠ 0) (hw : w < 2 ^ B)432    {P : List Nat} (h0 : nimSum P ≠ 0)433    (hne : nimSum P ≠ fibreRep B w (dotB B w (nimSum P))) :434    successB (attainF (fibreRep B w false) (fibreRep B w true)) (dotB B w (nimSum P)) P = false := by435  have key : ¬ gval (attainF (fibreRep B w false) (fibreRep B w true)) (dotB B w (nimSum P)) P =436      nimSum P := by437    generalize hbdef : dotB B w (nimSum P) = b at hne438    have ht : (if b then fibreRep B w true else fibreRep B w false) = fibreRep B w b := by439      cases b <;> rfl440    obtain ⟨tnz, _, tdot, tmin⟩ := fibreRep_spec hB hw0 hw b441    cases hc : cancelIdx (if b then fibreRep B w true else fibreRep B w false) P with442    | some m =>443      obtain ⟨i, v⟩ := m444      rw [gval_attainF_cancel hc, ht]445      exact fun e => hne e.symm446    | none =>447      rw [ht] at hc448      -- the fallback is used449      have hnt : ¬ Terminal P := by450        intro hterm451        apply h0452        have : ∀ q : List Nat, Terminal q → nimSum q = 0 := by453          intro q hq454          induction q with455          | nil => rfl456          | cons y ys ihq =>457            simp only [nimSum, hq y (by simp), Nat.zero_xor]458            exact ihq (fun z hz => hq z (List.mem_cons_of_mem _ hz))459        exact this P hterm460      cases hd : decIdx P with461      | none => exact absurd (decIdx_none hd) hnt462      | some m =>463        obtain ⟨i, v⟩ := m464        obtain ⟨x, hx, rfl, hxpos⟩ := decIdx_some hd465        have hF : attainF (fibreRep B w false) (fibreRep B w true) P b = some (i, x - 1) := by466          unfold attainF; rw [ht, hc]; exact hd467        unfold gval468        rw [hF]469        simp only [hx, show x - 1 < x by omega, if_true]470        intro hdelta471        -- top bit k of t = fibreRep B w b is absent from every heap472        let t := fibreRep B w b473        let k := t.log2474        have htk : t.testBit k = true := by475          cases hb' : t.testBit k with476          | true => rfl477          | false =>478            exfalso479            have hlt : t < 2 ^ k := by480              apply Nat.lt_pow_two_of_testBit481              intro i' hi'482              by_cases hik : i' = k483              · subst hik; exact hb'484              · apply Nat.testBit_lt_two_pow485                exact Nat.lt_of_lt_of_le Nat.lt_log2_self486                  (Nat.pow_le_pow_right (by decide) (by omega))487            exact absurd (Nat.log2_self_le tnz) (Nat.not_le.mpr hlt)488        have habove : ∀ i', k < i' → t.testBit i' = false := by489          intro i' hi'490          apply Nat.testBit_lt_two_pow491          exact Nat.lt_of_lt_of_le Nat.lt_log2_self (Nat.pow_le_pow_right (by decide) (by omega))492        have hnoheap : ∀ y ∈ P, y.testBit k = false := by493          intro y hy494          cases hyk : y.testBit k with495          | false => rfl496          | true =>497            exfalso498            apply cancelIdx_none hc y hy499            apply lt_of_top_testBit (k := k)500            · rw [Nat.testBit_xor, hyk, htk]; rfl501            · exact hyk502            · intro i' hi'; rw [Nat.testBit_xor, habove i' hi', Bool.xor_false]503        have hsk : (nimSum P).testBit k = false := by504          cases hsk' : (nimSum P).testBit k with505          | false => rfl506          | true =>507            obtain ⟨y, hy, hyk⟩ := exists_heap_testBit hsk'508            rw [hnoheap y hy] at hyk; cases hyk509        obtain ⟨s, hs⟩ := xor_pred_mask x hxpos510        rw [hdelta] at hs511        have hks : ¬ k < s := by512          intro hlt513          have := Nat.testBit_two_pow_sub_one s k514          rw [← hs, hsk] at this515          simp [hlt] at this516        have hσlt : nimSum P < t := by517          have h1 : nimSum P < 2 ^ s := by rw [hs]; have := Nat.two_pow_pos s; omega518          have h2 : 2 ^ s ≤ 2 ^ k := Nat.pow_le_pow_right (by decide) (by omega)519          have h3 : 2 ^ k ≤ t := Nat.log2_self_le tnz520          omega521        exact tmin (nimSum P) hσlt h0 hbdef522  cases hs : successB (attainF (fibreRep B w false) (fibreRep B w true)) (dotB B w (nimSum P)) P523  · rfl524  · exact absurd ((success_iff_gval h0).1 hs) key525526/-- EXACT SUCCESS COUNT for least representatives: #success = 2 q^N. -/527theorem attain_count_exact {B N w : Nat} (hB : 2 ≤ B) (hw0 : w ≠ 0) (hw : w < 2 ^ B) :528    succCount B (N + 1) (attainF (fibreRep B w false) (fibreRep B w true)) w =529      2 * ((2 ^ B : Nat) : Rat) ^ N := by530  obtain ⟨n0, l0, d0, _⟩ := fibreRep_spec hB hw0 hw false531  obtain ⟨n1, l1, d1, _⟩ := fibreRep_spec hB hw0 hw true532  have hne : fibreRep B w false ≠ fibreRep B w true := by533    intro e; rw [e, d1] at d0; cases d0534  have heq : succCount B (N + 1) (attainF (fibreRep B w false) (fibreRep B w true)) w =535      rsum (boards (2 ^ B) (N + 1))536        (fun P => (if nimSum P = fibreRep B w false then 1 else 0) +537          (if nimSum P = fibreRep B w true then 1 else 0)) := by538    unfold succCount539    apply rsum_congr540    intro P _541    by_cases h0 : nimSum P = fibreRep B w false542    · have hs := attain_success (a0 := fibreRep B w false) (a1 := fibreRep B w true)543        (b := dotB B w (nimSum P)) (P := P) (by rw [h0, d0]; simp) (by rw [h0]; exact n0)544      rw [h0] at hs545      simp [h0, hne, hs, n0]546    · by_cases h1 : nimSum P = fibreRep B w true547      · have hs := attain_success (a0 := fibreRep B w false) (a1 := fibreRep B w true)548          (b := dotB B w (nimSum P)) (P := P) (by rw [h1, d1]; simp) (by rw [h1]; exact n1)549        rw [h1] at hs550        simp [h1, hs, n1, Ne.symm hne]551      · simp only [h0, h1, if_false, Rat.add_zero]552        by_cases hz : nimSum P = 0553        · simp [hz]554        · have hguess : nimSum P ≠ fibreRep B w (dotB B w (nimSum P)) := by555            cases hb : dotB B w (nimSum P)556            · exact h0557            · exact h1558          have := attain_no_extra hB hw0 hw hz hguess559          simp [this]560  rw [heq, rsum_add, sigma_uniform B N _ l0, sigma_uniform B N _ l1]561  grind562563/-- EXACT ATTAINABILITY: for B ≥ 2, any nonzero B-bit functional w, every N ≥ 1,564    the least-representative readout succeeds with conditional probability exactly565    2/(2^B - 1). -/566theorem attain_exact {B N w : Nat} (hB : 2 ≤ B) (hw0 : w ≠ 0) (hw : w < 2 ^ B) :567    succCount B (N + 1) (attainF (fibreRep B w false) (fibreRep B w true)) w /568        nonzeroCount B (N + 1) = 2 / (((2 ^ B : Nat) : Rat) - 1) := by569  rw [attain_count_exact hB hw0 hw, nonzeroCount_eq']570  have ht := qpow_pos B N571  have hq2 := q_ge_two (B := B) (by omega)572  generalize ((2 ^ B : Nat) : Rat) ^ N = t at *573  generalize ((2 ^ B : Nat) : Rat) = q at *574  have h1 : q - 1 ≠ 0 := by grind575  have h2 : t ≠ 0 := Rat.ne_of_gt ht576  grind577578/-! ## Structured heads and the paper's B = 2 example -/579580/-- The readout fed the actual rollout outcome RO_{pi_j}(P) has the same success581    count as when fed <w_j, sigma(P)>. -/582theorem succCountRO_eq {B N j : Nat} (hj : j < B) (F : Readout) :583    succCountRO B N F j = succCount B N F (headVec j) := by584  unfold succCountRO succCount585  apply rsum_congr; intro P _586  rw [rollout_outcome_linear hj]587588/-- EXACT ATTAINABILITY FOR EACH STRUCTURED HEAD pi_j (j < B, B ≥ 2), with the589    readout fed the executed rollout outcome. -/590theorem attain_exact_head {B N j : Nat} (hB : 2 ≤ B) (hj : j < B) :591    succCountRO B (N + 1)592        (attainF (fibreRep B (headVec j) false) (fibreRep B (headVec j) true)) j /593      nonzeroCount B (N + 1) = 2 / (((2 ^ B : Nat) : Rat) - 1) := by594  rw [succCountRO_eq hj]595  exact attain_exact hB (headVec_ne_zero j) (headVec_lt hj)596597theorem rep_B2_false : fibreRep 2 (headVec 0) false = 2 := by decide598theorem rep_B2_true : fibreRep 2 (headVec 0) true = 1 := by decide599600/-- THE PAPER'S EXAMPLE: B = 2, head pi_0, guesses a_0 = 2, a_1 = 1, fallback601    "subtract 1": conditional success exactly 2/3 for every N ≥ 1. -/602theorem paper_example_two_thirds (N : Nat) :603    succCountRO 2 (N + 1) (attainF 2 1) 0 / nonzeroCount 2 (N + 1) = 2 / 3 := by604  have := attain_exact_head (B := 2) (N := N) (j := 0) (by decide) (by decide)605  rw [rep_B2_false, rep_B2_true] at this606  rw [this]607  have e : (((2 ^ 2 : Nat) : Rat) - 1) = 3 := by608    rw [show (2 ^ 2 : Nat) = 4 from rfl]; simp; grind609  rw [e]610611/-! ## Sharpness of the leading constant -/612613/-- CorrHyp forces η ≥ 0 (B ≥ 1). -/614theorem corrHyp_nonneg {B N : Nat} {F : Readout} {η : Rat} (hB : 1 ≤ B)615    (hyp : CorrHyp B N F η) : 0 ≤ η := by616  have h1 : 1 < 2 ^ B := Nat.one_lt_two_pow (by omega)617  obtain ⟨k1, k2⟩ := hyp false 0 1 (Nat.two_pow_pos B) (by decide) h1618  grind619620/-- SHARPNESS (finite, two-sided).  For B ≥ 2, N ≥ 1 and a structured head j < B:621    (1) the explicit readout attains exactly 2/(q-1);622    (2) every readout satisfying CorrHyp with error η succeeds with conditional623        probability at most 2/(q-1) + (q-1) η.624    Hence no constant below 2/(q-1) can replace the leading term in (2) for any625    class containing the explicit readout, PROVIDED that readout satisfies the626    correlation premise with η_N → 0.  That proviso is the circuit/correlation627    bridge (targets C/D); it is not proved here. -/628theorem sharpness {B N j : Nat} (hB : 2 ≤ B) (hj : j < B) :629    succCountRO B (N + 1)630        (attainF (fibreRep B (headVec j) false) (fibreRep B (headVec j) true)) j /631      nonzeroCount B (N + 1) = 2 / (((2 ^ B : Nat) : Rat) - 1) ∧632    ∀ (F : Readout) (η : Rat), CorrHyp B (N + 1) F η →633      succCountRO B (N + 1) F j / nonzeroCount B (N + 1) ≤634        2 / (((2 ^ B : Nat) : Rat) - 1) + (((2 ^ B : Nat) : Rat) - 1) * η :=635  ⟨attain_exact_head hB hj, fun F _ hyp => structured_head_bound hj F hyp⟩636637#print axioms cancelIdx_some638#print axioms cancelIdx_none639#print axioms decIdx_some640#print axioms decIdx_none641#print axioms decIdx_terminal642#print axioms cancelIdx_terminal643#print axioms attainF_legal644#print axioms attainF_move645#print axioms attainF_none_iff646#print axioms gval_attainF_cancel647#print axioms attain_success648#print axioms rsum_nonneg_ite649#print axioms attain_count_lower650#print axioms nonzeroCount_eq'651#print axioms qpow_pos652#print axioms q_ge_two653#print axioms attain_lower654#print axioms findLeast_some655#print axioms findLeast_isSome656#print axioms dotB_comm657#print axioms dotB_two_pow_right658#print axioms fibre_nonempty659#print axioms fibreRep_spec660#print axioms xor_pred_mask661#print axioms attain_no_extra662#print axioms attain_count_exact663#print axioms attain_exact664#print axioms succCountRO_eq665#print axioms attain_exact_head666#print axioms rep_B2_false667#print axioms rep_B2_true668#print axioms paper_example_two_thirds669#print axioms corrHyp_nonneg670#print axioms sharpness671672end Attain673end NimAudit