Family

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 WholeGame23/- Phase 6, Priority 1a: family-level resource certificates.  Written by Claude4   (10 October 2026).  Lean 4.26.0, core/Std only.56   CONVENTIONS (stated once, used throughout phase 6).7   * A FAMILY is indexed by a type ι with an admissibility predicate `adm` (here: B ≥ 1,8     N ≥ 1, and j < B for policies; degenerate indices B = 0 or N = 0 are excluded from9     the asymptotic statements and remain covered by the finite phase-5 theorems).10   * `len i` is the ACTUAL supplied Boolean input length of member i: 2·B·N for the two11     frames, B·N for one board, B·N + B for a board with B outcome bits, and the12     per-update width 6 + 6B + 3r (state plus one token) for the recurrent controller.13   * Formulas are `AC0.Circ` trees: size counts every node (leaves, NOT, AND, OR); depth14     counts NOT.  A MULTI-OUTPUT member is a list of output formulas in a fixed order;15     its size is the TOTAL size of the list (no sharing between outputs), so the number16     of outputs is also polynomially bounded.17   * AC0Fam is NONUNIFORM: it asserts existence of the formulas for each member with a18     fixed depth bound d and a total-size bound c·len^k whose c, k do not depend on the19     member.  (The phase-6 members are given by explicit Lean definitions, but no20     DLOGTIME-uniformity claim is made.)21   * NetFam is the corresponding statement for fixed-scale threshold networks: fixed W,22     fixed layer bound L, valid gates, first layer wired to the len inputs, polynomial23     widths/fan-ins and gate count.24   Every certificate below is stated for the SAME object as its semantics theorem. -/2526namespace NimAudit27namespace Family2829open Game Rollout Prob Attain Recurrent AC0 AC0.Circ CorrBridge AttainCircuit Bridge SelectCircuit30  BinReadout Controller ControllerBits PriorityEncoder ThresholdNet ThresholdInst FiniteNet WholeGame3132/-! ## Polynomial bounds over an indexed family -/3334section Poly35variable {ι : Type}3637/-- f is bounded by c·(len i)^k on admissible indices, with c and k fixed. -/38def PolyIn (adm : ι → Prop) (len : ι → Nat) (f : ι → Nat) : Prop :=39  ∃ c k : Nat, ∀ i, adm i → f i ≤ c * len i ^ k4041theorem polyIn_const (adm : ι → Prop) (len : ι → Nat) (a : Nat) : PolyIn adm len (fun _ => a) :=42  ⟨a, 0, fun i _ => by simp⟩4344theorem polyIn_leaf {adm : ι → Prop} {len : ι → Nat} {f : ι → Nat} (h : ∀ i, adm i → f i ≤ len i) :45    PolyIn adm len f :=46  ⟨1, 1, fun i hi => by simpa using h i hi⟩4748theorem polyIn_add {adm : ι → Prop} {len : ι → Nat} (hpos : ∀ i, adm i → 1 ≤ len i) {f g : ι → Nat}49    (hf : PolyIn adm len f) (hg : PolyIn adm len g) : PolyIn adm len (fun i => f i + g i) := by50  obtain ⟨c1, k1, h1⟩ := hf51  obtain ⟨c2, k2, h2⟩ := hg52  refine ⟨c1 + c2, max k1 k2, fun i hi => ?_⟩53  have p1 : len i ^ k1 ≤ len i ^ max k1 k2 := Nat.pow_le_pow_right (hpos i hi) (Nat.le_max_left _ _)54  have p2 : len i ^ k2 ≤ len i ^ max k1 k2 := Nat.pow_le_pow_right (hpos i hi) (Nat.le_max_right _ _)55  have := h1 i hi56  have := h2 i hi57  have := Nat.mul_le_mul_left c1 p158  have := Nat.mul_le_mul_left c2 p259  show f i + g i ≤ (c1 + c2) * len i ^ max k1 k260  rw [Nat.add_mul]61  omega6263theorem polyIn_mul {adm : ι → Prop} {len : ι → Nat} {f g : ι → Nat}64    (hf : PolyIn adm len f) (hg : PolyIn adm len g) : PolyIn adm len (fun i => f i * g i) := by65  obtain ⟨c1, k1, h1⟩ := hf66  obtain ⟨c2, k2, h2⟩ := hg67  refine ⟨c1 * c2, k1 + k2, fun i hi => ?_⟩68  calc f i * g i ≤ (c1 * len i ^ k1) * (c2 * len i ^ k2) := Nat.mul_le_mul (h1 i hi) (h2 i hi)69    _ = c1 * c2 * len i ^ (k1 + k2) := by rw [Nat.mul_mul_mul_comm, Nat.pow_add]7071theorem polyIn_pow {adm : ι → Prop} {len : ι → Nat} (m : Nat) {f : ι → Nat}72    (hf : PolyIn adm len f) : PolyIn adm len (fun i => f i ^ m) := by73  obtain ⟨c, k, h⟩ := hf74  refine ⟨c ^ m, k * m, fun i hi => ?_⟩75  calc f i ^ m ≤ (c * len i ^ k) ^ m := Nat.pow_le_pow_left (h i hi) m76    _ = c ^ m * len i ^ (k * m) := by rw [Nat.mul_pow, Nat.pow_mul]7778theorem polyIn_mono {adm : ι → Prop} {len : ι → Nat} {f g : ι → Nat} (h : ∀ i, adm i → f i ≤ g i)79    (hg : PolyIn adm len g) : PolyIn adm len f := by80  obtain ⟨c, k, hk⟩ := hg81  exact ⟨c, k, fun i hi => Nat.le_trans (h i hi) (hk i hi)⟩8283/-! Polynomial expressions by reflection (leaves are functions bounded by len). -/8485inductive PE (ι : Type) where86  | c : Nat → PE ι87  | v : Nat → PE ι88  | add : PE ι → PE ι → PE ι89  | mul : PE ι → PE ι → PE ι90  | pow : PE ι → Nat → PE ι9192instance : Add (PE ι) := ⟨PE.add⟩93instance : Mul (PE ι) := ⟨PE.mul⟩94instance : Pow (PE ι) Nat := ⟨PE.pow⟩95instance (n : Nat) : OfNat (PE ι) n := ⟨PE.c n⟩9697def PE.eval (L : Nat → ι → Nat) : PE ι → ι → Nat98  | .c a, _ => a99  | .v k, i => L k i100  | .add a b, i => PE.eval L a i + PE.eval L b i101  | .mul a b, i => PE.eval L a i * PE.eval L b i102  | .pow a m, i => PE.eval L a i ^ m103104/-- Every polynomial expression whose leaves are bounded by len is PolyIn. -/105theorem PE.poly {adm : ι → Prop} {len : ι → Nat} (hpos : ∀ i, adm i → 1 ≤ len i) (L : Nat → ι → Nat)106    (hL : ∀ k i, adm i → L k i ≤ len i) : ∀ e : PE ι, PolyIn adm len (PE.eval L e)107  | .c a => polyIn_const adm len a108  | .v k => polyIn_leaf (fun i hi => hL k i hi)109  | .add a b => polyIn_add hpos (PE.poly hpos L hL a) (PE.poly hpos L hL b)110  | .mul a b => polyIn_mul (PE.poly hpos L hL a) (PE.poly hpos L hL b)111  | .pow a m => polyIn_pow m (PE.poly hpos L hL a)112113end Poly114115/-! ## Family certificates -/116117/-- Total formula size of a list of output formulas (no sharing). -/118def tsize (cs : List Circ) : Nat := (cs.map size).sum119120theorem length_le_tsize (cs : List Circ) : cs.length ≤ tsize cs := by121  unfold tsize122  induction cs with123  | nil => simp124  | cons c cs ih => simp only [List.length_cons, List.map_cons, List.sum_cons]; have := Shared.size_pos' c; omega125126/-- AC0 FAMILY CERTIFICATE (nonuniform, multi-output).  For every admissible member:127    the input length is positive, every output formula has depth ≤ d and reads only128    the first len inputs, and the total size of the outputs is ≤ c·len^k with c, k129    independent of the member. -/130structure AC0Fam {ι : Type} (adm : ι → Prop) (len : ι → Nat) (outs : ι → List Circ) (d : Nat) : Prop where131  pos : ∀ i, adm i → 1 ≤ len i132  depth_le : ∀ i, adm i → ∀ c ∈ outs i, depth c ≤ d133  reads : ∀ i, adm i → ∀ c ∈ outs i, maxInput c ≤ len i134  size_poly : PolyIn adm len (fun i => tsize (outs i))135136/-- The number of outputs of an AC0 family is polynomially bounded as well. -/137theorem AC0Fam.outs_poly {ι : Type} {adm : ι → Prop} {len : ι → Nat} {outs : ι → List Circ} {d : Nat}138    (h : AC0Fam adm len outs d) : PolyIn adm len (fun i => (outs i).length) :=139  polyIn_mono (fun i _ => length_le_tsize (outs i)) h.size_poly140141/-- NETWORK FAMILY CERTIFICATE: fixed grid W, at most L layers, valid gates, first layer142    reading only the len inputs, polynomial widths/fan-ins and polynomial gate count. -/143structure NetFam {ι : Type} (adm : ι → Prop) (len : ι → Nat) (net : ι → List Layer) (W L : Nat) : Prop where144  pos : ∀ i, adm i → 1 ≤ len i145  valid : ∀ i, adm i → NetValid W (net i)146  wired : ∀ i, adm i → Wired (len i) (net i)147  layers : ∀ i, adm i → (net i).length ≤ L148  bounded : ∃ c k, ∀ i, adm i → NetBounded (c * len i ^ k) (net i)149  gates : PolyIn adm len (fun i => gateCount (net i))150151/-! ## Network families compile to AC0 families (same networks) -/152153theorem netBounded_mono {M M' : Nat} {ls : List Layer} (h : NetBounded M ls) (hM : M ≤ M') : NetBounded M' ls :=154  fun l hl => ⟨Nat.le_trans (h l hl).1 hM, fun g hg => Nat.le_trans ((h l hl).2 g hg) hM⟩155156/-- NETWORK-TO-AC0 AT FAMILY LEVEL.  If a network family satisfies NetFam with fixed W and157    L, then its first K i outputs (K polynomial) are computed by the compiled formulas158    netFormula W (len i) (net i), which form an AC0 family of depth ≤ 3L reading only the159    len inputs; on unpadded inputs the formulas equal the networks (Wired, nonempty). -/160theorem netFam_ac0 {ι : Type} {adm : ι → Prop} {len : ι → Nat} {net : ι → List Layer} {W L : Nat}161    (h : NetFam adm len net W L) (K : ι → Nat) (hK : PolyIn adm len K) :162    AC0Fam adm len (fun i => (List.range (K i)).map (netFormula W (len i) (net i))) (3 * L) ∧163    (∀ i, adm i → net i ≠ [] → ∀ o (x : Nat → Bool), eval x (netFormula W (len i) (net i) o) = evalNet (net i) x o) := by164  obtain ⟨c, k, hb⟩ := h.bounded165  have spec := fun i (hi : adm i) o => netFormula_spec (len i) (net i) (h.valid i hi) (hb i hi) o166  refine ⟨⟨h.pos, ?_, ?_, ?_⟩, ?_⟩167  · intro i hi c' hc168    obtain ⟨o, _, rfl⟩ := List.mem_map.mp hc169    have := (spec i hi o).2.1; have := h.layers i hi; omega170  · intro i hi c' hc171    obtain ⟨o, _, rfl⟩ := List.mem_map.mp hc172    exact (spec i hi o).2.2.2173  · -- each formula ≤ 2 (2W+3)^L (c len^k + 1)^(W L)174    have hpos := h.pos175    have hone : ∀ i, adm i → ∀ o, size (netFormula W (len i) (net i) o) ≤176        2 * ((2 * W + 3) ^ L * (c * len i ^ k + 1) ^ (W * L)) := by177      intro i hi o178      have h1 := (spec i hi o).2.2.1179      have hl := h.layers i hi180      have e1 : (2 * W + 3) ^ (net i).length ≤ (2 * W + 3) ^ L := Nat.pow_le_pow_right (by omega) hl181      have e2 : (c * len i ^ k + 1) ^ (W * (net i).length) ≤ (c * len i ^ k + 1) ^ (W * L) :=182        Nat.pow_le_pow_right (by omega) (Nat.mul_le_mul_left W hl)183      have := Nat.mul_le_mul e1 e2184      omega185    apply polyIn_mono (g := fun i => K i * (2 * ((2 * W + 3) ^ L * (c * len i ^ k + 1) ^ (W * L))))186    · intro i hi187      unfold tsize188      have := sum_map_le_mem (l := List.range (K i)) (f := fun o => size (netFormula W (len i) (net i) o))189        (g := fun _ => 2 * ((2 * W + 3) ^ L * (c * len i ^ k + 1) ^ (W * L))) (fun o _ => hone i hi o)190      rw [List.map_const', List.sum_replicate_nat, List.length_range] at this191      rw [List.map_map]192      exact this193    · apply polyIn_mul hK194      apply polyIn_mul (polyIn_const _ _ 2)195      apply polyIn_mul (polyIn_const _ _ _)196      apply polyIn_pow197      apply polyIn_add hpos _ (polyIn_const _ _ 1)198      apply polyIn_mul (polyIn_const _ _ c)199      apply polyIn_pow200      exact polyIn_leaf (fun i _ => Nat.le_refl _)201  · intro i hi hne o x202    exact (netFormula_wired (len i) (net i) (h.valid i hi) (hb i hi) (h.wired i hi) o203      (fun he => absurd he hne)).1 x204205/-! ## Index width and parameter bounds -/206207theorem log2_lt_self {N : Nat} (hN : 1 ≤ N) : N.log2 < N :=208  Nat.lt_of_lt_of_le Nat.lt_two_pow_self (Nat.log2_self_le (by omega))209210theorem rIdx_le {N : Nat} (hN : 1 ≤ N) : rIdx N ≤ N := by211  have := log2_lt_self hN; unfold rIdx; omega212213theorem rIdx_width (N : Nat) : N ≤ 2 ^ rIdx N := width_log N214215theorem rIdx_counter (N : Nat) : N < 2 ^ rIdx N := Nat.lt_log2_self216217/-- The output list of a binary selector has exactly 1 + r + B formulas and total size218    equal to `PriorityEncoder.totalSize`. -/219theorem tsize_bForms (S : BCirc) : tsize (bForms S) = PriorityEncoder.totalSize S := by220  simp [tsize, bForms, PriorityEncoder.totalSize, List.sum_append_nat]221  omega222223theorem bForms_mem {S : BCirc} {N B r D Sz M : Nat} (h : BinBound S N B r D Sz M) :224    ∀ c ∈ bForms S, depth c ≤ D ∧ size c ≤ Sz ∧ maxInput c ≤ M := fun c hc => h.all c hc225226/-- Generic certificate assembly for binary selectors with a BinBound. -/227theorem bin_cert {ι : Type} {adm : ι → Prop} {len : ι → Nat} {S : ι → BCirc}228    {N B r D Sz M : ι → Nat} {d : Nat}229    (hpos : ∀ i, adm i → 1 ≤ len i) (hb : ∀ i, adm i → BinBound (S i) (N i) (B i) (r i) (D i) (Sz i) (M i))230    (hD : ∀ i, adm i → D i ≤ d) (hM : ∀ i, adm i → M i ≤ len i)231    (hsize : PolyIn adm len (fun i => (1 + r i + B i) * Sz i)) :232    AC0Fam adm len (fun i => bForms (S i)) d := by233  refine ⟨hpos, fun i hi c hc => ?_, fun i hi c hc => ?_, ?_⟩234  · have := (bForms_mem (hb i hi) c hc).1; have := hD i hi; omega235  · have := (bForms_mem (hb i hi) c hc).2.2; have := hM i hi; omega236  · exact polyIn_mono (fun i hi => by rw [tsize_bForms]; exact PriorityEncoder.totalSize_le (hb i hi)) hsize237238theorem wired_mono {n n' : Nat} {ls : List Layer} (h : Wired n ls) (hn : n ≤ n') : Wired n' ls := by239  cases ls with240  | nil => trivial241  | cons l _ => exact fun g hg => Nat.le_trans (h g hg) hn242243/-- Generic network certificate for compiled binary selectors. -/244theorem binNet_cert {ι : Type} {adm : ι → Prop} {len : ι → Nat} {S : ι → BCirc}245    {N B r D Sz M : ι → Nat} {L : Nat}246    (hpos : ∀ i, adm i → 1 ≤ len i) (hb : ∀ i, adm i → BinBound (S i) (N i) (B i) (r i) (D i) (Sz i) (M i))247    (hD : ∀ i, adm i → 2 * D i + 2 ≤ L) (hM : ∀ i, adm i → M i ≤ len i)248    (hbd : ∃ c k, ∀ i, adm i → (1 + r i + B i) * Sz i + M i ≤ c * len i ^ k)249    (hg : PolyIn adm len (fun i => (2 * D i + 1) * ((1 + r i + B i) * Sz i) + (1 + r i + B i))) :250    NetFam adm len (fun i => binNet (S i)) 1 L := by251  refine ⟨hpos, fun i hi => (binNet_res (hb i hi)).1, fun i hi => ?_, fun i hi => ?_, ?_, ?_⟩252  · exact wired_mono (binNet_res (hb i hi)).2.1 (hM i hi)253  · have := (binNet_res (hb i hi)).2.2.1; have := hD i hi; omega254  · obtain ⟨c, k, h⟩ := hbd255    exact ⟨c, k, fun i hi => netBounded_mono (binNet_res (hb i hi)).2.2.2.1 (h i hi)⟩256  · exact polyIn_mono (fun i hi => (binNet_res (hb i hi)).2.2.2.2) hg257258/-- PolyIn from a reflected polynomial expression (pointwise equality by computation). -/259theorem polyE {ι : Type} {adm : ι → Prop} {len : ι → Nat} (hpos : ∀ i, adm i → 1 ≤ len i)260    (L : Nat → ι → Nat) (hL : ∀ k i, adm i → L k i ≤ len i) (e : PE ι) (f : ι → Nat)261    (h : ∀ i, f i = PE.eval L e i) : PolyIn adm len f :=262  polyIn_mono (fun i _ => Nat.le_of_eq (h i)) (PE.poly hpos L hL e)263264/-- Leaves for (B, N)-indexed families: 0 ↦ B, 1 ↦ N, otherwise ↦ r = log₂N + 1. -/265def leafBN : Nat → Nat × Nat → Nat266  | 0, i => i.1267  | 1, i => i.2268  | _, i => rIdx i.2269270/-- Leaves for (B, (N, j))-indexed families. -/271def leafBNj : Nat → Nat × (Nat × Nat) → Nat272  | 0, i => i.1273  | 1, i => i.2.1274  | _, i => rIdx i.2.1275276def vB {ι : Type} : PE ι := PE.v 0277def vN {ι : Type} : PE ι := PE.v 1278def vr {ι : Type} : PE ι := PE.v 2279280/-! ## (i) Two-frame restoration: formulas and network -/281282def restAdm : Nat × Nat → Prop := fun i => 1 ≤ i.1 ∧ 1 ≤ i.2283/-- Supplied input: the two frames, 2·B·N bits. -/284def restLen : Nat × Nat → Nat := fun i => 2 * (i.1 * i.2)285def restS (i : Nat × Nat) : BCirc := restBin i.1 i.2 (rIdx i.2)286287theorem restLen_pos (i : Nat × Nat) (hi : restAdm i) : 1 ≤ restLen i := by288  have := Nat.mul_le_mul hi.1 hi.2; unfold restLen; omega289theorem rest_B (i : Nat × Nat) (hi : restAdm i) : i.1 ≤ restLen i := by290  have := Nat.mul_le_mul_left i.1 hi.2; unfold restLen; simp at this; omega291theorem rest_N (i : Nat × Nat) (hi : restAdm i) : i.2 ≤ restLen i := by292  have := Nat.mul_le_mul_right i.2 hi.1; unfold restLen; simp at this; omega293theorem rest_leaves (k : Nat) (i : Nat × Nat) (hi : restAdm i) : leafBN k i ≤ restLen i := by294  match k with295  | 0 => exact rest_B i hi296  | 1 => exact rest_N i hi297  | _ + 2 => exact Nat.le_trans (rIdx_le hi.2) (rest_N i hi)298299/-- The size polynomial of the restoration selector (phase 5, restBin_bound). -/300def restSz (B N : Nat) : Nat :=301  4 * ((N + 2) * (12 * ((N + 2) * (B + 2) * (B * (2 * B + 3) + 9 + 2)) ^ 8 * (10 * N + 1 + 1) + 2)) ^ 3302def restSzE {ι : Type} : PE ι :=303  4 * ((vN + 2) * (12 * ((vN + 2) * (vB + 2) * (vB * (2 * vB + 3) + 9 + 2)) ^ 8 * (10 * vN + 1 + 1) + 2)) ^ 3304305theorem rest_bound (i : Nat × Nat) :306    BinBound (restS i) i.2 i.1 (rIdx i.2) 20 (restSz i.1 i.2) (2 * (i.1 * i.2)) :=307  restBin_bound (rIdx_width i.2)308309theorem rest_sizePoly : PolyIn restAdm restLen (fun i => (1 + rIdx i.2 + i.1) * restSz i.1 i.2) :=310  polyE restLen_pos leafBN rest_leaves ((1 + vr + vB) * restSzE) _ (fun _ => rfl)311312/-- TWO-FRAME FORMULA FAMILY CERTIFICATE (depth ≤ 20, total size polynomial in 2BN,313    reading only the two frames). -/314theorem rest_ac0 : AC0Fam restAdm restLen (fun i => bForms (restS i)) 20 :=315  bin_cert restLen_pos (fun i _ => rest_bound i) (fun _ _ => Nat.le_refl _)316    (fun i _ => Nat.le_refl _) rest_sizePoly317318def restN (i : Nat × Nat) : List Layer := restNet i.1 i.2 (rIdx i.2)319320/-- TWO-FRAME NETWORK FAMILY CERTIFICATE (W = 1, ≤ 42 layers, polynomial widths/gates). -/321theorem rest_net : NetFam restAdm restLen restN 1 42 :=322  binNet_cert (S := restS) restLen_pos (fun i _ => rest_bound i) (fun _ _ => by omega)323    (fun i _ => Nat.le_refl _)324    (polyE restLen_pos leafBN rest_leaves ((1 + vr + vB) * restSzE + 2 * (vB * vN)) _ (fun _ => rfl))325    (polyE restLen_pos leafBN rest_leaves ((2 * 20 + 1) * ((1 + vr + vB) * restSzE) + (1 + vr + vB)) _326      (fun _ => rfl))327328/-- Semantics of the SAME objects on the promised domain (previous nim-sum zero, legal329    transition): formulas and network output the restoring binary move. -/330theorem rest_semantics {B N : Nat} {Q Q' : List Nat} (hQ : Q.length = N) (hQ' : Q'.length = N)331    (hw : Width B Q) (hw' : Width B Q') (h0 : nimSum Q = 0) (hm : Move Q Q') :332    ∃ i v, binSem (restS (B, N)) N (LocalRestore.tf B N Q Q') = some (i, v) ∧333      netBinSem (restN (B, N)) N (rIdx N) B (LocalRestore.tf B N Q Q') = some (i, v) ∧334      restore Q Q' = some (Q'.set i v) ∧ Move Q' (Q'.set i v) ∧ nimSum (Q'.set i v) = 0 := by335  obtain ⟨i, v, h1, h2, h3, h4⟩ := restBin_correct (rIdx_width N) hQ hQ' hw hw' h0 hm336  have hb := restBin_bound (B := B) (N := N) (rIdx_width N)337  refine ⟨i, v, h1, ?_, h2, h3, h4⟩338  show netBinSem (binNet (restBin B N (rIdx N))) N (rIdx N) B (LocalRestore.tf B N Q Q') = some (i, v)339  rw [binNet_correct _ hb.idx_len hb.val_len]340  exact h1341342/-! ## (ii) Multi-head: one policy step and the outcome-conditioned readout -/343344/-- Policy members are indexed by (B, (N, j)). -/345def polAdm : Nat × (Nat × Nat) → Prop := fun i => 1 ≤ i.1 ∧ 1 ≤ i.2.1 ∧ i.2.2 < i.1346def polLen : Nat × (Nat × Nat) → Nat := fun i => i.1 * i.2.1347def polS (i : Nat × (Nat × Nat)) : BCirc := polBin i.1 i.2.1 i.2.2 (rIdx i.2.1)348349def polSz (B N : Nat) : Nat := 4 * ((N + 2) * (12 * ((N + 2) * (B + 2) * (4 * B + 9 + 2)) ^ 8 + 2)) ^ 3350def polSzE {ι : Type} : PE ι := 4 * ((vN + 2) * (12 * ((vN + 2) * (vB + 2) * (4 * vB + 9 + 2)) ^ 8 + 2)) ^ 3351352theorem polLen_pos (i : Nat × (Nat × Nat)) (hi : polAdm i) : 1 ≤ polLen i := by353  have := Nat.mul_le_mul hi.1 hi.2.1; unfold polLen; omega354theorem pol_B (i : Nat × (Nat × Nat)) (hi : polAdm i) : i.1 ≤ polLen i := by355  have := Nat.mul_le_mul_left i.1 hi.2.1; unfold polLen; simpa using this356theorem pol_N (i : Nat × (Nat × Nat)) (hi : polAdm i) : i.2.1 ≤ polLen i := by357  have := Nat.mul_le_mul_right i.2.1 hi.1; unfold polLen; simpa using this358theorem pol_leaves (k : Nat) (i : Nat × (Nat × Nat)) (hi : polAdm i) : leafBNj k i ≤ polLen i := by359  match k with360  | 0 => exact pol_B i hi361  | 1 => exact pol_N i hi362  | _ + 2 => exact Nat.le_trans (rIdx_le hi.2.1) (pol_N i hi)363364theorem pol_bound (i : Nat × (Nat × Nat)) :365    BinBound (polS i) i.2.1 i.1 (rIdx i.2.1) 17 (polSz i.1 i.2.1) (i.1 * i.2.1) :=366  polBin_bound (rIdx_width i.2.1)367368theorem pol_sizePoly : PolyIn polAdm polLen (fun i => (1 + rIdx i.2.1 + i.1) * polSz i.1 i.2.1) :=369  polyE polLen_pos leafBNj pol_leaves ((1 + vr + vB) * polSzE) _ (fun _ => rfl)370371/-- ONE STRUCTURED POLICY STEP: formula family certificate (depth ≤ 17, input B·N). -/372theorem pol_ac0 : AC0Fam polAdm polLen (fun i => bForms (polS i)) 17 :=373  bin_cert polLen_pos (fun i _ => pol_bound i) (fun _ _ => Nat.le_refl _) (fun _ _ => Nat.le_refl _)374    pol_sizePoly375376def polN (i : Nat × (Nat × Nat)) : List Layer := polNet i.1 i.2.1 i.2.2 (rIdx i.2.1)377378theorem pol_net : NetFam polAdm polLen polN 1 36 :=379  binNet_cert (S := polS) polLen_pos (fun i _ => pol_bound i) (fun _ _ => by omega) (fun _ _ => Nat.le_refl _)380    (polyE polLen_pos leafBNj pol_leaves ((1 + vr + vB) * polSzE + vB * vN) _ (fun _ => rfl))381    (polyE polLen_pos leafBNj pol_leaves ((2 * 17 + 1) * ((1 + vr + vB) * polSzE) + (1 + vr + vB)) _382      (fun _ => rfl))383384theorem pol_semantics {B N j : Nat} {P : List Nat} (hP : P.length = N) (hw : Width B P) :385    binSem (polS (B, N, j)) N (boardBits B P) = policyIdx j P ∧386    applyM P (netBinSem (polN (B, N, j)) N (rIdx N) B (boardBits B P)) = policyStep j P := by387  refine ⟨(polBin_correct (rIdx_width N) hP hw).1, ?_⟩388  exact polNet_correct (rIdx_width N) hP hw389390/-- Readout members (board plus B outcome wires). -/391def mhAdm : Nat × Nat → Prop := restAdm392def mhLen : Nat × Nat → Nat := fun i => i.1 * i.2 + i.1393def mhS (i : Nat × Nat) : BCirc := mhBin i.1 i.2 (rIdx i.2)394395def mhSz (B N : Nat) : Nat :=396  4 * ((N + 2) * (12 * ((N + 2) * (B + 2) * (B * (2 * B + 3) + 9 + 2)) ^ 8 * (9 + 1) + 2)) ^ 3397def mhSzE {ι : Type} : PE ι :=398  4 * ((vN + 2) * (12 * ((vN + 2) * (vB + 2) * (vB * (2 * vB + 3) + 9 + 2)) ^ 8 * (9 + 1) + 2)) ^ 3399400theorem mhLen_pos (i : Nat × Nat) (hi : mhAdm i) : 1 ≤ mhLen i := by401  have := hi.1; unfold mhLen; omega402theorem mh_B (i : Nat × Nat) (_hi : mhAdm i) : i.1 ≤ mhLen i := by unfold mhLen; omega403theorem mh_N (i : Nat × Nat) (hi : mhAdm i) : i.2 ≤ mhLen i := by404  have := Nat.mul_le_mul_right i.2 hi.1; unfold mhLen; simp at this; omega405theorem mh_leaves (k : Nat) (i : Nat × Nat) (hi : mhAdm i) : leafBN k i ≤ mhLen i := by406  match k with407  | 0 => exact mh_B i hi408  | 1 => exact mh_N i hi409  | _ + 2 => exact Nat.le_trans (rIdx_le hi.2) (mh_N i hi)410411theorem mh_bound (i : Nat × Nat) :412    BinBound (mhS i) i.2 i.1 (rIdx i.2) 19 (mhSz i.1 i.2) (i.1 * i.2 + i.1) :=413  mhBin_bound (rIdx_width i.2)414415theorem mh_sizePoly : PolyIn mhAdm mhLen (fun i => (1 + rIdx i.2 + i.1) * mhSz i.1 i.2) :=416  polyE mhLen_pos leafBN mh_leaves ((1 + vr + vB) * mhSzE) _ (fun _ => rfl)417418/-- OUTCOME-CONDITIONED READOUT: formula family certificate (depth ≤ 19, input B·N + B). -/419theorem mh_ac0 : AC0Fam mhAdm mhLen (fun i => bForms (mhS i)) 19 :=420  bin_cert mhLen_pos (fun i _ => mh_bound i) (fun _ _ => Nat.le_refl _) (fun _ _ => Nat.le_refl _) mh_sizePoly421422def mhN (i : Nat × Nat) : List Layer := mhNet i.1 i.2 (rIdx i.2)423424theorem mh_net : NetFam mhAdm mhLen mhN 1 40 :=425  binNet_cert (S := mhS) mhLen_pos (fun i _ => mh_bound i) (fun _ _ => by omega) (fun _ _ => Nat.le_refl _)426    (polyE mhLen_pos leafBN mh_leaves ((1 + vr + vB) * mhSzE + (vB * vN + vB)) _ (fun _ => rfl))427    (polyE mhLen_pos leafBN mh_leaves ((2 * 19 + 1) * ((1 + vr + vB) * mhSzE) + (1 + vr + vB)) _428      (fun _ => rfl))429430/-- Readout semantics for ARBITRARY outcome wires o (reconstruction then selection), and431    for executed outcomes; formulas and network agree. -/432theorem mh_semantics {B N : Nat} {P : List Nat} (hP : P.length = N) (hw : Width B P) (o : Nat → Bool) :433    binSem (mhS (B, N)) N (obsIn B N P o) = attainT (reconstruct B o) P ∧434    netBinSem (mhN (B, N)) N (rIdx N) B (obsIn B N P o) = attainT (reconstruct B o) P ∧435    netBinSem (mhN (B, N)) N (rIdx N) B (obsIn B N P (outcomes P)) = decisionMove P := by436  have hb := mhBin_bound (B := B) (N := N) (rIdx_width N)437  have h1 := mhBin_correct (rIdx_width N) hP hw o438  refine ⟨h1, ?_, mhNet_correct (rIdx_width N) hP hw⟩439  show netBinSem (binNet (mhBin B N (rIdx N))) N (rIdx N) B (obsIn B N P o) = attainT (reconstruct B o) P440  rw [binNet_correct _ hb.idx_len hb.val_len]441  exact h1442443/-! ## (iii) Recurrent controller: one update (state plus one token) -/444445def ctrlAdm : Nat × Nat → Prop := restAdm446/-- Per-update input: state (4 + 5B + 3r bits) plus one token (2 + B bits), r = log₂N + 1. -/447def ctrlLen : Nat × Nat → Nat := fun i => inWidth i.1 (rIdx i.2)448def ctrlF (i : Nat × Nat) : List Circ := ctrlForms i.1 (rIdx i.2)449450theorem ctrl_widths (B N : Nat) :451    inWidth B (rIdx N) = stateWidth B (rIdx N) + (2 + B) ∧452    (ctrlForms B (rIdx N)).length = stateWidth B (rIdx N) + outCount B (rIdx N) ∧453    stateWidth B (rIdx N) = 7 + 5 * B + 3 * N.log2 ∧ outCount B (rIdx N) = 5 + 3 * B + N.log2 ∧454    N < 2 ^ rIdx N := by455  refine ⟨by simp [inWidth, stateWidth]; omega, ctrlForms_length _ _, (counter_width (B := B) N).2,456    by simp [outCount, rIdx]; omega, rIdx_counter N⟩457458/-- Leaves for the controller: 0 ↦ B, otherwise ↦ r = log₂N + 1 (N itself is not a leaf:459    the per-update width is logarithmic in N). -/460def leafBr : Nat → Nat × Nat → Nat461  | 0, i => i.1462  | _, i => rIdx i.2463464def vR {ι : Type} : PE ι := PE.v 1465466theorem ctrlLen_pos (i : Nat × Nat) (_hi : ctrlAdm i) : 1 ≤ ctrlLen i := by unfold ctrlLen inWidth; omega467theorem ctrl_leaves (k : Nat) (i : Nat × Nat) (_hi : ctrlAdm i) : leafBr k i ≤ ctrlLen i := by468  match k with469  | 0 => show i.1 ≤ inWidth i.1 (rIdx i.2); unfold inWidth; omega470  | _ + 1 => show rIdx i.2 ≤ inWidth i.1 (rIdx i.2); unfold inWidth; omega471472def ctrlSzE {ι : Type} : PE ι :=473  ((4 + 5 * vB + 3 * vR) + (4 + 3 * vB + vR)) * (((vB * (2 * vB + 3) + 1) + 5 * vB + 2 * vR + 40) + 16)474475/-- RECURRENT UPDATE: formula family certificate (depth ≤ 8, input = state + token,476    total size polynomial in that width, hence in B + log N). -/477theorem ctrl_ac0 : AC0Fam ctrlAdm ctrlLen ctrlF 8 := by478  refine ⟨ctrlLen_pos, fun i _ c hc => (ctrlForms_res _ _ c hc).1, fun i _ c hc => (ctrlForms_res _ _ c hc).2.2, ?_⟩479  exact polyIn_mono (fun i _ => ctrlForms_size _ _) (polyE ctrlLen_pos leafBr ctrl_leaves ctrlSzE _ (fun _ => rfl))480481def ctrlN (i : Nat × Nat) : List Layer := ctrlNet i.1 (rIdx i.2)482483theorem ctrl_net : NetFam ctrlAdm ctrlLen ctrlN 1 18 := by484  refine ⟨ctrlLen_pos, fun i _ => (ctrlNet_res _ _).1, fun i _ => (ctrlNet_res _ _).2.1,485    fun i _ => (ctrlNet_res _ _).2.2.1, ?_, ?_⟩486  · obtain ⟨c, k, h⟩ := polyE ctrlLen_pos leafBr ctrl_leaves (ctrlSzE + (6 + 6 * vB + 3 * vR))487      (fun i => (stateWidth i.1 (rIdx i.2) + outCount i.1 (rIdx i.2)) * (cellSize i.1 (rIdx i.2) + 16) +488        inWidth i.1 (rIdx i.2)) (fun _ => rfl)489    refine ⟨c, k, fun i hi => netBounded_mono (ctrlNet_res _ _).2.2.2.1 ?_⟩490    have h5 := (ctrlNet_res i.1 (rIdx i.2)).2.2.2.2.2491    have h6 := h i hi492    dsimp only at h6493    unfold ctrlLen at h6 ⊢; omega494  · refine polyIn_mono (fun i _ => ?_) (polyE ctrlLen_pos leafBr ctrl_leaves495      (17 * ctrlSzE + ((4 + 5 * vB + 3 * vR) + (4 + 3 * vB + vR)))496      (fun i => 17 * ((stateWidth i.1 (rIdx i.2) + outCount i.1 (rIdx i.2)) * (cellSize i.1 (rIdx i.2) + 16)) +497        (stateWidth i.1 (rIdx i.2) + outCount i.1 (rIdx i.2))) (fun _ => rfl))498    have h1 := (ctrlNet_res i.1 (rIdx i.2)).2.2.2.2.1499    have h3 := (ctrlNet_res i.1 (rIdx i.2)).2.2.2.2.2500    have := Nat.mul_le_mul_left 17 h3501    show gateCount (ctrlNet i.1 (rIdx i.2)) ≤ _502    omega503504/-- Semantics of the SAME update formulas/network: for EVERY state vector v and token t,505    the formulas give the bit-level update bstep, and the network equals it. -/506theorem ctrl_semantics (B N : Nat) (v : Nat → Bool) (t : Tok) :507    (∀ k (hk : k < stateWidth B (rIdx N)),508      eval (inp B (rIdx N) v t) ((ctrlF (B, N))[k]'(by509        show k < (ctrlForms B (rIdx N)).length; rw [ctrlForms_length]; omega)) =510        (bstep B (rIdx N) v t).1 k) ∧511    tstep B (rIdx N) v t = bstep B (rIdx N) v t := by512  refine ⟨fun k hk => ?_, tstep_eq _ _ v t⟩513  simp only [ctrlF]514  rw [ctrlForms_get, if_pos hk]515  rfl516517/-! ## Axiom audit -/518519#print axioms polyIn_const520#print axioms polyIn_leaf521#print axioms polyIn_add522#print axioms polyIn_mul523#print axioms polyIn_pow524#print axioms polyIn_mono525#print axioms PE.poly526#print axioms length_le_tsize527#print axioms AC0Fam.outs_poly528#print axioms netBounded_mono529#print axioms netFam_ac0530#print axioms log2_lt_self531#print axioms rIdx_le532#print axioms rIdx_width533#print axioms rIdx_counter534#print axioms tsize_bForms535#print axioms bForms_mem536#print axioms bin_cert537#print axioms wired_mono538#print axioms binNet_cert539#print axioms polyE540#print axioms restLen_pos541#print axioms rest_B542#print axioms rest_N543#print axioms rest_leaves544#print axioms rest_bound545#print axioms rest_sizePoly546#print axioms rest_ac0547#print axioms rest_net548#print axioms rest_semantics549#print axioms polLen_pos550#print axioms pol_B551#print axioms pol_N552#print axioms pol_leaves553#print axioms pol_bound554#print axioms pol_sizePoly555#print axioms pol_ac0556#print axioms pol_net557#print axioms pol_semantics558#print axioms mhLen_pos559#print axioms mh_B560#print axioms mh_N561#print axioms mh_leaves562#print axioms mh_bound563#print axioms mh_sizePoly564#print axioms mh_ac0565#print axioms mh_net566#print axioms mh_semantics567#print axioms ctrl_widths568#print axioms ctrlLen_pos569#print axioms ctrl_leaves570#print axioms ctrl_ac0571#print axioms ctrl_net572#print axioms ctrl_semantics573574