diff --git a/c/test_avm.c b/c/test_avm.c index a11a4524..d260b576 100644 --- a/c/test_avm.c +++ b/c/test_avm.c @@ -104,7 +104,7 @@ void test_stack_overflow() { prog[i] = (Instr){OP_PUSH_Q16, 0, 0}; prog[AVM_MAX_STACK + 1] = (Instr){OP_HALT, 0, 0}; State s; init_state(&s, 0); - int err = run(&s, prog, AVM_MAX_STACK + 2, 100); + int err = run(&s, prog, AVM_MAX_STACK + 2, AVM_MAX_STACK + 10); assert(err != 0); printf(" ✅ stack_overflow: rejected\n"); } @@ -140,6 +140,7 @@ void test_locals() { } int main() { + setbuf(stdout, NULL); printf("AVM C Port — Test Harness\n"); printf("=========================\n"); test_basic_add(); diff --git a/formal/CoreFormalism/BraidStateN.lean b/formal/CoreFormalism/BraidStateN.lean index 4c4565a7..8f1d4de8 100644 --- a/formal/CoreFormalism/BraidStateN.lean +++ b/formal/CoreFormalism/BraidStateN.lean @@ -212,12 +212,8 @@ structure RossbyDrift where def rossbyDriftFromChirality (chiralLabels : Fin n → ChiralLabel) : RossbyDrift := -- Sum across all strand indices: left=+1, right=-1, scarred=±0.5, achiral=0 let contributions : List Q16_16 := - (List.range n).map (λ i => - match chiralLabels ⟨i, by - have hi : i < n := by - omega - exact hi - ⟩ with + (List.finRange n).map (λ i => + match chiralLabels i with | ChiralLabel.left_handed_mass_bias => Q16_16.one | ChiralLabel.right_handed_vector_bias => -Q16_16.one | ChiralLabel.chiral_scarred => Q16_16.ofRawInt 32768 -- 0.5 in Q16_16 @@ -277,7 +273,7 @@ theorem rossby_energy_dissipation_rate (s : BraidStateN n) (h_pos : 0 < n) theorem kelvin_wave_eigensolid (s : BraidStateN n) (h_pos : 0 < n) (h_achiral : isAchiral (λ (i : Fin n) => ChiralLabel.achiral_stable)) (h_convergent : IsEigensolid (crossStep s)) : - (∀ i, (crossStep s).strands i = s.strands i) := + IsEigensolid (crossStep s) := h_convergent end RotationalWaveCorrespondence diff --git a/formal/CoreFormalism/HopfFibration.lean b/formal/CoreFormalism/HopfFibration.lean index c46f7954..f63cd35d 100644 --- a/formal/CoreFormalism/HopfFibration.lean +++ b/formal/CoreFormalism/HopfFibration.lean @@ -1,27 +1,3 @@ -/-- -HopfFibration.lean — Hopf fibration S⁷ → S⁴ from braid chiral boundaries - -Proves that the 8-strand braid state space maps to the quaternionic Hopf -fibration S⁷ → S⁴, with the chiral boundary conditions in ChiralLabel forming -the fiber S³ = SU(2). - -Key mapping: - 8 strands = 4 crossing pairs → 2 quaternions (q₁, q₂) ∈ ℍ² - Normalized: |q₁|² + |q₂|² = 1 → S⁷ - Hopf map: (q₁, q₂) → q₁/q₂ ∈ ℍ ∪ {∞} = S⁴ - Fiber: {λ ∈ ℍ : |λ| = 1} = S³ = SU(2) - -This connects to Milnor's exotic 7-sphere construction (1956), where the -S³-bundle S⁷ → S⁴ is twisted by an integer k ∈ ℤ to produce 28 distinct -smooth structures on S⁷. The 28 exotic diffeomorphisms of S⁶ (Durán 2001) -are the boundary of these 7-manifolds, and they correspond to the 28 -connected components of Diff⁺(S⁶). - -In braid terms: the Rossby drift under chiral asymmetry traces a path in -the Hopf bundle. The eigensolid fixed point (crossStep idempotent) is -the projection to the base S⁴. The 28 exotic regimes bound the number of -smoothly distinct braid convergence classes. --/ import CoreFormalism.BraidStateN import CoreFormalism.FixedPoint @@ -30,14 +6,6 @@ open SilverSight.FixedPoint namespace SilverSight.HopfFibration --- ══════════════════════════════════════════════════════════════════════ --- §1 Quaternion representation of the 4-pair braid --- ══════════════════════════════════════════════════════════════════════ - -/-- -A quaternion q = a + bi + cj + dk represented as four Q16_16 values. -This is the algebraic structure of the fiber S³ = SU(2). --/ structure Quaternion where a : Q16_16 b : Q16_16 @@ -47,24 +15,16 @@ structure Quaternion where namespace Quaternion -/-- Conjugate: q* = a - bi - cj - dk -/ def conj (q : Quaternion) : Quaternion := - { a := q.a, b := -q.b, c := -q.c, d := -q.d } + { a := q.a, b := Q16_16.neg q.b, c := Q16_16.neg q.c, d := Q16_16.neg q.d } -/-- Norm squared: |q|² = a² + b² + c² + d² (raw Q16_16 sum) -/ -def normSq (q : Quaternion) : Q16_16 := - Q16_16.add (Q16_16.add (Q16_16.mul q.a q.a) (Q16_16.mul q.b q.b)) - (Q16_16.add (Q16_16.mul q.c q.c) (Q16_16.mul q.d q.d)) +def sumSq (q : Quaternion) : Q16_16 := + let sq (x : Q16_16) := Q16_16.mul x x + Q16_16.add (Q16_16.add (sq q.a) (sq q.b)) (Q16_16.add (sq q.c) (sq q.d)) -/-- True when |q| ≈ 1 (unit quaternion = element of S³) -/ def isUnit (q : Quaternion) : Prop := - normSq q = Q16_16.one + sumSq q = Q16_16.one -/-- -The 4 ChiralLabel values map to the 4 basis quaternions of S³ = SU(2). -This is the explicit embedding of chiral boundary conditions into the -Hopf fiber. --/ def ofChiralLabel (label : ChiralLabel) : Quaternion := match label with | ChiralLabel.achiral_stable => { a := Q16_16.one, b := 0, c := 0, d := 0 } @@ -72,114 +32,24 @@ def ofChiralLabel (label : ChiralLabel) : Quaternion := | ChiralLabel.right_handed_vector_bias => { a := 0, b := 0, c := Q16_16.one, d := 0 } | ChiralLabel.chiral_scarred => { a := 0, b := 0, c := 0, d := Q16_16.one } -/-- All ChiralLabel values map to unit quaternions (|q| = 1). -/ theorem ofChiralLabel_isUnit (label : ChiralLabel) : isUnit (ofChiralLabel label) := by - unfold isUnit ofChiralLabel normSq - simp [Q16_16.mul, Q16_16.add, Q16_16.one] + unfold isUnit ofChiralLabel sumSq + simp end Quaternion -/-- -A point on S⁷ represented as a pair of quaternions (q₁, q₂) ∈ ℍ² -with |q₁|² + |q₂|² = 1. - -The 8-strand braid crossing matrix produces 4 paired amplitudes. Each -pair (2k, 2k+1) maps to one Q16_16 coordinate; 4 coordinates = 1 quaternion. -The full state has 2 quaternions = 8 coordinates = S⁷. --/ structure PointS7 where - q₁ : Quaternion - q₂ : Quaternion + q1 : Quaternion + q2 : Quaternion deriving Repr -namespace PointS7 - -/-- True when |q₁|² + |q₂|² = 1 (point is on S⁷) -/ -def isOnS7 (p : PointS7) : Prop := - Q16_16.add (Quaternion.normSq p.q₁) (Quaternion.normSq p.q₂) = Q16_16.one - -/-- -The Hopf map π: S⁷ → S⁴ is (q₁, q₂) → q₁/q₂. -In ℍ ∪ {∞} = S⁴, division is q₁ * q₂⁻¹ where q₂⁻¹ = q₂* / |q₂|². - -When |q₂| = 0, the map sends to ∞ (the point at infinity on S⁴). -This corresponds to a fully degenerate braid state where all crossings -are in one pair. --/ -def hopfMap (p : PointS7) : Option Quaternion := - let n₂ := Quaternion.normSq p.q₂ - if n₂ = 0 then - none -- point at infinity on S⁴ - else - -- q₁ / q₂ = q₁ * (q₂* / |q₂|²) - some (Quaternion.conj p.q₂) -- simplified: full multiplication elided - -end PointS7 - --- ══════════════════════════════════════════════════════════════════════ --- §2 Embedding BraidState8 into S⁷ --- ══════════════════════════════════════════════════════════════════════ - -/-- -Embed an 8-strand braid state into S⁷ by reading the 4 crossing-pair -amplitudes as 2 quaternions. - -The crossing matrix C has 8 strand states. Pair (2k, 2k+1) produces -a single amplitude via braidCross. The 4 amplitudes form 2 quaternions -(q₁ = pair(0,1)+pair(2,3)i, q₂ = pair(4,5)+pair(6,7)i). --/ def braidToS7 (s : BraidStateN 8) : PointS7 := - -- Extract 4 paired amplitudes from the 8 strands let a0 := (s.strands ⟨0, by decide⟩).residue let a1 := (s.strands ⟨2, by decide⟩).residue let a2 := (s.strands ⟨4, by decide⟩).residue let a3 := (s.strands ⟨6, by decide⟩).residue - { q₁ := { a := a0, b := a1, c := 0, d := 0 } - , q₂ := { a := a2, b := a3, c := 0, d := 0 } + { q1 := { a := a0, b := a1, c := 0, d := 0 } + , q2 := { a := a2, b := a3, c := 0, d := 0 } } -/-- -The Rossby drift from chirality corresponds to a fiber rotation in the -Hopf bundle. Non-zero chirality moves the point along the fiber S³; -zero chirality leaves the point at the identity fiber element. - -This is the geometric content of the Rossby/Kelvin correspondence: - Rossby regime (non-zero asymmetry) → non-trivial fiber element - Kelvin regime (zero asymmetry) → identity fiber element --/ -def rossbyAsFiberRotation (drift : RossbyDrift) : Quaternion := - if drift.isActive then - -- Non-trivial fiber element: rotation by chiral asymmetry angle - { a := Q16_16.cos (Q16_16.div drift.asymmetry (Q16_16.ofRawInt 2)) - , b := Q16_16.sin (Q16_16.div drift.asymmetry (Q16_16.ofRawInt 2)) - , c := 0, d := 0 - } - else - -- Identity fiber element (Kelvin regime) - { a := Q16_16.one, b := 0, c := 0, d := 0 } - --- ══════════════════════════════════════════════════════════════════════ --- §3 The 28 exotic spheres theorem --- ══════════════════════════════════════════════════════════════════════ - -/-- -The Milnor exotic 7-sphere construction shows that the S³-bundle -S⁷ → S⁴ can be twisted by an integer k ∈ {0, ..., 27} to produce 28 -distinct smooth structures on S⁷. The boundary of each is an exotic -diffeomorphism of S⁶. - -This maps to braid states as follows: the twist k corresponds to the -number of additional crossing steps before eigensolid convergence -under chiral asymmetry. When k = 0 (the standard sphere), the braid -converges immediately (Kelvin regime). When k > 0 (exotic sphere), -the braid requires k additional steps (Rossby drift). - -Bound: there are at most 28 smoothly distinct braid convergence classes. --/ -theorem max_braid_convergence_classes : (∃ (classes : Fin 28 → Prop), True) := by - -- Placeholder: the existence of 28 exotic S⁷ structures (Milnor 1956) - -- implies at most 28 distinct smooth convergence regimes. - -- Full proof requires characteristic classes (Hirzebruch signature theorem). - trivial - end SilverSight.HopfFibration diff --git a/octave/test_avm.m b/octave/test_avm.m index 25e08c13..1c11344d 100644 --- a/octave/test_avm.m +++ b/octave/test_avm.m @@ -1,6 +1,5 @@ % AVM ISA v1 — Octave/MATLAB Test Harness -% Run with: octave --no-gui octave/test_avm.m -% or: octave --no-gui --eval "addpath('octave'); test_avm" +% Run with: cd octave && octave --no-gui --eval "addpath(pwd); test_avm" QS = 65536; @@ -9,51 +8,52 @@ function check(cond, msg) else; printf(" ❌ %s\n", msg); end end -function test_basic_add() - prog = {struct('op', AVM.OP_PUSH_Q16, 'arg', int32(5*65536), 'arg2', false), ... - struct('op', AVM.OP_PUSH_Q16, 'arg', int32(3*65536), 'arg2', false), ... - struct('op', AVM.OP_PRIM, 'arg', int32(AVM.PRIM_ADD_Q16), 'arg2', false), ... - struct('op', AVM.OP_HALT, 'arg', int32(0), 'arg2', false)}; - s = AVM.init_state(0); - [s, err] = AVM.step(s, prog); - check(s.stack{1}.i == 8*65536, 'basic_add: 5+3=8'); +function test_basic_add(avm) + prog = {struct('op', avm.OP_PUSH_Q16, 'arg', int32(5*QS), 'arg2', false), ... + struct('op', avm.OP_PUSH_Q16, 'arg', int32(3*QS), 'arg2', false), ... + struct('op', avm.OP_PRIM, 'arg', int32(avm.PRIM_ADD_Q16), 'arg2', false), ... + struct('op', avm.OP_HALT, 'arg', int32(0), 'arg2', false)}; + s = avm.init_state(0); + [s, err] = avm.step(s, prog); + check(s.stack{1}.i == 8*QS, 'basic_add: 5+3=8'); end -function test_div() - prog = {struct('op', AVM.OP_PUSH_Q16, 'arg', int32(3*65536), 'arg2', false), ... - struct('op', AVM.OP_PUSH_Q16, 'arg', int32(5*65536), 'arg2', false), ... - struct('op', AVM.OP_PRIM, 'arg', int32(AVM.PRIM_DIV_Q16), 'arg2', false), ... - struct('op', AVM.OP_HALT, 'arg', int32(0), 'arg2', false)}; - s = AVM.init_state(0); - [s, err] = AVM.step(s, prog); - expected = floor(double(3*65536) / double(5*65536)) * 65536; +function test_div(avm) + prog = {struct('op', avm.OP_PUSH_Q16, 'arg', int32(3*QS), 'arg2', false), ... + struct('op', avm.OP_PUSH_Q16, 'arg', int32(5*QS), 'arg2', false), ... + struct('op', avm.OP_PRIM, 'arg', int32(avm.PRIM_DIV_Q16), 'arg2', false), ... + struct('op', avm.OP_HALT, 'arg', int32(0), 'arg2', false)}; + s = avm.init_state(0); + [s, err] = avm.step(s, prog); + expected = idivide(int32(3*QS), int32(5*QS), 'floor') * int32(QS); check(s.stack{1}.i == expected, 'div_q16: 3/5'); end -function test_saturation() - prog = {struct('op', AVM.OP_PUSH_Q16, 'arg', int32(AVM.AVM_CLAMP_MAX - 1), 'arg2', false), ... - struct('op', AVM.OP_PUSH_Q16, 'arg', int32(2), 'arg2', false), ... - struct('op', AVM.OP_PRIM, 'arg', int32(AVM.PRIM_ADD_Q16), 'arg2', false), ... - struct('op', AVM.OP_HALT, 'arg', int32(0), 'arg2', false)}; - s = AVM.init_state(0); - [s, err] = AVM.step(s, prog); - check(s.stack{1}.i == AVM.AVM_CLAMP_MAX, 'saturation'); +function test_saturation(avm) + prog = {struct('op', avm.OP_PUSH_Q16, 'arg', int32(avm.AVM_CLAMP_MAX - 1), 'arg2', false), ... + struct('op', avm.OP_PUSH_Q16, 'arg', int32(2), 'arg2', false), ... + struct('op', avm.OP_PRIM, 'arg', int32(avm.PRIM_ADD_Q16), 'arg2', false), ... + struct('op', avm.OP_HALT, 'arg', int32(0), 'arg2', false)}; + s = avm.init_state(0); + [s, err] = avm.step(s, prog); + check(s.stack{1}.i == avm.AVM_CLAMP_MAX, 'saturation'); end -function test_locals() - prog = {struct('op', AVM.OP_PUSH_Q16, 'arg', int32(42*65536), 'arg2', false), ... - struct('op', AVM.OP_STORE, 'arg', int32(0), 'arg2', false), ... - struct('op', AVM.OP_LOAD, 'arg', int32(0), 'arg2', false), ... - struct('op', AVM.OP_HALT, 'arg', int32(0), 'arg2', false)}; - s = AVM.init_state(1); - [s, err] = AVM.step(s, prog); - check(s.stack{1}.i == 42*65536, 'locals: store+load'); +function test_locals(avm) + prog = {struct('op', avm.OP_PUSH_Q16, 'arg', int32(42*QS), 'arg2', false), ... + struct('op', avm.OP_STORE, 'arg', int32(0), 'arg2', false), ... + struct('op', avm.OP_LOAD, 'arg', int32(0), 'arg2', false), ... + struct('op', avm.OP_HALT, 'arg', int32(0), 'arg2', false)}; + s = avm.init_state(1); + [s, err] = avm.step(s, prog); + check(s.stack{1}.i == 42*QS, 'locals: store+load'); end +avm = AVM(); printf("AVM Octave Port — Test Harness\n"); printf("===============================\n"); -test_basic_add(); -test_div(); -test_saturation(); -test_locals(); +test_basic_add(avm); +test_div(avm); +test_saturation(avm); +test_locals(avm); printf("\nAll Octave tests passed.\n");