Research-Stack/0-Core-Formalism/lean/Semantics/TopologicalBraidAdapter_spec.md

TopologicalBraidAdapter.lean — Full LLM Implementation Spec

Architectural note (read first)

Do not modify PVGS_DQ_Bridge.lean. That file correctly maps PVGS → DualQuaternion with w1=0 (abelian / S² sector). This is mathematically correct for pure Gaussian states.

This adapter is the seam. Call adaptPVGS when topological charge is needed. If a better option appears (GKP encoding, direct anyon hardware, etc.), replace this adapter — not the bridge.

The key insight: PVGS_DQ_Bridge sets w1 := Q16_16.zero, which confines the DQ to S² (the equatorial great circle of S³, the abelian sector). SemanticMassPoint.mass provides the missing w1 real component that lifts the state from S² to full S³, enabling non-abelian Fibonacci anyon structure. States with mass > goldenRatioInv (= 40503 in Q16_16 = φ⁻¹) land in the τ anyon sector. States below land in the vacuum sector. This is exactly the toTernary threshold.

---

Task

Write Semantics/Semantics/TopologicalBraidAdapter.lean in the Lean 4 project at /home/allaun/Research Stack/0-Core-Formalism/lean/Semantics/.

This is a bridge/adapter module. It does NOT prove new mathematics. It wires together types that already exist in the codebase and proves that the existing structures are secretly the same mathematical object under different names.

---

Codebase conventions (CRITICAL — follow exactly)

• Language: Lean 4 (Mathlib4), Lean toolchain specified in lean-toolchain file
• Namespace: namespace Semantics.TopologicalBraidAdapter … end Semantics.TopologicalBraidAdapter
• Types: PascalCase. Functions: camelCase. (AGENTS.md §2)
• Fixed-point: Q16_16 = Fix16 with phaseModulus = 65536. Q0.16 values are Nat in [0, 65535].
• No open Classical — do not add it. Do not add haveI DecidableRel when open Classical is in scope.
• Every def must have either a #eval witness or a theorem using it. (AGENTS.md §4)
• Sorries allowed where proofs require genuinely hard tactics, but must be marked with a comment -- ANALYTIC_OPEN: or -- TACTIC_GAP: explaining WHY.
• noncomputable required on any def using ℝ or Real.sqrt. Avoid ℝ; use Q16_16 Nat arithmetic instead.
• Do not use simp on recursive defs — use conv_lhs => unfold instead.
• if_neg for decidable props; dif_neg for dependent if-then-else.

---

Existing files to import (READ THESE FILES before writing — get exact field names)

1. Semantics/Semantics/HydrogenicPhiTorsionBraid.lean — namespace Semantics.HydrogenicPhiTorsionBraid

inductive HardMathKind where
  | yangMillsMassGap | riemannCriticalLine | navierStokesRegularity
  | pVsNp | hodgeCycle | birchSwinnertonDyer

inductive GateDecision where
  | stableSignal | residue | quarantine | noCfdRoute

inductive EquationPart where
  | fibonacciSpine | orbitalGroove | planarSpine | phiTorsion
  | stairLift | strainField | emissionPacket | colorRope

inductive EdgeMode where | tension | compression

structure TensegrityEdge where
  source : EquationPart; target : EquationPart; mode : EdgeMode; restLength : Nat

structure HardProblemState where
  kind            : HardMathKind
  admissibleMass  : Nat   -- Q0.16: evidence mass supporting promotion
  residualRisk    : Nat   -- Q0.16: risk opposing promotion
  proofDebt       : Nat   -- Q0.16: unresolved proof obligations
  continuumPressure : Nat -- Q0.16: CFD/continuum pressure (KZ singularity proximity)
  latticePressure : Nat   -- Q0.16: Sidon lattice separation pressure
  evidenceMass    : Nat   -- Q0.16: verification evidence
  noCfdAllowed    : Bool

structure BraidSample where
  stairIndex      : Nat   -- number of braid crossings (braid word length)
  phase           : Nat   -- Q0.16: fibonacciSpine load
  strain          : Nat   -- Q0.16: phiTorsion load
  constraint      : Nat   -- Q0.16: orbitalGroove constraint (0 = quarantine)
  emittedAmplitude : Nat  -- Q0.16: emissionPacket amplitude

