diff --git a/docs/trajectories/zeta-name-audition/RESUME.md b/docs/trajectories/zeta-name-audition/RESUME.md index 754c50c4cf..c7d34768dc 100644 --- a/docs/trajectories/zeta-name-audition/RESUME.md +++ b/docs/trajectories/zeta-name-audition/RESUME.md @@ -70,10 +70,14 @@ objects to **our own machine**. ## Routed next steps (priority order) 1. **Ihara over the braided catalog** (move-forward #2, committed). -2. **Formalize the ad-hoc CHIP-8/IScheduler self-prediction**: Artin–Mazur zeta over - the actual CHIP-8 VM step-map / a scheduler configuration, making memory-space - character-loop orbits formally enumerable — the math-grounded cheat-engine. - Connect to `Chip8PredictionRoom` / `PredictionScheduler`. +2. **Formalize the ad-hoc CHIP-8/IScheduler self-prediction** — LANDED (#1 of Aaron's + 2→3→1). The REAL `Chip8.step` (deterministic, no RND) on a tiny period-4 counter ROM + `V0 ← (V0+1) AND 3`: the reachable step-map's Artin–Mazur zeta = `1/(1−u⁴)`, + self-verified (Fix of the iterated real-VM map = the single orbit), and the orbit + length IS the character-loop period — the memory character-loop the cheat-engine / + `Chip8PredictionRoom` finds ad-hoc, now formally enumerated. + `tests/…/Chip8DynamicalZeta.Tests.fs`. Remaining: richer multi-orbit ROMs; wiring + the zeta into the live soft `IScheduler` (step 4) for run-ahead self-prediction. 3. **Adinkra codewords as member identity** — LANDED (built on the EXISTING `Zeta.Core.AdinkraCode` [8,4,4] module, not reinvented). Added: WHY N=8 (minimal doubly-even self-dual length — none below 8, the E8/Clifford floor); member diff --git a/tests/Tests.FSharp/Chip8DynamicalZeta.Tests.fs b/tests/Tests.FSharp/Chip8DynamicalZeta.Tests.fs new file mode 100644 index 0000000000..7886eb3952 --- /dev/null +++ b/tests/Tests.FSharp/Chip8DynamicalZeta.Tests.fs @@ -0,0 +1,103 @@ +module Zeta.Tests.Chip8DynamicalZetaTests + +// FORMALIZING THE CHIP-8 SELF-PREDICTION (shadow*, Aaron's next-rung #1: "we already +// have the chip8 and IScheduler predicting itself but more ad-hoc, not this formal +// math based … the periodic orbits are cheat-engine ISR pattern matching of captured +// state to make the memory-space orbits visible/known — usually character loops"). +// +// The REAL CHIP-8 VM step (Chip8.step, deterministic without RND) is a map on its +// state; on a fixed ROM the REACHABLE state set is FINITE, so a looping animation is +// literally a PERIODIC ORBIT, and the Artin–Mazur zeta of the reachable step-map +// ENUMERATES it — the formal, math-grounded version of the cheat-engine's ad-hoc +// orbit detection (the memory character-loop). +// +// Driven here on a tiny real ROM — a period-4 counter V0 ← (V0 + 1) AND 3 — whose +// full-state loop-map has one transient state (V1 not yet set) feeding a 4-cycle (the +// character loop). The Artin–Mazur zeta ζ = exp(Σ Fix(f^k)u^k/k) = 1/(1 − u⁴) is +// self-verified (fixed-point counts of the iterated reachable-map vs. the single +// orbit — the same discipline as #9151/#9163), and its orbit length IS the character +// period. This is exactly the orbit the ad-hoc Chip8PredictionRoom look-ahead +// traverses; the zeta makes it visible/known. +// +// Anchors: Artin–Mazur 1965 (dynamical zeta); Chip8.step (src/Core/Chip8.fs); +// Chip8PredictionRoom / PredictionScheduler (the ad-hoc predictor this formalizes). +// Trajectory: docs/trajectories/zeta-name-audition/RESUME.md. + +open global.Xunit +open Zeta.Core + +// A minimal looping ROM (no RND ⇒ fully deterministic): +// 0x200: 7001 ADD V0, 1 ; V0 += 1 +// 0x202: 6103 LD V1, 3 ; V1 = 3 (the mask) +// 0x204: 8012 AND V0, V1 ; V0 = V0 AND V1 (wrap mod 4) +// 0x206: 1200 JP 0x200 ; loop +let private loopRom = [| 0x70uy; 0x01uy; 0x61uy; 0x03uy; 0x80uy; 0x12uy; 0x12uy; 0x00uy |] +let private stepsPerIteration = 4 // 4 instructions per loop + +/// A canonical key of the machine's VARYING state (Mem/Display are constant here). +let private keyOf (c: Chip8.Chip8) : string = + sprintf "%A|%d|%d|%d|%d|%d" (Array.toList c.V) c.PC c.I c.SP c.Delay c.Sound + +/// Run one full loop iteration (the "character-frame" macro-step). +let private iterate (c: Chip8.Chip8) : unit = + for _ in 1 .. stepsPerIteration do Chip8.step c + +/// Trace the reachable functional graph of the loop-map from the start state: +/// returns (reachable-state count m, cycle-start index j) — transient = s0..s(j-1), +/// cycle = sj..s(m-1) of length m − j. +let private reachableGraph () : int * int = + let c = Chip8.create 0UL + Chip8.loadRom loopRom c + let index = System.Collections.Generic.Dictionary() + let mutable i = 0 + let mutable cycleStart = -1 + let mutable go = true + while go do + let k = keyOf c + match index.TryGetValue k with + | true, j -> cycleStart <- j; go <- false // first repeat ⇒ cycle found + | _ -> + index.[k] <- i + iterate c + i <- i + 1 + (i, cycleStart) // m = i distinct states recorded, cycle starts at cycleStart + +/// The reachable step-map f as an int array on 0..m−1 (f i = i+1, wrapping the last +/// recorded state back to the cycle start). +let private reachableMap () : int[] * int = + let (m, j) = reachableGraph () + let f = Array.init m (fun i -> if i = m - 1 then j else i + 1) + (f, m - j) // (map, cycle length) + +let private fixCount (f: int[]) (k: int) : int64 = + let fk = Array.init f.Length (fun x -> let mutable y = x in (for _ in 1 .. k do y <- f.[y]); y) + Array.init f.Length (fun x -> if fk.[x] = x then 1L else 0L) |> Array.sum + +[] +let ``the real CHIP-8 loop-map has a period-4 orbit (the memory character-loop) plus a transient`` () = + let (f, cycleLen) = reachableMap () + Assert.Equal(4, cycleLen) // V0 = (V0+1) AND 3 ⇒ period 4 + Assert.True(f.Length > cycleLen, "there is a transient state (V1 unset before the first LD)") + +[] +let ``the CHIP-8 dynamical zeta self-verifies: exp(Σ Fix(f^k)u^k/k) = 1/(1 − u^period), and the orbit IS the character loop`` () = + let (f, cycleLen) = reachableMap () + let maxDeg = 12 + // exp side (integer log-derivative recurrence over the REAL VM's reachable map) + let byExp = + let c = Array.zeroCreate (maxDeg + 1) + c.[0] <- 1L + for m in 1 .. maxDeg do + let mutable s = 0L + for k in 1 .. m do s <- s + fixCount f k * c.[m - k] + Assert.True(s % int64 m = 0L, sprintf "recurrence: %d not divisible by %d" s m) + c.[m] <- s / int64 m + c + // orbit-product side: a single orbit of length `cycleLen` ⇒ 1/(1 − u^cycleLen) + // = the geometric series 1 + u^L + u^2L + … (1 exactly at multiples of L). + let byOrbit = Array.init (maxDeg + 1) (fun d -> if d % cycleLen = 0 then 1L else 0L) + for m in 0 .. maxDeg do + Assert.True(byExp.[m] = byOrbit.[m], sprintf "degree %d: exp %d, orbit %d" m byExp.[m] byOrbit.[m]) + Assert.Equal(1L, byExp.[0]) + Assert.Equal(0L, byExp.[cycleLen - 1]) // nothing shorter than the character period + Assert.Equal(1L, byExp.[cycleLen]) // the character loop appears at its period diff --git a/tests/Tests.FSharp/Tests.FSharp.fsproj b/tests/Tests.FSharp/Tests.FSharp.fsproj index 7407e1a1ac..88364040a9 100644 --- a/tests/Tests.FSharp/Tests.FSharp.fsproj +++ b/tests/Tests.FSharp/Tests.FSharp.fsproj @@ -357,6 +357,7 @@ +