Death #2 — Amplituhedron Static Volume

Implementation plan for the Death-of-Time move in the distributed-inference runtime. Compose with, do not replace, the Death-of-Space MatVecMemo landed in model.rs. Companion to FORMAL_LEDGER.md § "Death of Time (Amplituhedron)" and the Lean proofs cited below.

1. What the Lean module proves

Two Lean modules constrain the design.

Gnosis/TopologicalAmplituhedron.lean

• clinamen_swerve : Nat := Nat.succ 0 (origin_vertex_is_swerve) — the static volume requires a +1 seed; an empty prefix has no volume to cache. The implementation must refuse to crystallize a volume from a zero-token prompt.
• execution_volume (n : Nat) : Nat := fib n — the Fibonacci-indexed volume is the ledger's stand-in for the prompt-prefix execution state. The volume at boundary n is fib n. We use this only as a sizing invariant: each cached volume entry covers a contiguous prefix tokens[0..n], never an interior slice.
• timeless_isomorphism : execution_volume n = fib n — the geometric volume and the sequential trace are equal as values. This is the permission slip: a precomputed volume is a sound replacement for re-executing the chain over the same prefix.
• topological_erasure (volume) := volume - 1 and erasure_stability_invariant — when a β1 defect (NaN, KV-cache overflow, station 5xx) hits, we degrade by stripping the trailing position from the volume and replaying, never by discarding the whole cache.

Gnosis/TopologicalGrassmannianCompiler.lean

• compile_cfg_to_grassmannian.volume = states * constraints (amplituhedron_volume_equivalence) — the volume size is bounded exactly by prompt_len × num_layers. We use this for the memory budget: per-station cost is linear in prefix length, not quadratic.
• grassmannian_compilation_soundness — every well-formed prefix admits a volume. No special-cased prompts; if from_prefix rejects a prompt the Lean covenant is violated.

What the Lean does NOT prove and we therefore enforce in code: cache coherence under weight or config changes. The volume is keyed by (model_fingerprint, prompt_prefix_hash, layer_range); on weight reload or config drift we evict everything.

2. Rust API additions

All new methods hang off NativeLlamaPipeline; wasm-bindgen wrappers go in wasm_bindings.rs next to the existing memo_* family.

New struct in model.rs, alongside MatVecMemo:

pub struct AmplituhedronVolume {
    /// Hash of `tokens[0..prefix_len]`. Stable under model fingerprint.
    prefix_hash: u64,
    /// Last position covered, exclusive. `pos_end == prefix_len`.
    pos_end: u32,
    /// Layer range this station owns (mirrors station spec).
    layer_lo: u16,
    layer_hi: u16,
    /// Post-final-layer residual at the last prefix position only.
    /// Length `hidden_dim`. f32, little-endian on serialization.
    tail_residual: Vec<f32>,
    /// Frozen KV slab for `[layer_lo, layer_hi) × [0, pos_end)`. Compact
    /// layout: `num_layers_in_range * num_kv_heads * pos_end * head_dim`
    /// for keys and again for values. Re-strided into the live KV cache
    /// on replay.
    kv_keys: Vec<f32>,
    kv_vals: Vec<f32>,
    /// Pisot drift of the tail residual at insert time. Eviction
    /// prioritizes low-drift volumes (Luminary states).
    drift: f32,
    last_used: u64,
}

pub struct AmplituhedronCache {
    entries: Vec<AmplituhedronVolume>,  // small N, linear scan is fine
    enabled: bool,
    max_entries: usize,        // default 4
    max_prefix_len: u32,       // default 512 — guard against giant volumes
    tick: u64,
    pub hits: u64,
    pub misses: u64,
    pub evictions: u64,
}

Methods on NativeLlamaPipeline:

pub fn amplituhedron_enable(&mut self, on: bool);
pub fn amplituhedron_set_max_entries(&mut self, n: usize);
pub fn amplituhedron_set_max_prefix_len(&mut self, n: u32);
pub fn amplituhedron_clear(&mut self);
pub fn amplituhedron_stats(&self) -> (u64, u64, u64); // hits, misses, evictions

