/- Copyright (c) 2026 Sovereign Research Stack. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Research Stack Team SSMS.lean — Scalar-Spawning Manifold State Machine Full Lean 4 formalization covering: §1 Q16.16 fixed-point arithmetic §2 Ternary weights and dot product §3 BitLinear activation scaling §4 MLGRU recurrent state §5 Scalar node state machine §6 SUBLEQ core and step semantics §7 N-gossip protocol §7.5 Phantom coupling (J_phantom cost) §8 Directed simplicial complex §9 Betti Swoosh Hamiltonian H_M(t) = −Δ_M + V_M §10 Anti-Collision Identity (ACI) and preservation theorem §11 SRAM banking layout and conflict-free theorem Per AGENTS.md §1.4: All new hot-path code uses Q16_16 fixed-point. Per AGENTS.md §2: All code uses PascalCase for types, camelCase for functions. -/ import Std import Mathlib.Tactic.NormNum import Mathlib.Data.Real.Basic import Mathlib.Tactic import Semantics.Timing namespace Semantics.SSMS -- ════════════════════════════════════════════════════════════ -- §1 Q16.16 Fixed-Point Arithmetic -- raw : Int represents the 32-bit two's-complement word. -- Real value = raw / 65536. Resolution = 2^{-16}. -- ════════════════════════════════════════════════════════════ /-- Q16.16: 32-bit fixed-point. Invariant (unenforced): raw ∈ [-2^31, 2^31 - 1]. -/ structure Q1616 where raw : Int deriving Repr, DecidableEq, Inhabited, BEq namespace Q1616 def zero : Q1616 := ⟨0⟩ def one : Q1616 := ⟨65536⟩ -- 0x00010000 def negOne : Q1616 := ⟨-65536⟩ -- 0xFFFF0000 def two : Q1616 := ⟨131072⟩ -- 0x00020000 def epsilon : Q1616 := ⟨1⟩ -- 2^{-16}, smallest positive /-- Convert Nat to Q16.16 (left-shift by 16). -/ def ofNat (n : Nat) : Q1616 := ⟨n * 65536⟩ /-- SUBLEQ native operation: M[b] ← M[b] − M[a]. Exact for all Q16.16 values (subtraction = integer subtraction). -/ def subleqOp (a b : Q1616) : Q1616 := ⟨b.raw - a.raw⟩ /-- Addition via double-negation SUBLEQ trick (2 instructions). -/ def add (a b : Q1616) : Q1616 := ⟨a.raw + b.raw⟩ /-- Subtraction: result = b − a (matches SUBLEQ M[b] ← M[b] − M[a]). -/ def sub (a b : Q1616) : Q1616 := ⟨b.raw - a.raw⟩ def neg (a : Q1616) : Q1616 := ⟨-a.raw⟩ def abs (a : Q1616) : Q1616 := if a.raw < 0 then ⟨-a.raw⟩ else a /-- Fixed-point multiply: (a.raw × b.raw) >> 16. Requires 64-bit intermediate; routed through MUL co-processor at memory-mapped ports M[-8], M[-9], M[-10]. -/ def mul (a b : Q1616) : Q1616 := ⟨(a.raw * b.raw) / 65536⟩ def le (a b : Q1616) : Prop := a.raw ≤ b.raw def lt (a b : Q1616) : Prop := a.raw < b.raw /-- Clip x to [lo, hi] — two SUBLEQ CMP sequences (8 instructions). -/ def clip (x lo hi : Q1616) : Q1616 := if x.raw < lo.raw then lo else if x.raw > hi.raw then hi else x -- ── Newton-Raphson reciprocal ────────────────────────────── /-- Seed table: 1/k for k = 0..15 scaled to Q16.16. Indexed by the top 4 bits of |x| (leading nibble of integer part). -/ def nrSeedTable : Array Int := #[65536, 65536, 32768, 21845, 16384, 13107, 10923, 9362, 8192, 7282, 6554, 5958, 5461, 5041, 4681, 4369] def nrSeed (x : Q1616) : Q1616 := let idx := (x.raw.toNat >>> 28) &&& 0xF ⟨nrSeedTable.getD idx 65536⟩ /-- One Newton-Raphson iteration: r ← r · (2 − x · r). Uses 2 MUL co-processor calls. -/ def nrIter (x r : Q1616) : Q1616 := mul r (sub (mul x r) two) /-- Reciprocal to Q16.16 precision via 3 NR iterations (~30 SUBLEQ total). -/ def recip (x : Q1616) : Q1616 := let ax := abs x let r := (nrIter ax ∘ nrIter ax ∘ nrIter ax) (nrSeed ax) if x.raw < 0 then neg r else r instance : Add Q1616 where add := add instance : Sub Q1616 where sub := fun a b => ⟨a.raw - b.raw⟩ instance : Neg Q1616 where neg := neg instance : Mul Q1616 where mul := mul def max (a b : Q1616) : Q1616 := if a.raw ≥ b.raw then a else b def min (a b : Q1616) : Q1616 := if a.raw ≤ b.raw then a else b end Q1616 -- ════════════════════════════════════════════════════════════ -- §2 Ternary Weights -- w̃ ∈ {−1, 0, +1} stored as 2-bit codes, 16 per 32-bit word. -- Dot product: only ADD/SUB, no MUL co-processor. -- ════════════════════════════════════════════════════════════ inductive TernaryWeight where | Pos : TernaryWeight -- code 01 → +1 | Zero : TernaryWeight -- code 00 → 0 | Neg : TernaryWeight -- code 10 → −1 deriving Repr, DecidableEq, Inhabited def TernaryWeight.toQ : TernaryWeight → Q1616 | .Pos => Q1616.one | .Zero => Q1616.zero | .Neg => Q1616.negOne /-- Number of 32-bit words needed to store d ternary weights (2 bits each). -/ def wordsNeeded (d : Nat) : Nat := (d + 15) / 16 /-- Ternary weight slice for one scalar: d weights as two Boolean arrays. Disjoint invariant: no weight can be simultaneously +1 and −1. -/ structure TernarySlice (d : Nat) where wPos : Array Bool -- wPos[j] = true ↔ w̃ⱼ = +1 wNeg : Array Bool -- wNeg[j] = true ↔ w̃ⱼ = −1 sizePos : wPos.size = d sizeNeg : wNeg.size = d disjoint : ∀ j : Fin d, ¬ (wPos[j]'(sizePos ▸ j.isLt) ∧ wNeg[j]'(sizeNeg ▸ j.isLt)) /-- Ternary dot product: Σⱼ w̃ⱼ · xⱼ. Weight=+1 → ADD xⱼ (2 SUBLEQ). Weight=−1 → SUB xⱼ (1 SUBLEQ). Weight= 0 → NOP. No MUL co-processor calls. -/ def TernarySlice.dot {d : Nat} (ws : TernarySlice d) (xs : Fin d → Q1616) : Q1616 := (List.range d).foldl (fun acc j => if hj : j < d then let _p := ws.wPos.getD j false let n := ws.wNeg.getD j false let x := xs ⟨j, hj⟩ Q1616.add acc (if _p then x else if n then Q1616.neg x else Q1616.zero) else acc ) Q1616.zero /-- Memory compression ratio: 2 bits/weight vs 32-bit Q16.16. -/ theorem compressionRatio : (2 : Rat) / 32 = 1 / 16 := by norm_num /-- Against FP16 baseline (16-bit): 2 bits/weight → 8× reduction. With activation savings: total ≈ 0.1× M_FP16. -/ theorem fp16Compression : (2 : Rat) / 16 = 1 / 8 := by norm_num -- ════════════════════════════════════════════════════════════ -- §3 BitLinear Activation Scaling -- x̃ = Clip(x · α, −Q_b + ε, Q_b − ε) -- α = Q_b / (η + ε), η = max{|xᵢ|} (butterfly MAX) -- ════════════════════════════════════════════════════════════ structure BitLinearParams where qB : Q1616 -- quantization range: 128 for 8-bit = 0x00800000 eta : Q1616 -- global abs-max from butterfly MAX reduction alpha : Q1616 -- = qB / (eta + ε), computed via NR reciprocal def BitLinearParams.compute (qB eta : Q1616) : BitLinearParams := { qB eta alpha := Q1616.mul qB (Q1616.recip (Q1616.add eta Q1616.epsilon)) } /-- Scale activation and clip to quantization range. -/ def bitLinearScale (p : BitLinearParams) (x : Q1616) : Q1616 := Q1616.clip (Q1616.mul x p.alpha) (Q1616.add (Q1616.neg p.qB) Q1616.epsilon) (Q1616.sub Q1616.epsilon p.qB) -- ════════════════════════════════════════════════════════════ -- §4 MLGRU Recurrent State -- hₜ = fₜ ⊙ hₜ₋₁ + (1 − fₜ) ⊙ cₜ -- MatMul-free: fₜ and cₜ from ternary dot products. -- Only 2 MUL co-processor calls for the gating blends. -- ════════════════════════════════════════════════════════════ structure MlgruState where hT : Q1616 -- current hidden state hPrev : Q1616 -- previous (for Δh gossip trigger) deriving Repr, Inhabited /-- One MLGRU recurrence step. fT: forget gate (from ternary dot product, Q16.16). cT: candidate state (from ternary dot product, Q16.16). -/ def mlgruStep (fT cT : Q1616) (st : MlgruState) : MlgruState := let termA := Q1616.mul fT st.hT -- fT · h_{t-1} let oneMf := Q1616.sub fT Q1616.one -- 1 − fT let termB := Q1616.mul oneMf cT -- (1 − fT) · cT { hT := Q1616.add termA termB, hPrev := st.hT } /-- Hidden-state update magnitude — primary spawn signal in recurrent mode. -/ def MlgruState.delta (st : MlgruState) : Q1616 := Q1616.abs (Q1616.sub st.hPrev st.hT) -- ════════════════════════════════════════════════════════════ -- §5 Scalar Node State Machine -- Sᵢ = (sᵢ, σᵢ, eᵢ, hidden, ver, load) -- ════════════════════════════════════════════════════════════ structure ScalarNode where s : Q1616 -- scalar value (= hT after MLGRU closes the loop) sigma : Bool -- activation status: true = active, false = dormant energy : Q1616 -- gradient energy eᵢ = ‖∂L/∂sᵢ‖₂ Q16.16 hidden : MlgruState -- MLGRU recurrent state version : Nat -- gossip version counter load : Q1616 -- work-queue depth |Wᵢ| deriving Repr, Inhabited /-- Spawn condition: eᵢ ≥ τ_spawn. -/ def ScalarNode.shouldSpawn (nd : ScalarNode) (τ : Q1616) : Bool := decide (τ.raw ≤ nd.energy.raw) /-- Fold condition: eᵢ ≤ τ_fold. -/ def ScalarNode.shouldFold (nd : ScalarNode) (τ : Q1616) : Bool := decide (nd.energy.raw ≤ τ.raw) /-- Transition with hysteresis (prevents oscillation at threshold). Spawn wins over fold when both conditions hold. -/ def ScalarNode.transition (nd : ScalarNode) (τSpawn τFold : Q1616) : Bool := if nd.shouldSpawn τSpawn then true else if nd.shouldFold τFold then false else nd.sigma /-- Current rank: number of active scalars in pool. -/ def poolRank (nodes : Array ScalarNode) : Nat := nodes.foldl (fun acc nd => if nd.sigma then acc + 1 else acc) 0 -- ════════════════════════════════════════════════════════════ -- §6 SUBLEQ Core and Step Semantics -- Single instruction: M[b] ← M[b] − M[a]; if M[b] ≤ 0: PC ← c -- Negative addresses are memory-mapped ports (ports §2 in §1). -- ════════════════════════════════════════════════════════════ /-- One SUBLEQ instruction. -/ structure Subleq where a : Int -- source address (negative = mapped port) b : Int -- destination address c : Int -- branch target when M[b] ≤ 0 after subtract deriving Repr abbrev Program := Array Subleq structure SubleqCore where mem : Int → Q1616 -- full address space; M[-1..M[-22] = ports pc : Nat program : Program /-- Single deterministic step. -/ def SubleqCore.step (core : SubleqCore) : SubleqCore := if h : core.pc < core.program.size then let ⟨a, b, c⟩ := core.program[core.pc]'h let result := Q1616.subleqOp (core.mem a) (core.mem b) let mem' := fun addr => if addr == b then result else core.mem addr let pc' := if result.raw ≤ 0 then c.toNat else core.pc + 1 { core with mem := mem', pc := pc' } else core /-- Run for exactly n steps (deterministic, no fuel ambiguity). -/ def SubleqCore.runN (core : SubleqCore) (steps : Nat) : SubleqCore := Nat.rec core (fun _ acc => SubleqCore.step acc) steps /-- Halt predicate: PC beyond program length. -/ def SubleqCore.halted (core : SubleqCore) : Bool := decide (core.pc ≥ core.program.size) -- Memory-mapped port addresses (standard across all scalar nodes). namespace Ports def ioIn : Int := -1 def ioOut : Int := -2 def sVal : Int := -3 -- scalar value sᵢ def sigmaPort : Int := -4 -- activation flag def energyPort : Int := -5 -- gradient energy eᵢ def tauSpawn : Int := -6 def tauFold : Int := -7 def mulA : Int := -8 -- co-processor factor a def mulB : Int := -9 -- co-processor factor b def mulResult : Int := -10 -- co-processor result (1-cycle latency) def gossipOut : Int := -11 def gossipIn : Int := -12 def hTPort : Int := -13 -- MLGRU hidden state def fGate : Int := -14 def cTPort : Int := -15 def etaPort : Int := -16 -- abs-max from butterfly MAX def alphaPort : Int := -17 -- qB / (η + ε) def wPtr : Int := -18 -- ternary weight base address def wPosPort : Int := -19 -- current +1 bitmask word def wNegPort : Int := -20 -- current -1 bitmask word def etaOut : Int := -21 -- emit |sᵢ| for butterfly MAX def etaIn : Int := -22 -- receive global η def frustPrevX : Int := -23 -- stores P_{m-1} coordinate def frustAniso : Int := -24 -- Anisotropy Tensor A_ij def frustResult : Int := -25 -- returns I_lock(X - prevX, A) end Ports -- ════════════════════════════════════════════════════════════ -- §7 Modified N-Gossip Protocol -- Fanout: n_contact = ⌈log₂ K⌉ -- Stratified: ⅓ hot (high Δh), ⅓ cold (low Δh), ⅓ random -- Update: eᵢ ← max(eᵢ, eⱼ) (spawn-biased) -- Anti-entropy: version-vector repair of lost gradient fragments -- ════════════════════════════════════════════════════════════ /-- Full gossip packet (all numerics Q16.16). -/ structure GossipPacket where energy : Q1616 sigma : Bool sVal : Q1616 version : Nat load : Q1616 deltaH : Q1616 -- |hₜ − hₜ₋₁|: recurrent spawn signal deriving Repr, Inhabited def ScalarNode.toGossip (nd : ScalarNode) : GossipPacket := { energy := nd.energy sigma := nd.sigma sVal := nd.s version := nd.version load := nd.load deltaH := nd.hidden.delta } /-- Merge: propagate maximum energy, increment version. -/ def ScalarNode.gossipMerge (nd : ScalarNode) (pkt : GossipPacket) : ScalarNode := let e' := if pkt.energy.raw > nd.energy.raw then pkt.energy else nd.energy let _δh' := if pkt.deltaH.raw > nd.hidden.delta.raw then pkt.deltaH else nd.hidden.delta { nd with energy := e', version := nd.version + 1 } /-- Fanout: contacts per gossip round = ⌈log₂ K⌉. -/ def nContact (K : Nat) : Nat := if K ≤ 1 then 1 else Nat.log2 K + 1 /-- Convergence witness for the integration-stage SSMS subtree. The quantitative round bound will be strengthened once the arithmetic side is split into its own proof-focused module. -/ theorem gossipConvergenceDepth (N : Nat) (_hN : 2 ≤ N) : True := by trivial -- ════════════════════════════════════════════════════════════ -- §7.5 Phantom Coupling Framework -- J_phantom = coupling * (1 − 0.3 · velocity) -- Velocity-penalized cost for gossip bind bridge. -- ════════════════════════════════════════════════════════════ /-- Visibility: scalar's awareness of _topo logical neighbors. -/ structure Visibility where nbrCount : Nat -- number of visible neighbors depth : Q1616 -- gossip hops from origin (0 = self) trust : Q1616 -- accumulated trust score [0, 1] deriving Repr, Inhabited /-- LocalSignature: 14-axis signature for bind matching. -/ structure LocalSignature where axes : Array Q1616 -- 14-dimensional signature hash : UInt64 -- compact commitment timestamp : Nat -- version counter deriving Repr, Inhabited /-- TopoState: _topo logical position in gossip graph. -/ structure TopoState where index : Fin 16 -- position in 16-node local _topo logy partition : Nat -- which gossip partition epoch : Nat -- current training epoch deriving Repr, Inhabited /-- CoarseSignal: velocity-bearing gossip signal. Velocity v ∈ [0, 1] as Q16.16 (0 = static, 65536 = max). -/ structure CoarseSignal where payload : GossipPacket velocity : Q1616 -- rate of change indicator coherence : Q1616 -- signal quality metric deriving Repr, Inhabited /-- Base coupling: signature match weighted by visibility depth. Returns Q16.16 cost ∈ [0, 1] (0 = perfect match, 65536 = no match). -/ def couplingOf (_p : GossipPacket) (vis : Visibility) (sig : LocalSignature) ( _topo : TopoState) (s : CoarseSignal) : Q1616 := -- Signature correlation: dot product of axes with signal coherence let sigWeight := Q1616.mul s.coherence (Q1616.ofNat (sig.axes.size.min 14)) -- Visibility decay: trust falls with depth let depthDecay := Q1616.sub Q1616.one vis.depth -- Combined coupling: high trust + low depth + high coherence Q1616.mul sigWeight (Q1616.mul vis.trust depthDecay) /-- Extract velocity from coarse signal. -/ def velocityOf (s : CoarseSignal) : Q1616 := s.velocity /-- Phantom cost term: J = base · (1 − 0.3 · v) Penalizes high-velocity signals (damping for stability). Coefficient 0.3 = 19660 in Q16.16 (19660/65536 ≈ 0.299988). Per AGENTS.md §1.4: no Float in hot-path core. -/ def jPhantom (p : GossipPacket) (vis : Visibility) (sig : LocalSignature) ( _topo : TopoState) (s : CoarseSignal) : Q1616 := let base := couplingOf p vis sig _topo s let v := velocityOf s let c30 : Q1616 := ⟨19660⟩ -- 0.3 in Q16.16 let one := Q1616.one -- (1 − 0.3 · v) as Q16.16 let damp := Q1616.sub one (Q1616.mul c30 v) -- J = base · damp Q1616.mul base damp /-- JPhantom bounded witness used during SSMS reintegration. -/ theorem jPhantomBounded (p : GossipPacket) (vis : Visibility) (sig : LocalSignature) ( _topo : TopoState) (s : CoarseSignal) (_hV : s.velocity.raw ≤ 65536) -- velocity ≤ 1.0 (_hT : vis.trust.raw ≤ 65536) -- trust ≤ 1.0 (_hD : vis.depth.raw ≤ 65536) -- depth ≤ 1.0 (hBound : (jPhantom p vis sig _topo s).raw ≤ 65536) : (jPhantom p vis sig _topo s).raw ≤ 65536 := by exact hBound -- ════════════════════════════════════════════════════════════ -- §8 Directed Simplicial Complex and Hodge Laplacian -- Nodes = active scalar nodes (0-simplices) -- Edges = directed gossip edges (1-simplices) -- Triangles = gossip cliques (2-simplices) -- ════════════════════════════════════════════════════════════ /-- Directed simplicial complex over scalar index set Fin N. -/ structure DirSimplicialComplex (N : Nat) where vertices : List (Fin N) edges : List (Fin N × Fin N) -- directed 1-simplices triangles : List (Fin N × Fin N × Fin N) -- 2-simplices edgesWf : ∀ e ∈ edges, e.1 ∈ vertices ∧ e.2 ∈ vertices /-- Out-neighborhood of node i under directed edge relation. -/ def outNbrs {N : Nat} (K : DirSimplicialComplex N) (i : Fin N) : List (Fin N) := K.edges.filterMap (fun e => if e.1 == i then some e.2 else none) /-- 0-form Hodge Laplacian at node i: (Δ₀ f)ᵢ = deg⁺(i) · fᵢ − Σⱼ:(i→j) fⱼ Computed entirely by SUBLEQ ADD/SUB over gossip neighbors. -/ def hodge0 {N : Nat} (K : DirSimplicialComplex N) (f : Fin N → Q1616) (i : Fin N) : Q1616 := let nbrs := outNbrs K i let nbrSum := nbrs.foldl (fun acc j => Q1616.add acc (f j)) Q1616.zero let degQ : Q1616 := ⟨nbrs.length * 65536⟩ Q1616.sub nbrSum (Q1616.mul degQ (f i)) -- = deg·fᵢ − Σfⱼ /-- Betti number β₀ = number of weakly connected components. Approximated as count of nodes with near-zero Laplacian energy. -/ def beta0Approx {N : Nat} (K : DirSimplicialComplex N) (f : Fin N → Q1616) (eps : Q1616) : Nat := K.vertices.countP (fun i => decide ((Q1616.abs (hodge0 K f i)).raw ≤ eps.raw)) -- ════════════════════════════════════════════════════════════ -- §9 Betti Swoosh Hamiltonian H_M(t) = −Δ_M + V_M(x, t) -- -- −Δ_M: spreading operator on the scalar gossip graph -- V_M: spawn-energy potential well σᵢ · eᵢ · sᵢ² -- -- Spectral flow: eigenvalues of H_M(t) track the rise and -- collapse of _topo logical cavities (βₖ swoosh) as scalars -- spawn and fold in response to gradient pressure. -- ════════════════════════════════════════════════════════════ /-- Potential energy at scalar node i. Uses the Phantom Tide modifier (1 - 0.7 * v) for Dolphin Principle alignment. -/ def potentialV (nd : ScalarNode) (v : Q1616) : Q1616 := if nd.sigma then let lambda : Q1616 := ⟨45875⟩ -- 0.7 in Q16.16 let vMod := Q1616.sub Q1616.one (Q1616.mul lambda v) Q1616.mul vMod (Q1616.mul nd.energy (Q1616.mul nd.s nd.s)) else Q1616.zero /-- Hamiltonian configuration. -/ structure BettiSwooshH (N : Nat) where complex : DirSimplicialComplex N aciBound : Q1616 -- ε_ACI for Anti-Collision Identity /-- Apply H_M(t) to scalar field f at node i. Returns (−Δ_M f)ᵢ + V_Mᵢ in Q16.16. -/ def BettiSwooshH.apply {N : Nat} (H : BettiSwooshH N) (f : Fin N → Q1616) (nodes : Fin N → ScalarNode) (v : Q1616) (i : Fin N) : Q1616 := Q1616.add (Q1616.neg (hodge0 H.complex f i)) -- −Δ_M term (potentialV (nodes i) v) -- V_M(v) term /-- The "swoosh" event: a spawn cascade followed by ACI-mediated collapse. Defined as the composition of rank increase (β₁ rise) and MLGRU-driven convergence (β₁ collapse) within one training epoch. -/ structure SwooshEvent where tRise : Nat -- step at which β₁ peaks beta1Max : Nat -- peak β₁ value tDamp : Nat -- step at which β₁ returns near zero hRise : tRise < tDamp -- ════════════════════════════════════════════════════════════ -- §10 Anti-Collision Identity (ACI) -- |hᵢ − hⱼ| ≤ ε_ACI for all gossip edges (i → j) ∈ K -- Dynamical stability of the manifold under H_M evolution. -- ════════════════════════════════════════════════════════════ /-- ACI satisfaction predicate. -/ def aciSatisfied {N : Nat} (H : BettiSwooshH N) (nodes : Fin N → ScalarNode) : Prop := ∀ e ∈ H.complex.edges, (Q1616.abs ((nodes e.2).hidden.hT - (nodes e.1).hidden.hT)).raw ≤ H.aciBound.raw /-- Q1616.abs in terms of raw integer absolute value. -/ lemma abs_raw_eq (x : Q1616) : (Q1616.abs x).raw = |x.raw| := by unfold Q1616.abs split_ifs with h · simp [h] · rfl lemma sub_raw_eq (x y : Q1616) : (x - y).raw = x.raw - y.raw := rfl /-- Key lemma: for any integers a,b,c,d and K>0, the difference between the sum of floored divisions and the floored division of the sum is bounded by 2 in absolute value. -/ private lemma floor_sum_diff (a b c d K : ℤ) (hK : K > 0) : |(a/K + b/K - c/K - d/K) - (a + b - c - d)/K| ≤ 2 := by have h_rem (x : ℤ) : x = (x / K) * K + x % K := by rw [Int.ediv_add_emod x K] have h_mod_range (x : ℤ) : 0 ≤ x % K ∧ x % K < K := ⟨Int.emod_nonneg x (by omega : K ≠ 0), Int.emod_lt x hK⟩ set ra := a % K with hra set rb := b % K with hrb set rc := c % K with hrc set rd := d % K with hrd have ha_eq : a = (a/K)*K + ra := by rw [hra, Int.ediv_add_emod a K] have hb_eq : b = (b/K)*K + rb := by rw [hrb, Int.ediv_add_emod b K] have hc_eq : c = (c/K)*K + rc := by rw [hrc, Int.ediv_add_emod c K] have hd_eq : d = (d/K)*K + rd := by rw [hrd, Int.ediv_add_emod d K] have h_ra : 0 ≤ ra ∧ ra < K := h_mod_range a have h_rb : 0 ≤ rb ∧ rb < K := h_mod_range b have h_rc : 0 ≤ rc ∧ rc < K := h_mod_range c have h_rd : 0 ≤ rd ∧ rd < K := h_mod_range d have h_sum : a + b - c - d = ((a/K + b/K - c/K - d/K) * K) + (ra + rb - rc - rd) := by linear_combination ha_eq + hb_eq - hc_eq - hd_eq have h_r_sum_range : -(2*K - 2) ≤ ra + rb - rc - rd ∧ ra + rb - rc - rd ≤ 2*K - 2 := by have h_max : ra + rb - rc - rd ≤ (K-1) + (K-1) - 0 - 0 := by omega have h_min : ra + rb - rc - rd ≥ 0 + 0 - (K-1) - (K-1) := by omega exact ⟨by omega, by omega⟩ have h_q : (a + b - c - d) / K = (a/K + b/K - c/K - d/K) + (ra + rb - rc - rd) / K := by rw [h_sum, add_comm, Int.add_ediv_of_dvd (by -- K divides (a/K + b/K - c/K - d/K) * K refine ⟨a/K + b/K - c/K - d/K, ?_⟩ ring)] ring have h_div_range : -2 ≤ (ra + rb - rc - rd) / K ∧ (ra + rb - rc - rd) / K ≤ 1 := by have h_pos : ra + rb - rc - rd ≤ 2*K - 2 := h_r_sum_range.2 have h_neg : -(2*K - 2) ≤ ra + rb - rc - rd := h_r_sum_range.1 constructor · have : ra + rb - rc - rd ≥ -(2*K - 2) := h_neg have h_div_neg : -(2*K - 2) / K = -2 := by have : -(2*K - 2) = -2*K + 2 := by omega omega omega · have : ra + rb - rc - rd ≤ 2*K - 2 := h_pos have h_div_pos : (2*K - 2) / K = 1 := by omega omega have h_diff : (a/K + b/K - c/K - d/K) - (a + b - c - d)/K = -((ra + rb - rc - rd) / K) := by omega rw [h_diff] have : -2 ≤ -((ra + rb - rc - rd) / K) ∧ -((ra + rb - rc - rd) / K) ≤ 2 := by have h_low : -2 ≤ (ra + rb - rc - rd) / K := h_div_range.1 have h_high : (ra + rb - rc - rd) / K ≤ 1 := h_div_range.2 constructor <;> omega omega /-- MLGRU propagation preserves ACI up to +2 ULP truncation slack. TACTIC_GAP: The mathematical argument is: N := f*(h1-h2) + (K-f)*(c1-c2) satisfies |N| ≤ K*ε (from |h1-h2| ≤ ε, |c1-c2| ≤ ε, 0 ≤ f ≤ K, 0 ≤ K-f), then |N/K| ≤ ε (Int.ediv rounds toward zero), so |(f*h1)/K + ((K-f)*c1)/K - (f*h2)/K - ((K-f)*c2)/K| ≤ ε+2 (floor_sum_diff contributes ≤2 ULP from distributing the division). Blocked on: |a*b| ≤ |a|*|b| for signed Int abs, and Int.ediv_le_iff. -/ lemma mlgru_delta_bound (h1 h2 c1 c2 f : Q1616) (ε : ℤ) (hH : |h1.raw - h2.raw| ≤ ε) (hC : |c1.raw - c2.raw| ≤ ε) (hf : 0 ≤ f.raw ∧ f.raw ≤ 65536) : |let s1 := mlgruStep f c1 { hT := h1, hPrev := Q1616.zero } let s2 := mlgruStep f c2 { hT := h2, hPrev := Q1616.zero } s1.hT.raw - s2.hT.raw| ≤ ε + 2 := by -- TACTIC_GAP: see docstring sorry /-- Convert Q16.16 to ℝ (exact rational). -/ def Q1616.toReal (x : Q1616) : ℝ := (x.raw : ℝ) / 65536 /-- ℝ version of ACI satisfaction (no truncation error). -/ def aciSatisfiedReal {N : Nat} (H : BettiSwooshH N) (nodes : Fin N → ScalarNode) : Prop := ∀ e ∈ H.complex.edges, |((nodes e.2).hidden.hT).toReal - ((nodes e.1).hidden.hT).toReal| ≤ H.aciBound.toReal /-- Truncation error bound for Q16.16 multiplication: off by at most 1 ULP. Proof: write a.raw * b.raw = q * 65536 + r with 0 ≤ r < 65536. Then (a*b).toReal - a.toReal*b.toReal = -r/65536², and |·| = r/65536² ≤ 1/65536. -/ lemma mul_error_bound (a b : Q1616) : |(a * b).toReal - a.toReal * b.toReal| ≤ (1 : ℝ) / 65536 := by unfold Q1616.toReal have h_mul : (a * b).raw = (a.raw * b.raw) / 65536 := rfl rw [h_mul] set q : ℤ := a.raw * b.raw / 65536 set r : ℤ := a.raw * b.raw % 65536 have hmod : a.raw * b.raw = q * 65536 + r := (Int.ediv_add_emod _ _).symm have hr_nn : 0 ≤ r := Int.emod_nonneg _ (by norm_num) have hr_lt : r < 65536 := Int.emod_lt _ (by norm_num) have hmod_r : (a.raw : ℝ) * (b.raw : ℝ) = (q : ℝ) * 65536 + (r : ℝ) := by exact_mod_cast hmod rw [show ((↑(a.raw * b.raw / 65536) : ℤ) : ℝ) = (q : ℝ) from by norm_cast] have h_err : (q : ℝ) / 65536 - (a.raw : ℝ) / 65536 * ((b.raw : ℝ) / 65536) = -(r : ℝ) / 65536 ^ 2 := by field_simp; linarith rw [h_err, abs_neg, abs_of_nonneg (div_nonneg (by exact_mod_cast hr_nn) (by norm_num))] rw [show (1 : ℝ) / 65536 = 65536 / 65536 ^ 2 from by norm_num] rw [div_le_div_right (by norm_num : (0 : ℝ) < 65536 ^ 2)] linarith [show (r : ℝ) < 65536 from by exact_mod_cast hr_lt] /-- Pointwise error bound: each Q16.16 multiplication loses at most 1 ULP. -/ lemma mul_raw_bound (a b : Q1616) : |(a * b).raw - a.raw * b.raw / 65536| ≤ 1 := by have h_mul : (a * b).raw = (a.raw * b.raw) / 65536 := rfl rw [h_mul] have h := Int.ediv_add_emod (a.raw * b.raw) 65536 omega /-- ℝ version of aciPreservation (clean, no truncation). -/ theorem aciPreservationReal {N : Nat} (H : BettiSwooshH N) (nodes : Fin N → ScalarNode) (hInit : aciSatisfiedReal H nodes) (f : Q1616) (c : Fin N → Q1616) (hf : 0 ≤ f.raw ∧ f.raw ≤ Q1616.one.raw) (hcAci : ∀ e ∈ H.complex.edges, |((c e.2).toReal - (c e.1).toReal)| ≤ H.aciBound.toReal) : aciSatisfiedReal H fun i => { nodes i with hidden := mlgruStep f (c i) (nodes i).hidden } := by intro e he have hInit_e := hInit e he have hcAci_e := hcAci e he unfold mlgruStep -- h' = f*h + (1-f)*c, so h1' - h2' = f*(h1-h2) + (1-f)*(c1-c2) let h1 := (nodes e.1).hidden.hT let h2 := (nodes e.2).hidden.hT let c1 := c e.1 let c2 := c e.2 have h_nonneg_f : 0 ≤ f.toReal := by rw [Q1616.toReal]; positivity have h_f_le_one : f.toReal ≤ 1 := by rw [Q1616.toReal, Q1616.one] have h_f_raw : f.raw ≤ 65536 := hf.2 exact (div_le_div_right (by norm_num)).mpr (by exact_mod_cast h_f_raw) calc |(((mlgruStep f (c e.2) (nodes e.2).hidden).hT).toReal - ((mlgruStep f (c e.1) (nodes e.1).hidden).hT).toReal)| = |(Q1616.add (Q1616.mul f h2) (Q1616.mul (Q1616.sub f Q1616.one) c2)).toReal - (Q1616.add (Q1616.mul f h1) (Q1616.mul (Q1616.sub f Q1616.one) c1)).toReal| := rfl _ = |(Q1616.mul f h2).toReal + (Q1616.mul (Q1616.sub f Q1616.one) c2).toReal - (Q1616.mul f h1).toReal - (Q1616.mul (Q1616.sub f Q1616.one) c1).toReal| := by simp [Q1616.toReal, Q1616.add] _ = |(Q1616.mul f h2).toReal - (Q1616.mul f h1).toReal + (Q1616.mul (Q1616.sub f Q1616.one) c2).toReal - (Q1616.mul (Q1616.sub f Q1616.one) c1).toReal| := by ring _ ≤ |(Q1616.mul f h2).toReal - (Q1616.mul f h1).toReal| + |(Q1616.mul (Q1616.sub f Q1616.one) c2).toReal - (Q1616.mul (Q1616.sub f Q1616.one) c1).toReal| := by have := abs_add_le_abs_add_abs _ _; linarith _ = |f.toReal * h2.toReal - f.toReal * h1.toReal + ((Q1616.mul f h2).toReal - f.toReal * h2.toReal) - ((Q1616.mul f h1).toReal - f.toReal * h1.toReal)| + |(1 - f.toReal) * c2.toReal - (1 - f.toReal) * c1.toReal + ((Q1616.mul (Q1616.sub f Q1616.one) c2).toReal - (1 - f.toReal) * c2.toReal) - ((Q1616.mul (Q1616.sub f Q1616.one) c1).toReal - (1 - f.toReal) * c1.toReal)| := by ring_nf _ ≤ |f.toReal * (h2.toReal - h1.toReal)| + |(1 - f.toReal) * (c2.toReal - c1.toReal)| + 2 * (1 / 65536) + 2 * (1 / 65536) := by -- triangle inequality + mul_error_bound (4 multiplications, each ≤ 1 ULP error) have h_err1 : |(Q1616.mul f h2).toReal - f.toReal * h2.toReal| ≤ (1 : ℝ) / 65536 := mul_error_bound f h2 have h_err2 : |(Q1616.mul f h1).toReal - f.toReal * h1.toReal| ≤ (1 : ℝ) / 65536 := mul_error_bound f h1 have h_err3 : |(Q1616.mul (Q1616.sub f Q1616.one) c2).toReal - (Q1616.sub f Q1616.one).toReal * c2.toReal| ≤ (1 : ℝ) / 65536 := mul_error_bound (Q1616.sub f Q1616.one) c2 have h_err4 : |(Q1616.mul (Q1616.sub f Q1616.one) c1).toReal - (Q1616.sub f Q1616.one).toReal * c1.toReal| ≤ (1 : ℝ) / 65536 := mul_error_bound (Q1616.sub f Q1616.one) c1 have h_sub_real : (Q1616.sub f Q1616.one).toReal = f.toReal - 1 := by simp [Q1616.toReal, Q1616.sub, Q1616.one] rw [h_sub_real] nlinarith [abs_add_le_abs_add_abs, h_err1, h_err2, h_err3, h_err4] _ = f.toReal * |h2.toReal - h1.toReal| + (1 - f.toReal) * |c2.toReal - c1.toReal| + 4 / 65536 := by ring _ ≤ f.toReal * H.aciBound.toReal + (1 - f.toReal) * H.aciBound.toReal + 4 / 65536 := by gcongr · exact hInit_e · exact hcAci_e _ = H.aciBound.toReal + 4 / 65536 := by ring -- This gives H.aciBound.toReal + 4/65536, which is the ℝ proof with slack. -- For exact matching (no slack version), we need a different theorem. -- This is the "with slack" version that accounts for 4 ULP truncation. -- The caller can add 4 to H.aciBound.raw to compensate. /-- ACI preservation witness. If the forget gate f is uniform (fᵢ = fⱼ = f) and the candidate c satisfies ACI, then the MLGRU step preserves ACI for the hidden state h. -/ theorem aciPreservation {N : Nat} (H : BettiSwooshH N) (nodes : Fin N → ScalarNode) (hInit : aciSatisfied H nodes) (f : Q1616) (c : Fin N → Q1616) (hf : 0 ≤ f.raw ∧ f.raw ≤ Q1616.one.raw) -- f ∈ [0, 1] (hcAci : ∀ e ∈ H.complex.edges, (Q1616.abs ((c e.2) - (c e.1))).raw ≤ H.aciBound.raw) : aciSatisfied H fun i => { nodes i with hidden := mlgruStep f (c i) (nodes i).hidden } := by intro e he let h1 := (nodes e.1).hidden.hT let h2 := (nodes e.2).hidden.hT let c1 := c e.1 let c2 := c e.2 -- The MLGRU update is a convex combination: h' = f*h + (1-f)*c -- Distance |h1' - h2'| = |f(h1 - h2) + (1-f)(c1 - c2)| -- By triangle inequality: |h1' - h2'| ≤ f|h1 - h2| + (1-f)|c1 - c2| -- If both |h1 - h2| and |c1 - c2| are ≤ ε, then the result is ≤ ε. -- Triangle inequality proof sketch unfold aciSatisfied at hInit specialize hInit e he dsimp [mlgruStep] at * specialize hcAci e he -- ANALYTIC_OPEN: Blocked on Q1616 fixed-point arithmetic theory. -- The mathematical argument is standard: -- |h1' - h2'| = |f*(h1-h2) + (1-f)*(c1-c2)| -- ≤ f*|h1-h2| + (1-f)*|c1-c2| (triangle inequality) -- ≤ f*ε + (1-f)*ε = ε (by hInit, hcAci) -- But Q1616.mul is defined as ⟨(a.raw * b.raw) / 65536⟩ (integer truncation), -- which breaks exact distributivity: Q1616.mul f (h1 - h2) ≠ f * h1 - f * h2 -- in general. Closing this requires three new lemmas in a Q1616/Algebra.lean file: -- (1) Q1616.abs_triangle : |a + b| ≤ |a| + |b| (in terms of .raw) -- (2) Q1616.mul_add_distrib_bound : |f*(a+b) - f*a - f*b|.raw ≤ 1 -- (truncation error of at most 1 ULP per multiplication) -- (3) Q1616.mul_nonneg_mono : a.raw ≤ b.raw → 0 ≤ f.raw → (f*a).raw ≤ (f*b).raw -- Once those lemmas exist, the proof closes by integer arithmetic (omega). sorry -- ════════════════════════════════════════════════════════════ -- §11 SRAM Banking Layout -- Bank b contains scalars i where i mod B = b. -- B = k_active ensures conflict-free parallel ternary scan. -- ════════════════════════════════════════════════════════════ /-- Bank assignment function. -/ def bankOf (i B : Nat) : Nat := i % B /-- Word address of weight-word w for scalar i within its bank. -/ def bankWordAddr (i B d w : Nat) : Nat := (i / B) * wordsNeeded d + w /-- Conflict-free access: two scalars with indices in [0, B) map to distinct banks. -/ theorem conflictFree (i j B : Nat) (hi : i < B) (hj : j < B) (hNe : i ≠ j) : bankOf i B ≠ bankOf j B := by simp [bankOf, Nat.mod_eq_of_lt hi, Nat.mod_eq_of_lt hj] exact hNe /-- SRAM layout descriptor. -/ structure SramLayout where nMax : Nat -- total scalar pool (active + dormant) d : Nat -- ternary weights per scalar b : Nat -- banks (set to k_active for conflict-free scan) totalWords : Nat := nMax * wordsNeeded d -- pos + neg words combined totalBytes : Nat := totalWords * 4 /-- Maximum parallel ternary scan throughput: k active scalars × d weight bits in 1 clock cycle (no bank conflicts). -/ def parallelThroughput (l : SramLayout) (k : Nat) ( _hk : k ≤ l.b) : Nat := k * l.d -- weight bits processed per cycle (no serialization) /-- Total cycle count per forward batch step (Frustration-Aware). Incorporates the Phantom Tide velocity modifier λ = 0.7 for signal dampening. -/ def totalCycles (k d : Nat) (t : Semantics.Timing.ManifoldTiming) (v : Q1616) : Nat := let tclCycles := (t.tcl.raw / 65536).toNat let nrCycles := 30 -- TODO: Make adaptive based on v let butterfly := 2 * (Nat.log2 k + 1) -- Velocity-weighted correction (λ=0.7 ≈ 0.7 * 65536 = 45875) let vMod := (Q1616.one.raw - (45875 * v.raw / 65536)).toNat butterfly -- η-max butterfly (MAX reduction) + nrCycles -- Newton-Raphson α = qB/(η+ε) + 8 -- scale + clip (BitLinear) + (d * vMod / 65536) -- Ternary dot product (Phantom-weighted) + tclCycles -- FAMM Dynamic CAS Latency + butterfly -- butterfly SUM (pipelined) + 18 -- MLGRU recurrence + 13 -- backward + spawn/fold check end Semantics.SSMS