Windows

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 Bypass23/- Phase 6, Priority 3c: the remaining parts of Theorem thm:sim-ac0 and two small local4   claims.  Written by Claude (10 October 2026).  Lean 4.26.0, core/Std only.56   * FIXED MULTI-STATE RECURRENCE WINDOWS (Definition def:RNN-formal): an update may read7     the current input block and the w most recent states (input-independent initial8     states before time 0).  T updates unroll to formulas of depth ≤ 3·L·T, size ≤9     rnnSize W M L T + 1 ≤ 2·((2W+3)^L (M+1)^{WL})^T, reading only the T input blocks.  For10     constant T (and W, L) and polynomial M this is an AC0 family.11   * GATE-REALISED ATTENTION-STYLE COMPOSITION (Definition def:LTST-formal): a model given12     as a constant number K of stages (score computation, coefficient selection,13     aggregation, over the T window positions), EACH realised by a valid fixed-scale gate14     network, is one network (layers concatenated); the simulation theorem applies.  No15     claim about standard softmax attention is made.  A finite coefficient set alone is16     not the model's premise: the {0,1}-coefficient majority gate violates the bounded17     threshold premise for every fixed W once the fan-in exceeds 2W.18   * Remark rem:local-vs-global-parity: XOR of a constant number of formulas (e.g. of t19     B-bit blocks, bitwise) has constant depth and constant-factor size.20   * The literal-representation remark of Section 2: s − a·x ≥ θ ⇔ s + a(1−x) ≥ θ + a. -/2122namespace NimAudit23namespace Windows2425open AC0 AC0.Circ FiniteNet Family2627/-! ## Fixed recurrence windows -/2829/-- Update input layout: the current block (n bits), then the w most recent states30    (m bits each, most recent first); zero elsewhere. -/31def winIn (n m w : Nat) (x : Nat → Bool) (hs : Nat → Nat → Bool) : Nat → Bool := fun j =>32  if j < n then x j else if j < n + w * m then hs ((j - n) / m) ((j - n) % m) else false3334/-- State after t updates (h0 before time 0 and as the initial state). -/35def wState (cell : List Layer) (n m w : Nat) (h0 : Nat → Bool) (x : Nat → Bool) : Nat → Nat → Bool36  | 0 => h037  | t + 1 => evalNet cell (winIn n m w (fun j => x (t * n + j))38      (fun δ => if δ ≤ t then wState cell n m w h0 x (t - δ) else h0))39termination_by t => t40decreasing_by exact Nat.lt_succ_of_le (Nat.sub_le _ _)4142/-- The unrolled formulas. -/43def wCirc (W : Nat) (cell : List Layer) (n m w : Nat) (h0 : Nat → Bool) : Nat → Nat → Circ44  | 0 => fun i => const (h0 i)45  | t + 1 => compileNet W cell (fun j => if j < n then input (t * n + j) else if j < n + w * m then46      (if (j - n) / m ≤ t then wCirc W cell n m w h0 (t - (j - n) / m) ((j - n) % m) else const (h0 ((j - n) % m)))47      else const false)48termination_by t => t49decreasing_by exact Nat.lt_succ_of_le (Nat.sub_le _ _)5051theorem wState_succ (cell : List Layer) (n m w : Nat) (h0 x : Nat → Bool) (t : Nat) :52    wState cell n m w h0 x (t + 1) = evalNet cell (winIn n m w (fun j => x (t * n + j))53      (fun δ => if δ ≤ t then wState cell n m w h0 x (t - δ) else h0)) := wState.eq_2 cell n m w h0 x t5455theorem wCirc_succ (W : Nat) (cell : List Layer) (n m w : Nat) (h0 : Nat → Bool) (t : Nat) :56    wCirc W cell n m w h0 (t + 1) = compileNet W cell (fun j => if j < n then input (t * n + j) else if j < n + w * m then57      (if (j - n) / m ≤ t then wCirc W cell n m w h0 (t - (j - n) / m) ((j - n) % m) else const (h0 ((j - n) % m)))58      else const false) := wCirc.eq_2 W cell n m w h0 t5960theorem sizeBound_ge (W M S L : Nat) : S ≤ sizeBound W M S L := by61  induction L with62  | zero => simp [sizeBound]63  | succ L ih =>64    simp only [sizeBound]65    have : 1 ≤ gfac W M := by unfold gfac; omega66    have := Nat.le_mul_of_pos_left (sizeBound W M S L + 1) (show 0 < gfac W M by omega)67    omega6869theorem rnnSize_mono (W M L : Nat) {t t' : Nat} (h : t ≤ t') : rnnSize W M L t ≤ rnnSize W M L t' := by70  induction t' with71  | zero => have : t = 0 := by omega72            subst this; exact Nat.le_refl _73  | succ t' ih =>74    rcases Nat.lt_or_ge t (t' + 1) with h1 | h175    · exact Nat.le_trans (ih (by omega)) (by simp only [rnnSize]; exact sizeBound_ge W M _ L)76    · have : t = t' + 1 := by omega77      subst this; exact Nat.le_refl _7879/-- WINDOW SIMULATION THEOREM.  For a valid L-layer cell with fan-ins/widths ≤ M reading80    the input block and the w most recent states, the state after T updates is computed by81    formulas with depth ≤ 3·L·T, size ≤ rnnSize W M L T, reading only the T input blocks. -/82theorem window_ac0 {W M : Nat} (cell : List Layer) (hv : NetValid W cell) (hb : NetBounded M cell)83    (n m w : Nat) (h0 : Nat → Bool) : ∀ T i,84    (∀ x : Nat → Bool, eval x (wCirc W cell n m w h0 T i) = wState cell n m w h0 x T i) ∧85    size (wCirc W cell n m w h0 T i) ≤ rnnSize W M cell.length T ∧86    depth (wCirc W cell n m w h0 T i) ≤ 3 * cell.length * T ∧87    maxInput (wCirc W cell n m w h0 T i) ≤ T * n := by88  intro T89  induction T using Nat.strongRecOn with90  | ind T ih =>91    intro i92    cases T with93    | zero => simp [wCirc.eq_1, wState.eq_1, rnnSize]94    | succ t =>95      -- the leaves of the last update96      let prev : Nat → Circ := fun j => if j < n then input (t * n + j) else if j < n + w * m then97        (if (j - n) / m ≤ t then wCirc W cell n m w h0 (t - (j - n) / m) ((j - n) % m) else const (h0 ((j - n) % m)))98        else const false99      have hprev : ∀ j, size (prev j) ≤ rnnSize W M cell.length t ∧ depth (prev j) ≤ 3 * cell.length * t ∧100          maxInput (prev j) ≤ (t + 1) * n := by101        intro j102        simp only [prev]103        split104        · simp; refine ⟨rnnSize_pos _ _ _ _, ?_⟩; rw [Nat.succ_mul]; omega105        · split106          · split107            · next hδ =>108              have hlt : t - (j - n) / m < t + 1 := Nat.lt_succ_of_le (Nat.sub_le _ _)109              have hle : t - (j - n) / m ≤ t := Nat.sub_le _ _110              obtain ⟨_, h2, h3, h4⟩ := ih (t - (j - n) / m) hlt ((j - n) % m)111              refine ⟨Nat.le_trans h2 (rnnSize_mono W M _ hle), Nat.le_trans h3 (Nat.mul_le_mul_left _ hle),112                Nat.le_trans h4 ?_⟩113              rw [Nat.succ_mul]; exact Nat.le_trans (Nat.mul_le_mul_right n hle) (Nat.le_add_right _ _)114            · simp; exact rnnSize_pos _ _ _ _115          · simp; exact rnnSize_pos _ _ _ _116      have hsd := compileNet_sd (W := W) cell hb prev (rnnSize W M cell.length t) (3 * cell.length * t)117        (fun j => (hprev j).1) (fun j => (hprev j).2.1) i118      have hmx := compileNet_max (W := W) cell prev ((t + 1) * n) (fun j => (hprev j).2.2) i119      refine ⟨fun x => ?_, ?_, ?_, ?_⟩120      · rw [wCirc_succ, wState_succ, eval_compileNet cell hv]121        congr 1122        funext j123        unfold winIn124        split125        · simp126        · split127          · split128            · next hδ => simp only [if_pos hδ]; exact (ih (t - (j - n) / m) (Nat.lt_succ_of_le (Nat.sub_le _ _)) ((j - n) % m)).1 x129            · next hδ => simp [hδ]130          · simp131      · rw [wCirc_succ]; simp only [rnnSize]; exact hsd.1132      · rw [wCirc_succ]; have := hsd.2; rw [Nat.mul_succ]; omega133      · rw [wCirc_succ]; exact hmx134135/-- Closed polynomial size bound for a fixed number T of updates. -/136theorem window_size_closed (W M L T : Nat) :137    rnnSize W M L T + 1 ≤ 2 * ((2 * W + 3) ^ L * (M + 1) ^ (W * L)) ^ T := rnnSize_closed W M L T138139/-! ## Gate-realised attention-style composition -/140141theorem evalNet_append (ls1 ls2 : List Layer) (x : Nat → Bool) :142    evalNet (ls1 ++ ls2) x = evalNet ls2 (evalNet ls1 x) := by143  induction ls1 generalizing x with144  | nil => rfl145  | cons l ls ih => simp only [List.cons_append, evalNet]; exact ih _146147/-- Staged evaluation: stages applied in order. -/148def runStages : List (List Layer) → (Nat → Bool) → (Nat → Bool)149  | [], x => x150  | st :: sts, x => runStages sts (evalNet st x)151152theorem evalNet_flatten (sts : List (List Layer)) (x : Nat → Bool) : evalNet sts.flatten x = runStages sts x := by153  induction sts generalizing x with154  | nil => rfl155  | cons st sts ih => simp only [List.flatten_cons, evalNet_append, runStages]; exact ih _156157theorem flatten_length_le {sts : List (List Layer)} {L : Nat} (h : ∀ st ∈ sts, st.length ≤ L) :158    sts.flatten.length ≤ sts.length * L := by159  induction sts with160  | nil => simp161  | cons st sts ih =>162    simp only [List.flatten_cons, List.length_append, List.length_cons, Nat.succ_mul]163    have := h st (by simp); have := ih (fun s hs => h s (by simp [hs])); omega164165/-- GATE-REALISED COMPOSITION THEOREM.  If every stage is a W-valid network with at most L166    layers and widths/fan-ins ≤ M, the K-stage model is computed (on zero-extended n-bit167    inputs) by formulas of depth ≤ 3·K·L, size ≤ 2 (2W+3)^{KL} (M+1)^{W·KL}, reading only168    the n inputs; the formulas compute the staged evaluation. -/169theorem staged_ac0 {W M L : Nat} (sts : List (List Layer)) (hv : ∀ st ∈ sts, NetValid W st)170    (hb : ∀ st ∈ sts, NetBounded M st) (hl : ∀ st ∈ sts, st.length ≤ L) (n i : Nat) :171    (∀ x : Nat → Bool, eval x (netFormula W n sts.flatten i) = runStages sts (pad n x) i) ∧172    depth (netFormula W n sts.flatten i) ≤ 3 * (sts.length * L) ∧173    size (netFormula W n sts.flatten i) ≤ 2 * ((2 * W + 3) ^ (sts.length * L) * (M + 1) ^ (W * (sts.length * L))) ∧174    maxInput (netFormula W n sts.flatten i) ≤ n := by175  have hv' : NetValid W sts.flatten := by176    intro l hl' g hg177    obtain ⟨st, hst, hlst⟩ := List.mem_flatten.mp hl'178    exact hv st hst l hlst g hg179  have hb' : NetBounded M sts.flatten := by180    intro l hl'181    obtain ⟨st, hst, hlst⟩ := List.mem_flatten.mp hl'182    exact hb st hst l hlst183  obtain ⟨h1, h2, h3, h4⟩ := netFormula_spec n sts.flatten hv' hb' i184  have hlen := flatten_length_le hl185  refine ⟨fun x => by rw [h1, evalNet_flatten], Nat.le_trans h2 (Nat.mul_le_mul_left 3 hlen), Nat.le_trans h3 ?_, h4⟩186  apply Nat.mul_le_mul_left187  exact Nat.mul_le_mul (Nat.pow_le_pow_right (by omega) hlen)188    (Nat.pow_le_pow_right (by omega) (Nat.mul_le_mul_left W hlen))189190/-- A {0,1}-coefficient majority gate on m inputs (threshold ⌈m/2⌉). -/191def majGate (m : Nat) : Gate := ⟨List.replicate m 1, List.replicate m false, (m + 1) / 2⟩192193/-- Finite coefficients are not enough: the majority gate's threshold exceeds every fixed194    W once m > 2W, so it is outside the fixed-scale model although all its coefficients195    lie in {0,1}. -/196theorem majGate_not_valid (W m : Nat) (hm : 2 * W < m) : ¬ Gate.Valid W (majGate m) := by197  intro h; have := h.1; simp [majGate] at this; omega198199theorem majGate_coeffs (m : Nat) : ∀ a ∈ (majGate m).coeffs, a ≤ 1 := by200  intro a ha; simp [majGate] at ha; omega201202/-! ## Constant-size XOR and the literal remark -/203204/-- XOR of a list of formulas (by repeated two-input XOR). -/205def xorChain : List Circ → Circ206  | [] => const false207  | c :: cs => CorrBridge.xor2 c (xorChain cs)208209theorem xorChain_eval (z : Nat → Bool) : ∀ cs : List Circ, eval z (xorChain cs) = cs.foldr (fun c b => xor (eval z c) b) false210  | [] => by simp [xorChain]211  | c :: cs => by simp [xorChain, CorrBridge.eval_xor2, xorChain_eval z cs]212213/-- XOR of t formulas of depth ≤ d and size ≤ s (s ≥ 1): depth ≤ d + 3t, size ≤ 6^t (s + 1). -/214theorem xorChain_res {d s : Nat} (hs : 1 ≤ s) : ∀ cs : List Circ, (∀ c ∈ cs, depth c ≤ d ∧ size c ≤ s) →215    depth (xorChain cs) ≤ d + 3 * cs.length ∧ size (xorChain cs) ≤ 6 ^ cs.length * (s + 1)216  | [], _ => by simp [xorChain]217  | c :: cs, h => by218    obtain ⟨ih1, ih2⟩ := xorChain_res hs cs (fun c' hc' => h c' (by simp [hc']))219    obtain ⟨hd, hsz⟩ := h c (by simp)220    obtain ⟨x1, x2, _⟩ := RolloutExec.xor2_res c (xorChain cs)221    simp only [xorChain, List.length_cons]222    refine ⟨by omega, ?_⟩223    rw [x2, Nat.pow_succ]224    have hp : 1 ≤ 6 ^ cs.length := Nat.one_le_pow _ _ (by decide)225    have : s + 1 ≤ 6 ^ cs.length * (s + 1) := Nat.le_mul_of_pos_left _ (by omega)226    have e : 6 ^ cs.length * 6 * (s + 1) = 6 * (6 ^ cs.length * (s + 1)) := by227      rw [Nat.mul_comm (6 ^ cs.length) 6, Nat.mul_assoc]228    rw [e]; omega229230/-- Bitwise XOR of t blocks of B bits (block k occupies inputs B·k .. B·k + B − 1). -/231def blockXor (B t q : Nat) : Circ := xorChain ((List.range t).map (fun k => input (B * k + q)))232233theorem blockXor_res (B t q : Nat) : depth (blockXor B t q) ≤ 3 * t ∧ size (blockXor B t q) ≤ 6 ^ t * 2 := by234  have := xorChain_res (d := 0) (s := 1) (by decide) ((List.range t).map (fun k => input (B * k + q)))235    (fun c hc => by obtain ⟨k, _, rfl⟩ := List.mem_map.mp hc; simp)236  simpa [blockXor] using this237238/-- The literal-representation remark: replacing −a·x by a·(1 − x) adds a to the threshold. -/239theorem literal_shift (s a x θ : Int) : (θ ≤ s - a * x) ↔ (θ + a ≤ s + a * (1 - x)) := by240  rw [Int.mul_sub, Int.mul_one]; omega241242/-! ## Axiom audit -/243244#print axioms wState_succ245#print axioms wCirc_succ246#print axioms sizeBound_ge247#print axioms rnnSize_mono248#print axioms window_ac0249#print axioms window_size_closed250#print axioms evalNet_append251#print axioms evalNet_flatten252#print axioms flatten_length_le253#print axioms staged_ac0254#print axioms majGate_not_valid255#print axioms majGate_coeffs256#print axioms xorChain_eval257#print axioms xorChain_res258#print axioms blockXor_res259#print axioms literal_shift260261