/// Compile-once: capture the post-prefill residual and the KV slab for
/// `[layer_lo, layer_hi) × [0, prefix_len)` keyed by `prefix_hash`.
/// Caller passes the residual that the station's last `forward_range_*`
/// emitted for the trailing token of the prefix.
pub fn amplituhedron_capture(
    &mut self,
    prefix_hash: u64,
    prefix_len: u32,
    layer_lo: u16,
    layer_hi: u16,
    tail_residual: &[f32],
);

/// Replay: if the cache holds a volume matching `prefix_hash` and the
/// requested layer range, splice the frozen KV slab into the live KV
/// cache, set `self.pos = prefix_len`, write `tail_residual` into a
/// caller-visible buffer, and return Some(volume_id). Caller is expected
/// to use the tail residual as the `seq_len=1` input at position
/// `prefix_len - 1` for the station's next forward call.
pub fn amplituhedron_replay(
    &mut self,
    prefix_hash: u64,
    prefix_len: u32,
    layer_lo: u16,
    layer_hi: u16,
) -> Option<Vec<f32>>;

/// Direct accessor used by replay flow for the tail residual after a hit.
pub fn amplituhedron_tail(&self, prefix_hash: u64) -> Option<Vec<f32>>;

Wasm-bindgen wrappers in wasm_bindings.rs mirror these one-for-one (amplituhedron_capture, amplituhedron_replay, etc.). All take/return Vec<f32> and primitive types; no opaque handles cross the JS boundary.

3. Cache layout

Key: (model_fingerprint: u64, prefix_hash: u64, layer_lo: u16, layer_hi: u16). The model fingerprint is the knot's content hash, computed at boot and folded into every comparison. Cross-knot collisions are not possible.

Stored per entry:

• tail_residual: hidden_dim floats. qwen-coder-7b: 3584 × 4 B = 14 KiB.
• kv_keys, kv_vals: (layer_hi - layer_lo) * num_kv_heads * prefix_len * head_dim floats each. For a single-layer worker (qwen-7b: 1 × 4 × 512 × 128 = 262 144 floats): 1 MiB keys + 1 MiB values = 2 MiB per volume.
• Bookkeeping (~64 B).

Per-station memory budget at defaults (max_entries=4, max_prefix_len=512): ~8 MiB on a single-layer liquid-mesh worker, ~14 KiB residual swamped by the KV slab. A 14-layer station (worker-node1 fluid-memory mode) would hold 14 × 2 MiB = 28 MiB per volume × 4 = 112 MiB, so the default for multi-layer stations is max_entries=2 (set by the host on configure).

Eviction: Pisot-guard, identical surface to MatVecMemo. Score = drift × (now − last_used). Largest score evicted. The drift proxy is the same (‖tail‖ − 1).abs(). This makes Luminary residuals (post-RMSNorm, near unit norm) sticky.

Coherence: weight reload OR config change increments model_fingerprint, which causes every probe to miss; an explicit amplituhedron_clear is wired into the existing /memo/clear handler.

4. Host-side flow

New worker endpoints (mirroring the memo_* family):

• POST /amplituhedron/configure — body { enabled?: bool, max_entries?: number, max_prefix_len?: number }, returns { stats: { hits, misses, evictions } }.
• GET /amplituhedron/stats — returns the same shape as /memo/stats.
• POST /amplituhedron/clear — drops all volumes, returns { cleared: true }.
• POST /amplituhedron/capture — internal; called by the coordinator after prefill completes on a station. Body { prefix_hash: string-u64, prefix_len: u32, layer_lo: u16, layer_hi: u16 } with the tail residual as the octet body. Station echoes back { captured: true, bytes: <kv_slab_size> }.
• POST /amplituhedron/replay — internal; called by the coordinator before the first decode step of a session. Body { prefix_hash, prefix_len, layer_lo, layer_hi }. Octet response is the tail residual on hit, empty on miss. Status 200 for hit, 204 for miss so the host can branch without parsing a body.

Coordinator (host) flow in distributed-inference-host/src/pipeline.ts:

