mirror of
https://github.com/allaunthefox/SilverSight.git
synced 2026-07-31 01:25:21 +00:00
Remove AVM_DERIVATION.md
This commit is contained in:
Allaun Silverfox
parent
cca929b61c
commit
fc7d5a89ae
1 changed files with 0 additions and 244 deletions
|
|
@ -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 |
|
||||
Loading…
Add table
Reference in a new issue