diff --git a/docs/AVM_DERIVATION.md b/docs/AVM_DERIVATION.md deleted file mode 100644 index 2c81065e..00000000 --- a/docs/AVM_DERIVATION.md +++ /dev/null @@ -1,244 +0,0 @@ -# AVM ISA Value Derivation - -Every AVM constant traces back to one of the **4 fundamental equations** -(`UnifiedCovariant.lean:12-24`). No parameter tuning. No magic numbers. - ---- - -## The 4 Fundamental Equations - -| ID | Equation | Domain | Source | -|----|----------|--------|--------| -| **I₁** | φ² − φ − 1 = 0 | Golden ratio braid scaling | Braid crossing operator | -| **I₂** | σ − τ = 17/1792 > 0 | Spectral gap positivity | Cartan connection weights | -| **I₃** | F₇ = 13, F₈ = 21 | Fibonacci Temperley-Lieb dimensions | TL quotient | -| **I₄** | 2^a + 2^b = 2^c + 2^d ⇒ {a,b} = {c,d} | Sidon address uniqueness | Binary expansion | - -### Constants derived from I₂ - -``` -σ = 9984/65536 = 39/256 spectral radius (Cartan diagonal weight) -τ = 1/7 spectral threshold (chaotic floor) -D = lcm(7, 256) = 1792 exact integer denominator -σ·D = 39 × 7 = 273 integer LHS -τ·D = 1 × 256 = 256 integer RHS -gap = 273 − 256 = 17 signed integer difference -σ − τ = 17/1792 exact rational gap -``` - -### Domain provenance - -| Constant | Origin | Equation | -|----------|--------|----------| -| 7 | Sidon doublings (2→128, 7 steps) | I₂, I₄ | -| 256 = 2⁸ | 8-strand braid, 8-bit precision | I₄ | -| 1792 = 7 × 256 | LCM of denominators | I₂ | -| 39 = (7+1)(7+1)/2 − 1 | Cartan C₂ weight | I₂ | -| 9984 = 39 × 256 | σ in Q16_16 units | I₂ | - ---- - -## Derivation: AVM Types - -| Type | Derivation | Equation | -|------|-----------|----------| -| `Q16_16` | Crossing weights (39/256, 1/7), spectral gap (17/1792) require 16 integer + 16 fraction bits | I₂ | -| `Q0_16` | Simplex probabilities (p ∈ [0,1]) for Fisher metric on Δ₇ | I₁ (Chentsov forces Fisher) | -| `Bool` | Comparison results for eigensolid detection, Sidon uniqueness | I₄ | - -**Why not more types?** The 3-type universe is the minimum needed to represent: -- The C crossing matrix (Q16_16 entries) -- Tangent vectors on Δ₇ (Q0_16 simplex) -- Sidon comparisons and gap detection (Bool) - -No UInt8, Int32, or Float types — they are not needed for any equation I₁–I₄. - ---- - -## Derivation: 11 Primitives - -### Q16_16 arithmetic (6 primitives from I₂ + I₄) - -| Primitive | Needed for | Equation | -|-----------|-----------|----------| -| `addSatQ16` | Accumulate crossing weights; `C[i,k]·X[k]` sum | I₂ | -| `subSatQ16` | Receipt normalization; `e_i − e_j` tangent vectors | I₂ | -| `mulSatQ16` | Crossing matrix × state vector: `(C·s)_i = Σ C[i,j]·s[j]` | I₂, I₄ | -| `divSatQ16` | Receipt dimension scaling; `× 65536` in div | I₂ | -| `ltQ16` | Spectral gap check: `σ − τ > 0`, eigensolid detection | I₂ | -| `eqQ16` | Fixed-point check: `crossStep(s) = s` | I₂ | - -All Q16_16 operations are **saturating** (not wrapping). Saturation ensures -`crossStep(s) = s` has a unique fixed point — wrapping would create aliases. - -### Q0_16 arithmetic (2 primitives from I₁ + Chentsov) - -| Primitive | Needed for | Equation | -|-----------|-----------|----------| -| `addSatQ0` | Probability accumulation on Δ₇ | I₁ | -| `subSatQ0` | Tangent vector difference; Fisher metric | I₁ | - -### Boolean logic (3 primitives from I₄) - -| Primitive | Needed for | Equation | -|-----------|-----------|----------| -| `and` | Gap condition: `gap(s) ∧ gap(e)` | I₄ | -| `or` | Control flow; type checking | I₄ | -| `not` | Complement; cross-block detection | I₄ | - -### Why these 11 and no more? - -- **No `sqrt`**: The spectral gap is rational (17/1792). No irrational spectral - computation is required for the PIST classification gate. -- **No `abs`**: Crossing weights are non-negative; Sidon uniqueness (I₄) is - a boolean condition, not a magnitude. -- **No `sin`/`cos`**: Phase accumulation is linear (crossing sum, not - trigonometric). Trigonometric functions are pulled in at the Hopf fibration - layer (HopfFibration.lean), not the AVM ISA. -- **No `fma`**: `mulSatQ16` + `addSatQ16` is sufficient — the crossing matrix - has max 2 non-zero entries per row (block-diagonal from I₄). - ---- - -## Derivation: 10 Instructions - -| Instruction | Needed for | Derivation | -|-------------|-----------|------------| -| `push` | Stack-based evaluation model | Minimal formal semantics | -| `pop` | Discard computed value | Stack management | -| `dup` | Duplicate for paired operations | Sidon pair comparison (I₄) | -| `swap` | Reorder operands | Binary operation order | -| `load` | Read local variables | Crossing matrix row cache | -| `store` | Write local variables | Accumulator update | -| `jump` | Loop for braid steps (k iterations) | Eigensolid convergence loop | -| `jumpIf` | Conditional branch on gap condition | `σ − τ > 0` check (I₂) | -| `prim` | Dispatch arithmetic primitives | Finite closed-world dispatch | -| `halt` | Termination | Total execution guarantee | - -**Why stack-based?** Stack semantics have the simplest formal model: -- `step(program, state)` is a structural induction on the instruction list -- No register allocation needed in the formal proof -- Trivially cross-language (every language has lists) -- Fuel argument gives a total run function - -**Why 10?** This is the minimum usable set: -- 4 stack ops (push, pop, dup, swap) -- 2 memory ops (load, store) -- 2 control flow ops (jump, jumpIf) -- 1 primitive dispatch (prim) -- 1 termination (halt) - -No `call`/`ret`: the braid loop is a straight-line pipeline (no dynamic -dispatch). Jump + locals is sufficient for all finite-state programs -needed by I₁–I₄. - ---- - -## Derivation: Scaling Constants - -| Constant | Value | Derivation | Equation | -|----------|-------|-----------|----------| -| `65536` | 2¹⁶ | Standard Q16_16 fraction bits; enough to resolve 17/1792 ≈ 0.0095 to 3.5 bits of precision | I₂ | -| `2147483647` | INT32_MAX | Symmetric upper bound for saturated arithmetic; guarantees `neg(neg(x)) = x` | I₂ (receipt invertibility) | -| `−2147483647` | −(INT32_MAX) | Symmetric lower bound; INT32_MIN (−2147483648) excluded because `neg(INT32_MIN) = INT32_MIN` | I₂ | -| `32767` | INT16_MAX / 2 | Q0_16 symmetric bound for simplex probabilities | I₁ | -| `−32767` | −32767 | Symmetric; INT16_MIN excluded for same negation-involution reason | I₁ | -| `1024` | stack depth | ~12 KB max (1024 × ~12 bytes), fits L1 cache | I₂ (k ≤ 1024 for braid loops) | -| `9984` | 39 × 256 | `σ` in Q16_16 raw units: `9984/65536 = 39/256` | I₂ | -| `273` | 39 × 7 | `C_int[i,i]` = 1792 × σ in the integer bypass | I₂ | -| `256` | 2⁸ | `C_int[i,j]` = 1792 × τ for paired strands | I₂, I₄ | - ---- - -## Derivation: Crossing Matrix Structure - -From I₂ + I₄, the crossing weight matrix C has a fixed block-diagonal structure: - -``` -C[i,j] = - σ = 39/256 if i = j (I₂: diagonal) - τ = 1/7 if i/2 = j/2, i ≠ j (I₂: same-block off-diagonal) - 0 if i/2 ≠ j/2 (I₄: cross-block zero) -``` - -This is not an approximation — it is forced by the Sidon pair structure (I₄): -strand pairs (0,1), (2,3), (4,5), (6,7) are the only interacting pairs. -All cross-block entries are structurally zero. - -The 4 disjoint 2×2 blocks mean every matrix-vector multiply requires at most -2 multiplications and 1 addition per row — hence the primitive set needs only -`addSatQ16`, `mulSatQ16`, and no `fma` or vector primitives. - ---- - -## Derivation: Symmetric Clamping (Negation Involution) - -Receipt invertibility (`decode(encode(s)) = s`) requires every operation to -have a well-defined inverse. For negation, this means: - -``` -∀ x ∈ AVM.values: neg(neg(x)) = x -``` - -Standard INT32_MIN (−2147483648) fails: `neg(INT32_MIN) = INT32_MIN` (wraps). - -Fix: clamp to [−2147483647, 2147483647] instead of INT32 full range. -Now `neg(neg(x)) = x` for every representable value. - -This is not a cosmetic choice — it is required by **I₂** (receipt invertibility -for the crossing matrix). Without symmetric clamping, receipt decoding would -have a branching condition for the INT32_MIN case, which would break the -bijection proof. - ---- - -## Derivation: Fuel and Totality - -Every AVM program must terminate. The `run` function takes a `Fuel` parameter: - -``` -run : Fuel → Program → State → Outcome State -``` - -The braid loop converges in at most k ≤ 1024 steps (empirically from the -spectral gap: `σ − τ = 17/1792 ≈ 0.95% contraction per step`, so -`(1775/1792)^k ≤ ε` gives k ≤ 1024). The fuel bound of 1024 comes from this -contraction rate. - ---- - -## Summary: What Is Not Tunable - -| AVM feature | Tuning? | Why | -|-------------|---------|-----| -| 3 types | No | Minimum to represent I₁–I₄ | -| 11 primitives | No | Minimum closed-world for C matrix + Bool | -| 10 instructions | No | Minimum for stack-based execution | -| 65536 scale | No | Standard Q16_16; 2¹⁶ fraction bits | -| 1792 denominator | No | lcm(7, 256) from I₂ | -| 17/1792 gap | No | σ − τ = 39/256 − 1/7, exact rational | -| Symmetric clamping | No | Required by negation involution | -| Stack depth 1024 | No | Bounded by contraction rate | -| Block-diagonal C matrix | No | Forced by Sidon pair structure (I₄) | -| Saturating arithmetic | No | Required for unique fixed point | -| No CALL/RET | No | No dynamic dispatch in braid pipeline | -| No Float | No | Float breaks associativity, breaks invertibility | - -Every AVM value and design decision traces back to one of the 4 equations. -If an AVM value cannot be linked to I₁, I₂, I₃, or I₄, it is a bug. - ---- - -## References - -| File | Content | -|------|---------| -| `formal/SilverSight/PIST/UnifiedCovariant.lean` | 4 fundamental equations (I₁–I₄) | -| `formal/SilverSight/PIST/CartanConnection.lean` | Integer bypass using D = 1792 | -| `formal/SilverSight/PIST/YangBaxter.lean` | 2×2 Sidon crossing block B | -| `formal/SilverSight/AVMIsa/Instr.lean` | 11 primitives, 10 instructions | -| `formal/SilverSight/AVMIsa/Step.lean` | Step semantics, symmetric clamping | -| `formal/SilverSight/AVMIsa/Types.lean` | 3-type universe | -| `docs/avm_isa_audit.md` | Wolfram Alpha arithmetic audit | -| `docs/reviews/CARTAN_CONNECTION_FORMULA.md` | Cartan connection formula derivation | -| `docs/reviews/SIDON_ORTHOGONALITY_BYPASS_FORMULA.md` | Spectral gap derivation |