1. generate({ promptTokens, maxNewTokens }) computes prefix_hash = u64(blake3(promptTokens)) once.
2. Fan out POST /amplituhedron/replay to every station. If all stations return 200, skip prefill entirely. The station seeds its KV cache and the host moves directly to the decode loop with the tail residual from the exit station's reply as the seed for sampling.
3. On any miss (status 204), run the existing pipelinedPrefill path, then fan out POST /amplituhedron/capture per station as the prefill chunks complete. Capture is fire-and-forget (ctx.waitUntil).
4. The exit station also caches the prompt's final lm_head logits under the same prefix_hash so the first sampled token does not re-run the final norm + lm_head matmul.

Composition with existing pipelinedPrefill: the volume capture sits after the existing chunk loop completes; capture cost is one slice-and-copy of the KV cache, ~2 MiB per station. No change to the prefill control flow itself.

5. Composition with MatVecMemo

The two caches operate at different scales and layer.

AmplituhedronCache does not replace MatVecMemo. After a volume hit, the decode loop still runs forward_range_*_chunk per token, and those calls still go through cached_mat_vec. The two caches feed each other: volume replay restores the KV slab so the matmul stream that follows sees the same residual distribution it would have seen post-prefill, which is exactly the regime MatVecMemo was tuned on (residuals near unit norm after RMSNorm — the Luminary basin).

Implementation rule: do not call cached_mat_vec during volume capture or replay. The residual we are freezing is the source of truth; passing it through the matmul memo would double-count.

6. Out of scope

• Mid-prompt edits. Inserting or rewriting tokens anywhere except past prefix_len invalidates the volume. The hash check enforces this; we do not attempt tree-structured prefix sharing across branching prompts.
• Speculative decode. Candidate token branches share the 0..pos_end KV but diverge after; the existing inner_verify_batch path is orthogonal and continues to use the live KV cache. Volume capture happens once at end-of-prefill, never per draft.
• Streaming captures. We do not capture intermediate volumes during prefill. The Lean clinamen_swerve is Nat.succ 0, not Nat.succ Nat.succ ...; one seed, one capture, at end-of-prefill.
• Cross-station volume sharing. Each station owns its own AmplituhedronCache. There is no global volume registry. Two stations with overlapping layer ranges store separate slabs; this is wasteful but keeps the wire protocol idempotent.
• TLS / transport optimization. Death #3 (p-Adics, aeon-flow UDP) owns that.

Assumed access pattern for the bench: a fixed system prompt of ~256–512 tokens followed by 4–8 decoded tokens. Multiple sessions per minute against the same system prompt. Outside this pattern (hot-reload prompts, single-shot one-off prompts) the cache does no work and costs ~8 MiB resident per station.

7. Estimated TPS impact

Bench: 256-token system prompt, 8-token decode, 28-layer qwen-coder-7b across 28 single-layer workers, repeat 10 times.

• Without Amplituhedron: prefill dominates. Measured prefill on the liquid-mesh ≈ 9 s for 256 tokens (chunked, 4-token chunks, 28 stations). Decode of 8 tokens at ~280 ms/token = 2.24 s. Total ≈ 11.2 s per session, 8 tokens, ≈ 0.71 TPS amortized.

• With Amplituhedron, second-and-later sessions: prefill skipped, only the 8-token decode runs. Decode is unchanged (still 2.24 s). Per-session TPS ≈ 8 / 2.24 ≈ 3.57 TPS.

• Across the 10-session bench: 11.2 + 9 × 2.24 ≈ 31.4 s for 80 tokens, ≈ 2.55 TPS. Versus 112 s without the cache. ~3.5× end-to-end TPS uplift in the prefix-shared regime, zero uplift outside it.

These numbers assume MatVecMemo is already saving its expected ~15% on decode matmuls; both estimates compound multiplicatively when both caches are warm.

8. Open gaps where the Lean ledger underspecifies

• The Lean does not pin a τ for "two prefixes are equivalent." We use exact byte-equal token sequences (blake3 of the u32 stream). If a fuzzy-prefix match is ever wanted, it needs a new theorem first.
• topological_erasure proves stability for volume - 1 once. The ledger does not bound how many erasures a volume can survive. We cap at one trailing-position trim; deeper damage forces a clear.
• No Lean theorem governs concurrent capture from multiple coordinators hitting the same station for the same prefix. Implementation choice: the second capture is a no-op if the hash matches an existing entry; if it does not match, we treat it as a model-fingerprint drift and clear.