structure ColorRope where
  c : Nat   -- Q0.16: monitor/constraint channel
  m : Nat   -- Q0.16: evidence/verify channel
  y : Nat   -- Q0.16: prune/residual channel (high Y = fray)
  k : Nat   -- Q0.16: action/admissible channel

-- Already defined — call these, do not redefine:
def colorRope         (p : HardProblemState) (s : BraidSample) : ColorRope
def decideGate        (p : HardProblemState) (s : BraidSample) : GateDecision
def tensegrityCoherent(p : HardProblemState) (s : BraidSample) : Bool
def totalTensegrityStrain (p : HardProblemState) (s : BraidSample) (edges : List TensegrityEdge) : Nat
def partLoad          (p : HardProblemState) (s : BraidSample) (part : EquationPart) : Nat
def promotionPressure (p : HardProblemState) (s : BraidSample) : Nat
def residualPressure  (p : HardProblemState) : Nat
def shouldRouteNoCfd  (p : HardProblemState) : Bool
def defaultTensegrity : List TensegrityEdge   -- 6-edge chain
def avgQ0 (a b : Nat) : Nat
def satQ0 (n : Nat) : Nat
def q0Max : Nat := 65535

2. Semantics/Semantics/SLUG3.lean — namespace Semantics.SLUG3

inductive Ternary where
  | low   -- -1: undercrossing / σᵢ⁻¹ / anyon annihilated
  | mid   --  0: identity / no crossing
  | high  -- +1: overcrossing / σᵢ / stable τ anyon

def Ternary.toInt : Ternary → Int
def Ternary.toIdx : Ternary → Nat  -- low→0, mid→1, high→2

structure SLUG3State where
  y : Ternary; u : Ternary; v : Ternary
def SLUG3State.key (s : SLUG3State) : Nat   -- 9*y.toIdx + 3*u.toIdx + v.toIdx

3. Semantics/Semantics/UnitQuaternion.lean — namespace Semantics.UnitQuaternion

READ THIS FILE for exact field names. Known facts:

-- imports Semantics.SLUG3
structure UnitQuaternion where  -- element of S³, fields in Q16_16 (Fix16)
  -- UNKNOWN FIELD NAMES: read the file (likely w, x, y, z)

def slerp (a b : UnitQuaternion) (t : Q16_16) : UnitQuaternion  -- braid holonomy
def chiralIncompatible (a b : UnitQuaternion) : Bool             -- topological obstruction
def toTernary (a b : UnitQuaternion) (threshold : Q16_16) : SLUG3.Ternary
-- threshold goldenRatioInv = 40503: above → τ anyon (high), below → vacuum (mid/low)

4. Semantics/Semantics/DualQuaternion.lean — namespace Semantics.DualQuaternion

READ THIS FILE for exact field names. PVGS_DQ_Bridge.lean line 37 reveals likely names:

-- From PVGS_DQ_Bridge.lean:37:
{ w1 := Q16_16.zero, x1 := Q16_16.zero, y1 := p.μ_re, z1 := p.μ_im ...
-- So DualQuaternion fields are likely: w1, x1, y1, z1, w2, x2, y2, z2
-- Verify in DualQuaternion.lean before using.

5. Semantics/Semantics/GoldenRatioSeparation.lean — namespace Semantics.GoldenRatioSeparation

def goldenRatio    : Nat := 106008  -- φ ≈ 1.618034 in Q16_16
def goldenRatioInv : Nat := 40503   -- φ⁻¹ ≈ 0.618034 in Q16_16
def phaseModulus   : Nat := 65536
-- PROVED: goldenRatioSquared = goldenRatio + phaseModulus  (φ² = φ+1)
def unitSeparated (v : Nat) : Prop := goldenRatioInv < v ∧ v < goldenRatio

6. Semantics/Semantics/TopologyPhinary.lean — namespace Semantics.TopologyPhinary

structure TopoPhinVector where
  bits  : List Bool
  valid : Bool   -- true iff no adjacent 1s (Fibonacci fusion rule enforced)

def mkTopoPhinVector : List Bool → TopoPhinVector
def natToTopoPhin    : Nat → TopoPhinVector
def topoPhinToNat    : TopoPhinVector → Nat
def phinaryAdd       : TopoPhinVector → TopoPhinVector → TopoPhinVector

7. Semantics/Semantics/PVGS_DQ_Bridge.lean — namespace Semantics.PVGS_DQ_Bridge

structure PVGSParams where
  μ_re    : Q16_16
  μ_im    : Q16_16
  ζ_mag   : Q16_16
  ζ_angle : Q16_16
  -- ... (read file for full fields)

-- Maps PVGS → DQ with w1=0 (abelian sector, S² not S³)
-- DO NOT MODIFY THIS FUNCTION
def pvgsToDQ (p : PVGSParams) : DualQuaternion

8. Semantics/Semantics/SemanticMass.lean — namespace Semantics

structure SemanticMassPoint (n : Nat) where
  coord      : Fin n → ℚ   -- manifold coordinates
  mass       : ℚ            -- semantic mass (non-negative) — THIS lifts w1
  binding    : ℚ
  turbulence : ℚ
  routeCost  : ℚ
  velocity   : Fin n → ℚ

def massNonneg (p : SemanticMassPoint n) : Prop := p.mass >= 0

---

What to write: TopologicalBraidAdapter.lean

File path: Semantics/Semantics/TopologicalBraidAdapter.lean

Structure outline

§0   Imports + Namespace
§1   AnyonBraid — finite braid word in B_n
§2   FusionTree — Zeckendorf ↔ anyon fusion basis
§3   B₃ crossing → SLUG3State
§4   BraidSample stairIndex → braid parameters
§5   ColorRope → DualQuaternion mapping (abelian baseline)
§5b  PVGS + SemanticMass → lifted DualQuaternion (τ anyon sector)
§6   GateDecision → topological charge (Ternary)
§7   Quantum dimension bound (φ⁻¹ threshold)
§8   Yang-Baxter coherence theorem
§9   Full pipeline + eval witnesses

---

Section-by-section spec

§0 Imports + Namespace

import Semantics.HydrogenicPhiTorsionBraid
import Semantics.UnitQuaternion
import Semantics.DualQuaternion
import Semantics.SLUG3
import Semantics.GoldenRatioSeparation
import Semantics.TopologyPhinary
import Semantics.PVGS_DQ_Bridge
import Semantics.SemanticMass

namespace Semantics.TopologicalBraidAdapter

open Semantics.HydrogenicPhiTorsionBraid
open Semantics.SLUG3
open Semantics.GoldenRatioSeparation
open Semantics.TopologyPhinary

§1 AnyonBraid

structure BraidCrossing where
  strandIdx : Nat    -- 0 = σ₁, 1 = σ₂, etc.
  positive  : Bool   -- true = overcrossing σᵢ, false = σᵢ⁻¹
  deriving Repr, DecidableEq, BEq

structure AnyonBraid where
  strands : Nat
  word    : List BraidCrossing
  deriving Repr, DecidableEq

def AnyonBraid.length (b : AnyonBraid) : Nat := b.word.length
def AnyonBraid.trivial (n : Nat) : AnyonBraid := { strands := n, word := [] }

def braidFromSample (s : BraidSample) : AnyonBraid :=
  let crossings := List.range s.stairIndex |>.map (fun i =>
    { strandIdx := i % 2, positive := s.phase > s.strain })
  { strands := 3, word := crossings }

§2 FusionTree (Zeckendorf = Fibonacci anyon fusion basis)

Why: Fibonacci fusion rule τ×τ = 1+τ means no two adjacent internal fusion edges can both be τ. This is exactly the Zeckendorf no-adjacent-1s constraint. TopoPhinVector.valid enforces the fusion rule.

def fusionTree (bits : List Bool) : Option TopoPhinVector :=
  let v := mkTopoPhinVector bits
  if v.valid then some v else none

def vacuumSector (n : Nat) : TopoPhinVector :=
  mkTopoPhinVector (List.replicate (if n ≥ 2 then n - 2 else 0) false)

-- Hilbert space dim for n Fibonacci anyons = Fibonacci(n-1)
def fusionSpaceDim : Nat → Nat
  | 0 | 1 | 2 => 1
  | n + 1 => fusionSpaceDim n + fusionSpaceDim (n - 1)

theorem fusionSpaceDim_four  : fusionSpaceDim 4 = 3  := by native_decide
theorem fusionSpaceDim_five  : fusionSpaceDim 5 = 5  := by native_decide
theorem fusionSpaceDim_six   : fusionSpaceDim 6 = 8  := by native_decide
theorem fusionSpaceDim_eight : fusionSpaceDim 8 = 13 := by native_decide
-- 8 E8 worldlines span a 13-dimensional fusion Hilbert space

§3 B₃ crossing → SLUG3State

Why: B₃ generators σ₁, σ₂ act on strands (0,1) and (1,2). SLUG3State (y,u,v) encodes 3-strand braid state. high=σᵢ, low=σᵢ⁻¹, mid=identity.

def crossingToSLUG3 (c : BraidCrossing) : SLUG3State :=
  let sign := if c.positive then Ternary.high else Ternary.low
  match c.strandIdx % 2 with
  | 0 => { y := sign, u := .mid, v := .mid }
  | _ => { y := .mid, u := sign, v := .mid }

def identitySLUG3 : SLUG3State := { y := .mid, u := .mid, v := .mid }

def composeSLUG3 (a b : SLUG3State) : SLUG3State :=
  let fuse : Ternary → Ternary → Ternary
    | .high, .high => .high  | .low, .low  => .high
    | .high, .low  => .low   | .low, .high => .low
    | x,     .mid  => x      | .mid, y     => y
  { y := fuse a.y b.y, u := fuse a.u b.u, v := fuse a.v b.v }

def braidToSLUG3 (b : AnyonBraid) : SLUG3State :=
  b.word.foldl (fun acc c => composeSLUG3 acc (crossingToSLUG3 c)) identitySLUG3

§4 BraidSample → braid parameters

def sampleToSLUG3 (s : BraidSample) : SLUG3State :=
  braidToSLUG3 (braidFromSample s)

-- Monodromy phase: stairIndex crossings at golden angle φ⁻¹
def accumulatedPhase (s : BraidSample) : Nat :=
  (s.stairIndex * 40503) % 65536   -- 40503 = goldenRatioInv

§5 ColorRope → DualQuaternion (abelian baseline)

Why: Zhang et al. (arXiv:2406.08320) — braid gates live on SU(2)×SU(2) = S³×S³ = DualQuaternion. ColorRope (C,M,Y,K) embeds as Q₁=(C,M) and Q₂=(Y,K) in S³. Q0.16 Nat ∈ [0,65535] maps directly to Q16_16 Fix16 (same bit pattern, both represent [0,1)).

-- ADJUST: use actual Fix16 constructor from FixedPoint.lean
def q016ToFix16 (v : Nat) : Q16_16 := ⟨v⟩

-- w = sqrt(1 - x² - y²) in Q0.16 integer arithmetic
-- ANALYTIC_OPEN: Nat.sqrt is floor; true unit normalization needs exact real sqrt.
def computeW (x y : Nat) : Nat :=
  let xsq := (x * x) / 65536
  let ysq := (y * y) / 65536
  let rem := if xsq + ysq ≤ 65536 then 65536 - xsq - ysq else 0
  Nat.sqrt rem

-- ADJUST field names to match DualQuaternion.lean
-- (PVGS_DQ_Bridge line 37 suggests: w1, x1, y1, z1, w2, x2, y2, z2)
def colorRopeToDualQuat (rope : ColorRope) : DualQuaternion :=
  { w1 := q016ToFix16 (computeW rope.c rope.m)
    x1 := q016ToFix16 rope.c
    y1 := q016ToFix16 rope.m
    z1 := q016ToFix16 0
    w2 := q016ToFix16 (computeW rope.y rope.k)
    x2 := q016ToFix16 rope.y
    y2 := q016ToFix16 rope.k
    z2 := q016ToFix16 0 }

def stateSampleToDualQuat (p : HardProblemState) (s : BraidSample) : DualQuaternion :=
  colorRopeToDualQuat (colorRope p s)

§5b PVGS + SemanticMass → lifted DualQuaternion (τ anyon sector)

Why: PVGS_DQ_Bridge.pvgsToDQ sets w1 := Q16_16.zero, confining the state to S² (abelian sector, equatorial great circle of S³). SemanticMassPoint.mass provides the missing w1 real component that lifts to full S³.

The non-abelian structure is NOT in the Gaussian evolution — it is in the sector label (= mass-determined w1) and the fusion rule that fires when two sectors interact. Gaussian operations evolve within-sector (abelian). Semantic mass determines which sector (topological charge).

States with mass > goldenRatioInv (φ⁻¹ = 40503) → τ anyon sector (Ternary.high).
States with mass ≤ goldenRatioInv → vacuum sector (Ternary.mid or low).
This is the same threshold as toTernary in UnitQuaternion — not a coincidence.

-- Inject semantic mass as w1, renormalizing the DQ.
-- mass is a Q0.16 Nat (0–65535); mass > 40503 = τ anyon sector.
-- ANALYTIC_OPEN: renormalization after injecting w1 requires real sqrt — approximated.
def liftDQWithMass (dq : DualQuaternion) (mass : Nat) : DualQuaternion :=
  let shrink := computeW mass 0   -- scalar shrink for x1 to preserve approx unit norm
  { dq with
    w1 := q016ToFix16 mass
    x1 := q016ToFix16 ((dq.x1.val.toNat * shrink) / 65536) }
  -- ADJUST: use actual DQ field names and Fix16 accessor

-- Top-level PVGS entry point.
-- mass = none  → abelian baseline (w1=0, matches pvgsToDQ exactly)
-- mass = some m → lifted to S³ (w1=m, τ anyon sector if m > 40503)
def adaptPVGS (p : HardProblemState) (s : BraidSample)
    (pvgs : PVGS_DQ_Bridge.PVGSParams) (mass : Option Nat) : BraidAdapterOutput :=
  let baseDQ := PVGS_DQ_Bridge.pvgsToDQ pvgs
  let liftedDQ := match mass with
    | none   => baseDQ
    | some m => liftDQWithMass baseDQ m
  { dq     := liftedDQ
    slug3  := sampleToSLUG3 s
    charge := sampleTopologicalCharge p s
    phase  := accumulatedPhase s }

§6 GateDecision → topological charge

def topologicalCharge (d : GateDecision) : Ternary :=
  match d with
  | .stableSignal => .high   -- τ anyon: topologically protected, quantum dim φ
  | .noCfdRoute   => .high   -- τ anyon in topological sector (KZ singularity avoided)
  | .residue      => .mid    -- vacuum sector, abelian, partial promotion
  | .quarantine   => .low    -- annihilated / forbidden

def sampleTopologicalCharge (p : HardProblemState) (s : BraidSample) : Ternary :=
  topologicalCharge (decideGate p s)

§7 Quantum dimension bound

def hasQuantumDimension (p : HardProblemState) : Prop :=
  p.admissibleMass ≥ goldenRatioInv

theorem stableSignal_implies_coherent (p : HardProblemState) (s : BraidSample) :
    decideGate p s = GateDecision.stableSignal →
    (colorRope p s).coherent = true := by
  intro h
  simp only [decideGate] at h
  -- TACTIC_GAP: unfold if-then-else branches; stableSignal requires .coherent ∧ ...
  -- Try: split_ifs at h with h1 h2 h3; then extract coherent component
  sorry

theorem noCfd_avoids_continuum (p : HardProblemState) (s : BraidSample) :
    decideGate p s = GateDecision.noCfdRoute →
    shouldRouteNoCfd p = true := by
  intro h
  simp only [decideGate] at h
  -- TACTIC_GAP: noCfdRoute is the first branch: if shouldRouteNoCfd p then noCfdRoute
  -- Try: split_ifs at h with h1; exact h1
  sorry

§8 Yang-Baxter coherence

-- Trivially-true core of YBE: load sum commutativity
theorem tensegrity_yang_baxter_bound (p : HardProblemState) (s : BraidSample) :
    tensegrityCoherent p s = true →
    partLoad p s .fibonacciSpine + partLoad p s .phiTorsion =
    partLoad p s .phiTorsion + partLoad p s .fibonacciSpine := by
  intro _; exact Nat.add_comm _ _

-- Non-trivial YBE content: coherence bounds total strain
theorem tensegrity_implies_braid_coherence (p : HardProblemState) (s : BraidSample) :
    tensegrityCoherent p s = true →
    totalTensegrityStrain p s defaultTensegrity ≤
      avgQ0 (satQ0 p.residualRisk) q0Max := by
  intro h
  -- TACTIC_GAP: tensegrityCoherent IS this bound; unfold it
  -- Try: simp only [tensegrityCoherent] at h; exact h
  sorry

§9 Full pipeline + eval witnesses

structure BraidAdapterOutput where
  dq     : DualQuaternion
  slug3  : SLUG3State
  charge : Ternary
  phase  : Nat

def adaptBraidSample (p : HardProblemState) (s : BraidSample) : BraidAdapterOutput :=
  { dq     := stateSampleToDualQuat p s
    slug3  := sampleToSLUG3 s
    charge := sampleTopologicalCharge p s
    phase  := accumulatedPhase s }

def sampleFusionBasis (s : BraidSample) : TopoPhinVector :=
  natToTopoPhin s.stairIndex

-- Eval witnesses (AGENTS.md §4)
#eval fusionSpaceDim 8                              -- Expected: 13
#eval topologicalCharge GateDecision.stableSignal   -- Expected: high
#eval topologicalCharge GateDecision.quarantine     -- Expected: low
#eval (50000 : Nat) ≥ goldenRatioInv               -- Expected: true
#eval (List.range 10).map fusionSpaceDim            -- Expected: [1,1,1,1,2,3,5,8,13,21]
#eval let s : BraidSample := { stairIndex := 5, phase := 50000, strain := 30000,
        constraint := 1, emittedAmplitude := 0 }
      accumulatedPhase s                            -- Expected: 5907
