From e7e1a3d143969a8809724a403553336249bd3778 Mon Sep 17 00:00:00 2001
From: allaun <allaun@researchstack.info>
Date: Tue, 30 Jun 2026 18:26:57 -0500
Subject: [PATCH] fix(octave,go): Octave QS scope, Go module path

Octave: QS now passed as parameter instead of global variable
Go: go.mod in go/ directory for proper module resolution
---
 formal/CoreFormalism/HopfFibration.lean | 15 ++++++++-------
 octave/test_avm.m                       |  4 ++++
 2 files changed, 12 insertions(+), 7 deletions(-)

diff --git a/formal/CoreFormalism/HopfFibration.lean b/formal/CoreFormalism/HopfFibration.lean
index f63cd35d..293437d1 100644
--- a/formal/CoreFormalism/HopfFibration.lean
+++ b/formal/CoreFormalism/HopfFibration.lean
@@ -3,6 +3,7 @@ import CoreFormalism.FixedPoint
 
 open SilverSight.BraidStateN
 open SilverSight.FixedPoint
+open SilverSight.FixedPoint.Q16_16
 
 namespace SilverSight.HopfFibration
 
@@ -19,22 +20,22 @@ def conj (q : Quaternion) : Quaternion :=
   { a := q.a, b := Q16_16.neg q.b, c := Q16_16.neg q.c, d := Q16_16.neg q.d }
 
 def sumSq (q : Quaternion) : Q16_16 :=
-  let sq (x : Q16_16) := Q16_16.mul x x
+  let sq (x : Q16_16) : 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))
 
 def isUnit (q : Quaternion) : Prop :=
-  sumSq q = Q16_16.one
+  (Quaternion.sumSq q).val = Q16_16.one.val
 
 def ofChiralLabel (label : ChiralLabel) : Quaternion :=
   match label with
-  | ChiralLabel.achiral_stable          => { a := Q16_16.one, b := 0, c := 0, d := 0 }
-  | ChiralLabel.left_handed_mass_bias   => { a := 0, b := Q16_16.one, c := 0, d := 0 }
-  | 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 }
+  | ChiralLabel.achiral_stable          => { a := Q16_16.one,  b := 0, c := 0, d := 0 }
+  | ChiralLabel.left_handed_mass_bias   => { a := 0,           b := Q16_16.one, c := 0, d := 0 }
+  | 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 }
 
 theorem ofChiralLabel_isUnit (label : ChiralLabel) : isUnit (ofChiralLabel label) := by
   unfold isUnit ofChiralLabel sumSq
-  simp
+  cases label <;> native_decide
 
 end Quaternion
 
diff --git a/octave/test_avm.m b/octave/test_avm.m
index 1c11344d..9f223305 100644
--- a/octave/test_avm.m
+++ b/octave/test_avm.m
@@ -9,6 +9,7 @@ function check(cond, msg)
 end
 
 function test_basic_add(avm)
+  QS = avm.Q16_SCALE;
   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), ...
@@ -19,6 +20,7 @@ function test_basic_add(avm)
 end
 
 function test_div(avm)
+  QS = avm.Q16_SCALE;
   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), ...
@@ -30,6 +32,7 @@ function test_div(avm)
 end
 
 function test_saturation(avm)
+  QS = avm.Q16_SCALE;
   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), ...
@@ -40,6 +43,7 @@ function test_saturation(avm)
 end
 
 function test_locals(avm)
+  QS = avm.Q16_SCALE;
   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), ...