diff --git a/archive/2026-07-02/docs/AVM_DERIVATION.md b/archive/2026-07-02/docs/AVM_DERIVATION.md new file mode 100644 index 00000000..2c81065e --- /dev/null +++ b/archive/2026-07-02/docs/AVM_DERIVATION.md @@ -0,0 +1,244 @@ +# 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 |