#eval let s : BraidSample := { stairIndex := 0, phase := 0, strain := 0,
        constraint := 1, emittedAmplitude := 0 }
      sampleToSLUG3 s                              -- Expected: {y:=mid, u:=mid, v:=mid}

end Semantics.TopologicalBraidAdapter

---

Mathematical identifications

Codebase	Fibonacci anyon physics	Source
phi_squared : φ²=φ+1	Quantum dimension d_τ²=d_τ+1, so d_τ=φ	Standard TQC
validPhinaryDigits no-adj-1s	Fusion rule τ×τ=1+τ: no two adjacent τ in [1]	Hadjiivanov & Georgiev 2404.01778
phi_pow recurrence (a,b)→(b,a+b)	Fibonacci anyon braid matrix recurrence	ibid.
Tensegrity tension/compression alternation	Overcrossing/undercrossing in braid diagram	Zhang et al. 2406.08320
ColorRope (C,M,Y,K)	4-channel braid invariant (Jones poly at q=e^{2πi/5})	ibid.
shouldRouteNoCfd / noCfdRoute	KZ singularity avoidance (poles at z_i=z_j collisions)	Gu et al. 2112.07195
SLUG3.Ternary {low,mid,high}	B₃: σᵢ=high, σᵢ⁻¹=low, identity=mid	Fan et al. 2210.12145
toTernary threshold = goldenRatioInv	Fibonacci anyon amplitude threshold φ⁻¹	GoldenRatioSeparation Lemma 3.4
fusionSpaceDim = Fibonacci numbers	Hilbert space dim for n anyons = F(n-1)	Kitaev 2003
DualQuaternion (w1…z2) ∈ S³×S³	Two-qubit tetrahedron = SU(2)×SU(2)	Zhang et al.
pvgsToDQ sets w1=0	PVGS lives on S² (abelian sector, equatorial great circle)	PVGS_DQ_Bridge.lean:37
SemanticMassPoint.mass → w1	Lifts S²→S³; mass > φ⁻¹ = τ anyon sector	This codebase

---

Sorries and their status

Location	Type	Reason
stableSignal_implies_coherent	TACTIC_GAP	Unfold nested if-then-else in decideGate
noCfd_avoids_continuum	TACTIC_GAP	First branch condition in decideGate
tensegrity_implies_braid_coherence	TACTIC_GAP	tensegrityCoherent definition unfold
liftDQWithMass renormalization	ANALYTIC_OPEN	Exact unit norm requires real sqrt
DQ field names (w1,x1…)	CODE_GAP	Verify in DualQuaternion.lean
UQ field names	CODE_GAP	Verify in UnitQuaternion.lean
Fix16 constructor ⟨v⟩	CODE_GAP	Verify in FixedPoint.lean

---

Build check

cd "/home/allaun/Research Stack/0-Core-Formalism/lean/Semantics"
lake build Semantics.TopologicalBraidAdapter 2>&1 | head -50

0 errors expected. Sorries OK. If field name errors appear, read DualQuaternion.lean and UnitQuaternion.lean and patch the ADJUST lines.