10 KiB
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+addSatQ16is 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 |