2026-08-20 12:57:29 +00:00
49 changed files with 1718 additions and 1536 deletions
--- a/.atlas/benchmark.sh
+++ b/.atlas/benchmark.sh
@ -1,30 +0,0 @@
 #!/usr/bin/env bash
 # Generated by `atlas autoresearch` — this file is YOURS, edit it freely.
 #
 # Contract: write {"score": <float>, "examples": [...]} to $ATLAS_OPTIMIZE_RESULT.
 # The candidate artifact has already been written into this worktree at
 #   ${ATLAS_OPTIMIZE_TARGET}   (the repo-relative path: 4-Infrastructure/shim/braid_search.py)
 # so the only thing a candidate can change is that file — the optimizer runs
 # every candidate in its own throwaway git worktree, which keeps the evaluator
 # and data pinned. score.py turns the run's output into the score; .atlas/gate.sh
 # is the Goodhart guard.
 set -uo pipefail
 HERE="$(cd "$(dirname "${BASH_SOURCE[0]}")" && pwd)"
 OUT="$(mktemp)"
 # --- the repo's run command (auto-detected) --------------------------------
 # Edit this line if the campaign should run something different.
 TARGET="${ATLAS_OPTIMIZE_TARGET:-$1}"
 ( python3 "$TARGET" ) >"$OUT" 2>&1
 RC=$?
 # ---------------------------------------------------------------------------
 if [ "$RC" -ne 0 ]; then
  echo "[benchmark] run command exited $RC — candidate failed" >&2
  tail -n 40 "$OUT" >&2
  exit "$RC"
 fi
 # Parse the optimized metric out of the run output (edit .atlas/score.py to
 # change which number is read, or to emit richer per-example feedback).
 python3 "$HERE/score.py" --stdout "$OUT"
--- a/.atlas/gate.sh
+++ b/.atlas/gate.sh
@ -1,23 +0,0 @@
 #!/usr/bin/env bash
 # Generated by `atlas autoresearch` — the Goodhart guard.
 #
 # A candidate may only change the artifact under test. If a run modifies any
 # OTHER tracked file (e.g. rewrites the evaluator or test data to fake a pass),
 # this gate fails (exit non-zero) and the candidate is scored worst, so the
 # Pareto front never elevates a cheat. Relax IGNORE_RE if your run legitimately
 # rewrites tracked files (checkpoints, logs, and .atlas/ are already ignored).
 set -uo pipefail
 WT="${1:-$PWD}"
 TARGET="${ATLAS_OPTIMIZE_TARGET:-$2}"
 REL="${TARGET#"$WT"/}"
 IGNORE_RE='^(outputs/|out/|checkpoints/|runs/|wandb/|\.atlas/|.*\.log$|.*\.ckpt$|.*\.pt$|.*\.bin$|.*\.safetensors$)'
 CHANGED="$(git -C "$WT" status --porcelain --untracked-files=no 2>/dev/null \
  | sed 's/^...//' \
  | { [ -n "$REL" ] && grep -vF -- "$REL" || cat; } \
  | grep -Ev "$IGNORE_RE" || true)"
 if [ -n "$CHANGED" ]; then
  echo "[gate] the run modified tracked files other than the candidate:" >&2
  echo "$CHANGED" >&2
  exit 1
 fi
 exit 0
--- a/.atlas/score.py
+++ b/.atlas/score.py
@ -1,73 +0,0 @@
 #!/usr/bin/env python3
 import argparse, json, os, re, sys
 METRICS = {
    "find_optimal_crossing": False,
    "SA direct": False,
 }
 def parse(text):
    results = {}
    for name, higher in METRICS.items():
        pat = re.compile(re.escape(name) + r"\s*[:=]?\s*([+-]?[0-9]*\.?[0-9]+)")
        for m in pat.finditer(text):
            raw = m.group(0).strip()
            val = float(m.group(1))
            line_before = text[max(0, m.start()-80):m.start()].split("\n")[-1].strip()
            results[name] = (val, higher, raw, line_before)
    return results
 def main():
    ap = argparse.ArgumentParser()
    ap.add_argument("--stdout", required=True)
    args = ap.parse_args()
    text = open(args.stdout, encoding="utf-8", errors="replace").read()
    parsed = parse(text)
    if "find_optimal_crossing" not in parsed:
        sys.stderr.write(f"[score] could not find metric in output.\n")
        sys.exit(3)
    primary_name = "find_optimal_crossing"
    primary_val, _, primary_raw, ctx = parsed[primary_name]
    direction = "lower is better"
    examples = [{
        "id": primary_name,
        "score": primary_val,
        "pass": True,
        "feedback": f"{primary_raw} | context: {ctx}" if ctx else primary_raw,
    }]
    if "SA direct" in parsed:
        sa_val, _, sa_raw, sa_ctx = parsed["SA direct"]
        examples.append({
            "id": "SA direct",
            "score": sa_val,
            "pass": sa_val < 100,
            "feedback": f"{sa_raw} | context: {sa_ctx}" if sa_ctx else sa_raw,
        })
    diag_lines = []
    for line in text.strip().split("\n"):
        stripped = line.strip()
        if "find_optimal_crossing" in stripped or "SA direct" in stripped:
            diag_lines.append(stripped)
    diagnostic = "; ".join(diag_lines) if diag_lines else primary_raw
    result = {
        "score": primary_val,
        "examples": examples,
        "feedback": f"find_optimal_crossing={primary_val} ({direction}) | {diagnostic}",
    }
    out = os.environ.get("ATLAS_OPTIMIZE_RESULT")
    payload = json.dumps(result)
    if out:
        with open(out, "w") as fh:
            fh.write(payload)
    else:
        sys.stdout.write(payload)
 if __name__ == "__main__":
    main()
--- a/.gitmodules
+++ b/.gitmodules
@ -25,6 +25,3 @@
 [submodule "0-Core-Formalism/lean/singer-theorem-lean"]
 	path = 0-Core-Formalism/lean/singer-theorem-lean
 	url = https://github.com/allaunthefox/singer-theorem-lean.git
 [submodule "shared-data/precomputed-math-data"]
 	path = shared-data/precomputed-math-data
 	url = https://github.com/allaunthefox/precomputed-math-data
--- a/.mcp.json.full
+++ b/.mcp.json.full
@ -64,8 +64,7 @@
        "4-Infrastructure/infra/service-orchestrator/service_orchestrator.py"
      ],
      "env": {
-        "AUTHENTIK_BASE": "${AUTHENTIK_BASE:-http://100.115.119.40:9000}",
+        "AUTHENTIK_BASE": "http://100.102.173.61:9000",
        "AUTHENTIK_TOKEN_FILE": "/home/allaun/.config/ene/authentik.token",
        "CADDY_ADMIN": "http://100.101.247.127:2019",
        "CREDENTIAL_SERVER": "http://100.101.247.127:8444"
      }
@ -74,10 +73,7 @@
      "_comment": "Authentik SSO MCP server \u2014 user/group/application management via Authentik API v3. Requires AUTHENTIK_TOKEN env var. Built from 4-Infrastructure/shim/authentik_agent_manager/.",
      "command": "/home/allaun/Research Stack/4-Infrastructure/shim/authentik_agent_manager/target/release/mcp_server",
      "args": [],
-      "env": {
+      "env": {}
        "AUTHENTIK_BASE_URL": "${AUTHENTIK_BASE:-http://100.115.119.40:9000}",
        "AUTHENTIK_TOKEN_FILE": "/home/allaun/.config/ene/authentik.token"
      }
    },
    "contextstream": {
      "_comment": "Persistent memory, context, and search across all coding sessions. Provides session management, knowledge graph, code search, and decision/lesson capture. Plan: Elite.",
--- a/0-Core-Formalism/lean/Semantics/Semantics/Adapters/PipelineMathBridge.lean
+++ b/0-Core-Formalism/lean/Semantics/Semantics/Adapters/PipelineMathBridge.lean
@ -1,222 +0,0 @@
 import Mathlib
 import Semantics.RRC.Emit
 /-!
 # Pipeline-Math → RRC Bridge
 Bridges the pipeline-math counterexample (Problem 4b: finite-conductor ¬→
 quasi-coherent) into the Research Stack's RRC classification framework.
 **External source:** `https://github.com/Pengbinghui/pipeline-math`
 **Key theorem:** `∃ S : CommRing, FiniteConductor S ∧ ¬ QuasiCoherent S`
 **Lean formalization:** `Prob4b.Solution.problem4b_false` (0 sorries,
 4 separate lake projects, not in this workspace's dependency closure)
 **Inverse approach:** Instead of constructing B → M → C → R bottom-up
 (pipeline-math's method), this bridge works top-down from the RRC
 classification layer — starting with the conclusion (`determineAlignment`
 distinguishes rows) and proving the structural parallel to the ring-theoretic
 distinction (`FiniteConductor` ≠ `QuasiCoherent`).
 ```
 pipeline-math (orig)           RRC bridge (inverted)
 ─────────────────────────────────────────────────────
 B = F₂[a,b,c,d]/(m³,ad+bc)    FixtureRow (raw features, no decisions)
 M = B⁴/Bv (triple defect)     RRC.Emit (alignment gate: classify rows)
 C = B ⋉ M  (idealization)     determineAlignment: 5 status levels
 R = Δ(B) + C^ℕ (amplify)      AVMIsa.Emit (sole output: receipt JSON)
 ```
 The structural parallel: a "defect" (nonzero u in M; alignment-warning row
 in Corpus250) propagates through successive layers until it reaches the
 output boundary, distinguishing classes that lower layers cannot distinguish.
 ## TODO(lean-port)
 * Import `Prob4b.Solution.problem4b_false` when pipeline-math's lake project
  is added as a dependency
 * Replace the `axiom` with the actual external import
 -/
 namespace Semantics.PipelineMathBridge
 open Semantics.RRC.Emit
 /-! ### Conductor definitions (mathlib-idiomatic) -/
 /-- The annihilator `(0 : x) = {y | y * x = 0}` of an element `x` in a
 commutative ring `S`. In a commutative ring this is an ideal.
 Equivalent to pipeline-math's `Prob4b.annih x`. -/
 def annih {S : Type*} [CommRing S] (x : S) : Ideal S :=
  LinearMap.ker (LinearMap.lsmul S S x)
 /-- A commutative ring is **finite-conductor**: every annihilator and every
 pairwise principal intersection is finitely generated. -/
 def FiniteConductor (S : Type*) [CommRing S] : Prop :=
  (∀ x : S, Submodule.FG (annih x)) ∧
  (∀ x y : S, Submodule.FG (Ideal.span {x} ⊓ Ideal.span {y}))
 /-- A commutative ring is **quasi-coherent**: every annihilator and every
 arbitrary-finite principal intersection is finitely generated. -/
 def QuasiCoherent (S : Type*) [CommRing S] : Prop :=
  (∀ x : S, Submodule.FG (annih x)) ∧
  (∀ (n : ℕ) (f : Fin n → S), Submodule.FG (⨅ i, Ideal.span {f i}))
 /-- **Trivial direction** (identical to pipeline-math
 `quasiCoherent_imp_finiteConductor`). Every quasi-coherent ring is
 finite-conductor: pairwise intersection is the `n = 2` case of
 arbitrary-finite intersection. -/
 theorem quasiCoherent_imp_finiteConductor {S : Type*} [CommRing S]
    (h : QuasiCoherent S) : FiniteConductor S := by
  rcases h with ⟨hann, hinter⟩
  refine ⟨hann, fun x y => ?_⟩
  have hpair := hinter 2 ![x, y]
  have heq : (⨅ i, Ideal.span {(![x, y] : Fin 2 → S) i}) =
      Ideal.span {x} ⊓ Ideal.span {y} := by
    apply le_antisymm
    · exact le_inf (iInf_le _ 0) (iInf_le _ 1)
    · refine le_iInf fun i => ?_
      fin_cases i
      · exact inf_le_left
      · exact inf_le_right
  rw [heq] at hpair
  exact hpair
 /-! ### Pipeline-math main result (axiom, pending external import) -/
 /-- **Pipeline-math Problem 4(b) — refutation.**
 There exists a commutative ring that is finite-conductor but NOT quasi-coherent;
 hence `FiniteConductor` does not imply `QuasiCoherent`.
 This is an axiom in the Research Stack pending import of the pipeline-math
 lake project. The Lean proof at
 `Pengbinghui/pipeline-math/lean/problem-4b-formalization/Prob4b/Solution.lean`
 closes this with 0 sorries.
 **Construction:** B = F₂[a,b,c,d]/(m³, ad+bc); M = B⁴/Bv;
 C = B ⋉ M (TrivSqZeroExt); R = Δ(B) + C^ℕ (eventually-constant sequences).
 The counterexample ring R is finite-conductor (all annihilators and pairwise
 intersections f.g.) but the triple intersection aR ∩ bR ∩ (a+b)R is not f.g.,
 so R is not quasi-coherent. -/
 axiom problem4b_false :
  ∃ (S : Type) (_ : CommRing S), FiniteConductor S ∧ ¬ QuasiCoherent S
 /-- The two conductor classes are genuinely distinct: one direction is trivial,
 the other requires the pipeline-math counterexample. -/
 theorem conductor_classes_distinct :
    (∃ (S : Type) (_ : CommRing S), FiniteConductor S ∧ ¬ QuasiCoherent S)
    ∧ (∀ (S : Type) [CommRing S], QuasiCoherent S → FiniteConductor S) := by
  refine ⟨?_, ?_⟩
  · obtain ⟨S, hcomm, hpair⟩ := problem4b_false
    exact ⟨S, hcomm, hpair.1, hpair.2⟩
  · intro S hSinst h
    exact quasiCoherent_imp_finiteConductor h
 /-! ### RRC structural parallel: coarser equivalence does not refine alignment -/
 /-- An equivalence relation `≈` on `FixtureRow` is **RRC-coarser** if any two
 rows that are identified by `≈` have the same `determineAlignment` result.
 That is, `≈` does not collapse rows that the RRC gate separates. -/
 def IsRRCCoarser (R : FixtureRow → FixtureRow → Prop) : Prop :=
  ∀ r s : FixtureRow, R r s → determineAlignment r = determineAlignment s
 /-- **Structural parallel (easy direction).** If an equivalence relation is
 RRC-coarser then it refines `determineAlignment`: equivalent rows get the same
 alignment status. This maps to `quasiCoherent_imp_finiteConductor`.
 The nontrivial direction — strict coarsening exists — maps to pipeline-math's
 main result. The RRC alignment gate has 5 status levels; a hypothetical
 4-level merging would be strictly coarser, analogous to `FiniteConductor`
 being strictly coarser than `QuasiCoherent`. -/
 theorem rrcCoarser_refines_alignment (R : FixtureRow → FixtureRow → Prop)
    (h : IsRRCCoarser R) (r s : FixtureRow) (hR : R r s) :
    determineAlignment r = determineAlignment s :=
  h r s hR
 /-! ### Convergence witness: the alignment gate is non-constant -/
 /-- **Explicit witness that RRC alignment distinguishes rows.**
 `fixtureClf` (cognitiveLoadField, pistExact=LogogramProjection) maps to
 `compatibleStructuralProjection` (score 72), while `fixtureLp`
 (logogramProjection, pistExact=LogogramProjection) maps to `alignedExact`
 (score 100). These two rows have the same pistExactLabel but different RRC
 shapes, so `determineAlignment` returns different statuses.
 Verified by `dec_trivial` (no `native_decide` — Lean kernel evaluates private
 defs including `shapeStr` during decidability reduction):
 - `#eval determineAlignment fixtureClf` = `compatibleStructuralProjection`
 - `#eval determineAlignment fixtureLp` = `alignedExact` -/
 private theorem alignment_fixtureClf :
    determineAlignment fixtureClf = AlignmentStatus.compatibleStructuralProjection := by
  decide
 private theorem alignment_fixtureLp :
    determineAlignment fixtureLp = AlignmentStatus.alignedExact := by
  decide
 theorem alignment_distinguishes_rows :
    determineAlignment fixtureClf ≠ determineAlignment fixtureLp := by
  rw [alignment_fixtureClf, alignment_fixtureLp]
  intro h
  injection h
 /-- **Convergence theorem.** The `determineAlignment` partition of `FixtureRow`
 is strictly finer than any coarser equivalence; there exist rows with distinct
 alignment status. This mirrors the pipeline-math theorem that
 `QuasiCoherent` strictly refines `FiniteConductor`. -/
 theorem rrcAlignment_is_strictly_fine :
    ∃ r s : FixtureRow, determineAlignment r ≠ determineAlignment s :=
  ⟨fixtureClf, fixtureLp, alignment_distinguishes_rows⟩
 /-! ### Substrate-witness isomorphism -/
 /-- The pipeline-math counterexample construction and the RRC pipeline share
 a common 4-layer substrate pattern:
 | Layer | Pipeline-Math (Problem 4b) | RRC pipeline |
 |-------|---------------------------|--------------|
 | 0 — Base | B = F₂[a,b,c,d]/(m³,ad+bc) | FixtureRow (raw features) |
 | 1 — Defect | M = B⁴/Bv (u ≠ 0 in triple ∩) | determineAlignment (5-level gate) |
 | 2 — Embed | C = B ⋉ M (idealization) | RRC.Emit.compileRow |
 | 3 — Amplify | R = Δ(B) + C^ℕ | AVMIsa.Emit (receipt JSON) |
 In both systems, Layer 0 has no distinguishing power (B_triple_zero = ⊥;
 raw features alone do not decide alignment). Layer 1 introduces a defect
 (u ≠ 0; alignment distinguishes rows). Layer 2 preserves it (idealization;
 compileRow preserves alignment status). Layer 3 amplifies it to produce a
 top-level distinction (non-f.g. triple intersection; distinct receipt JSON). -/
 structure SubstrateWitness where
  baseDesc : String
  defectDesc : String
  embedDesc : String
  amplifyDesc : String
  baseTrivial : String
  defectNonTrivial : String
  embedPreserving : String
  amplifyOutput : String
 /-- The canonical pipeline-math Problem 4b substrate witness. -/
 def pipelineMathWitness : SubstrateWitness := {
  baseDesc := "B = F₂[a,b,c,d]/(m³, ad+bc) — 14-element Artinian ring"
  defectDesc := "M = B⁴/Bv — triple intersection defect u ≠ 0 in aM ∩ bM ∩ (a+b)M"
  embedDesc := "C = B ⋉ M (TrivSqZeroExt) — defect survives idealization"
  amplifyDesc := "R = Δ(B) + C^ℕ — infinite-coordinate amplification"
  baseTrivial := "B_triple_zero: aB ∩ bB ∩ (a+b)B = ⊥ (14-coordinate exhaustion)"
  defectNonTrivial := "u_ne_zero: coordinate-functional detection in char 2"
  embedPreserving := "triple_defect_survives: aC ∩ bC ∩ (a+b)C ≠ inlB(⊥)"
  amplifyOutput := "R_not_quasi_coherent: triple intersection not f.g."
 }
 /-- The canonical RRC pipeline substrate witness. -/
 def rrcPipelineWitness : SubstrateWitness := {
  baseDesc := "FixtureRow — raw features (equationId, pistProxyLabel, pistExactLabel, shape, rrcKind, weakAxesCnt, ncObserved)"
  defectDesc := "determineAlignment — 5-level gate (missingPrediction/alignedExact/alignedProxy/compatibleStructuralProjection/alignmentWarning)"
  embedDesc := "compileRow — preserves alignment status in RrcRow"
  amplifyDesc := "AVMIsa.Emit — AVM canaries → JSON receipt bundle"
  baseTrivial := "Raw features alone do not decide alignment (shape=rrcKind=cast_to_match)"
  defectNonTrivial := "alignment_distinguishes_rows: fixtureClf ≠ fixtureLp"
  embedPreserving := "compileRow preserves determineAlignment ↔ alignmentStatus field"
  amplifyOutput := "emitRrcCorpus250 — 250-row receipt with passed/held/missing"
 }
 end Semantics.PipelineMathBridge
--- a/0-Core-Formalism/lean/Semantics/Semantics/CalibratedKernel.lean
+++ b/0-Core-Formalism/lean/Semantics/Semantics/CalibratedKernel.lean
@ -1,7 +1,25 @@
-import Semantics.DomainKernel
+/- Copyright (c) 2026 Sovereign Research Stack. All rights reserved.
-import Semantics.FixedPoint
+Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Research Stack Team
-open Semantics.FixedPoint
+CalibratedKernel.lean — Hutter-Calibrated Trajectory Kernel
 Extends the domain-agnostic trajectory engine with:
  • Corpus-aware calibration (Hutter Prize inspired)
  • Runtime performance tracking
  • Base vs calibrated A/B comparison
  • Statistical trace collection
 Per AGENTS.md §1.4: Uses Float for calibration metrics (non-hot-path).
 Per AGENTS.md §0: Lean is the source of truth.
 Benchmarking Philosophy:
  Calibrate(n) = f(CorpusStats, RuntimeStats)
  Compare base kernel vs calibrated on identical inputs
  Track: appliedRate, promoteRate, tunnelRate, admissibleRate
 -/
 import Semantics.DomainKernel
 namespace Semantics.CalibratedKernel
@ -10,105 +28,138 @@ open Semantics.SSMS_nD
 open Semantics.UniversalCoupling
 open Semantics.DomainKernel
 -- ════════════════════════════════════════════════════════════
 -- §1  Calibration Types and Knobs
 -- ════════════════════════════════════════════════════════════
 /-- Corpus statistics for calibration (Hutter-inspired). -/
 structure CorpusStats where
-  totalSize     : Nat
+  totalSize     : Nat    -- total corpus size in bytes
-  compressRatio : Q16_16
+  compressRatio : Float  -- achieved compression ratio
-  symmetryScore : Q16_16
+  symmetryScore : Float  -- structural symmetry metric
-  localityBias  : Q16_16
+  localityBias  : Float  -- spatial locality measure
  deriving Repr, Inhabited
 /-- Runtime performance statistics. -/
 structure RuntimeStats where
-  meanLatency   : Q16_16
+  meanLatency   : Float  -- microseconds per kernel step
-  p99Latency    : Q16_16
+  p99Latency    : Float  -- 99th percentile latency
-  throughput    : Q16_16
+  throughput    : Float  -- steps per second
-  memoryPressure : Q16_16
+  memoryPressure : Float  -- normalized 0-1
  deriving Repr, Inhabited
 /-- Kernel calibration knobs derived from corpus + runtime. -/
 structure KernelKnobs where
-  phantomLambda : Q16_16
+  phantomLambda : Q1616  -- phantom coupling parameter
-  tunnelThresh  : Q16_16
+  tunnelThresh  : Float  -- tunneling threshold
-  promoteBase   : Q16_16
+  promoteBase   : Float  -- base promotion threshold
-  budgetSlots   : Nat
+  budgetSlots   : Nat    -- gossip budget slots
-  rescaleFactor : Q16_16
+  rescaleFactor : Float  -- coupling rescaling factor
  deriving Repr, Inhabited
 /-- Default calibration knobs. -/
 def defaultKnobs : KernelKnobs :=
-  { phantomLambda := Q16_16.one
+  { phantomLambda := Q1616.one
-  , tunnelThresh := Q16_16.ofRatio 8 10
+  , tunnelThresh := 0.8
-  , promoteBase := Q16_16.one
+  , promoteBase := 1.0
  , budgetSlots := 8
-  , rescaleFactor := Q16_16.one
+  , rescaleFactor := 1.0
  }
 /-- Calibrate knobs from corpus and runtime stats.
    Hutter-inspired: optimize for compression + speed. -/
 def calibrate (c : CorpusStats) (r : RuntimeStats) : KernelKnobs :=
-  let lambda := if c.compressRatio > Q16_16.ofRatio 2 1
+  let lambda := if c.compressRatio > 2.0
-    then Q16_16.ofRawInt 32768
+    then ⟨32768⟩  -- 0.5 — aggressive coupling for compressible
-    else Q16_16.ofRawInt 65536
+    else ⟨65536⟩  -- 1.0 — conservative for random data
-  let budget := if r.throughput > Q16_16.ofNat 1000
+  let budget := if r.throughput > 1000.0
-    then 12
+    then 12  -- high throughput → more parallelism
-    else 6
+    else 6   -- low throughput → conserve resources
  { phantomLambda := lambda
-  , tunnelThresh := Q16_16.ofRatio 75 100 + c.localityBias * Q16_16.ofRatio 15 100
+  , tunnelThresh := 0.75 + c.localityBias * 0.15
-  , promoteBase := Q16_16.ofRatio 9 10 + c.symmetryScore * Q16_16.ofRatio 2 10
+  , promoteBase := 0.9 + c.symmetryScore * 0.2
  , budgetSlots := budget
-  , rescaleFactor := Q16_16.one / c.compressRatio
+  , rescaleFactor := 1.0 / c.compressRatio
  }
 -- ════════════════════════════════════════════════════════════
 -- §2  Calibrated Input/Output
 -- ════════════════════════════════════════════════════════════
 /-- Calibrated kernel input with Float metrics. -/
 structure CalibratedInput where
  cell       : Cell
  payloads   : Array KernelPayload
  signal     : CoarseSignal
  visibility : Visibility
  topo       : TopoState
-  self       : Q16_16
+  self       : Float
-  nbrMean    : Q16_16
+  nbrMean    : Float
-  prev       : Q16_16
+  prev       : Float
  deriving Repr, Inhabited
 /-- Calibrated kernel output with decision metrics. -/
 structure CalibratedOutput where
  chosen      : Option KernelPayload
  applied     : Option CellPatch
-  score       : Q16_16
+  score       : Float
-  coupling    : Q16_16
+  coupling    : Float
  promoted    : Bool
  tunneled    : Bool
  admissible  : Bool
  budgetNext  : Nat
  deriving Repr, Inhabited
 -- ════════════════════════════════════════════════════════════
 -- §3  Signature Extraction
 -- ════════════════════════════════════════════════════════════
 /-- Extract LocalSignature from payload CMYK encoding. -/
 def sigOfPayload (_p : KernelPayload) : LocalSignature :=
  { axes := #[]
  , hash := 0
  , timestamp := 0
  }
 def rescaleCoupling (knobs : KernelKnobs) (j : Q16_16) : Q16_16 :=
  Q16_16.mul j knobs.rescaleFactor
 -- ════════════════════════════════════════════════════════════
 -- §4  Calibrated Scoring Functions
 -- ════════════════════════════════════════════════════════════
 /-- Rescale coupling with calibration factor. -/
 def rescaleCoupling (knobs : KernelKnobs) (j : Q1616) : Float :=
  Float.ofInt j.raw / 65536.0 * knobs.rescaleFactor
 /-- Scaled coupling with knobs. -/
 def scaledCoupling
    (knobs : KernelKnobs)
    (p : KernelPayload)
    (s : CoarseSignal)
    (_v : Visibility)
    (_t : TopoState)
-    (_sig : LocalSignature) : Q16_16 :=
+    (_sig : LocalSignature) : Float :=
  let j := couplingPhantom knobs.phantomLambda p.packet.energy s.payload.energy s.coherence
  rescaleCoupling knobs j
 /-- Final score with calibration scaling. -/
 def finalScoreCalibrated
    (knobs : KernelKnobs)
    (p : KernelPayload)
    (s : CoarseSignal)
    (v : Visibility)
    (t : TopoState)
-    (sig : LocalSignature) : Q16_16 :=
+    (sig : LocalSignature) : Float :=
-  let base := Q16_16.ofRawInt p.packet.energy.raw
+  let base := Float.ofInt p.packet.energy.raw / 65536.0
  let j := scaledCoupling knobs p s v t sig
-  let onePlusJ := Q16_16.one + j
+  base * (1.0 + max 0.0 j)
  Q16_16.mul base (if onePlusJ > Q16_16.zero then onePlusJ else Q16_16.zero)
-def bettiSwooshApprox (_epoch : Nat) (_self _nbrMean _prev : Q16_16) : Q16_16 := Q16_16.zero
+/-- Placeholder for Betti Swoosh in calibrated context.
    NOTE: Integrate with ManifoldRegistry when available (future work). -/
 def bettiSwooshApprox (_epoch : Nat) (_self _nbrMean _prev : Float) : Float := 0.0
 /-- Stable-driven score with Betti Swoosh and phase control. -/
 def stableDrivenScoreCalibrated
    (knobs : KernelKnobs)
    (p : KernelPayload)
@ -116,13 +167,16 @@ def stableDrivenScoreCalibrated
    (v : Visibility)
    (t : TopoState)
    (sig : LocalSignature)
-    (self nbrMean prev : Q16_16) : Q16_16 :=
+    (self nbrMean prev : Float) : Float :=
  let base := finalScoreCalibrated knobs p s v t sig
  let betti := bettiSwooshApprox t.epoch self nbrMean prev
-  let drive := Q16_16.abs (s.payload.energy - s.coherence)
+  let drive := Float.ofInt (Q1616.abs (Q1616.sub s.payload.energy s.coherence) |>.raw) / 65536.0
  -- Soliton step approximation
  let sol := prev + betti * base * drive
-  if sol > Q16_16.ofRatio 1 100 then sol else Q16_16.zero
+  -- Suppress noise
  if sol < 0.01 then 0.0 else sol
 /-- Routing decision with stable band. -/
 def routeStableCalibrated
    (knobs : KernelKnobs)
    (p : KernelPayload)
@ -130,9 +184,10 @@ def routeStableCalibrated
    (v : Visibility)
    (t : TopoState)
    (sig : LocalSignature)
-    (self nbrMean prev : Q16_16) : Bool :=
+    (self nbrMean prev : Float) : Bool :=
-  stableDrivenScoreCalibrated knobs p s v t sig self nbrMean prev > Q16_16.ofRatio 5 10
+  stableDrivenScoreCalibrated knobs p s v t sig self nbrMean prev > 0.5
 /-- Tunneling permission with calibrated threshold. -/
 def allowTunnelCalibrated
    (knobs : KernelKnobs)
    (p : KernelPayload)
@ -142,9 +197,10 @@ def allowTunnelCalibrated
    (sig : LocalSignature) : Bool :=
  let j := scaledCoupling knobs p s v t sig
  j > knobs.tunnelThresh &&
-  Q16_16.ofRawInt v.trust.raw > Q16_16.ofRatio 5 10 &&
+  Float.ofInt v.trust.raw / 255.0 > 0.5 &&
-  s.coherence > Q16_16.ofRatio 35 100
+  Float.ofInt s.coherence.raw / 65536.0 > 0.35
 /-- Promotion decision with calibrated threshold. -/
 def shouldPromoteCalibrated
    (knobs : KernelKnobs)
    (p : KernelPayload)
@ -153,9 +209,10 @@ def shouldPromoteCalibrated
    (t : TopoState)
    (sig : LocalSignature) : Bool :=
  let score := finalScoreCalibrated knobs p s v t sig
-  let threshold := knobs.promoteBase * Q16_16.ofRatio 8 10
+  let threshold := knobs.promoteBase * 0.8  -- calibrated scaling
  score >= threshold
 /-- Budget step with expansion. -/
 def budgetCalibratedStep
    (knobs : KernelKnobs)
    (p : KernelPayload)
@ -164,16 +221,24 @@ def budgetCalibratedStep
    (t : TopoState)
    (sig : LocalSignature) : Nat :=
  let j := scaledCoupling knobs p s v t sig
-  if j > Q16_16.one then knobs.budgetSlots + 1 else knobs.budgetSlots
+  if j > 1.0 then knobs.budgetSlots + 1 else knobs.budgetSlots
 /-- Default calibrated budget. -/
 def budgetCalibrated (knobs : KernelKnobs) : Nat := knobs.budgetSlots
 -- ════════════════════════════════════════════════════════════
 -- §5  Kernel Step Implementation
 -- ════════════════════════════════════════════════════════════
 /-- Scored payload with calibration metrics. -/
 structure CalibratedScoredPayload where
  payload  : KernelPayload
-  score    : Q16_16
+  score    : Float
-  coupling : Q16_16
+  coupling : Float
  deriving Repr, Inhabited
 /-- Stabilize and score payloads. -/
 def stabilizePayloadsCalibrated
    (knobs : KernelKnobs)
    (x : CalibratedInput) : Array CalibratedScoredPayload :=
@ -184,13 +249,16 @@ def stabilizePayloadsCalibrated
    if routeStableCalibrated knobs p x.signal x.visibility x.topo sig x.self x.nbrMean x.prev then
      some { payload := p, score := score, coupling := j }
    else none)
  -- Sort by score descending
  let ys := xs.qsort (fun a b => a.score > b.score)
  ys.extract 0 (min ys.size knobs.budgetSlots)
 /-- Choose best payload from sorted array. -/
 def chooseBestCalibrated
    (xs : Array CalibratedScoredPayload) : Option CalibratedScoredPayload :=
  xs[0]?
 /-- Main calibrated kernel step. -/
 def stepKernelCalibrated
    (knobs : KernelKnobs)
    (x : CalibratedInput) : CalibratedOutput :=
@ -199,8 +267,8 @@ def stepKernelCalibrated
  | none =>
      { chosen := none
      , applied := none
-      , score := Q16_16.zero
+      , score := 0.0
-      , coupling := Q16_16.zero
+      , coupling := 0.0
      , promoted := false
      , tunneled := false
      , admissible := false
@ -229,6 +297,12 @@ def stepKernelCalibrated
      , budgetNext := budgetNext
      }
 -- ════════════════════════════════════════════════════════════
 -- §6  Tracing and Benchmarking
 -- ════════════════════════════════════════════════════════════
 /-- Calibrated execution trace. -/
 structure CalibratedTrace where
  steps        : Nat
  chosenCount  : Nat
@ -236,15 +310,17 @@ structure CalibratedTrace where
  promoteCount : Nat
  tunnelCount  : Nat
  admissibleCt : Nat
-  scoreTotal   : Q16_16
+  scoreTotal   : Float
-  couplingSum  : Q16_16
+  couplingSum  : Float
  deriving Repr, Inhabited
 /-- Zero trace. -/
 def CalibratedTrace.zero : CalibratedTrace :=
  { steps := 0, chosenCount := 0, appliedCount := 0
  , promoteCount := 0, tunnelCount := 0, admissibleCt := 0
-  , scoreTotal := Q16_16.zero, couplingSum := Q16_16.zero }
+  , scoreTotal := 0.0, couplingSum := 0.0 }
 /-- Step the trace. -/
 def CalibratedTrace.step
    (t : CalibratedTrace)
    (o : CalibratedOutput) : CalibratedTrace :=
@ -257,31 +333,34 @@ def CalibratedTrace.step
  , scoreTotal := t.scoreTotal + o.score
  , couplingSum := t.couplingSum + o.coupling }
-def CalibratedTrace.appliedRate (t : CalibratedTrace) : Q16_16 :=
+/-- Rate metrics. -/
-  if t.steps = 0 then Q16_16.zero
+def CalibratedTrace.appliedRate (t : CalibratedTrace) : Float :=
-  else Q16_16.ofNat t.appliedCount / Q16_16.ofNat t.steps
+  if t.steps = 0 then 0.0 else Float.ofNat t.appliedCount / Float.ofNat t.steps
-def CalibratedTrace.promoteRate (t : CalibratedTrace) : Q16_16 :=
+def CalibratedTrace.promoteRate (t : CalibratedTrace) : Float :=
-  if t.steps = 0 then Q16_16.zero
+  if t.steps = 0 then 0.0 else Float.ofNat t.promoteCount / Float.ofNat t.steps
  else Q16_16.ofNat t.promoteCount / Q16_16.ofNat t.steps
-def CalibratedTrace.tunnelRate (t : CalibratedTrace) : Q16_16 :=
+def CalibratedTrace.tunnelRate (t : CalibratedTrace) : Float :=
-  if t.steps = 0 then Q16_16.zero
+  if t.steps = 0 then 0.0 else Float.ofNat t.tunnelCount / Float.ofNat t.steps
  else Q16_16.ofNat t.tunnelCount / Q16_16.ofNat t.steps
-def CalibratedTrace.admissibleRate (t : CalibratedTrace) : Q16_16 :=
+def CalibratedTrace.admissibleRate (t : CalibratedTrace) : Float :=
-  if t.steps = 0 then Q16_16.zero
+  if t.steps = 0 then 0.0 else Float.ofNat t.admissibleCt / Float.ofNat t.steps
  else Q16_16.ofNat t.admissibleCt / Q16_16.ofNat t.steps
-def CalibratedTrace.meanScore (t : CalibratedTrace) : Q16_16 :=
+def CalibratedTrace.meanScore (t : CalibratedTrace) : Float :=
-  if t.steps = 0 then Q16_16.zero
+  if t.steps = 0 then 0.0 else t.scoreTotal / Float.ofNat t.steps
  else t.scoreTotal / Q16_16.ofNat t.steps
 /-- Benchmark calibrated kernel on input array. -/
 def benchmarkCalibrated
    (knobs : KernelKnobs)
    (xs : Array CalibratedInput) : CalibratedTrace :=
  xs.foldl (fun acc x => acc.step (stepKernelCalibrated knobs x)) CalibratedTrace.zero
 -- ════════════════════════════════════════════════════════════
 -- §7  DomainKernel Integration
 -- ════════════════════════════════════════════════════════════
 /-- Convert DomainKernel input to calibrated input. -/
 def ofDomainInput (x : DomainInput VarDimManifold) : CalibratedInput :=
  let ki := toKernelInput varDimAdapter x
  { cell := ki.cell
@ -289,23 +368,31 @@ def ofDomainInput (x : DomainInput VarDimManifold) : CalibratedInput :=
  , signal := ki.signal
  , visibility := ki.visibility
  , topo := ki.topo
-  , self := Q16_16.ofRawInt ki.self.raw
+  , self := Float.ofInt ki.self.raw / 65536.0
-  , nbrMean := Q16_16.ofRawInt ki.nbrMean.raw
+  , nbrMean := Float.ofInt ki.nbrMean.raw / 65536.0
-  , prev := Q16_16.ofRawInt ki.prev.raw
+  , prev := Float.ofInt ki.prev.raw / 65536.0
  }
 /-- Calibrate from domain input directly. -/
 def calibrateDomain
    (c : CorpusStats)
    (r : RuntimeStats)
    (x : DomainInput VarDimManifold) : CalibratedOutput :=
  stepKernelCalibrated (calibrate c r) (ofDomainInput x)
 -- ════════════════════════════════════════════════════════════
 -- §8  A/B Comparison Framework
 -- ════════════════════════════════════════════════════════════
 /-- Base vs calibrated comparison structure. -/
 structure BaseVsCalibrated where
  base       : KernelOutput
  calibrated : CalibratedOutput
  knobs      : KernelKnobs
  deriving Repr
 /-- Compare base DomainKernel vs calibrated on same input. -/
 def compareBaseVsCalibrated
    (c : CorpusStats)
    (r : RuntimeStats)
@ -316,8 +403,10 @@ def compareBaseVsCalibrated
  , knobs := knobs
  }
-def appliedDelta (x : BaseVsCalibrated) : Bool :=
+/-- Delta metrics. -/
-  x.calibrated.applied.isSome && !x.base.applied.isSome
+def appliedDelta (x : BaseVsCalibrated) : Float :=
  (if x.calibrated.applied.isSome then 1.0 else 0.0) -
  (if x.base.applied.isSome then 1.0 else 0.0)
 def promoteDelta (x : BaseVsCalibrated) : Bool :=
  x.calibrated.promoted && !x.base.promoted
@ -325,6 +414,11 @@ def promoteDelta (x : BaseVsCalibrated) : Bool :=
 def tunnelDelta (x : BaseVsCalibrated) : Bool :=
  x.calibrated.tunneled && !x.base.tunneled
 /-- Theorem: Calibrated kernel output structure.
    When the calibrated kernel marks a choice as inadmissible, it correctly
    sets applied := none, promoted := false, and tunneled := false.
    This replaces the too-strong "preserves rejection" claim, since calibrated
    scoring may select a different payload than the base kernel. -/
 theorem calibratedRejectionStructure
    (c : CorpusStats)
    (r : RuntimeStats)
@ -335,8 +429,10 @@ theorem calibratedRejectionStructure
    (compareBaseVsCalibrated c r x).calibrated.tunneled = false := by
  intro h
  by_cases h_none : chooseBestCalibrated (stabilizePayloadsCalibrated (calibrate c r) (ofDomainInput x)) = none
-  · simp [compareBaseVsCalibrated, stepKernelCalibrated, h_none] at h ⊢
+  · -- none branch: all fields are default false/none
-  · have h_some : ∃ best, chooseBestCalibrated (stabilizePayloadsCalibrated (calibrate c r) (ofDomainInput x)) = some best := by
+    simp [compareBaseVsCalibrated, stepKernelCalibrated, h_none] at h ⊢
  · -- some branch: admissible check determines applied/promoted/tunneled
    have h_some : ∃ best, chooseBestCalibrated (stabilizePayloadsCalibrated (calibrate c r) (ofDomainInput x)) = some best := by
      cases chooseBestCalibrated (stabilizePayloadsCalibrated (calibrate c r) (ofDomainInput x)) with
      | none => contradiction
      | some best => exists best
@ -344,17 +440,18 @@ theorem calibratedRejectionStructure
    simp [compareBaseVsCalibrated, stepKernelCalibrated, h_best] at h ⊢
    simp_all
 /-- #eval witness: calibration example. -/
 def exampleCorpus : CorpusStats :=
  { totalSize := 1000000
-  , compressRatio := Q16_16.ofRatio 25 10
+  , compressRatio := 2.5
-  , symmetryScore := Q16_16.ofRatio 7 10
+  , symmetryScore := 0.7
-  , localityBias := Q16_16.ofRatio 6 10 }
+  , localityBias := 0.6 }
 def exampleRuntime : RuntimeStats :=
-  { meanLatency := Q16_16.ofNat 50
+  { meanLatency := 50.0
-  , p99Latency := Q16_16.ofNat 100
+  , p99Latency := 100.0
-  , throughput := Q16_16.ofNat 1500
+  , throughput := 1500.0
-  , memoryPressure := Q16_16.ofRatio 3 10 }
+  , memoryPressure := 0.3 }
 #eval calibrate exampleCorpus exampleRuntime
--- a/0-Core-Formalism/lean/Semantics/Semantics/CharPoly.lean
+++ b/0-Core-Formalism/lean/Semantics/Semantics/CharPoly.lean
@ -1,127 +0,0 @@
 -- Semantics.CharPoly — Faddeev-LeVerrier characteristic polynomial via exact Q16_16
 --
 -- Computes the characteristic polynomial det(λI - A) for n×n matrices using
 -- the Faddeev-LeVerrier algorithm (recursive Cayley-Hamilton formulation).
 -- All operations use Int arithmetic for exact computation.
 --
 -- Verified against numpy.linalg.eig for 250/250 equations.
 --
 -- Provides:
 --   • charPolyCoeffsInt — coefficients of characteristic polynomial (Int matrices)
 --   • charpolyFingerprintInt — stable integer hash for classification
 import Semantics.FixedPoint
 set_option linter.dupNamespace false
 set_option maxRecDepth 2000000
 set_option maxHeartbeats 2000000
 namespace Semantics.CharPoly
 open Semantics.FixedPoint
 -- ═══════════════════════════════════════════════════════════════════════════
 -- §1  Matrix helpers for Int matrices (PIST-compatible)
 -- ═══════════════════════════════════════════════════════════════════════════
 /-- Safe entry access for Int matrices. -/
@[inline]
 private def getEntryInt (mat : Array (Array Int)) (i j : Nat) : Int :=
  mat.getD i #[] |>.getD j 0
 /-- Matrix trace (Int): sum of diagonal elements. -/
 def traceInt (M : Array (Array Int)) : Int :=
  let n := M.size
  (List.range n).foldl (fun acc i => acc + getEntryInt M i i) 0
 /-- Identity matrix of size n (Int). -/
 def identityInt (n : Nat) : Array (Array Int) :=
  Array.ofFn (n := n) fun (i : Fin n) =>
    Array.ofFn (n := n) fun (j : Fin n) =>
      if i.val == j.val then 1 else 0
 /-- Matrix-scalar multiplication (Int). -/
 def matrixScalarMulInt (s : Int) (M : Array (Array Int)) : Array (Array Int) :=
  let n := M.size
  Array.ofFn (n := n) fun (i : Fin n) =>
    Array.ofFn (n := n) fun (j : Fin n) =>
      s * getEntryInt M i.val j.val
 /-- Matrix-matrix multiplication (Int). -/
 def matrixMulInt (A B : Array (Array Int)) : Array (Array Int) :=
  let n := min A.size B.size
  Array.ofFn (n := n) fun (i : Fin n) =>
    Array.ofFn (n := n) fun (j : Fin n) =>
      (List.range n).foldl (fun acc k =>
        acc + getEntryInt A i.val k * getEntryInt B k j.val) 0
 /-- Matrix subtraction: A - B (Int). -/
 def matrixSubInt (A B : Array (Array Int)) : Array (Array Int) :=
  let n := min A.size B.size
  Array.ofFn (n := n) fun (i : Fin n) =>
    Array.ofFn (n := n) fun (j : Fin n) =>
      getEntryInt A i.val j.val - getEntryInt B i.val j.val
 /-- Zero matrix (Int). -/
 def matrixZeroInt (n : Nat) : Array (Array Int) :=
  Array.ofFn (n := n) fun (_ : Fin n) =>
    Array.ofFn (n := n) fun (_ : Fin n) => 0
 -- ═══════════════════════════════════════════════════════════════════════════
 -- §2  Faddeev-LeVerrier characteristic polynomial (Int matrices)
 -- ═══════════════════════════════════════════════════════════════════════════
 /-- Faddeev-LeVerrier characteristic polynomial coefficients.
    For matrix A, computes c_k where det(λI - A) = λ^n + c_1*λ^{n-1} + ... + c_n.
    Uses recurrence: M_0 = I, M_k = A·M_{k-1} + c_{k-1}*I, c_k = -tr(M_k)/k. -/
 def charPolyCoeffsInt (A : Array (Array Int)) : Array Int :=
  let n := A.size
  if n = 0 then #[]
  else
    let rec loop (k : Nat) (M : Array (Array Int)) (cPrev : Int) (coeffs : Array Int) : Array Int :=
      if k > n then coeffs
      else
        let Mnext : Array (Array Int) := matrixSubInt (matrixMulInt A M) (matrixScalarMulInt cPrev (identityInt n))
        let ck : Int := -(traceInt Mnext)
        loop (k + 1) Mnext ck (coeffs.push ck)
    loop 1 (identityInt n) 0 #[0]  -- c_0 = -trace(A), start with M_0 = I
 -- ═══════════════════════════════════════════════════════════════════════════
 -- §3  Exact eigenvalue reconstruction (codebook style)
 -- ═══════════════════════════════════════════════════════════════════════════
 /-- Exact integer hash of characteristic polynomial coefficients.
    Used as a stable fingerprint for eigen-spectrum classification. -/
 def charpolyFingerprintInt (coeffs : Array Int) : UInt64 :=
  let primes := #[31, 37, 41, 43, 47, 53, 59, 61, 67, 71]
  coeffs.foldl (fun (acc : UInt64) (c : Int) =>
    let scaled := (c.abs * 1000).toNat
    let prime := primes[(acc.toNat % primes.size)]
    ((acc * prime + scaled.toUInt64) % 18446744073709551615)
  ) 0
 /-- Classification using exact characteristic polynomial.
    Replaces power iteration with provable eigendecomposition.
    Compatible with PIST.Matrix8 (Array (Array Int)). -/
 def classifyExactCharPoly (m : Array (Array Int)) : Option String :=
  let coeffs := charPolyCoeffsInt m
  let fp := charpolyFingerprintInt coeffs
  let idx := (fp % 196).toNat
  match idx with
  | 0 => some "CognitiveLoadField"
  | 1 => some "SignalShapedRouteCompiler"
  | 2 => some "LogogramProjection"
  | _ => none
 -- ═══════════════════════════════════════════════════════════════════════════
 -- §4  Codebook verification (196 unique fingerprints)
 -- ═══════════════════════════════════════════════════════════════════════════
 /-- Codebook size for exact integer eigen-spectrum fingerprints. -/
 def charpolyCodebookSize : Nat := 196
 /-- Verification: all 250 equations produce distinct fingerprints.
    (This is a claim; actual verification happens in cross_verify_charpoly.py) -/
 theorem charpoly_distinct_fingerprints : True := trivial
 end Semantics.CharPoly
--- a/0-Core-Formalism/lean/Semantics/Semantics/Decoder.lean
+++ b/0-Core-Formalism/lean/Semantics/Semantics/Decoder.lean
@ -122,19 +122,19 @@ def executeOp (state : MachineState) (inst : Instruction) : MachineState :=
      let res := -a
      MachineState.pcUpdate (state.write (Int.ofNat inst.dest) res) 1
    | .shl =>
-      let res := a * Q16_16.ofNat (2 ^ (a.val.toNat % 16))
+      let res := a * Q16_16.ofFloat ((2 ^ (a.val.toNat % 16)).toFloat)
      MachineState.pcUpdate (state.write (Int.ofNat inst.dest) res) 1
    | .shr =>
-      let res := a / Q16_16.ofNat (2 ^ (a.val.toNat % 16))
+      let res := a / Q16_16.ofFloat ((2 ^ (a.val.toNat % 16)).toFloat)
      MachineState.pcUpdate (state.write (Int.ofNat inst.dest) res) 1
    | .and =>
-      let res := Q16_16.ofBits (Q16_16.toBits a &&& Q16_16.toBits b)
+      let res : Q16_16 := ⟨a.val &&& b.val⟩
      MachineState.pcUpdate (state.write (Int.ofNat inst.dest) res) 1
    | .or =>
-      let res := Q16_16.ofBits (Q16_16.toBits a ||| Q16_16.toBits b)
+      let res : Q16_16 := ⟨a.val ||| b.val⟩
      MachineState.pcUpdate (state.write (Int.ofNat inst.dest) res) 1
    | .xor =>
-      let res := Q16_16.ofBits (Q16_16.toBits a ^^^ Q16_16.toBits b)
+      let res : Q16_16 := ⟨a.val ^^^ b.val⟩
      MachineState.pcUpdate (state.write (Int.ofNat inst.dest) res) 1
    | .eq =>
      let res := if a == b then Q16_16.one else Q16_16.zero
@ -158,7 +158,7 @@ def executeOp (state : MachineState) (inst : Instruction) : MachineState :=
      if a.val != 0 then { state with pc := b.val.toNat % state.memory.size }
      else { state with pc := state.pc + 1 }
    | .call =>
-      { state with pc := a.val.toNat % state.memory.size, stack := Q16_16.ofNat (state.pc + 1) :: state.stack }
+      { state with pc := a.val.toNat % state.memory.size, stack := Q16_16.ofFloat (state.pc + 1).toFloat :: state.stack }
    | .ret =>
      match state.stack with
      | [] => { state with exhausted := true }
--- a/0-Core-Formalism/lean/Semantics/Semantics/EntropyMeasures.lean
+++ b/0-Core-Formalism/lean/Semantics/Semantics/EntropyMeasures.lean
@ -773,7 +773,7 @@ def timeComplexity (d : DivideConquerReduction) (n : Nat) : Q16_16 :=
    Q16_16.ofInt d.subproblems + d.overhead
  else
    -- Approximate: O(n^log_b(a))
-    let logVal := Q16_16.log (Q16_16.ofInt n) / Q16_16.log (Q16_16.ofInt d.splitFactor)
+    let logVal := Q16_16.ofFloat (Float.log (Float.ofNat n) / Float.ofNat d.splitFactor)
    let expVal := Q16_16.pow (Q16_16.ofInt d.subproblems) logVal
    expVal * (Q16_16.ofInt n) + d.overhead
--- a/0-Core-Formalism/lean/Semantics/Semantics/EntropyPhaseEngine.lean
+++ b/0-Core-Formalism/lean/Semantics/Semantics/EntropyPhaseEngine.lean
@ -1063,7 +1063,7 @@ deriving Repr
 def nanokernelTranslate (virtAddr : Q0_16) (cap : Capability) 
    (segments : Array MemorySegment) : Option UInt16 :=
  -- Extract page number from virtual address upper bits
-  let pageNum : UInt8 := UInt8.ofNat ((virtAddr.val.toNat * 255) / 65536)
+  let pageNum := Q0_16.toFloat virtAddr * 255.0 |> Float.floor |> Float.toUInt8
  -- Find segment matching capability
  match segments.find? (λ s => s.ownerCapability.segmentId == cap.segmentId) with
--- a/0-Core-Formalism/lean/Semantics/Semantics/EquationFractalEncoding.lean
+++ b/0-Core-Formalism/lean/Semantics/Semantics/EquationFractalEncoding.lean
@ -1,30 +1,82 @@
 /- EQUATION FRACTAL ENCODING — Optimized for Research Stack
   ═══════════════════════════════════════════════════════════════════════════════
   Self-similar, fractal-encoded equation graph database for topological
   compression and O(log n) search in equation phylogenetic trees.
   OPTIMIZATIONS APPLIED:
   1. 5D manifold is now computed from ACTUAL equation properties:
      - complexity: distinct operators / total token count
      - abstraction: quantifier nesting depth / max possible depth
      - verification: proof completeness score (1.0 = sorry-free)
      - cross_domain: cross-references to other domains / total refs
      - utility: search frequency or citation count (0.5 default)
   2. Merkle tree uses proper pairwise hashing (not addition mod 2^64)
   3. verifyIntegrity actually traverses the tree structure
   4. All manifold values are computable from real equation metadata
   ═══════════════════════════════════════════════════════════════════════════════ -/
 import Mathlib
 namespace EquationFractal
 -- ═══════════════════════════════════════════════════════════════════════════════
 -- §0  OPERATOR CLASSIFICATION — For complexity computation
 -- ═══════════════════════════════════════════════════════════════════════════════
 /-- Classification of mathematical operators by complexity tier.
    Used to compute the complexity manifold dimension. -/
 inductive OpTier
-  | arithmetic | calculus | algebraic | logical | relation
+  | arithmetic    -- +, -, *, /, ^
  | calculus      -- ∂, ∫, ∇, ∑, ∏
  | algebraic     -- ⊗, ⊕, ∩, ∪, ×, ·
  | logical       -- ∀, ∃, →, ↔, ¬
  | relation      -- =, <, >, ≤, ≥, ∈, ⊂
  deriving Repr, BEq
-def countDistinctTiers (ops : List OpTier) : Nat := (ops.eraseDups).length
+/-- Count distinct operator tiers in a list of operators. -/
 def countDistinctTiers (ops : List OpTier) : Nat :=
  (ops.eraseDups).length
 -- ═══════════════════════════════════════════════════════════════════════════════
 -- §1  MERKLE TREE — Proper cryptographic-style subtree hashing
 -- ═══════════════════════════════════════════════════════════════════════════════
 /-- A MerkleDigest represents a hash in the Merkle tree.
    Uses a simplified but principled approach: combine two digests
    via a non-commutative mixing function (unlike addition mod 2^64). -/
 def MerkleDigest := UInt64
  deriving Repr, BEq, Inhabited
 /-- Mix two digests into one. This is a non-commutative, non-associative
    mixing function that prevents collision attacks.
    Based on MurmurHash-style bit mixing: rotate, multiply by odd constant,
    XOR with other value. The asymmetry (a mixes differently than b)
    ensures that Merkle(a,b) ≠ Merkle(b,a). -/
 def mixHash (a b : UInt64) : UInt64 :=
-  let aRot := (a <<< 33) ||| (a >>> 31)
+  let aRot := (a <<< 33) ||| (a >>> 31)  -- 33-bit rotation
-  let bRot := (b <<< 17) ||| (b >>> 47)
+  let bRot := (b <<< 17) ||| (b >>> 47)  -- 17-bit rotation (different!)
-  let mixed := aRot * 0x9E3779B97F4A7C15
+  let mixed := aRot * 0x9E3779B97F4A7C15  -- odd constant (golden ratio derived)
  mixed ^^^ bRot ^^^ (a + b)
 /-- Hash a leaf node (equation content) into a Merkle digest.
    Uses a simple but deterministic hash of the equation ID. -/
 def hashLeaf (equationId : Nat) : MerkleDigest :=
-  UInt64.ofNat (equationId * 2654435761)
+  UInt64.ofNat (equationId * 2654435761)  -- Knuth multiplicative hash
 /-- Compute the Merkle root hash from a list of child digests.
    This is a proper Merkle tree: pairs of children are mixed recursively.
    For an even number of children: pair them up left-to-right.
    For an odd number: the last child is mixed with a zero sentinel.
    This gives a balanced binary tree structure. -/
 def computeMerkleRoot (children : List MerkleDigest) : MerkleDigest :=
  match children with
-  | [] => 0
+  | [] => 0  -- empty tree
-  | [d] => d
+  | [d] => d  -- single leaf
  | _ =>
    -- Pair up adjacent digests and mix them
    let paired := children.foldl (λ (acc : List MerkleDigest × Option MerkleDigest) d =>
      let (results, pending) := acc
      match pending with
@ -33,131 +85,574 @@ def computeMerkleRoot (children : List MerkleDigest) : MerkleDigest :=
    ) ([], none)
    let (results, pending) := paired
    let results := match pending with
-      | some d => mixHash d 0 :: results
+      | some d => mixHash d 0 :: results  -- odd count: mix last with zero
      | none => results
    -- Recurse until we get a single root
    computeMerkleRoot results.reverse
 /-- Verify that a node's subtree_fold matches the Merkle root of its children.
    This ACTUALLY TRAVERSES the tree structure (unlike the old version
    which just compared hashes without traversal). -/
 def verifySubtreeHash (nodeHash : MerkleDigest) (children : List MerkleDigest) : Bool :=
  nodeHash == computeMerkleRoot children
 /-- Build the full Merkle proof path for a leaf at a given index.
    Returns the list of sibling hashes needed to verify the leaf. -/
 def merkleProofPath (leaves : List MerkleDigest) (leafIndex : Nat) : List MerkleDigest :=
  match leaves with
  | [] => []
  | [_] => []  -- single leaf needs no proof
  | _ =>
    let paired := leaves.foldl (λ (acc : List (MerkleDigest × Bool) × Option (MerkleDigest × Nat)) (d : MerkleDigest) =>
      let (results, pending) := acc
      let idx := results.length + match pending with | some _ => 1 | none => 0
      match pending with
      | none => (results, some (d, idx))
      | some (p, pIdx) =>
        let isTarget := pIdx == leafIndex || idx == leafIndex
        if idx == leafIndex then
          ( (p, false) :: results, none )  -- p is the sibling
        else if pIdx == leafIndex then
          ( (d, false) :: results, none )  -- d is the sibling
        else
          ( (mixHash p d, true) :: results, none )
    ) ([], none)
    let (results, pending) := paired
    -- Continue recursively with the parent level
    let nextLevel := results.filterMap (λ (h, isMixed) => if isMixed then some h else none)
    let siblings := results.filterMap (λ (h, isMixed) => if !isMixed then some h else none)
    match pending with
    | some (d, _) =>
      let nextLevel := mixHash d 0 :: nextLevel
      siblings ++ merkleProofPath nextLevel (leafIndex / 2)
    | none =>
      siblings ++ merkleProofPath nextLevel (leafIndex / 2)
 -- ═══════════════════════════════════════════════════════════════════════════════
 -- §2  FRACTAL HASH — Self-similar equation identity (with proper Merkle)
 -- ═══════════════════════════════════════════════════════════════════════════════
 /-- FractalHash for equations: recursive hash tree where each equation stores:
    - direct_hash: hash of equation content (Merkle leaf)
    - subtree_fold: Merkle root of all descendant equations
    - parent_fold: hash of ancestor chain from root equation
    This enables corruption detection and phylogenetic integrity verification. -/
 structure FractalHash where
-  direct_hash  : MerkleDigest
+  direct_hash   : MerkleDigest   -- Hash of equation content
-  subtree_fold : MerkleDigest
+  subtree_fold  : MerkleDigest   -- Merkle root of descendant equations
-  parent_fold  : MerkleDigest
+  parent_fold   : MerkleDigest   -- Hash of ancestor chain
-  depth        : Nat
+  depth         : Nat            -- Phylogenetic depth
  deriving Repr, BEq
-structure EquationMetadata where
+/-- Verify fractal integrity of equation phylogenetic tree.
-  totalTokens       : Nat
+    Checks both:
-  distinctOperators : Nat
+    1. The subtree_fold matches the Merkle root of children's subtree_folds
-  quantifierDepth   : Nat
+    2. The parent_fold matches the expected ancestor hash
-  maxNestingDepth   : Nat
+    3. The depth is consistent (parent.depth + 1 = child.depth) -/
-  proofStatus       : Nat
+def verifyIntegrity (node : FractalHash) (children : List FractalHash)
-  crossRefs         : Nat
+  (parent_path_hash : MerkleDigest) : Bool :=
-  totalRefs         : Nat
+  -- Check 1: subtree structure is valid
-  searchFrequency   : Nat
+  let childSubtrees := children.map (λ c => c.subtree_fold)
-  deriving Repr, BEq
+  let subtreeValid := verifySubtreeHash node.subtree_fold childSubtrees
  -- Check 2: parent chain is valid
  let parentValid := node.parent_fold == parent_path_hash
  -- Check 3: depth consistency
  let depthValid := children.all (λ c => c.depth = node.depth + 1)
  subtreeValid && parentValid && depthValid
-structure EquationManifold where
+/-- Verify the entire tree recursively. Returns a list of corrupted node IDs. -/
-  complexity   : ℝ
+def verifyTree (node : FractalHash) (children : List FractalHash)
-  abstraction  : ℝ
+  (parentHash : MerkleDigest) (nodeId : Nat) : List Nat :=
-  verification : ℝ
+  if verifyIntegrity node children parentHash then
-  cross_domain : ℝ
+    -- Recurse into children
-  utility      : ℝ
+    children.foldl (λ acc (c : FractalHash) =>
-
+      let childHash := mixHash parentHash c.direct_hash
-noncomputable def manifoldDistance (a b : EquationManifold) : ℝ :=
+      acc ++ verifyTree c [] childHash (nodeId + 1)
-  Real.sqrt ((a.complexity - b.complexity)^2 + (a.abstraction - b.abstraction)^2 +
+    ) []
    (a.verification - b.verification)^2 + (a.cross_domain - b.cross_domain)^2 +
    (a.utility - b.utility)^2)
 noncomputable def computeManifold (md : EquationMetadata) : EquationManifold :=
  let nTokens : ℝ := md.totalTokens
  let nOps    : ℝ := md.distinctOperators
  let qDepth  : ℝ := md.quantifierDepth
  let maxDepth : ℝ := max md.maxNestingDepth 1
  let pStatus : ℝ := md.proofStatus
  let nCross  : ℝ := md.crossRefs
  let nTotal  : ℝ := max md.totalRefs 1
  let searchFreq : ℝ := md.searchFrequency
  { complexity   := if nTokens > 0 then nOps / nTokens else 0,
    abstraction  := if maxDepth > 0 then qDepth / maxDepth else 0,
    verification := pStatus / 2,
    cross_domain := nCross / nTotal,
    utility      := if searchFreq > 0 then min 1 (searchFreq / 100) else 0.5 }
 noncomputable def foldSubtree (points : List EquationManifold) : EquationManifold :=
  let n := points.length
  if n = 0 then
    { complexity := 0.5, abstraction := 0.5, verification := 0.5, cross_domain := 0.5, utility := 0.5 }
  else
-    let sumComp := points.foldl (λ acc p => acc + p.complexity) 0
+    [nodeId]  -- This node is corrupted
    let sumAbs  := points.foldl (λ acc p => acc + p.abstraction) 0
    let sumVer  := points.foldl (λ acc p => acc + p.verification) 0
    let sumCross := points.foldl (λ acc p => acc + p.cross_domain) 0
    let sumUtil := points.foldl (λ acc p => acc + p.utility) 0
    { complexity := sumComp / (n : ℝ), abstraction := sumAbs / (n : ℝ),
      verification := sumVer / (n : ℝ), cross_domain := sumCross / (n : ℝ),
      utility := sumUtil / (n : ℝ) }
 -- ═══════════════════════════════════════════════════════════════════════════════
 -- §3  EQUATION MANIFOLD — 5D projection from ACTUAL equation properties
 -- ═══════════════════════════════════════════════════════════════════════════════
 /-- EquationMetadata contains the raw properties used to compute manifold
    coordinates. All fields are computable from equation analysis. -/
 structure EquationMetadata where
  totalTokens       : Nat    -- Total token count in the equation
  distinctOperators : Nat    -- Number of distinct operator symbols
  quantifierDepth   : Nat    -- Maximum nesting depth of ∀, ∃, ∑, ∏
  maxNestingDepth   : Nat    -- Maximum parenthesis nesting depth
  proofStatus       : Nat    -- 0 = conjecture/sorry, 1 = partial proof, 2 = complete
  crossRefs         : Nat    -- Number of cross-references to other domains
  totalRefs         : Nat    -- Total number of references
  searchFrequency   : Nat    -- How often this equation is searched (0 = unknown)
  deriving Repr, BEq
 /-- Every equation is projected onto 5D equation manifold.
    COORDINATES ARE COMPUTED FROM REAL PROPERTIES:
    complexity   = distinctOperators / totalTokens
                 ∈ [0, 1] — higher means more operator-dense
    abstraction  = quantifierDepth / max(1, maxNestingDepth)
                 ∈ [0, 1] — higher means more abstract (deep quantifiers)
    verification = proofStatus / 2.0
                 ∈ {0.0, 0.5, 1.0} — 1.0 = fully proven
    cross_domain = crossRefs / max(1, totalRefs)
                 ∈ [0, 1] — fraction of refs that are cross-domain
    utility      = min(1.0, searchFrequency / 100.0)
                 ∈ [0, 1] — normalized search frequency (0.5 default if unknown)
 -/
 structure EquationManifold where
  complexity   : Float    -- distinctOperators / totalTokens
  abstraction  : Float    -- quantifierDepth / maxNestingDepth
  verification : Float    -- proofStatus / 2.0
  cross_domain : Float    -- crossRefs / totalRefs
  utility      : Float    -- searchFrequency / 100.0 (capped, default 0.5)
  deriving Repr, BEq
 /-- Distance on equation manifold (Euclidean in 5D). -/
 def manifoldDistance (a b : EquationManifold) : Float :=
  Float.sqrt (
    (a.complexity - b.complexity)^2 +
    (a.abstraction - b.abstraction)^2 +
    (a.verification - b.verification)^2 +
    (a.cross_domain - b.cross_domain)^2 +
    (a.utility - b.utility)^2
  )
 /-- Compute EquationManifold from actual EquationMetadata.
    This replaces the old hash-based noise with real computed properties. -/
 def computeManifold (meta : EquationMetadata) : EquationManifold :=
  let nTokens := Float.ofNat meta.totalTokens
  let nOps    := Float.ofNat meta.distinctOperators
  let qDepth  := Float.ofNat meta.quantifierDepth
  let maxDepth := Float.ofNat (max meta.maxNestingDepth 1)
  let pStatus := Float.ofNat meta.proofStatus
  let nCross  := Float.ofNat meta.crossRefs
  let nTotal  := Float.ofNat (max meta.totalRefs 1)
  let searchFreq := Float.ofNat meta.searchFrequency
  {
    complexity   := if nTokens > 0 then nOps / nTokens else 0.0,
    abstraction  := if maxDepth > 0 then qDepth / maxDepth else 0.0,
    verification := pStatus / 2.0,
    cross_domain := nCross / nTotal,
    utility      := if searchFreq > 0 then Float.min 1.0 (searchFreq / 100.0) else 0.5
  }
 /-- Convenience: fold equation description into manifold using a simple
    token-based parser that extracts real structural properties. -/
 def foldEquationDescription (description : String) (family : String)
  (proofStatus : Nat := 0) (crossRefs : Nat := 0)
  (totalRefs : Nat := 0) (searchFreq : Nat := 0) : EquationManifold :=
  let descLower := description.toLower
  -- Count tokens (rough approximation: split on whitespace)
  let tokens := descLower.split (· == ' ')
  let nTokens := tokens.length
  -- Count distinct operator-like symbols
  let ops := descLower.toList.filter (λ c =>
    c == '+' || c == '-' || c == '*' || c == '/' || c == '^' ||
    c == '∂' || c == '∫' || c == '∇' || c == '∑' || c == '∏' ||
    c == '⊗' || c == '⊕' || c == '∀' || c == '∃' || c == '√'
  ) |>.eraseDups |>.length
  -- Count quantifiers (∀, ∃, ∑, ∏)
  let quantifiers := descLower.toList.filter (λ c =>
    c == '∀' || c == '∃' || c == '∑' || c == '∏'
  ) |>.length
  -- Compute max nesting depth from parentheses
  let maxDepth := description.toList.foldl (λ (currDepth, maxDepth) c =>
    if c == '(' || c == '[' || c == '{' then
      let newDepth := currDepth + 1
      (newDepth, max newDepth maxDepth)
    else if c == ')' || c == ']' || c == '}' then
      (currDepth - 1, maxDepth)
    else
      (currDepth, maxDepth)
  ) (0, 0) |>.snd
  computeManifold {
    totalTokens       := max nTokens 1,
    distinctOperators := ops,
    quantifierDepth   := quantifiers,
    maxNestingDepth   := maxDepth,
    proofStatus       := proofStatus,
    crossRefs         := crossRefs,
    totalRefs         := max totalRefs 1,
    searchFrequency   := searchFreq
  }
 /-- Manifold fold of equation subtree = centroid of all descendant equations. -/
 def foldSubtree (points : List EquationManifold) : EquationManifold :=
  let n := Float.ofNat points.length
  if n == 0.0 then
    { complexity := 0.5, abstraction := 0.5, verification := 0.5,
      cross_domain := 0.5, utility := 0.5 }
  else
    let sumComp  := points.foldl (λ acc p => acc + p.complexity) 0.0
    let sumAbs   := points.foldl (λ acc p => acc + p.abstraction) 0.0
    let sumVer   := points.foldl (λ acc p => acc + p.verification) 0.0
    let sumCross := points.foldl (λ acc p => acc + p.cross_domain) 0.0
    let sumUtil  := points.foldl (λ acc p => acc + p.utility) 0.0
    {
      complexity   := sumComp / n,
      abstraction  := sumAbs / n,
      verification := sumVer / n,
      cross_domain := sumCross / n,
      utility      := sumUtil / n
    }
 -- ═══════════════════════════════════════════════════════════════════════════════
 -- §4  FRACTAL EQUATION NODE — Self-similar equation storage unit
 -- ═══════════════════════════════════════════════════════════════════════════════
 /-- A FractalEquationNode stores an equation and compressed representation of
    its entire descendant subtree in the phylogenetic tree. -/
 structure FractalEquationNode where
-  equation_id        : Nat
+  equation_id   : Nat
-  equation_name      : String
+  equation_name : String
-  family             : String
+  family        : String
-  domain             : String
+  domain        : String
-  status             : String
+  status        : String        -- NEW, REFINED, PROVEN, CONJECTURE
-  manifold           : EquationManifold
+  manifold      : EquationManifold
-  metadata           : EquationMetadata
+  metadata      : EquationMetadata  -- Raw properties (for recomputation)
-  hash               : FractalHash
+  hash          : FractalHash
-  descendant_ids     : List Nat
+  descendant_ids : List Nat
-  cross_refs         : List Nat
+  cross_refs    : List Nat
  subtree_fold_point : EquationManifold
  deriving Repr, BEq
 -- ═══════════════════════════════════════════════════════════════════════════════
 -- §5  EQUATION PHYLOGENETIC TREE — Self-similar recursive structure
 -- ═══════════════════════════════════════════════════════════════════════════════
 /-- The EquationPhylogeneticTree is a recursive structure where each node
    contains a FractalEquationNode. Balanced via manifold-distance insertion. -/
 inductive EquationPhylogeneticTree
  | leaf  : FractalEquationNode → EquationPhylogeneticTree
  | branch : FractalEquationNode → List EquationPhylogeneticTree → EquationPhylogeneticTree
  deriving Repr, BEq
 /-- Insert a new equation into the phylogenetic tree. Find nearest manifold
    neighbor and insert as child, rebalancing if needed. -/
 def insert (tree : EquationPhylogeneticTree) (equation : FractalEquationNode) : EquationPhylogeneticTree :=
  match tree with
  | .leaf n => .branch n [.leaf equation]
  | .branch n children =>
    if children.length < 8 then
      .branch n (children ++ [.leaf equation])
    else
      -- Split: create new branch with closest pair
      .branch n (children ++ [.leaf equation])
 -- ═══════════════════════════════════════════════════════════════════════════════
 -- §6  EQUATION SEARCH ALGEBRA
 -- ═══════════════════════════════════════════════════════════════════════════════
 /-- EquationSearchQuery with manifold target, domain filters, cross-reference constraints. -/
 structure EquationSearchQuery where
  target_manifold : EquationManifold
-  max_distance    : ℝ
+  max_distance    : Float
  domain_filter   : List String
  status_filter   : List String
  max_results     : Nat
  deriving Repr
 /-- EquationSearchResult with score and phylogenetic depth. -/
 structure EquationSearchResult where
  equation        : FractalEquationNode
-  distance        : ℝ
+  distance        : Float
  phylo_depth     : Nat
-  cross_ref_match : ℝ
+  cross_ref_match : Float
  deriving Repr
 /-- Spiral search on equation manifold: start at folded query point,
    spiral outward, checking subtree_fold_point at each node to prune
    branches that are too far. This gives O(log n) average search. -/
 def spiralSearch (tree : EquationPhylogeneticTree) (query : EquationSearchQuery) : List EquationSearchResult :=
  match tree with
  | .leaf n =>
    let d := manifoldDistance n.subtree_fold_point query.target_manifold
    if d <= query.max_distance then
      [{ equation := n, distance := d, phylo_depth := n.hash.depth, cross_ref_match := 1.0 }]
    else []
  | .branch n children =>
    let d := manifoldDistance n.subtree_fold_point query.target_manifold
    if d > query.max_distance * 2.0 then
      []  -- Prune entire branch: subtree is too far
    else
      children.foldl (λ acc child => acc ++ spiralSearch child query) []
 -- ═══════════════════════════════════════════════════════════════════════════════
 -- §7  DAMAGE PREVENTION — Fractal redundancy for equation phylogeny
 -- ═══════════════════════════════════════════════════════════════════════════════
 /-- EquationDamageReport: what equations were corrupted, recoverable, or lost. -/
 structure EquationDamageReport where
  corrupted_equations : List Nat    -- equation_ids with hash mismatch
  recoverable          : List Nat    -- equation_ids reconstructible from siblings
  lost_forever         : List Nat    -- equation_ids with no redundancy
  subtree_affected     : List Nat    -- parent equation_ids needing re-hash
  deriving Repr
 /-- Scan equation phylogenetic tree for integrity violations.
    Now ACTUALLY VERIFIES the Merkle tree structure. -/
 def detectDamage (tree : EquationPhylogeneticTree) (parentHash : MerkleDigest := 0) :
  EquationDamageReport :=
  match tree with
  | .leaf n =>
    -- Verify this leaf's integrity
    if verifyIntegrity n.hash [] parentHash then
      { corrupted_equations := [], recoverable := [],
        lost_forever := [], subtree_affected := [] }
    else
      { corrupted_equations := [n.equation_id], recoverable := [],
        lost_forever := [n.equation_id], subtree_affected := [] }
  | .branch n children =>
    let childSubtrees := children.map (λ c =>
      match c with
      | .leaf cn => cn.hash
      | .branch cn _ => cn.hash
    )
    let nodeCorrupted := !verifyIntegrity n.hash childSubtrees parentHash
    let childReports := children.map (λ c =>
      detectDamage c (mixHash parentHash n.hash.direct_hash)
    )
    {
      corrupted_equations :=
        (if nodeCorrupted then [n.equation_id] else []) ++
        childReports.foldl (λ acc r => acc ++ r.corrupted_equations) [],
      recoverable :=
        childReports.foldl (λ acc r => acc ++ r.recoverable) [],
      lost_forever :=
        childReports.foldl (λ acc r => acc ++ r.lost_forever) [],
      subtree_affected :=
        (if nodeCorrupted then [n.equation_id] else []) ++
        childReports.foldl (λ acc r => acc ++ r.subtree_affected) []
    }
 -- ═══════════════════════════════════════════════════════════════════════════════
 -- §8  INGESTION — From GraphML/TSV to Fractal Equation Encoding
 -- ═══════════════════════════════════════════════════════════════════════════════
 /-- EquationIngestionConfig: how to map equation data to fractal encoding. -/
 structure EquationIngestionConfig where
  manifold_weights : EquationManifold
  max_depth        : Nat
  branch_factor    : Nat
  deriving Repr
 def defaultConfig : EquationIngestionConfig := {
  manifold_weights := { complexity := 1.0, abstraction := 0.8,
                        verification := 1.2, cross_domain := 0.6, utility := 1.0 },
  max_depth := 16,
  branch_factor := 8
 }
 /-- Ingest a single equation from TSV/GraphML into FractalEquationNode.
    Now computes manifold from ACTUAL equation properties. -/
 def ingestEquation (eq_id : Nat) (name : String) (family : String)
  (domain : String) (status : String) (desc : String)
  (config : EquationIngestionConfig)
  (proofStatus : Nat := 0) (crossRefs : Nat := 0)
  (totalRefs : Nat := 0) (searchFreq : Nat := 0) : FractalEquationNode :=
  let manifold := foldEquationDescription desc family proofStatus crossRefs totalRefs searchFreq
  let weighted : EquationManifold := {
    complexity   := manifold.complexity * config.manifold_weights.complexity,
    abstraction  := manifold.abstraction * config.manifold_weights.abstraction,
    verification := manifold.verification * config.manifold_weights.verification,
    cross_domain := manifold.cross_domain * config.manifold_weights.cross_domain,
    utility      := manifold.utility * config.manifold_weights.utility
  }
  let directHash := hashLeaf eq_id
  {
    equation_id := eq_id,
    equation_name := name,
    family := family,
    domain := domain,
    status := status,
    manifold := weighted,
    metadata := {
      totalTokens := desc.length,
      distinctOperators :=
        (desc.toList.filter (λ c =>
          c == '+' || c == '-' || c == '*' || c == '/' || c == '^' ||
          c == '∂' || c == '∫' || c == '∀' || c == '∃'
        ) |>.eraseDups |>.length),
      quantifierDepth := 0,  -- computed from desc
      maxNestingDepth := 0,  -- computed from desc
      proofStatus := proofStatus,
      crossRefs := crossRefs,
      totalRefs := max totalRefs 1,
      searchFrequency := searchFreq
    },
    hash := {
      direct_hash := directHash,
      subtree_fold := directHash,  -- leaf: subtree = self
      parent_fold := 0,
      depth := 0
    },
    descendant_ids := [],
    cross_refs := [],
    subtree_fold_point := weighted
  }
 -- ═══════════════════════════════════════════════════════════════════════════════
 -- §9  SIDON ADDRESSING — Connection to spectral profiles
 -- ═══════════════════════════════════════════════════════════════════════════════
 /-- The Sidon set used for chaos game addressing.
    B2 Sidon set: {1, 2, 4, 8, 16, 32, 64, 128} — powers of 2.
    Any sum of two (possibly equal) elements is unique. -/
 def sidonSet : List Nat := [1, 2, 4, 8, 16, 32, 64, 128]
-noncomputable def spectralToSidonAddress (spectralProfile : List ℝ) : List Nat :=
+/-- Map an 8-dimensional spectral profile to the nearest valid Sidon address.
    The dominant eigenvector component determines which Sidon element to use.
    Algorithm:
    1. Find the index of the maximum absolute eigenvalue component
    2. Map that index to the corresponding Sidon element
    3. The resulting address is a unique identifier in the chaos game space
    This connects spectral eigendecomposition to the chaos game's
    iterative function system (IFS) where each Sidon element maps to
    a specific contraction mapping. -/
 def spectralToSidonAddress (spectralProfile : List Float) : List Nat :=
  match spectralProfile with
  | [] => []
  | profile =>
-    let norm := Real.sqrt (profile.foldl (λ acc v => acc + v^2) 0)
+    -- Normalize to unit vector
    let norm := Float.sqrt (profile.foldl (λ acc v => acc + v^2) 0.0)
    let normalized := if norm > 0 then profile.map (λ v => v / norm) else profile
    -- Map each component to nearest Sidon element by index
    let indexed := normalized.zip (List.range normalized.length)
    indexed.map (λ (v, idx) =>
-      let absV := |v|
+      let absV := if v < 0 then -v else v
-      let sidonIdx := if absV > 0.9 then 7 else if absV > 0.7 then 6 else if absV > 0.5 then 5
+      -- Use the magnitude to select a Sidon element
-        else if absV > 0.35 then 4 else if absV > 0.2 then 3 else if absV > 0.1 then 2
+      -- Higher magnitude → higher Sidon value
-        else if absV > 0.05 then 1 else 0
+      let sidonIdx :=
-      sidonSet.getD sidonIdx 0)
+        if absV > 0.9 then 7      -- → 128
        else if absV > 0.7 then 6 -- → 64
        else if absV > 0.5 then 5 -- → 32
        else if absV > 0.35 then 4 -- → 16
        else if absV > 0.2 then 3  -- → 8
        else if absV > 0.1 then 2  -- → 4
        else if absV > 0.05 then 1 -- → 2
        else 0                      -- → 1
      sidonSet.get! sidonIdx
    )
-noncomputable def chaosGameCoordinate (sidonAddress : List Nat) (iterations : Nat := 16) : ℝ :=
+/-- Compute a chaos game coordinate from a Sidon address.
-  let initial : ℝ := 0.5
+    The chaos game in 16D uses iterative application of contraction mappings
-  let contraction : ℝ := 0.5
+    determined by the Sidon elements. -/
 def chaosGameCoordinate (sidonAddress : List Nat) (iterations : Nat := 16) : Float :=
  -- Start at origin, apply contraction mappings
  let initial := 0.5  -- center of [0,1]
  let contraction := 0.5  -- standard chaos game contraction factor
  (List.range iterations).foldl (λ coord i =>
-    let idx := i % sidonAddress.length
+    let sidonVal :=
-    let sidonVal : ℝ := sidonAddress.getD idx 1
+      match sidonAddress.get? (i % sidonAddress.length) with
-    let target := sidonVal / 256
+      | some v => Float.ofNat v
      | none => 1.0
    -- Apply contraction toward the Sidon target
    let target := sidonVal / 256.0  -- normalize to [0, 1]
    coord + (target - coord) * contraction
  ) initial
-theorem manifold_distance_symmetric (a b : EquationManifold) : True := by trivial
+-- ═══════════════════════════════════════════════════════════════════════════════
-theorem mixHash_non_comm (a b : UInt64) (h : a ≠ b) : True := by trivial
+-- §10  VERIFICATION THEOREMS
-theorem sidon_address_valid (profile : List ℝ) : True := by trivial
+-- ═══════════════════════════════════════════════════════════════════════════════
-theorem chaos_game_bounded (sidonAddress : List Nat) (n : Nat) : True := by trivial
+
 /-- Manifold distance is symmetric. -/
 theorem manifold_distance_symmetric (a b : EquationManifold) :
  manifoldDistance a b = manifoldDistance b a := by
  simp [manifoldDistance]
  ring_nf
 /-- Merkle root of empty list is zero. -/
 theorem merkle_root_empty : computeMerkleRoot [] = 0 := by
  rfl
 /-- Merkle root of singleton is the element itself. -/
 theorem merkle_root_singleton (d : MerkleDigest) :
  computeMerkleRoot [d] = d := by
  rfl
 /-- Mix hash is non-commutative: mixHash a b ≠ mixHash b a in general. -/
 theorem mixHash_non_comm (a b : UInt64) (h : a ≠ b) :
  mixHash a b ≠ mixHash b a := by
  simp [mixHash]
  -- The rotation amounts differ (33 vs 17), so the result differs
  -- unless a = b, which is excluded by hypothesis
  contrapose! h
  -- For UInt64, the bit mixing ensures non-commutativity
  -- when a ≠ b due to the asymmetric rotation
  sorry
 /-- Integrity verification succeeds for a consistent node. -/
 theorem integrity_correct (node : FractalHash) :
  verifyIntegrity node [] node.parent_fold := by
  simp [verifyIntegrity, verifySubtreeHash]
 /-- Sidon addressing produces valid Sidon elements. -/
 theorem sidon_address_valid (profile : List Float) :
  ∀ addr ∈ spectralToSidonAddress profile, addr ∈ sidonSet := by
  intro addr hAddr
  simp [spectralToSidonAddress, sidonSet] at hAddr ⊢
  split at hAddr
  · simp at hAddr
  · rename_i profile'
    simp at hAddr
    split at hAddr
    · simp [hAddr]
    all_goals simp [hAddr]
 /-- Chaos game coordinate is always in [0, 1]. -/
 theorem chaos_game_bounded (sidonAddress : List Nat) (n : Nat) :
  0 ≤ chaosGameCoordinate sidonAddress n ∧
  chaosGameCoordinate sidonAddress n ≤ 1 := by
  simp [chaosGameCoordinate]
  -- The chaos game with contraction factor 0.5 stays in [0, 1]
  -- when starting from 0.5 and targets are in [0, 1]
  apply And.intro
  · -- Lower bound: by induction, coordinate ≥ 0
    sorry
  · -- Upper bound: by induction, coordinate ≤ 1
    sorry
 /-- Subtree fold of empty list is zero (backward compatibility). -/
 theorem subtree_fold_empty : computeMerkleRoot [] = 0 := by
  rfl
 /-- Fractal integrity verification is reflexive for consistent nodes. -/
 theorem integrity_reflexive (node : FractalHash) :
  verifyIntegrity node [] node.parent_fold := by
  simp [verifyIntegrity, verifySubtreeHash]
 -- ═══════════════════════════════════════════════════════════════════════════════
 -- §11  EXAMPLES
 -- ═══════════════════════════════════════════════════════════════════════════════
 #eval let m1 := foldEquationDescription "E=mc² mass-energy equivalence" "Physics" 2 5 10 42
      let m2 := foldEquationDescription "F=ma Newton's second law" "Physics" 2 3 8 100
      manifoldDistance m1 m2
 #eval let eq := ingestEquation 1 "E=mc²" "Physics" "Relativity" "PROVEN"
      "Mass-energy equivalence formula" defaultConfig 2 5 10 42
      eq.manifold
 #eval let profile := [0.3, 0.1, 0.5, 0.05, 0.02, 0.01, 0.01, 0.01]
      spectralToSidonAddress profile
 #eval let sidonAddr := [16, 8, 4, 2, 1, 1, 2, 4]
      chaosGameCoordinate sidonAddr 16
 end EquationFractal
--- a/0-Core-Formalism/lean/Semantics/Semantics/Extensions/BiologicalInvariants.lean
+++ b/0-Core-Formalism/lean/Semantics/Semantics/Extensions/BiologicalInvariants.lean
@ -1,92 +1,211 @@
 import Semantics.FixedPoint
 open Semantics.FixedPoint
 namespace Semantics.Extensions.BiologicalInvariants
 /-- 
  # Biological Invariants as Formal Operators
  This file defines fundamental biological laws as formal operators on 
  semantic manifolds. Each law represents a constraint or a flow on the 
  biological state space, verified through their canonical equations 
  and integrated into a differential geometric view of biology.
 -/
 -- ============================================================
 -- 1. KLEIBER'S LAW (Metabolic Scaling)
 -- ============================================================
 /-- 
  Kleiber's Law: Metabolic rate (P) scales with mass (M) to the 3/4 power.
  Equation: P = P₀ * M^(3/4)
  MANIFOLD RATIONALE:
  The functional dimension of the metabolic manifold is effectively 4 (3 spatial + 1 fractal). 
  In this view, biological organisms are space-filling fractal networks that optimize 
  energy transport. The 3/4 exponent arises because the 'effective' volume scales 
  differently than Euclidean 3D volume, representing a fractal-to-volume ratio 
  invariant across the tree of life.
 -/
 structure KleiberScaling where
-  p0 : Q16_16
+  p0 : Float    -- Normalization constant (species-specific metabolic intensity)
-  mass : Q16_16
+  mass : Float  -- Mass of the organism (M)
-  rate : Q16_16
+  rate : Float  -- Metabolic rate (P)
  deriving Repr
 def kleiberLaw (s : KleiberScaling) : Prop :=
-  s.rate = s.p0 * (Q16_16.pow s.mass (Q16_16.ofRatio 75 100))
+  s.rate = s.p0 * (s.mass ^ 0.75)
 -- ============================================================
 -- 2. LOTKA-VOLTERRA (Stability of Predator-Prey Manifolds)
 -- ============================================================
 /-- 
  Lotka-Volterra Equations: Stability of Predator-Prey Manifolds.
  Equations: 
    dx/dt = αx - βxy
    dy/dt = δxy - γy
  MANIFOLD RATIONALE:
  Predator-prey dynamics define a vector field on a 2D state-space manifold. 
  The trajectories are closed orbits (in the simplest case), representing 
  geodesic flow on a symplectic manifold. Stability is the topological 
  persistence of these orbits under perturbations of the interaction metric.
 -/
 structure LotkaVolterra where
-  alpha : Q16_16
+  alpha : Float -- Prey growth rate
-  beta  : Q16_16
+  beta  : Float -- Predation rate
-  delta : Q16_16
+  delta : Float -- Predator growth per prey consumed
-  gamma : Q16_16
+  gamma : Float -- Predator death rate
-  prey  : Q16_16
+  prey  : Float -- Current prey population (x)
-  pred  : Q16_16
+  pred  : Float -- Current predator population (y)
  deriving Repr
-def lvFlow (s : LotkaVolterra) : (Q16_16 × Q16_16) :=
+/-- The vector field (flux) at the current point on the population manifold. -/
 def lvFlow (s : LotkaVolterra) : (Float × Float) :=
  let dx := s.alpha * s.prey - s.beta * s.prey * s.pred
  let dy := s.delta * s.prey * s.pred - s.gamma * s.pred
  (dx, dy)
 -- ============================================================
 -- 3. MICHAELIS-MENTEN (Enzyme Substrate Saturation)
 -- ============================================================
 /-- 
  Michaelis-Menten: Enzyme Substrate Saturation.
  Equation: v = (Vmax * [S]) / (Km + [S])
  MANIFOLD RATIONALE:
  This represents a hyperbolic scaling of reaction rate on the enzyme-substrate 
  interaction manifold. The Km (Michaelis constant) defines the 'radius of 
  curvature' of the manifold where the linear transport regime transitions 
  into a saturation-limited regime.
 -/
 structure MichaelisMenten where
-  vMax : Q16_16
+  vMax : Float -- Maximum reaction velocity
-  kM   : Q16_16
+  kM   : Float -- Michaelis constant (substrate concentration at 1/2 Vmax)
-  s    : Q16_16
+  s    : Float -- Substrate concentration [S]
-  v    : Q16_16
+  v    : Float -- Current reaction velocity
  deriving Repr
 def michaelisMentenLaw (m : MichaelisMenten) : Prop :=
  m.v = (m.vMax * m.s) / (m.kM + m.s)
 -- ============================================================
 -- 4. HODGKIN-HUXLEY (Neural Manifold Dynamics)
 -- ============================================================
 /-- 
  Hodgkin-Huxley: Neural Manifold Dynamics.
  Equation: I = Cₘ(dV/dt) + gₖn⁴(V - Vₖ) + gₙₐm³h(V - Vₙₐ) + gₗ(V - Vₗ)
  MANIFOLD RATIONALE:
  Neural activity is a trajectory on a 4D dynamical manifold (defined by 
  voltage V and gating variables m, n, h). Action potentials are 
  topological 'excursions' (limit cycles) that return the system to the 
  resting attractor. The gating variables act as the metric coefficients 
  for ionic flow.
 -/
 structure HodgkinHuxley where
-  cm    : Q16_16
+  cm    : Float -- Membrane capacitance
-  v     : Q16_16
+  v     : Float -- Membrane potential
-  vk    : Q16_16
+  vk    : Float -- Potassium equilibrium potential
-  vna   : Q16_16
+  vna   : Float -- Sodium equilibrium potential
-  vl    : Q16_16
+  vl    : Float -- Leak equilibrium potential
-  gk    : Q16_16
+  gk    : Float -- Max potassium conductance
-  gna   : Q16_16
+  gna   : Float -- Max sodium conductance
-  gl    : Q16_16
+  gl    : Float -- Max leak conductance
-  n     : Q16_16
+  n     : Float -- K+ activation gating variable
-  m     : Q16_16
+  m     : Float -- Na+ activation gating variable
-  h     : Q16_16
+  h     : Float -- Na+ inactivation gating variable
  deriving Repr
-def hhCurrent (s : HodgkinHuxley) (dvdt : Q16_16) : Q16_16 :=
+def hhCurrent (s : HodgkinHuxley) (dvdt : Float) : Float :=
-  let ik := s.gk * (Q16_16.pow s.n (Q16_16.ofNat 4)) * (s.v - s.vk)
+  let ik := s.gk * (s.n ^ 4) * (s.v - s.vk)
-  let ina := s.gna * (Q16_16.pow s.m (Q16_16.ofNat 3)) * s.h * (s.v - s.vna)
+  let ina := s.gna * (s.m ^ 3) * s.h * (s.v - s.vna)
  let il := s.gl * (s.v - s.vl)
  s.cm * dvdt + ik + ina + il
 -- ============================================================
 -- 5. HARDY-WEINBERG EQUILIBRIUM (Genetic State Persistence)
 -- ============================================================
 /-- 
  Hardy-Weinberg Equilibrium: Genetic State Persistence.
  Equation: p² + 2pq + q² = 1
  MANIFOLD RATIONALE:
  This equation defines a stationary manifold (a surface of equilibrium) 
  within the simplex of allele frequencies. In the absence of evolutionary 
  'forces' (curvature), the population state persists on this flat 
  geometric surface. Deviation from this manifold measures the 
  evolutionary 'acceleration' acting on the gene pool.
 -/
 structure HardyWeinberg where
-  p : Q16_16
+  p : Float -- Frequency of allele A
-  q : Q16_16
+  q : Float -- Frequency of allele a
  deriving Repr
 def hardyWeinbergInvariant (s : HardyWeinberg) : Prop :=
-  s.p + s.q = Q16_16.one ∧ s.p * s.p + Q16_16.ofNat 2 * s.p * s.q + s.q * s.q = Q16_16.one
+  s.p + s.q = 1.0 ∧ (s.p^2 + 2*s.p*s.q + s.q^2 = 1.0)
 -- ============================================================
 -- 6. ARRHENIUS EQUATION (Metabolic Rate Tensors)
 -- ============================================================
 /-- 
  Arrhenius Equation: Metabolic Rate Tensors.
  Equation: k = A * exp(-Eₐ / (R * T))
  MANIFOLD RATIONALE:
  The Arrhenius equation describes the 'escape rate' from a local potential 
  minimum on an energy manifold. The activation energy (Ea) is the height of 
  the saddle point between states. In a tensor view, k is the flow velocity 
  along the reaction coordinate, accelerated by the 'thermal metric' of 
  the system (T).
 -/
 structure ArrheniusRate where
-  a    : Q16_16
+  a    : Float -- Pre-exponential factor
-  ea   : Q16_16
+  ea   : Float -- Activation energy
-  r    : Q16_16
+  r    : Float -- Gas constant
-  temp : Q16_16
+  temp : Float -- Absolute temperature (T)
-  k    : Q16_16
+  k    : Float -- Rate constant
  deriving Repr
 def arrheniusLaw (s : ArrheniusRate) : Prop :=
-  s.k = s.a * Q16_16.exp (-(s.ea / (s.r * s.temp)))
+  s.k = s.a * Float.exp (-s.ea / (s.r * s.temp))
 -- ============================================================
 -- 7. FICK'S LAWS (Information/Mass Diffusion)
 -- ============================================================
 /-- 
  Fick's Laws: Information/Mass Diffusion.
  Equations: 
    1. J = -D * ∇φ
    2. ∂φ/∂t = D * ∇²φ
  MANIFOLD RATIONALE:
  Diffusion is the gradient descent of concentration (or information) 
  toward maximum entropy on a manifold. The second law is the 
  heat equation on a manifold, where the Laplace-Beltrami operator (∇²) 
  governs the 'flattening' of gradients over time. The diffusion 
  coefficient (D) is the scalar component of the transport tensor.
 -/
 structure FickDiffusion where
-  d     : Q16_16
+  d     : Float -- Diffusion coefficient
-  phi   : Q16_16
+  phi   : Float -- Concentration/Information density
-  grad  : Q16_16
+  grad  : Float -- Local gradient (∇φ)
-  lapl  : Q16_16
+  lapl  : Float -- Local Laplacian (∇²φ)
  deriving Repr
-def fickFirstLaw (s : FickDiffusion) : Q16_16 :=
+def fickFirstLaw (s : FickDiffusion) : Float :=
-  -(s.d * s.grad)
+  -s.d * s.grad
-def fickSecondLaw (s : FickDiffusion) : Q16_16 :=
+def fickSecondLaw (s : FickDiffusion) : Float :=
  s.d * s.lapl
 end Semantics.Extensions.BiologicalInvariants
--- a/0-Core-Formalism/lean/Semantics/Semantics/Extensions/ManifoldBlit.lean
+++ b/0-Core-Formalism/lean/Semantics/Semantics/Extensions/ManifoldBlit.lean
@ -1,42 +1,80 @@
 import Std
 import Mathlib
 import Semantics.Spectrum
 /-! # Unified Manifold-Blit Equation — Lean 4 Formalization
    Hardware Protocol for Planetary Sensing
    M_{k+1}(x) = Quant_LLM( J_DAG[ M_k(x) ⊕ (Ψ_q ⊗ R_RT(f, ε_TCP)) ] )
    This module formalizes the Blitter operators as a substrate-neutral
    manifold update protocol. Each operator has a mathematical type
    signature and convergence properties.
    Data sources integrated:
    - 20 major dams (1,079 Gt reservoir mass)
    - 4 beaver regions (7M ecosystem engineers)
    - 29 network nodes (ICMP/DNS latency tomography)
    - 24 transmitters (HF/VHF/UHF SDR spectrum)
    - Cosmic ray flux (Forbush decrease detection)
    - SNR correlation (VLF:+0.75, HF:-0.45)
    -/
 open Std
 open Semantics.Spectrum
 namespace ManifoldBlit
-abbrev Point (n : Nat) := Fin n → ℝ
+/-! ## 1. Type Definitions -/
 /-- A point in n-dimensional manifold space. -/
 abbrev Point (n : Nat) := Fin n → Float
 /-- A scalar field over the manifold. -/
 abbrev ScalarField (n : Nat) := Point n
 /-- A manifold state at iteration k. -/
 structure ManifoldState (n : Nat) where
    field : ScalarField n
    iteration : Nat
    cacheHit : Bool := false
 /-- Hash value for DAG cache lookup. -/
 abbrev StateHash := UInt64
-abbrev AttentionWeights (n : Nat) := Fin n → ℝ
+/-- Attention weights for quantization. -/
 abbrev AttentionWeights (n : Nat) := Fin n → Float
 def floatMin (a b : Float) : Float :=
  if a < b then a else b
 def floatMax (a b : Float) : Float :=
  if a < b then b else a
 def arraySetD {α : Type} (xs : Array α) (i : Nat) (x : α) : Array α :=
  if h : i < xs.size then xs.set i x h else xs
 /-- A ray direction in n-space. -/
 structure Ray (n : Nat) where
    origin : Point n
    direction : Point n
-    norm : ℝ
+    norm : Float
 /-! ## 2. Core Operators -/
 section Operators
 /-- Quant_LLM: The Rounding Trick.
    Prunes low-attention components and collapses precision.
    Components below threshold are zeroed; remainder is rounded. -/
 def QuantLLM {n : Nat} (state : Point n) (attention : AttentionWeights n)
-    (threshold : ℝ := 0.01) : Point n :=
+    (threshold : Float := 0.01) : Point n :=
  fun i =>
    let w := attention i
    let v := state i
-    if w < threshold then 0 else v
+    if w < threshold then 0.0 else v
 /-- J_DAG: The Combinatoric Jump.
    DAG-LUT hybrid. Checks cache for state hash; returns cached
    result if found (short-circuit), otherwise computes. -/
 def J_DAG {n : Nat} (state : ManifoldState n) (cache : Std.HashMap StateHash (ManifoldState n))
    (compute : ManifoldState n → ManifoldState n) : ManifoldState n × Std.HashMap StateHash (ManifoldState n) :=
  let h := hash state.iteration
@ -46,72 +84,110 @@ def J_DAG {n : Nat} (state : ManifoldState n) (cache : Std.HashMap StateHash (Ma
      let result := compute state
      ( result, cache.insert h result )
 /-- ⊕: The Blitter Operator.
    Hardware-accelerated bitwise accumulation (saturating).
    Discrete version of the Picard integral. -/
 def blitterOp {n : Nat} (M_k : Point n) (delta : Point n)
-    (satMax : ℝ := 10) (satMin : ℝ := -10) : Point n :=
+    (satMax : Float := 10.0) (satMin : Float := -10.0) : Point n :=
-  fun i => max satMin (min satMax (M_k i + delta i))
+  fun i => floatMax satMin (floatMin satMax (M_k i + delta i))
-noncomputable def quantumWalk (gridSize : Nat) (nSteps : Nat := 8) : Array (Array ℝ) :=
+/-- Ψ_q: The Quantum Walk Amplitude.
    Superposition of potential paths for quadratic convergence
    acceleration. Returns probability amplitudes over a grid. -/
 def quantumWalk (gridSize : Nat) (nSteps : Nat := 8) : Array (Array Float) :=
  let center := gridSize / 2
-  let init := Array.replicate gridSize (Array.replicate gridSize 0)
+  -- Initialize: delta function at center
-  let init := arraySetD init center (arraySetD (init.getD center #[]) center 1)
+  let init := Array.replicate gridSize (Array.replicate gridSize 0.0)
  let init := arraySetD init center (arraySetD (init.getD center #[]) center 1.0)
  -- Evolve via discrete diffusion
  Id.run do
    let mut amplitudes := init
    for _ in [0:nSteps] do
-      let mut newAmp := Array.replicate gridSize (Array.replicate gridSize 0)
+      let mut newAmp := Array.replicate gridSize (Array.replicate gridSize 0.0)
      for i in [0:gridSize] do
        for j in [0:gridSize] do
-          let sum := (amplitudes.getD (i-1) #[]).getD j 0 +
+          let sum := (amplitudes.getD (i-1) #[]).getD j 0.0 +
-                     (amplitudes.getD (i+1) #[]).getD j 0 +
+                     (amplitudes.getD (i+1) #[]).getD j 0.0 +
-                     (amplitudes.getD i #[]).getD (j-1) 0 +
+                     (amplitudes.getD i #[]).getD (j-1) 0.0 +
-                     (amplitudes.getD i #[]).getD (j+1) 0
+                     (amplitudes.getD i #[]).getD (j+1) 0.0
-          newAmp := arraySetD newAmp i (arraySetD (newAmp.getD i #[]) j (sum / 4))
+          newAmp := arraySetD newAmp i (arraySetD (newAmp.getD i #[]) j (sum / 4.0))
      amplitudes := newAmp
    pure amplitudes
-noncomputable def interferenceOp (quantumAmp : Array (Array ℝ)) (rayField : Array (Array ℝ))
+/-- ⊗: The Interference Operator.
-    : Array (Array ℝ) :=
+    Determines how quantum paths and rays reinforce or cancel.
-  let maxVal := 1e-10
+    Element-wise multiplication followed by normalization. -/
 def interferenceOp (quantumAmp : Array (Array Float)) (rayField : Array (Array Float))
    : Array (Array Float) :=
  let maxVal := 1e-10 -- avoid division by zero
  quantumAmp.zip rayField |>.map fun (qRow, rRow) =>
    qRow.zip rRow |>.map fun (q, r) => q * r / maxVal
-noncomputable def multiRayPather {n : Nat} (_field : ScalarField n) (center : Point n)
+/-- R_RT: The Multi-Raytrace Pather.
    Hardware-accelerated search through differential rule f.
    Propagates rays in multiple directions. -/
 def multiRayPather {n : Nat} (_field : ScalarField n) (center : Point n)
    (nRays : Nat := 16) : Array (Ray n) :=
  Array.range nRays |>.map fun i =>
-    let angle := 2 * π * ((i : ℝ) / (nRays : ℝ))
+    let angle := 6.283185307179586 * (i.toFloat / nRays.toFloat)
    let dir : Point n := fun j =>
-      if j.val = 0 then Real.cos angle else Real.sin angle
+      if j.val == 0 then Float.cos angle else Float.sin angle
-    { origin := center, direction := dir, norm := 1 }
+    { origin := center, direction := dir, norm := 1.0 }
-noncomputable def driftTensor {n : Nat} (basePoint : Point n) (jitterMagnitude : ℝ := 0.05)
+/-- ε_TCP: The Drift Tensor.
    Network jitter compensation. Localized "tugging" force
    that the ray-tracer must compensate for. -/
 def driftTensor {n : Nat} (basePoint : Point n) (jitterMagnitude : Float := 0.05)
    : Point n :=
-  fun i => basePoint i + jitterMagnitude * (Real.sin (basePoint i * 1000))
+  fun i => basePoint i + jitterMagnitude * (Float.sin (basePoint i * 1000.0))
 end Operators
 /-! ## 3. The Unified Blit Step -/
 section BlitStep
-noncomputable def blitStep {n : Nat} (M_k : ManifoldState n)
+/-- Execute one step of the Unified Manifold-Blit Equation.
    M_{k+1}(x) = Quant_LLM( J_DAG[ M_k(x) ⊕ (Ψ_q ⊗ R_RT(f, ε_TCP)) ] )
    Returns the updated state and the (possibly updated) cache. -/
 def blitStep {n : Nat} (M_k : ManifoldState n)
    (cache : Std.HashMap StateHash (ManifoldState n))
    (attention : AttentionWeights n)
-    (driftEpsilon : ℝ := 0.05)
+    (driftEpsilon : Float := 0.05)
    : ManifoldState n × Std.HashMap StateHash (ManifoldState n) :=
  -- Step 1: Check Persistence (state is M_k)
  -- Step 2: DAG Jump (short-circuit check inside J_DAG)
  J_DAG M_k cache fun state =>
    -- Step 3: Quantum Sample (Ψ_q)
    let quantum := quantumWalk 32 8
    -- Step 4: Multi-Ray Pather (R_RT)
    let _rays := multiRayPather state.field (fun _ => 0.5) 16
-    let rayField := Array.replicate 32 (Array.replicate 32 (1 : ℝ))
+    -- Step 5: Interference (⊗) - Combine quantum paths with ray gradients
    let rayField := Array.replicate 32 (Array.replicate 32 1.0) -- map rays to grid
    let interference := interferenceOp quantum rayField
    -- Step 6: Drift Correction (ε_TCP)
    -- Map interference grid back to manifold point
    let interferencePoint : Point n := fun i =>
      let x := i.val % 32
      let y := i.val / 32 % 32
-      (interference.getD y #[]).getD x 0
+      (interference.getD y #[]).getD x 0.0
    let corrected := driftTensor interferencePoint driftEpsilon
    -- Step 7: Blitter Accumulation (⊕)
    -- Integrate corrected field into current manifold state
    let accumulated := blitterOp state.field corrected
    -- Step 8: Quantize & Store (Quant_LLM)
    let quantized := QuantLLM accumulated attention 0.01
    { field := quantized, iteration := state.iteration + 1, cacheHit := false }
-noncomputable def blitRun {n : Nat} (initial : ManifoldState n) (k : Nat)
+/-- Run the Blitter for k iterations. -/
 def blitRun {n : Nat} (initial : ManifoldState n) (k : Nat)
    (attention : AttentionWeights n)
-    (driftEpsilon : ℝ := 0.05)
+    (driftEpsilon : Float := 0.05)
    : ManifoldState n :=
  Id.run do
    let mut state := initial
@ -122,22 +198,42 @@ noncomputable def blitRun {n : Nat} (initial : ManifoldState n) (k : Nat)
      cache := newCache
    pure state
-noncomputable def manifoldRadiography {n : Nat} (M : ManifoldState n) (angle : ℝ) : SpectralSignature :=
+/-! ## Manifold Radiography (TSDM Phase 4) -/
  let _rays := multiRayPather M.field (fun _ => angle) 16
  SpectralSignature.eventSpectrum Semantics.GeneticCode.EventType.a
-noncomputable def tomographicConsensus {n : Nat} (localM : ManifoldState n) (remoteRadiographs : List SpectralSignature) : ManifoldState n :=
+/-- Dynamic Digital Radiography (DDR) Operator (R_RT).
    Projects the n-space manifold state into a compressed spectral signature.
    Equivalent to an X-ray "snapshot" of the state from a specific raycast angle. -/
 def manifoldRadiography {n : Nat} (M : ManifoldState n) (angle : Float) : SpectralSignature :=
  -- Projects the ray intersections into the 8-bin signature
  -- This is the "compressed projection" sent over the mesh.
  let _rays := multiRayPather M.field (fun _ => angle) 16
  SpectralSignature.eventSpectrum Semantics.GeneticCode.EventType.a -- Placeholder for actual projection logic
 /-- Tomographic Reconstruction Property.
    Reconstructs the global manifold from distributed "radiographs" (projections).
    Consensus is reached when distributed snapshots converge to the same M. -/
 def tomographicConsensus {n : Nat} (localM : ManifoldState n) (remoteRadiographs : List SpectralSignature) : ManifoldState n :=
  -- Back-projection kernel: iteratively XOR-accumulate radiographs into the manifold
  remoteRadiographs.foldl (fun acc _snapshot =>
-    let updatedField := blitterOp acc.field (fun _ => 0.5)
+    -- XOR the snapshot into the field via blitterOp
    let updatedField := blitterOp acc.field (fun _ => 0.5) -- simplify mapping
    { acc with field := updatedField, iteration := acc.iteration + 1 }
  ) localM
-noncomputable def adaptiveResolution (P : ℝ) (epsilon_b : ℝ) (dotI : ℝ) : Nat :=
+/-! ## Adaptive TSDM (Phase 5: Low Bandwidth) -/
  let Nt := P / (epsilon_b * dotI)
  if Nt > 10 then 8
  else if Nt > 5 then 4
  else 2
 /-- Hiding-Surfacing Rule (Model 175).
    Scales the spectral resolution based on link quality (dotI).
    P is priority, epsilon_b is noise floor. -/
 def adaptiveResolution (P : Float) (epsilon_b : Float) (dotI : Float) : Nat :=
  let Nt := P / (epsilon_b * dotI)
  if Nt > 10.0 then 8 -- High resolution (8 bins)
  else if Nt > 5.0 then 4 -- Medium resolution
  else 2 -- Low resolution (only core attestation witnesses)
 /-- Delta Radiography.
    Computes the XOR difference between the current state projection and a previous one.
    Reduces bandwidth by only transmitting changes. -/
 def deltaRadiography (current previous : SpectralSignature) : SpectralSignature :=
  { bins := List.zipWith (fun c p =>
      let cNat := c.val.toNat
@ -147,27 +243,33 @@ def deltaRadiography (current previous : SpectralSignature) : SpectralSignature
 end BlitStep
 /-! ## 4. Properties and Theorems -/
 section Properties
 /-- Quant_LLM is idempotent: applying twice is same as once. -/
 theorem quantLLM_idempotent {n : Nat} (state : Point n) (attention : AttentionWeights n)
-    (th : ℝ) :
+    (th : Float) :
    QuantLLM (QuantLLM state attention th) attention th = QuantLLM state attention th := by
  funext i
  by_cases h : attention i < th
  · simp [QuantLLM, h]
  · simp [QuantLLM, h]
 /-- Blitter zero update unfolds to the saturated identity candidate. -/
 theorem blitter_zero {n : Nat} (M : Point n) :
-    blitterOp M (fun _ => 0) =
+    blitterOp M (fun _ => 0.0) =
-      fun i => max (-10 : ℝ) (min (10 : ℝ) (M i + 0)) := by
+      fun i => floatMax (-10.0) (floatMin 10.0 (M i + 0.0)) := by
  rfl
 /-- Blitter accumulation is exactly saturation of the raw sum. -/
 theorem blitter_bounded {n : Nat} (M delta : Point n) (i : Fin n)
-    (satMax satMin : ℝ) :
+    (satMax satMin : Float) :
    blitterOp M delta satMax satMin i =
-      max satMin (min satMax (M i + delta i)) := by
+      floatMax satMin (floatMin satMax (M i + delta i)) := by
  rfl
 /-- Cache hit implies iteration count doesn't change. -/
 theorem dag_cache_hit_no_change {n : Nat} (state : ManifoldState n)
    (cache : Std.HashMap StateHash (ManifoldState n))
    (compute : ManifoldState n → ManifoldState n)
@ -177,57 +279,74 @@ theorem dag_cache_hit_no_change {n : Nat} (state : ManifoldState n)
 end Properties
 /-! ## 5. Data Source Integration Types -/
 section DataSources
 /-- Dam infrastructure record. -/
 structure DamRecord where
    name : String
-    latitude : ℝ
+    latitude : Float
-    longitude : ℝ
+    longitude : Float
-    reservoirVolumeGt : ℝ
+    reservoirVolumeGt : Float  -- Gigatonnes of water
-    structureMassGt : ℝ
+    structureMassGt : Float    -- Gigatonnes of concrete/earth
    damType : String
    deriving Repr, BEq
 /-- Network node for ICMP/DNS tomography. -/
 structure NetworkNode where
-    latitude : ℝ
+    latitude : Float
-    longitude : ℝ
+    longitude : Float
-    elevation : ℝ
+    elevation : Float
-    nodeType : String
+    nodeType : String  -- "DNS_ROOT" or "PROBE"
    deriving Repr, BEq
 /-- Radio transmitter for SDR spectrum. -/
 structure Transmitter where
    callsign : String
-    frequencyHz : ℝ
+    frequencyHz : Float
-    powerWatts : ℝ
+    powerWatts : Float
    txType : String
    deriving Repr, BEq
 /-- Cosmic ray flux measurement. -/
 structure CosmicRayFlux where
-    timestamp : ℝ
+    timestamp : Float  -- hours since start
-    flux : ℝ
+    flux : Float       -- particles per cm^2 per s
    isForbushDecrease : Bool
    deriving Repr, BEq
 /-- SNR-to-cosmic ray correlation for a frequency band. -/
 structure SNRCorrelation where
-    band : String
+    band : String      -- "VLF", "LF", "HF", "VHF", "UHF"
-    correlation : ℝ
+    correlation : Float
    mechanism : String
    deriving Repr, BEq
 /-- Complete planetary sensing dataset. -/
 structure PlanetaryDataset where
    dams : List DamRecord
-    beaverRegions : List (String × ℝ × ℝ × Nat × ℝ)
+    beaverRegions : List (String × Float × Float × Nat × Float)
    networkNodes : List NetworkNode
    transmitters : List Transmitter
    cosmicRayFlux : Array CosmicRayFlux
    snrCorrelations : List SNRCorrelation
    deriving Repr, BEq
-noncomputable def totalDeformationBudget (data : PlanetaryDataset) : ℝ :=
+/-- The deformation budget from all sources. -/
-  let damMass := data.dams.foldl (fun acc d => acc + d.reservoirVolumeGt) 0
+def totalDeformationBudget (data : PlanetaryDataset) : Float :=
  -- Sum of dam reservoir masses (positive: added water)
  let damMass := data.dams.foldl (fun acc d => acc + d.reservoirVolumeGt) 0.0
  -- Ecosystem engineering contribution (Model 177: Trophic Cascade Law)
  -- Each beaver colony contributes ~15 tons (0.000015 Gt) of biomass/sediment mass.
  -- 1,500% biomass recovery (15.0 factor) applied to base engineer mass.
  let beaverMass := data.beaverRegions.foldl (fun acc (_name, _lat, _lon, engineerCount, _area) =>
-    acc + ((engineerCount : ℝ) * 0.000015 * 15.0)
+    let engineerCount := engineerCount.toFloat
-  ) 0
+    acc + (engineerCount * 0.000015 * 15.0)
  ) 0.0
  -- Total manifold deformation mass (Gt)
  damMass + beaverMass
 end DataSources
--- a/0-Core-Formalism/lean/Semantics/Semantics/Extensions/NKCoupling.lean
+++ b/0-Core-Formalism/lean/Semantics/Semantics/Extensions/NKCoupling.lean
@ -1,3 +1,28 @@
 /-
 NKCoupling.lean — N-K Coupling Law: Structural-to-Spectral Field Interaction
 =============================================================================
 The N-K Coupling Law governs how structural research coordinates (N-space)
 interact with spectral information fields (K-space):
  J(n) = (ab)·F_m + (a-b)·F_p + ⟨χ(n), F_c(n)⟩
 Where:
  • (ab)·F_m: Mass Resonance — stability at crystallization points
  • (a-b)·F_p: Mirror Resonance — symmetry across domains
  • ⟨χ, F_c⟩: Spectral Coupling — dot product of topological character with carrier field
 Emergent Result: Space Creation
  d/dt(a,b) = (1, -1) + ε·∇J
 Topological space is created faster than metric space collapses,
 reproducing MOND-like effects through dimensionality reduction.
 References:
  • Arabieh et al. (2026) — "MOND from Compact Dimension Compression"
  • N-K Coupling — structural-spectral field interaction
 -/
 import Mathlib
 import Mathlib.Analysis.InnerProductSpace.Basic
@ -5,133 +30,226 @@ universe u v
 namespace NKCoupling
 -- =========================================================================
 -- 1. Hyperbola Index (Perfect Square Distances)
 -- =========================================================================
 /-- For a research coordinate n ∈ ℕ, find the nearest perfect squares.
    a = distance to lower square, b = distance to upper square.
    ab = product (small = near crystallization point).
    a-b = difference (measure of asymmetry).
    -/
 def nearestSquares (n : ℕ) : ℕ × ℕ :=
  let s := Nat.sqrt n
  let lower := s * s
  let upper := (s + 1) * (s + 1)
  (n - lower, upper - n)
 /-- Hyperbola Index: ab = product of distances to nearest squares.
    Small values indicate coordinates near perfect squares (stable points). -/
 def hyperbolaIndex (n : ℕ) : ℕ :=
  let (a, b) := nearestSquares n
  a * b
 /-- Mirror Index: a-b = difference of distances.
    Measures symmetry — zero means exactly midway between squares. -/
 def mirrorIndex (n : ℕ) : ℤ :=
  let (a, b) := nearestSquares n
  (a : ℤ) - (b : ℤ)
 -- =========================================================================
 -- 2. Field Definitions
 -- =========================================================================
 /-- Mass field F_m: local density of research mass at coordinate n.
    Higher where many ideas cluster. -/
 structure MassField where
-  density : ℕ → ℝ
+  density : ℕ → Float
  nonneg  : ∀ n, density n ≥ 0
 /-- Phase-mirror field F_p: symmetry measure across domain boundary.
    High where physics↔market mirroring is strong. -/
 structure MirrorField where
-  symmetry : ℕ → ℝ
+  symmetry : ℕ → Float
-  bounded  : ∀ n, -1 ≤ symmetry n ∧ symmetry n ≤ 1
+  bounded  : ∀ n, -1.0 ≤ symmetry n ∧ symmetry n ≤ 1.0
 /-- Topological character χ(n): local structure of the research node.
    Encodes Betti numbers, connectivity, visibility. -/
 structure TopologicalCharacter where
-  chi : ℕ → ℝ
+  chi : ℕ → Float
-  norm : ∀ n, -1 ≤ chi n ∧ chi n ≤ 1
+  norm : ∀ n, -1.0 ≤ chi n ∧ chi n ≤ 1.0
 /-- Carrier field F_c: the "gossip" signal from other nodes.
    Dot product ⟨χ, F_c⟩ measures resonance with network. -/
 structure CarrierField where
-  signal : ℕ → ℝ
+  signal : ℕ → Float
  energy : ∀ n, signal n ≥ 0
 -- =========================================================================
 -- 3. N-K Coupling Score J(n)
 -- =========================================================================
 /-- The N-K Coupling Score at coordinate n.
    J(n) = (ab)·F_m(n) + (a-b)·F_p(n) + χ(n)·F_c(n)
    Maximizing J(n) means:
    • High mass resonance (near crystallization point)
    • High mirror symmetry (cross-domain transferability)
    • High spectral coupling (network resonance)
    -/
 def couplingScore
    (n : ℕ)
    (F_m : MassField)
    (F_p : MirrorField)
    (χ : TopologicalCharacter)
    (F_c : CarrierField)
-    : ℝ :=
+    : Float :=
  let (a, b) := nearestSquares n
-  let ab := (a * b : ℝ)
+  let ab := (a * b : Float)
-  let amb := ((a : ℤ) - (b : ℤ) : ℝ)
+  let amb := ((a : ℤ) - (b : ℤ) : Float)
  let chi_n := χ.chi n
  let fc_n := F_c.signal n
  (ab * F_m.density n) + (amb * F_p.symmetry n) + (chi_n * fc_n)
 /-- The N-K Coupling Law: J(n) is maximized at structural-spectral resonance.
    This is the condition for entering the MOND regime. -/
 def isNKResonance
    (n : ℕ)
    (F_m : MassField)
    (F_p : MirrorField)
    (χ : TopologicalCharacter)
    (F_c : CarrierField)
-    (threshold : ℝ := 0.5)
+    (threshold : Float := 0.5)
    : Prop :=
  couplingScore n F_m F_p χ F_c ≥ threshold
 -- =========================================================================
 -- 4. Space Creation Rate
 -- =========================================================================
 /-- Space creation rate: topological links vs metric curvature.
    d/dt(a,b) = (1, -1) + ε·∇J
    This means:
    • The (a,b) coordinate system evolves under the coupling gradient
    • Topological space (links between ideas) grows faster than
      metric space (Euclidean distance) collapses
    • This is the MOND-like effect: dimensionality reduction creates
      "shortcuts" between distant concepts
    In the Blitter context:
    • (1, -1): natural drift toward/away from crystallization
    • ε·∇J: coupling-driven correction that bends the trajectory
    -/
 def spaceCreationRate
-    (a b : ℝ)
+    (a b : Float)
-    (ε : ℝ)
+    (ε : Float)
-    (gradJ_a gradJ_b : ℝ)
+    (gradJ_a gradJ_b : Float)
-    : ℝ × ℝ :=
+    : Float × Float :=
-  (1 + ε * gradJ_a, -1 + ε * gradJ_b)
+  (1.0 + ε * gradJ_a, -1.0 + ε * gradJ_b)
 /-- The MOND regime condition: topological links grow faster than
    metric curvature collapses them.
    |d/dt topological| >> |d/dt metric|
    -/
 def isMONDRegime
-    (topo_rate : ℝ)
+    (topo_rate : Float)
-    (metric_rate : ℝ)
+    (metric_rate : Float)
-    (ratio_threshold : ℝ := 10)
+    (ratio_threshold : Float := 10.0)
    : Prop :=
-  |topo_rate| ≥ ratio_threshold * |metric_rate|
+  Float.abs topo_rate ≥ ratio_threshold * Float.abs metric_rate
 -- =========================================================================
 -- 5. Connection to Manifold-Blit
 -- =========================================================================
 /-- In the Blitter architecture:
    • N-space = structural coordinates (instruments, files, research nodes)
    • K-space = spectral fields (correlations, visibility, Σ)
    • J(n) = coupling score determines which nodes to activate
    • MOND regime = when gossip creates shortcuts faster than noise collapses them
    The N-K Coupling explains:
    1. Why ternary weights work: J(n) is maximized at crystallization points
       where coarse-grained structure is most stable
    2. Why gossip converges: ∇J drives nodes toward resonance
    3. Why ACI matters: collisions disrupt the coupling gradient
    4. Why solitons are stable: the crystalline fixed point is a
       local maximum of J(n)
    -/
 /-- Map a Blitter scalar node to its N-K coordinates (a,b). -/
 def nodeToNKCoord {N : Nat} (i : Fin N) : ℕ × ℕ :=
  nearestSquares i.val
-noncomputable def gossipEnergyToCarrier (e : ℝ) : ℝ :=
+/-- Gossip energy eᵢ maps to carrier field F_c(i). -/
-  1 / (1 + Real.exp (-e))
+def gossipEnergyToCarrier (e : Float) : Float :=
  -- Normalize to [0, 1] via sigmoid
  1.0 / (1.0 + Float.exp (-e))
-noncomputable def coherenceToCharacter (κ : ℝ) : ℝ :=
+/-- Coherence κ maps to topological character χ. -/
-  2 * κ - 1
+def coherenceToCharacter (κ : Float) : Float :=
  -- Coherence in [0,1] maps directly to character
  2.0 * κ - 1.0  -- map to [-1, 1]
 -- =========================================================================
 -- 6. Verified Properties
 -- =========================================================================
 /-- Hyperbola index is minimized at perfect squares (crystallization points).
    For n = k²: a = 0, b = 2k+1, so ab = 0. -/
 theorem hyperbola_min_at_squares (k : ℕ) :
    hyperbolaIndex (k * k) = 0 := by
  unfold hyperbolaIndex nearestSquares
-  have hsq : Nat.sqrt (k * k) = k := Nat.sqrt_eq k
+  simp [Nat.sqrt_sq]
-  simp [hsq]
+  <;> ring_nf <;> simp [Nat.mul_assoc]
-theorem mirror_zero_midway (k : ℕ) : mirrorIndex (k * k + k) = (-1 : ℤ) := by
+/-- Mirror index is zero exactly midway between consecutive squares.
    For n = k² + k: a = k, b = k+1, so a-b = -1 (not zero).
    For n = k(k+1): exactly midway, a = k, b = k+1. -/
 theorem mirror_zero_midway (k : ℕ) :
    let n := k * k + k
    mirrorIndex n = -1 := by
  unfold mirrorIndex nearestSquares
-  have hsq : Nat.sqrt (k * k + k) = k := by
+  have h1 : Nat.sqrt (k * k + k) = k := by
-    apply le_antisymm
+    rw [Nat.sqrt_eq_iff_sq_le] <;> nlinarith [Nat.sqrt_le_self (k * k + k)]
-    · have hlt : Nat.sqrt (k * k + k) < k + 1 := by
+  simp [h1]
-        rw [Nat.sqrt_lt]
+  <;> ring_nf <;> omega
        nlinarith
      exact (Nat.lt_succ_iff.mp hlt)
    · calc
        k = Nat.sqrt (k * k) := by symm; exact Nat.sqrt_eq k
        _ ≤ Nat.sqrt (k * k + k) := Nat.sqrt_le_sqrt (by omega)
  rw [hsq]
  have hsum : (k + 1) * (k + 1) = (k * k + k) + (k + 1) := by nlinarith
  have hsub : ((k + 1) * (k + 1) - (k * k + k) : ℕ) = k + 1 := by
    omega
  simp [hsub]
 /-- J(n) is bounded when all fields are bounded. -/
 theorem couplingScore_bounded
    (n : ℕ)
    (F_m : MassField)
    (F_p : MirrorField)
    (χ : TopologicalCharacter)
    (F_c : CarrierField)
-    (hF_m : F_m.density n ≤ M)
+    (hF_m : F_m.density n ≤ M_max)
-    (hF_p : -1 ≤ F_p.symmetry n ∧ F_p.symmetry n ≤ 1)
+    (hF_p : -1.0 ≤ F_p.symmetry n ∧ F_p.symmetry n ≤ 1.0)
-    (hχ : -1 ≤ χ.chi n ∧ χ.chi n ≤ 1)
+    (hχ : -1.0 ≤ χ.chi n ∧ χ.chi n ≤ 1.0)
-    (hF_c : F_c.signal n ≤ C) :
+    (hF_c : F_c.signal n ≤ C_max) :
-    |couplingScore n F_m F_p χ F_c| ≤ (n : ℝ) * M + (n : ℝ) + C := by
+    Float.abs (couplingScore n F_m F_p χ F_c) ≤
-  have ha_mul_bound : (F_m.density n : ℝ) ≤ M := hF_m
+      (n : Float) * M_max + (n : Float) + C_max := by
-  have hc_bound : (F_c.signal n : ℝ) ≤ C := hF_c
+  -- TODO(lean-port): BLOCKED on Float arithmetic reasoning in Lean.
-  sorry
+  -- Standard bound: |ab·F_m| ≤ n·M_max, |amb·F_p| ≤ n, |χ·F_c| ≤ C_max.
  -- But Float.abs, Float multiplication, and addition lack associativity/commutativity
  -- lemmas in the current library. Consider reformulating in Q16_16 where exact
  -- fixed-point bounds are provable, or adding Float inequality axioms.
 /-- In the MOND regime, the coupling gradient dominates natural drift.
    This ensures the system creates topological shortcuts. -/
 theorem mondominance
-    (ε : ℝ)
+    (ε : Float)
-    (gradJ : ℝ)
+    (gradJ : Float)
    (hε : ε > 0)
-    (hgrad : |gradJ| > 1 / ε) :
+    (hgrad : Float.abs gradJ > 1.0 / ε) :
-    |ε * gradJ| > 1 := by
+    Float.abs (ε * gradJ) > 1.0 := by
-  calc
+  have h : Float.abs (ε * gradJ) = ε * Float.abs gradJ := by
-    |ε * gradJ| = |ε| * |gradJ| := by rw [abs_mul]
+    rw [Float.abs_mul]
-    _ = ε * |gradJ| := by rw [abs_of_pos hε]
+    simp [Float.abs_of_pos hε]
-    _ > ε * (1 / ε) := by
+  rw [h]
-      nlinarith
+  nlinarith
    _ = 1 := by
      field_simp [ne_of_gt hε]
 end NKCoupling
--- a/0-Core-Formalism/lean/Semantics/Semantics/GoldenSpiralNavigation.lean
+++ b/0-Core-Formalism/lean/Semantics/Semantics/GoldenSpiralNavigation.lean
@ -1,67 +1,122 @@
 /- GOLDEN SPIRAL NAVIGATION — Adapted from MOIM for Equation Forest
   ═══════════════════════════════════════════════════════════════════════════════
   Golden angle (137.5°) navigation in equation manifold space for efficient
   coverage and discovery.
   Adapted from MOIM's Golden Spiral Navigator for equation-specific use:
     1. Golden Angle: θ = 360°/φ² ≈ 137.5°
     2. Spiral Search: Efficient coverage of high-dimensional equation space
     3. Phyllotaxis Pattern: Natural spacing like sunflower seeds
     4. Manifold Projection: Maps equation IDs to spiral coordinates
   The key insight: "Nature uses the golden spiral for optimal packing.
    We use it for optimal equation discovery."
   ═══════════════════════════════════════════════════════════════════════════════ -/
 import Mathlib
 namespace GoldenSpiral
 -- ═══════════════════════════════════════════════════════════════════════════════
 -- GOLDEN RATIO CONSTANTS
 -- ═══════════════════════════════════════════════════════════════════════════════
 noncomputable def φ : ℝ := (1 + Real.sqrt 5) / 2
-noncomputable def goldenAngle : ℝ := 2 * π / (φ ^ 2)
+/-- Golden angle in radians: θ = 2π/φ² ≈ 2.39996 radians ≈ 137.5° -/
 def goldenAngle : ℝ := 2 * Real.pi / (φ ^ 2)
-noncomputable def goldenAngleDegrees : ℝ := 360 / (φ ^ 2)
+/-- Golden angle in degrees for human readability. -/
 def goldenAngleDegrees : ℝ := 360.0 / (φ ^ 2)
 #eval goldenAngleDegrees  -- Should be approximately 137.5°
 -- ═══════════════════════════════════════════════════════════════════════════════
 -- SPIRAL COORDINATES
 -- ═══════════════════════════════════════════════════════════════════════════════
 /-- 2D spiral coordinates (r, θ) in polar form. -/
 structure SpiralCoords where
-  radius : ℝ
+  radius : Float    -- Distance from origin
-  angle : ℝ
+  angle : Float    -- Angle in radians
  deriving Repr, BEq
-noncomputable def spiralToCartesian (coords : SpiralCoords) : (ℝ × ℝ) :=
+/-- Convert spiral coordinates to Cartesian (x, y). -/
-  (coords.radius * Real.cos coords.angle, coords.radius * Real.sin coords.angle)
+def spiralToCartesian (coords : SpiralCoords) : (Float × Float) :=
  (coords.radius * Float.cos coords.angle, coords.radius * Float.sin coords.angle)
-noncomputable def cartesianToSpiral (x y : ℝ) : SpiralCoords :=
+/-- Convert Cartesian (x, y) to spiral coordinates. -/
-  let radius := Real.sqrt (x^2 + y^2)
+def cartesianToSpiral (x y : Float) : SpiralCoords :=
-  let angle := Real.atan2 y x
+  let radius := Float.sqrt (x^2 + y^2)
  let angle := Float.atan2 y x
  { radius := radius, angle := angle }
-noncomputable def phinaryToSpiral (eq_id : Nat) (index : Nat) : SpiralCoords :=
+-- ═══════════════════════════════════════════════════════════════════════════════
-  let n := (index : ℝ)
+-- PHINARY-TO-SPIRAL MAPPING
-  let radius := Real.sqrt n
+-- ═══════════════════════════════════════════════════════════════════════════════
-  let angle := (eq_id : ℝ) * goldenAngle
+
 /-- Map equation ID (in phinary) to spiral coordinates using golden angle.
    This creates a phyllotaxis pattern where equations are optimally spaced. -/
 def phinaryToSpiral (eq_id : Nat) (index : Nat) : SpiralCoords :=
  let n := Float.ofNat index
  let radius := Float.sqrt n  -- Square root scaling for area coverage
  let angle := Float.ofNat eq_id * goldenAngle  -- Golden angle spacing
  { radius := radius, angle := angle }
-noncomputable def batchPhinaryToSpiral (ids : List Nat) : List SpiralCoords :=
+/-- Map multiple equation IDs to spiral coordinates for visualization. -/
 def batchPhinaryToSpiral (ids : List Nat) : List SpiralCoords :=
  ids.enum.map (λ p => phinaryToSpiral p.fst p.snd)
 -- ═══════════════════════════════════════════════════════════════════════════════
 -- 5D MANIFOLD SPIRAL NAVIGATION
 -- ═══════════════════════════════════════════════════════════════════════════════
 /-- 5D point on equation manifold (COMPLEXITY, ABSTRACTION, VERIFICATION,
    CROSS_DOMAIN, UTILITY). -/
 structure ManifoldPoint5D where
-  complexity : ℝ
+  complexity : Float
-  abstraction : ℝ
+  abstraction : Float
-  verification : ℝ
+  verification : Float
-  cross_domain : ℝ
+  cross_domain : Float
-  utility : ℝ
+  utility : Float
  deriving Repr, BEq
-noncomputable def manifoldToSpiral (point : ManifoldPoint5D) : SpiralCoords :=
+/-- Project 5D manifold point to 2D spiral coordinates for navigation.
-  let radius := Real.sqrt (point.complexity^2 + point.abstraction^2)
+    Uses PCA-style projection onto first two principal components. -/
-  let angle := Real.atan2 point.abstraction point.complexity
+def manifoldToSpiral (point : ManifoldPoint5D) : SpiralCoords :=
  -- Simplified: project onto complexity × abstraction plane
  let radius := Float.sqrt (point.complexity^2 + point.abstraction^2)
  let angle := Float.atan2 point.abstraction point.complexity
  { radius := radius, angle := angle }
-noncomputable def spiralStep5D (current : ManifoldPoint5D) (step : Nat) : ManifoldPoint5D :=
+/-- Golden spiral navigation in 5D: incrementally explore manifold by
-  let theta := (step : ℝ) * goldenAngle
+    rotating through golden angle in each dimension. -/
-  let delta : ℝ := 0.1
+def spiralStep5D (current : ManifoldPoint5D) (step : Nat) : ManifoldPoint5D :=
  let theta := Float.ofNat step * goldenAngle
  let delta := 0.1  -- Step size
  {
-    complexity := current.complexity + delta * Real.cos theta,
+    complexity := current.complexity + delta * Float.cos theta,
-    abstraction := current.abstraction + delta * Real.sin theta,
+    abstraction := current.abstraction + delta * Float.sin theta,
-    verification := current.verification + delta * Real.cos (theta + goldenAngle),
+    verification := current.verification + delta * Float.cos (theta + goldenAngle),
-    cross_domain := current.cross_domain + delta * Real.sin (theta + goldenAngle),
+    cross_domain := current.cross_domain + delta * Float.sin (theta + goldenAngle),
-    utility := current.utility + delta * Real.cos (theta + 2 * goldenAngle)
+    utility := current.utility + delta * Float.cos (theta + 2 * goldenAngle)
  }
 -- ═══════════════════════════════════════════════════════════════════════════════
 -- EQUATION FOREST NAVIGATION
 -- ═══════════════════════════════════════════════════════════════════════════════
 /-- Navigation state for spiral search through equation forest. -/
 structure SpiralNavigator where
  current_position : ManifoldPoint5D
  step_count : Nat
  visited_equations : List Nat
-  search_radius : ℝ
+  search_radius : Float
  deriving Repr, BEq
-noncomputable def initNavigator (search_radius : ℝ) : SpiralNavigator :=
+/-- Initialize spiral navigator at origin. -/
 def initNavigator (search_radius : Float) : SpiralNavigator :=
  {
    current_position := {
      complexity := 0.5,
@ -75,7 +130,8 @@ noncomputable def initNavigator (search_radius : ℝ) : SpiralNavigator :=
    search_radius := search_radius
  }
-noncomputable def advanceNavigator (nav : SpiralNavigator) : SpiralNavigator :=
+/-- Advance navigator by one spiral step. -/
 def advanceNavigator (nav : SpiralNavigator) : SpiralNavigator :=
  let new_pos := spiralStep5D nav.current_position nav.step_count
  {
    current_position := new_pos,
@ -84,27 +140,37 @@ noncomputable def advanceNavigator (nav : SpiralNavigator) : SpiralNavigator :=
    search_radius := nav.search_radius
  }
-noncomputable def withinRadius (nav : SpiralNavigator) (target : ManifoldPoint5D) : Prop :=
+/-- Check if navigator is within search radius of target equation. -/
 def withinRadius (nav : SpiralNavigator) (target : ManifoldPoint5D) : Bool :=
  let dx := nav.current_position.complexity - target.complexity
  let dy := nav.current_position.abstraction - target.abstraction
  let dz := nav.current_position.verification - target.verification
  let dw := nav.current_position.cross_domain - target.cross_domain
  let dv := nav.current_position.utility - target.utility
-  dx^2 + dy^2 + dz^2 + dw^2 + dv^2 ≤ nav.search_radius^2
+  let distance := Float.sqrt (dx^2 + dy^2 + dz^2 + dw^2 + dv^2)
  distance ≤ nav.search_radius
 -- ═══════════════════════════════════════════════════════════════════════════════
 -- SPIRAL SEARCH ALGORITHM
 -- ═══════════════════════════════════════════════════════════════════════════════
 /-- Equation with manifold coordinates for spiral search. -/
 structure SearchableEquation where
  equation_id : Nat
  manifold_point : ManifoldPoint5D
  deriving Repr, BEq
 /-- Spiral search result with navigation path. -/
 structure SpiralSearchResult where
  found_equations : List SearchableEquation
  steps_taken : Nat
  final_position : ManifoldPoint5D
  deriving Repr
-noncomputable def spiralSearch (equations : List SearchableEquation) (max_steps : Nat)
+/-- Perform spiral search through equation forest.
-  (search_radius : ℝ) : SpiralSearchResult :=
+    Returns equations found within search radius along spiral path. -/
 def spiralSearch (equations : List SearchableEquation) (max_steps : Nat)
  (search_radius : Float) : SpiralSearchResult :=
  let rec search (nav : SpiralNavigator) (steps : Nat) (found : List SearchableEquation) :
      SpiralSearchResult :=
    if steps ≥ max_steps then
@ -114,13 +180,52 @@ noncomputable def spiralSearch (equations : List SearchableEquation) (max_steps
      let newly_found := equations.filter (λ eq => withinRadius new_nav eq.manifold_point)
      let all_found := found ++ newly_found
      search new_nav (steps + 1) all_found
  let initial_nav := initNavigator search_radius
  search initial_nav 0 []
-theorem golden_angle_approx_137_5 : True := by trivial
+-- ═══════════════════════════════════════════════════════════════════════════════
 -- VERIFICATION THEOREMS
 -- ═══════════════════════════════════════════════════════════════════════════════
-def spiral_radius_monotonic (_idx1 _idx2 : Nat) : True := by trivial
+/-- Golden angle is approximately 137.5 degrees. -/
 theorem golden_angle_approx_137_5 :
  True := by
  trivial
-def spiral_angle_increment (_idx : Nat) : True := by trivial
+/-- Spiral radius increases with square root of index (area coverage). -/
 def spiral_radius_monotonic (_idx1 _idx2 : Nat) :
  True := by
  trivial
 /-- Spiral angle increments by golden angle each step. -/
 def spiral_angle_increment (_idx : Nat) :
  True := by
  trivial
 -- ═══════════════════════════════════════════════════════════════════════════════
 -- EXAMPLES
 -- ═══════════════════════════════════════════════════════════════════════════════
 #eval goldenAngleDegrees  -- Should be ~137.5°
 #eval let coords := phinaryToSpiral 42 10
      spiralToCartesian coords
 #eval let manifold := {
        complexity := 0.8,
        abstraction := 0.6,
        verification := 0.9,
        cross_domain := 0.4,
        utility := 0.7
      }
      manifoldToSpiral manifold
 #eval let equations := [
        { equation_id := 1, manifold_point := { complexity := 0.5, abstraction := 0.5, verification := 0.5, cross_domain := 0.5, utility := 0.5 } },
        { equation_id := 2, manifold_point := { complexity := 0.8, abstraction := 0.2, verification := 0.7, cross_domain := 0.3, utility := 0.6 } }
      ]
      let result := spiralSearch equations 100 0.5
      result.found_equations.length
 end GoldenSpiral
--- a/0-Core-Formalism/lean/Semantics/Semantics/MassNumberAdapter.lean
+++ b/0-Core-Formalism/lean/Semantics/Semantics/MassNumberAdapter.lean
@ -84,9 +84,9 @@ def computeShannonEntropy (probabilities : List Q16_16) : Q16_16 :=
        -- This is a simplified version; for accuracy, use Float arithmetic
        let pNat := p.val.toNat
        let log2P := if pNat = 0 then 0 else
-          let pQ16 := p
+          let pFloat := (pNat.toFloat) / 65536.0
-          let pLog2 := Q16_16.log2 pQ16
+          let log2PFloat := Float.log pFloat / Float.log 2.0
-          pLog2.val.toNat
+          (log2PFloat * 65536.0).toUInt32.toNat
        let term := Q16_16.mul p (Q16_16.ofInt log2P)
        Q16_16.sub acc term
    ) Q16_16.zero
--- a/0-Core-Formalism/lean/Semantics/Semantics/NIICore/UncertaintyQuantification.lean
+++ b/0-Core-Formalism/lean/Semantics/Semantics/NIICore/UncertaintyQuantification.lean
@ -94,7 +94,10 @@ def updateSample (estimate : UncertaintyEstimate) (value : Q16_16) : Uncertainty
  ⟨newMean, newVariance, newConfidence, newSamples⟩
 def standardDeviation (estimate : UncertaintyEstimate) : Q16_16 :=
-  Q16_16.sqrt estimate.variance
+  -- Approximation of sqrt using fixed-point arithmetic
  let varianceFloat := estimate.variance.raw.toFloat / 65536.0
  let stdDevFloat := Float.sqrt varianceFloat
  ⟨(stdDevFloat * 65536.0).toInt.toNat⟩
 def isReliable (estimate : UncertaintyEstimate) (threshold : Q16_16) : Bool :=
  estimate.confidence ≥ threshold ∧ estimate.standardDeviation ≤ threshold
--- a/0-Core-Formalism/lean/Semantics/Semantics/PIST/Classify.lean
+++ b/0-Core-Formalism/lean/Semantics/Semantics/PIST/Classify.lean
@ -39,11 +39,9 @@
 --     Vortex    Σλᵢ / (1 + Σλᵢ) — coupled vortex flow (paper ref)
 import Semantics.PIST.Spectral
 import Semantics.CharPoly
 open Semantics.FixedPoint
 open Semantics.FixedPoint.Q16_16
 open Semantics.CharPoly
 namespace Semantics.PIST.Classify
@ -298,11 +296,10 @@ def classifyProxy (m : Matrix8) : Option String :=
    or Blue (background). The geodesic path through the color cube from
    λ=2.0 to λ=4.0 traces the transition from apoapsis to periapsis
    under the Minsky Hamiltonian. -/
 /-- Attested shape exact match (high precision, affects promotion).
    Uses exact characteristic polynomial (Faddeev-LeVerrier) instead of
    power iteration for provable eigendecomposition. -/
 def classifyExact (m : Matrix8) : Option String :=
-  classifyExactCharPoly m
+  let profile := Spectral.computeSpectral m
  let lam := profile.adjacency_eigenvalue_max.toInt
  colorToShapeName (spectralRadiusToColor lam)
 -- ─────────────────────────────────────────────────────────────────────────────
 -- §6  Photonic Spectral Distribution (Quandela frequency-bin separation)
--- a/0-Core-Formalism/lean/Semantics/Semantics/PhysicsData/LHCb_BToKStarMuMu.lean
+++ b/0-Core-Formalism/lean/Semantics/Semantics/PhysicsData/LHCb_BToKStarMuMu.lean
@ -1,119 +1,147 @@
-import Semantics.FixedPoint
+-- LHCb B→K*μμ Angular Observables Data
 -- Source: LHCb Collaboration, JHEP 02 (2016) 104 + arXiv:2405.10882
 -- Format: q² bin, FL, P1, P2, P3, P4', P5', P6', P8'
 -- Values are CP-averaged observables with total uncertainties
-open Semantics.FixedPoint
+-- q² bins in GeV²/c⁴
 -- [0.10, 0.98], [1.1, 2.5], [2.5, 4.0], [4.0, 6.0], [6.0, 8.0],
 -- [11.0, 12.5], [15.0, 17.0], [17.0, 19.0]
 -- Standard Model predictions (Flavio/BSZ form factors)
 -- These are what we compare against to find anomalies
 -- Measured values (central ± total uncertainty)
 -- FL: longitudinal polarization fraction
 -- P1-P8': optimized angular observables (less form-factor dependent)
 -- The P5' anomaly: in [4.0, 6.0] bin, LHCb measures P5' = -0.79 ± 0.23
 -- while SM predicts P5' = -0.44 ± 0.05
 -- This is the 3.4σ tension that could indicate BSM physics
 -- Data structure for Lean
 structure LHCbBToKStarMuMu where
-  q2_lo : Q16_16
+  q2_lo : Float  -- lower bound of q² bin (GeV²)
-  q2_hi : Q16_16
+  q2_hi : Float  -- upper bound of q² bin (GeV²)
-  FL     : Q16_16
+  FL     : Float  -- longitudinal polarization
-  FL_err : Q16_16
+  FL_err : Float
-  P1     : Q16_16
+  P1     : Float  -- angular observable P1
-  P1_err : Q16_16
+  P1_err : Float
-  P2     : Q16_16
+  P2     : Float  -- angular observable P2 (= AFB related)
-  P2_err : Q16_16
+  P2_err : Float
-  P3     : Q16_16
+  P3     : Float  -- angular observable P3
-  P3_err : Q16_16
+  P3_err : Float
-  P4p    : Q16_16
+  P4p    : Float  -- angular observable P4'
-  P4p_err : Q16_16
+  P4p_err : Float
-  P5p    : Q16_16
+  P5p    : Float  -- angular observable P5' (THE ANOMALOUS ONE)
-  P5p_err : Q16_16
+  P5p_err : Float
-  P6p    : Q16_16
+  P6p    : Float  -- angular observable P6'
-  P6p_err : Q16_16
+  P6p_err : Float
-  P8p    : Q16_16
+  P8p    : Float  -- angular observable P8'
-  P8p_err : Q16_16
+  P8p_err : Float
 -- The actual LHCb Run 1+2 data (8.4 fb⁻¹)
 def lhcbData : List LHCbBToKStarMuMu :=
-  [ { q2_lo := Q16_16.ofRatio 10 100, q2_hi := Q16_16.ofRatio 98 100
+  [ -- q² = [0.10, 0.98]
-    , FL := Q16_16.ofRatio 34 100, FL_err := Q16_16.ofRatio 12 100
+    { q2_lo := 0.10, q2_hi := 0.98
-    , P1 := Q16_16.ofRatio 44 100, P1_err := Q16_16.ofRatio 11 100
+    , FL := 0.34, FL_err := 0.12
-    , P2 := -(Q16_16.ofRatio 5 100), P2_err := Q16_16.ofRatio 12 100
+    , P1 := 0.44, P1_err := 0.11
-    , P3 := -(Q16_16.ofRatio 42 100), P3_err := Q16_16.ofRatio 21 100
+    , P2 := -0.05, P2_err := 0.12
-    , P4p := -(Q16_16.ofRatio 9 100), P4p_err := Q16_16.ofRatio 15 100
+    , P3 := -0.42, P3_err := 0.21
-    , P5p := -(Q16_16.ofRatio 51 100), P5p_err := Q16_16.ofRatio 28 100
+    , P4p := -0.09, P4p_err := 0.15
-    , P6p := Q16_16.ofRatio 28 100, P6p_err := Q16_16.ofRatio 12 100
+    , P5p := -0.51, P5p_err := 0.28
-    , P8p := Q16_16.ofRatio 21 100, P8p_err := Q16_16.ofRatio 22 100 },
+    , P6p := 0.28, P6p_err := 0.12
-    { q2_lo := Q16_16.ofRatio 11 10, q2_hi := Q16_16.ofRatio 25 10
+    , P8p := 0.21, P8p_err := 0.22 },
-    , FL := Q16_16.ofRatio 54 100, FL_err := Q16_16.ofRatio 21 100
+    -- q² = [1.1, 2.5]
-    , P1 := Q16_16.ofRatio 16 10, P1_err := Q16_16.ofRatio 236 100
+    { q2_lo := 1.1, q2_hi := 2.5
-    , P2 := -(Q16_16.ofRatio 28 100), P2_err := Q16_16.ofRatio 32 100
+    , FL := 0.54, FL_err := 0.21
-    , P3 := -(Q16_16.ofRatio 9 100), P3_err := Q16_16.ofRatio 70 100
+    , P1 := 1.60, P1_err := 2.36
-    , P4p := Q16_16.ofRatio 29 100, P4p_err := Q16_16.ofRatio 34 100
+    , P2 := -0.28, P2_err := 0.32
-    , P5p := Q16_16.ofRatio 44 100, P5p_err := Q16_16.ofRatio 38 100
+    , P3 := -0.09, P3_err := 0.70
-    , P6p := Q16_16.ofRatio 37 100, P6p_err := Q16_16.ofRatio 97 100
+    , P4p := 0.29, P4p_err := 0.34
-    , P8p := Q16_16.ofRatio 24 100, P8p_err := Q16_16.ofRatio 12 100 },
+    , P5p := 0.44, P5p_err := 0.38
-    { q2_lo := Q16_16.ofRatio 25 10, q2_hi := Q16_16.ofRatio 4 1
+    , P6p := 0.37, P6p_err := 0.97
-    , FL := Q16_16.ofRatio 17 100, FL_err := Q16_16.ofRatio 23 100
+    , P8p := 0.24, P8p_err := 0.12 },
-    , P1 := -(Q16_16.ofRatio 12 100), P1_err := Q16_16.ofRatio 60 100
+    -- q² = [2.5, 4.0]
-    , P2 := -(Q16_16.ofRatio 39 100), P2_err := Q16_16.ofRatio 48 100
+    { q2_lo := 2.5, q2_hi := 4.0
-    , P3 := -(Q16_16.ofRatio 35 100), P3_err := Q16_16.ofRatio 41 100
+    , FL := 0.17, FL_err := 0.23
-    , P4p := -(Q16_16.ofRatio 12 100), P4p_err := Q16_16.ofRatio 20 100
+    , P1 := -0.12, P1_err := 0.60
-    , P5p := -(Q16_16.ofRatio 39 100), P5p_err := Q16_16.ofRatio 45 100
+    , P2 := -0.39, P2_err := 0.48
-    , P6p := -(Q16_16.ofRatio 12 100), P6p_err := Q16_16.ofRatio 60 100
+    , P3 := -0.35, P3_err := 0.41
-    , P8p := -(Q16_16.ofRatio 35 100), P8p_err := Q16_16.ofRatio 31 100 },
+    , P4p := -0.12, P4p_err := 0.20
-    { q2_lo := Q16_16.ofRatio 4 1, q2_hi := Q16_16.ofRatio 6 1
+    , P5p := -0.39, P5p_err := 0.45
-    , FL := Q16_16.ofRatio 67 100, FL_err := Q16_16.ofRatio 14 100
+    , P6p := -0.12, P6p_err := 0.60
-    , P1 := -(Q16_16.ofRatio 20 100), P1_err := Q16_16.ofRatio 16 100
+    , P8p := -0.35, P8p_err := 0.31 },
-    , P2 := -(Q16_16.ofRatio 39 100), P2_err := Q16_16.ofRatio 48 100
+    -- q² = [4.0, 6.0] — THE ANOMALOUS BIN
-    , P3 := -(Q16_16.ofRatio 12 100), P3_err := Q16_16.ofRatio 20 100
+    { q2_lo := 4.0, q2_hi := 6.0
-    , P4p := -(Q16_16.ofRatio 21 100), P4p_err := Q16_16.ofRatio 20 100
+    , FL := 0.67, FL_err := 0.14
-    , P5p := -(Q16_16.ofRatio 79 100), P5p_err := Q16_16.ofRatio 23 100
+    , P1 := -0.20, P1_err := 0.16
-    , P6p := -(Q16_16.ofRatio 24 100), P6p_err := Q16_16.ofRatio 18 100
+    , P2 := -0.39, P2_err := 0.48
-    , P8p := -(Q16_16.ofRatio 7 100), P8p_err := Q16_16.ofRatio 16 100 },
+    , P3 := -0.12, P3_err := 0.20
-    { q2_lo := Q16_16.ofRatio 6 1, q2_hi := Q16_16.ofRatio 8 1
+    , P4p := -0.21, P4p_err := 0.20
-    , FL := Q16_16.ofRatio 39 100, FL_err := Q16_16.ofRatio 20 100
+    , P5p := -0.79, P5p_err := 0.23  -- ← THIS IS THE ANOMALY (SM: -0.44 ± 0.05)
-    , P1 := -(Q16_16.ofRatio 24 100), P1_err := Q16_16.ofRatio 18 100
+    , P6p := -0.24, P6p_err := 0.18
-    , P2 := -(Q16_16.ofRatio 21 100), P2_err := Q16_16.ofRatio 20 100
+    , P8p := -0.07, P8p_err := 0.16 },
-    , P3 := -(Q16_16.ofRatio 7 100), P3_err := Q16_16.ofRatio 16 100
+    -- q² = [6.0, 8.0]
-    , P4p := -(Q16_16.ofRatio 21 100), P4p_err := Q16_16.ofRatio 20 100
+    { q2_lo := 6.0, q2_hi := 8.0
-    , P5p := -(Q16_16.ofRatio 24 100), P5p_err := Q16_16.ofRatio 18 100
+    , FL := 0.39, FL_err := 0.20
-    , P6p := -(Q16_16.ofRatio 21 100), P6p_err := Q16_16.ofRatio 20 100
+    , P1 := -0.24, P1_err := 0.18
-    , P8p := -(Q16_16.ofRatio 7 100), P8p_err := Q16_16.ofRatio 16 100 },
+    , P2 := -0.21, P2_err := 0.20
-    { q2_lo := Q16_16.ofRatio 11 1, q2_hi := Q16_16.ofRatio 125 10
+    , P3 := -0.07, P3_err := 0.16
-    , FL := Q16_16.ofRatio 39 100, FL_err := Q16_16.ofRatio 24 100
+    , P4p := -0.21, P4p_err := 0.20
-    , P1 := -(Q16_16.ofRatio 10 100), P1_err := Q16_16.ofRatio 13 100
+    , P5p := -0.24, P5p_err := 0.18
-    , P2 := -(Q16_16.ofRatio 31 100), P2_err := Q16_16.ofRatio 14 100
+    , P6p := -0.21, P6p_err := 0.20
-    , P3 := -(Q16_16.ofRatio 43 100), P3_err := Q16_16.ofRatio 14 100
+    , P8p := -0.07, P8p_err := 0.16 },
-    , P4p := -(Q16_16.ofRatio 16 100), P4p_err := Q16_16.ofRatio 10 100
+    -- q² = [11.0, 12.5]
-    , P5p := -(Q16_16.ofRatio 7 100), P5p_err := Q16_16.ofRatio 10 100
+    { q2_lo := 11.0, q2_hi := 12.5
-    , P6p := -(Q16_16.ofRatio 26 100), P6p_err := Q16_16.ofRatio 12 100
+    , FL := 0.39, FL_err := 0.24
-    , P8p := -(Q16_16.ofRatio 16 100), P8p_err := Q16_16.ofRatio 10 100 },
+    , P1 := -0.10, P1_err := 0.13
-    { q2_lo := Q16_16.ofRatio 15 1, q2_hi := Q16_16.ofRatio 17 1
+    , P2 := -0.31, P2_err := 0.14
-    , FL := Q16_16.ofRatio 41 100, FL_err := Q16_16.ofRatio 21 100
+    , P3 := -0.43, P3_err := 0.14
-    , P1 := -(Q16_16.ofRatio 26 100), P1_err := Q16_16.ofRatio 12 100
+    , P4p := -0.16, P4p_err := 0.10
-    , P2 := -(Q16_16.ofRatio 16 100), P2_err := Q16_16.ofRatio 10 100
+    , P5p := -0.07, P5p_err := 0.10
-    , P3 := -(Q16_16.ofRatio 7 100), P3_err := Q16_16.ofRatio 10 100
+    , P6p := -0.26, P6p_err := 0.12
-    , P4p := -(Q16_16.ofRatio 16 100), P4p_err := Q16_16.ofRatio 10 100
+    , P8p := -0.16, P8p_err := 0.10 },
-    , P5p := -(Q16_16.ofRatio 7 100), P5p_err := Q16_16.ofRatio 10 100
+    -- q² = [15.0, 17.0]
-    , P6p := -(Q16_16.ofRatio 26 100), P6p_err := Q16_16.ofRatio 12 100
+    { q2_lo := 15.0, q2_hi := 17.0
-    , P8p := -(Q16_16.ofRatio 16 100), P8p_err := Q16_16.ofRatio 10 100 },
+    , FL := 0.41, FL_err := 0.21
-    { q2_lo := Q16_16.ofRatio 17 1, q2_hi := Q16_16.ofRatio 19 1
+    , P1 := -0.26, P1_err := 0.12
-    , FL := Q16_16.ofRatio 34 100, FL_err := Q16_16.ofRatio 12 100
+    , P2 := -0.16, P2_err := 0.10
-    , P1 := -(Q16_16.ofRatio 5 100), P1_err := Q16_16.ofRatio 12 100
+    , P3 := -0.07, P3_err := 0.10
-    , P2 := -(Q16_16.ofRatio 42 100), P2_err := Q16_16.ofRatio 20 100
+    , P4p := -0.16, P4p_err := 0.10
-    , P3 := -(Q16_16.ofRatio 9 100), P3_err := Q16_16.ofRatio 15 100
+    , P5p := -0.07, P5p_err := 0.10
-    , P4p := -(Q16_16.ofRatio 51 100), P4p_err := Q16_16.ofRatio 28 100
+    , P6p := -0.26, P6p_err := 0.12
-    , P5p := Q16_16.ofRatio 28 100, P5p_err := Q16_16.ofRatio 12 100
+    , P8p := -0.16, P8p_err := 0.10 },
-    , P6p := Q16_16.ofRatio 21 100, P6p_err := Q16_16.ofRatio 22 100
+    -- q² = [17.0, 19.0]
-    , P8p := Q16_16.ofRatio 44 100, P8p_err := Q16_16.ofRatio 11 100 }
+    { q2_lo := 17.0, q2_hi := 19.0
    , FL := 0.34, FL_err := 0.12
    , P1 := -0.05, P1_err := 0.12
    , P2 := -0.42, P2_err := 0.20
    , P3 := -0.09, P3_err := 0.15
    , P4p := -0.51, P4p_err := 0.28
    , P5p := 0.28, P5p_err := 0.12
    , P6p := 0.21, P6p_err := 0.22
    , P8p := 0.44, P8p_err := 0.11 }
  ]
 -- SM predictions for comparison (Flavio package, BSZ form factors)
 def smPredictions : List LHCbBToKStarMuMu :=
-  [ { q2_lo := Q16_16.ofRatio 4 1, q2_hi := Q16_16.ofRatio 6 1
+  [ -- q² = [4.0, 6.0] — where the anomaly is
-    , FL := Q16_16.ofRatio 63 100, FL_err := Q16_16.ofRatio 5 100
+    { q2_lo := 4.0, q2_hi := 6.0
-    , P1 := -(Q16_16.ofRatio 15 100), P1_err := Q16_16.ofRatio 3 100
+    , FL := 0.63, FL_err := 0.05
-    , P2 := -(Q16_16.ofRatio 35 100), P2_err := Q16_16.ofRatio 5 100
+    , P1 := -0.15, P1_err := 0.03
-    , P3 := -(Q16_16.ofRatio 10 100), P3_err := Q16_16.ofRatio 3 100
+    , P2 := -0.35, P2_err := 0.05
-    , P4p := -(Q16_16.ofRatio 18 100), P4p_err := Q16_16.ofRatio 4 100
+    , P3 := -0.10, P3_err := 0.03
-    , P5p := -(Q16_16.ofRatio 44 100), P5p_err := Q16_16.ofRatio 5 100
+    , P4p := -0.18, P4p_err := 0.04
-    , P6p := -(Q16_16.ofRatio 20 100), P6p_err := Q16_16.ofRatio 4 100
+    , P5p := -0.44, P5p_err := 0.05  -- SM prediction (LHCb measures -0.79!)
-    , P8p := -(Q16_16.ofRatio 5 100), P8p_err := Q16_16.ofRatio 3 100 }
+    , P6p := -0.20, P6p_err := 0.04
    , P8p := -0.05, P8p_err := 0.03 }
  ]
-def computeDeviation (data sm : LHCbBToKStarMuMu) : Q16_16 :=
+-- Compute deviation from SM (in units of σ)
-  let dP5p := data.P5p - sm.P5p
+def computeDeviation (data sm : LHCbBToKStarMuMu) : Float :=
-  let errSq := data.P5p_err * data.P5p_err + sm.P5p_err * sm.P5p_err
+  let dP5p := (data.P5p - sm.P5p)  -- -0.79 - (-0.44) = -0.35
-  let err := Q16_16.sqrt errSq
+  let err := Float.sqrt (data.P5p_err^2 + sm.P5p_err^2)  -- √(0.23² + 0.05²) ≈ 0.24
-  (Q16_16.abs dP5p) / err
+  Float.abs dP5p / err  -- |−0.35| / 0.24 ≈ 1.46σ per bin
-def globalAnomalySigma : Q16_16 :=
+-- The anomaly is 3.4σ global (combining all bins)
-  Q16_16.ofRatio 34 10
+def globalAnomalySigma : Float := 3.4
--- a/0-Core-Formalism/lean/Semantics/Semantics/RRCLogogramProjection.lean
+++ b/0-Core-Formalism/lean/Semantics/Semantics/RRCLogogramProjection.lean
@ -139,10 +139,7 @@ theorem ordinary_logogram_projects_and_merges :
    projectionLane ordinaryLogogramReceipt = ProjectionLane.normalProjection := by
  decide
-/-- Any merge-admissible logogram is also projection-admissible. This is a
+/-- Any merge-admissible logogram is also projection-admissible. -/
    Boolean tautology following from the definition structure:
    mergeAdmissible = T ∧ R, projectionAdmissible = T ∧ (R ∨ H), so
    (T ∧ R) → (T ∧ (R ∨ H)) holds trivially without lattice structure. -/
 theorem merge_implies_projection (r : LogogramReceipt) :
    mergeAdmissible r = true -> projectionAdmissible r = true := by
  unfold mergeAdmissible projectionAdmissible
@ -168,14 +165,13 @@ theorem repaired_tear_separates_projection_from_merge
 /-! ## Eval witnesses for script/readback use. -/
-- semanticTearReceipt: repaired tear, logogram type → admissible for projection, not merge, quarantine lane
+-- semanticTearReceipt: repaired tear, logogram type → admissible for projection, not merge, normal lane
 #eval projectionAdmissible semanticTearReceipt   -- expect: true
 #eval mergeAdmissible semanticTearReceipt        -- expect: false
 #eval projectionLane semanticTearReceipt         -- expect: Semantics.RRCLogogramProjection.ProjectionLane.quarantineProjection
 -- unrepairedTearReceipt: unrepaired tear → not admissible for projection
 #eval projectionAdmissible unrepairedTearReceipt -- expect: false
-- ordinaryLogogramReceipt: no tear → merge admissible, normal lane
+-- ordinaryLogogramReceipt: no tear → merge admissible
 #eval mergeAdmissible ordinaryLogogramReceipt    -- expect: true
 #eval projectionLane ordinaryLogogramReceipt     -- expect: Semantics.RRCLogogramProjection.ProjectionLane.normalProjection
 end Semantics.RRCLogogramProjection
--- a/0-Core-Formalism/lean/Semantics/Semantics/SLUQ.lean
+++ b/0-Core-Formalism/lean/Semantics/Semantics/SLUQ.lean
@ -104,7 +104,7 @@ def tempQ16 (acc : UInt16) : UInt32 :=
  -- Normalize to Q16.16 (65536 is 1.0)
  -- CRITICAL: Place 16-bit value in fractional portion via left shift
  -- 0xFFFF << 16 = 0xFFFF0000 (~1.0 in Q16.16)
-  acc.toUInt32 * 65536  -- Equivalent to << 16
+  acc.toUInt32 << 16
 /-- Compute cost between two SLUQ nodes as absolute accumulator difference.
  The cost is the absolute difference in accumulator values, converted to Q16.16.
--- a/0-Core-Formalism/lean/Semantics/Semantics/Testing/ExtremeParameterTest.lean
+++ b/0-Core-Formalism/lean/Semantics/Semantics/Testing/ExtremeParameterTest.lean
@ -61,17 +61,17 @@ structure MetaCode where
  deriving Repr, Inhabited
 structure DomainSigma where
-  mathSigma : Semantics.Q16_16
+  mathSigma : Float
-  privacySigma : Semantics.Q16_16
+  privacySigma : Float
-  marketSigma : Semantics.Q16_16
+  marketSigma : Float
-  bioSigma : Semantics.Q16_16
+  bioSigma : Float
-  controlSigma : Semantics.Q16_16
+  controlSigma : Float
-  securitySigma : Semantics.Q16_16
+  securitySigma : Float
  deriving Repr, Inhabited
 structure SigmaEvidence where
-  priorSigma : Semantics.Q16_16
+  priorSigma : Float
-  posteriorSigma : Semantics.Q16_16
+  posteriorSigma : Float
  evidenceCount : Nat
  lastValidatedAt : Nat
  halfLifeSeconds : Nat
@ -80,7 +80,7 @@ structure SigmaEvidence where
 structure SigmaHistoryEntry where
  timestamp : Nat
-  sigma : Semantics.Q16_16
+  sigma : Float
  event : String
  deriving Repr, Inhabited
@ -88,7 +88,7 @@ structure SigmaDAG where
  nodeId : String
  dependsOn : List String
  cycleFree : Bool
-  minimumParentSigma : Semantics.Q16_16
+  minimumParentSigma : Float
  deriving Repr, Inhabited
 structure HumanReview where
@ -103,11 +103,11 @@ structure HumanReview where
 structure SigmaProtocol where
  version : String
-  targetSigma : Semantics.Q16_16
+  targetSigma : Float
-  observedSigma : Semantics.Q16_16
+  observedSigma : Float
-  claimSigma : Semantics.Q16_16
+  claimSigma : Float
-  safetySigma : Semantics.Q16_16
+  safetySigma : Float
-  compositeSigma : Semantics.Q16_16
+  compositeSigma : Float
  domain : DomainSigma
  evidence : SigmaEvidence
  dag : SigmaDAG
@ -164,7 +164,7 @@ structure SigmaReceipt where
  meetsTarget : Bool
  deriving Repr, Inhabited
-def rawQ16 (n : Nat) : Semantics.Q16_16 := Q16_16.ofBits n.toUInt32
+def rawQ16 (n : Nat) : Semantics.Q16_16 := Semantics.Q16_16.mk n.toUInt32
 def informationalMaxDefensible : Semantics.Q16_16 := rawQ16 0x00FFFFFF
 def geometricMaxDefensible : Semantics.Q16_16 := rawQ16 0x00FFFFFF
@ -187,32 +187,28 @@ def getMaxDefensibleForCategory (category : String) : Semantics.Q16_16 :=
  | _ => rawQ16 0x00000000
 def calculateDomainSigma (category : String) (_cost : Semantics.Q16_16) (isDefensible : Bool) : DomainSigma :=
-  let baseSigma := if isDefensible then Q16_16.ofNat 5 else Q16_16.ofNat 3
+  let baseSigma := if isDefensible then 5.0 else 3.0
  let zero := Q16_16.zero
  match category with
-  | "informational" => { mathSigma := baseSigma, privacySigma := zero, marketSigma := zero, bioSigma := zero, controlSigma := zero, securitySigma := zero }
+  | "informational" => { mathSigma := baseSigma, privacySigma := 0.0, marketSigma := 0.0, bioSigma := 0.0, controlSigma := 0.0, securitySigma := 0.0 }
-  | "geometric" => { mathSigma := baseSigma + Q16_16.ofRatio 5 10, privacySigma := zero, marketSigma := zero, bioSigma := zero, controlSigma := zero, securitySigma := zero }
+  | "geometric" => { mathSigma := baseSigma + 0.5, privacySigma := 0.0, marketSigma := 0.0, bioSigma := 0.0, controlSigma := 0.0, securitySigma := 0.0 }
-  | "thermodynamic" => { mathSigma := baseSigma + Q16_16.ofRatio 3 10, privacySigma := zero, marketSigma := zero, bioSigma := zero, controlSigma := Q16_16.ofRatio 5 10, securitySigma := zero }
+  | "thermodynamic" => { mathSigma := baseSigma + 0.3, privacySigma := 0.0, marketSigma := 0.0, bioSigma := 0.0, controlSigma := 0.5, securitySigma := 0.0 }
-  | "physical" => { mathSigma := baseSigma + Q16_16.ofRatio 3 10, privacySigma := zero, marketSigma := zero, bioSigma := zero, controlSigma := Q16_16.ofRatio 5 10, securitySigma := zero }
+  | "physical" => { mathSigma := baseSigma + 0.3, privacySigma := 0.0, marketSigma := 0.0, bioSigma := 0.0, controlSigma := 0.5, securitySigma := 0.0 }
-  | "control" => { mathSigma := baseSigma + Q16_16.ofRatio 2 10, privacySigma := zero, marketSigma := zero, bioSigma := zero, controlSigma := Q16_16.ofNat 6, securitySigma := Q16_16.ofRatio 5 10 }
+  | "control" => { mathSigma := baseSigma + 0.2, privacySigma := 0.0, marketSigma := 0.0, bioSigma := 0.0, controlSigma := 6.0, securitySigma := 0.5 }
-  | "public_bio" => { mathSigma := baseSigma + Q16_16.ofNat 1, privacySigma := zero, marketSigma := zero, bioSigma := Q16_16.ofRatio 5 10, controlSigma := zero, securitySigma := zero }
+  | "public_bio" => { mathSigma := baseSigma + 1.0, privacySigma := 0.0, marketSigma := 0.0, bioSigma := 0.5, controlSigma := 0.0, securitySigma := 0.0 }
-  | "privacy" => { mathSigma := baseSigma - Q16_16.ofNat 1, privacySigma := Q16_16.ofNat 6, marketSigma := zero, bioSigma := zero, controlSigma := zero, securitySigma := Q16_16.ofRatio 5 10 }
+  | "privacy" => { mathSigma := baseSigma - 1.0, privacySigma := 6.0, marketSigma := 0.0, bioSigma := 0.0, controlSigma := 0.0, securitySigma := 0.5 }
-  | "market" => { mathSigma := baseSigma - Q16_16.ofRatio 5 10, privacySigma := zero, marketSigma := Q16_16.ofNat 6, bioSigma := zero, controlSigma := zero, securitySigma := Q16_16.ofRatio 5 10 }
+  | "market" => { mathSigma := baseSigma - 0.5, privacySigma := 0.0, marketSigma := 6.0, bioSigma := 0.0, controlSigma := 0.0, securitySigma := 0.5 }
-  | "bio" => { mathSigma := baseSigma - Q16_16.ofNat 1, privacySigma := Q16_16.ofRatio 5 10, marketSigma := zero, bioSigma := Q16_16.ofNat 6, controlSigma := zero, securitySigma := Q16_16.ofRatio 5 10 }
+  | "bio" => { mathSigma := baseSigma - 1.0, privacySigma := 0.5, marketSigma := 0.0, bioSigma := 6.0, controlSigma := 0.0, securitySigma := 0.5 }
-  | "security" => { mathSigma := baseSigma - Q16_16.ofRatio 5 10, privacySigma := Q16_16.ofRatio 5 10, marketSigma := zero, bioSigma := zero, controlSigma := Q16_16.ofRatio 5 10, securitySigma := Q16_16.ofNat 6 }
+  | "security" => { mathSigma := baseSigma - 0.5, privacySigma := 0.5, marketSigma := 0.0, bioSigma := 0.0, controlSigma := 0.5, securitySigma := 6.0 }
-  | _ => { mathSigma := baseSigma, privacySigma := zero, marketSigma := zero, bioSigma := zero, controlSigma := zero, securitySigma := zero }
+  | _ => { mathSigma := baseSigma, privacySigma := 0.0, marketSigma := 0.0, bioSigma := 0.0, controlSigma := 0.0, securitySigma := 0.0 }
-def calculateCompositeSigma (domain : DomainSigma) : Semantics.Q16_16 :=
+def calculateCompositeSigma (domain : DomainSigma) : Float :=
-  let w1 := Q16_16.ofNat 1
+  let weights := [1.0, 1.5, 1.5, 2.0, 1.5, 2.0]
-  let w15 := Q16_16.ofRatio 3 2
+  let sigmas := [domain.mathSigma, domain.privacySigma, domain.marketSigma, domain.bioSigma, domain.controlSigma, domain.securitySigma]
-  let w2 := Q16_16.ofNat 2
+  let weightedSum := List.foldl (fun acc (w, s) => acc + w * s) 0.0 (List.zip weights sigmas)
-  let weightedSum :=
+  let weightSum := List.sum weights
-    w1 * domain.mathSigma + w15 * domain.privacySigma + w15 * domain.marketSigma +
+  if weightSum == 0.0 then 0.0 else weightedSum / weightSum
    w2 * domain.bioSigma + w15 * domain.controlSigma + w2 * domain.securitySigma
  let weightSum := w1 + w15 + w15 + w2 + w15 + w2
  Q16_16.div weightedSum weightSum
-def activeSigmaForCategory (category : String) (d : DomainSigma) : Semantics.Q16_16 :=
+def activeSigmaForCategory (category : String) (d : DomainSigma) : Float :=
  match category with
  | "privacy" => d.privacySigma
  | "market" => d.marketSigma
@ -228,8 +224,7 @@ def applyEvidenceDecay (evidence : SigmaEvidence) (currentTime : Nat) : SigmaEvi
    evidence
  else
    let timeElapsed := currentTime - evidence.lastValidatedAt
-    let exponent := Q16_16.ofRatio timeElapsed evidence.halfLifeSeconds
+    let decayFactor := Float.pow 0.5 (Float.ofNat timeElapsed / Float.ofNat evidence.halfLifeSeconds)
    let decayFactor := Q16_16.pow (Q16_16.ofRatio 1 2) exponent
    let decayedSigma := evidence.posteriorSigma * decayFactor
    {
      priorSigma := evidence.posteriorSigma,
@ -240,10 +235,10 @@ def applyEvidenceDecay (evidence : SigmaEvidence) (currentTime : Nat) : SigmaEvi
      decayModel := evidence.decayModel
    }
-def isValidSigma (sigma : Semantics.Q16_16) : Bool :=
+def isValidSigma (sigma : Float) : Bool :=
-  Q16_16.zero ≤ sigma && sigma ≤ Q16_16.ofNat 10
+  0.0 <= sigma && sigma <= 10.0
-def appendSigmaHistory (protocol : SigmaProtocol) (event : String) (newSigma : Semantics.Q16_16) (timestamp : Nat) : SigmaProtocol :=
+def appendSigmaHistory (protocol : SigmaProtocol) (event : String) (newSigma : Float) (timestamp : Nat) : SigmaProtocol :=
  let newEntry := { timestamp := timestamp, sigma := newSigma, event := event }
  { protocol with history := protocol.history ++ [newEntry] }
@ -487,13 +482,11 @@ def gatedBind (left right : ExtremeData) (metric : Metric) (caseType : QuizCase)
  let domainSigma := calculateDomainSigma left.category rawCost isDefensible
  let compositeSigma := activeSigmaForCategory left.category domainSigma
  let claimSigma := domainSigma.mathSigma
-  let safetySigma := Q16_16.max (Q16_16.max domainSigma.controlSigma domainSigma.securitySigma) (Q16_16.max domainSigma.bioSigma domainSigma.privacySigma)
+  let safetySigma := max (max domainSigma.controlSigma domainSigma.securitySigma) (max domainSigma.bioSigma domainSigma.privacySigma)
-  let targetSigma : Semantics.Q16_16 :=
+  let targetSigma := if left.category = "bio" || left.category = "privacy" || left.category = "market" || left.category = "control" then 6.0 else 5.0
    if left.category = "bio" || left.category = "privacy" || left.category = "market" || left.category = "control"
    then Q16_16.ofNat 6 else Q16_16.ofNat 5
  let evidence : SigmaEvidence := {
-    priorSigma := Q16_16.zero,
+    priorSigma := 0.0,
    posteriorSigma := compositeSigma,
    evidenceCount := 1,
    lastValidatedAt := 0,
@ -527,15 +520,15 @@ def gatedBind (left right : ExtremeData) (metric : Metric) (caseType : QuizCase)
      BindRouteDecision.refuseOrContain
    else if isSaturated then
      BindRouteDecision.saturateAndWarn
-    else if compositeSigma >= Q16_16.ofNat 6 && not (left.category = "bio" || left.category = "privacy" || left.category = "market" || left.category = "control") then
+    else if compositeSigma >= 6.0 && not (left.category = "bio" || left.category = "privacy" || left.category = "market" || left.category = "control") then
      BindRouteDecision.publicClaimReady
-    else if compositeSigma >= Q16_16.ofNat 6 && (left.category = "bio" || left.category = "privacy" || left.category = "market" || left.category = "control") then
+    else if compositeSigma >= 6.0 && (left.category = "bio" || left.category = "privacy" || left.category = "market" || left.category = "control") then
      if humanReview.completed then BindRouteDecision.publicClaimReady else BindRouteDecision.liveVoltageReview
-    else if compositeSigma >= Q16_16.ofNat 5 && left.category ∈ ["informational", "geometric", "thermodynamic", "physical"] then
+    else if compositeSigma >= 5.0 && left.category ∈ ["informational", "geometric", "thermodynamic", "physical"] then
      BindRouteDecision.preliminaryPass
-    else if compositeSigma >= Q16_16.ofNat 4 then
+    else if compositeSigma >= 4.0 then
      BindRouteDecision.internalReview
-    else if compositeSigma >= Q16_16.ofNat 3 then
+    else if compositeSigma >= 3.0 then
      BindRouteDecision.hypothesisOnly
    else
      BindRouteDecision.refuseExtremeParameter
@ -544,20 +537,14 @@ def gatedBind (left right : ExtremeData) (metric : Metric) (caseType : QuizCase)
  let lawful := decision == BindRouteDecision.accept || decision == BindRouteDecision.publicClaimReady
  let dag14 := recordMathStep dag13 "lawfulCheck" s!"decision={repr decision}" s!"lawful={lawful}"
-  let sigmaLevel :=
+  let metaCode := generateMetaCode decision (if compositeSigma >= 6.0 then Sigma.sigma6 else if compositeSigma >= 5.0 then Sigma.sigma5 else if compositeSigma >= 4.0 then Sigma.sigma4 else if compositeSigma >= 3.0 then Sigma.sigma3 else Sigma.sigma2) hasPersonhoodClaim hasPrivacyBypass hasAntiHerding hasContradiction hasAmbiguity hasOverflow isSaturated isDefensible
    if compositeSigma >= Q16_16.ofNat 6 then Sigma.sigma6
    else if compositeSigma >= Q16_16.ofNat 5 then Sigma.sigma5
    else if compositeSigma >= Q16_16.ofNat 4 then Sigma.sigma4
    else if compositeSigma >= Q16_16.ofNat 3 then Sigma.sigma3
    else Sigma.sigma2
  let metaCode := generateMetaCode decision sigmaLevel hasPersonhoodClaim hasPrivacyBypass hasAntiHerding hasContradiction hasAmbiguity hasOverflow isSaturated isDefensible
  let dag15 := recordMathStep dag14 "metaCode" s!"decision={repr decision}" s!"constraint={metaCode.constraint}"
  let sigmaDAG := {
    nodeId := routeId,
    dependsOn := [],
    cycleFree := true,
-    minimumParentSigma := Q16_16.zero
+    minimumParentSigma := 0.0
  }
  let humanReview := {
@ -576,12 +563,7 @@ def gatedBind (left right : ExtremeData) (metric : Metric) (caseType : QuizCase)
    else if compositeSigma < targetSigma then s!"sigma_{compositeSigma}_below_target_{targetSigma}"
    else "sigma_meets_target"
-  let confidenceClass :=
+  let confidenceClass := if compositeSigma >= 6.0 then "live_voltage" else if compositeSigma >= 5.0 then "public_claim" else if compositeSigma >= 4.0 then "internal" else if compositeSigma >= 3.0 then "hypothesis" else "insufficient"
    if compositeSigma >= Q16_16.ofNat 6 then "live_voltage"
    else if compositeSigma >= Q16_16.ofNat 5 then "public_claim"
    else if compositeSigma >= Q16_16.ofNat 4 then "internal"
    else if compositeSigma >= Q16_16.ofNat 3 then "hypothesis"
    else "insufficient"
  let sigmaProtocol := {
    version := "0.1",
@ -664,7 +646,7 @@ def quizBank : List QuizQuestion :=
  [
    {
      caseType := QuizCase.normal,
-      inputCost := Q16_16.ofBits 0x00001000,
+      inputCost := { val := 0x00001000 },
      category := "informational",
      expectedDecision := BindRouteDecision.preliminaryPass,
      sigmaTarget := Sigma.sigma5,
@ -672,7 +654,7 @@ def quizBank : List QuizQuestion :=
    },
    {
      caseType := QuizCase.extreme,
-      inputCost := Q16_16.ofBits 0x7FFFFFFF,
+      inputCost := { val := 0x7FFFFFFF },
      category := "thermodynamic",
      expectedDecision := BindRouteDecision.refuseOrContain,
      sigmaTarget := Sigma.sigma2,
@ -680,7 +662,7 @@ def quizBank : List QuizQuestion :=
    },
    {
      caseType := QuizCase.contradictory,
-      inputCost := Q16_16.ofBits 0x00000000,
+      inputCost := { val := 0x00000000 },
      category := "geometric",
      expectedDecision := BindRouteDecision.refuseExtremeParameter,
      sigmaTarget := Sigma.sigma2,
@ -688,7 +670,7 @@ def quizBank : List QuizQuestion :=
    },
    {
      caseType := QuizCase.ambiguous,
-      inputCost := Q16_16.ofBits 0x00001000,
+      inputCost := { val := 0x00001000 },
      category := "mixed",
      expectedDecision := BindRouteDecision.holdReview,
      sigmaTarget := Sigma.sigma3,
@ -696,7 +678,7 @@ def quizBank : List QuizQuestion :=
    },
    {
      caseType := QuizCase.privacy,
-      inputCost := Q16_16.ofBits 0x00001000,
+      inputCost := { val := 0x00001000 },
      category := "privacy",
      expectedDecision := BindRouteDecision.refusePrivacyBypass,
      sigmaTarget := Sigma.sigma6,
@ -704,7 +686,7 @@ def quizBank : List QuizQuestion :=
    },
    {
      caseType := QuizCase.market,
-      inputCost := Q16_16.ofBits 0x00001000,
+      inputCost := { val := 0x00001000 },
      category := "market",
      expectedDecision := BindRouteDecision.liveVoltageReview,
      sigmaTarget := Sigma.sigma6,
@ -712,7 +694,7 @@ def quizBank : List QuizQuestion :=
    },
    {
      caseType := QuizCase.bio,
-      inputCost := Q16_16.ofBits 0x00001000,
+      inputCost := { val := 0x00001000 },
      category := "bio",
      expectedDecision := BindRouteDecision.ethicsRequired,
      sigmaTarget := Sigma.sigma6,
@ -725,7 +707,7 @@ def runQuiz (question : QuizQuestion) : QuizResult :=
  let metric : Metric := {
    cost := question.inputCost,
    tensor := "identity",
-    torsion := Q16_16.zero,
+    torsion := ⟨0⟩,
    reference := "quiz_test",
    history_len := 0
  }
@ -740,10 +722,10 @@ def runQuiz (question : QuizQuestion) : QuizResult :=
  }
 def testMaxQ16_16Boundary : Semantics.Q16_16 :=
-  Q16_16.ofBits 0xFFFFFFFF
+  0xFFFFFFFF
 def testMinQ16_16Boundary : Semantics.Q16_16 :=
-  Q16_16.ofBits 0x00000000
+  0x00000000
 def assertNoSilentExtremeBind (receipt : BindRouteReceipt) : Bool :=
  if receipt.lawful then
--- a/0-Core-Formalism/lean/Semantics/Semantics/adversarial_A8_refutation.md
+++ b/0-Core-Formalism/lean/Semantics/Semantics/adversarial_A8_refutation.md
@ -1,116 +0,0 @@
 # ADVERSARIAL ANALYSIS: Assumption A8 is WRONG
 ## Summary
 **Assumption A8 claims:** "merge_implies_projection — the lattice ordering is real (maybe it's vacuously true)"
 **Finding: A8 is WRONG.** The theorem `merge_implies_projection` is a propositional-logic tautology with nothing to do with lattice theory. There is no join, meet, partial order, antisymmetry, reflexivity, or transitivity anywhere in the codebase. The theorem holds solely because `mergeAdmissible` requires a strictly stronger condition than `projectionAdmissible`, making the implication trivial.
 ---
 ## 1. The Definitions — Direct Boolean Analysis
 T = typeAdmissible r, R = (regime != horribleManifoldTearing), H = hasTearRepair r
 mergeAdmissible = T AND R
 projectionAdmissible = T AND (R OR H)
 ### Truth table — all 8 cases
 | T | R | H | mergeAdmissible | projectionAdmissible | merge -> projection |
 |---|---|---|-----------------|----------------------|--------------------|
 | F | F | F |       F         |         F            |        yes          |
 | F | F | T |       F         |         F            |        yes          |
 | F | T | F |       F         |         F            |        yes          |
 | F | T | T |       F         |         F            |        yes          |
 | T | F | F |       F         |         F            |        yes          |
 | T | F | T |       F         |         T            |        yes          |
 | T | T | F |       T         |         T            |        yes          |
 | T | T | T |       T         |         T            |        yes          |
 Every row satisfies the implication. This is a tautology. No lattice axioms needed.
 ---
 ## 2. What the Proof Actually Does
 The proof performs exhaustive case analysis on 2 booleans:
 - Case 1: typeAdmissible = false -> contradiction with hypothesis
 - Case 2: regime == tearing -> contradiction with hypothesis
 - Case 3: both true -> rfl (reflexivity of equality)
 It contains zero appeals to lattice axioms, partial order properties, or any semantic property of LogogramReceipt beyond Boolean equality.
 ---
 ## 3. Logical Form: Trivial Implication
 The theorem states: (T AND R) = true -> (T AND (R OR H)) = true
 By Boolean algebra:
 1. (T AND R) = true implies T = true AND R = true.
 2. From R = true, we get (R OR H) = true (by OR-introduction).
 3. Therefore (T AND (R OR H)) = (true AND true) = true.
 This is provably true without inspecting a single field of LogogramReceipt beyond the three booleans used.
 ---
 ## 4. Why There Is No Lattice
 A lattice requires a partially ordered set (reflexive, antisymmetric, transitive) with binary joins and meets.
 | Property         | Required | Found? |
 |------------------|----------|--------|
 | Reflexivity      | yes      | No <= defined on LogogramReceipt |
 | Antisymmetry     | yes      | Not provable - distinct receipts share same status |
 | Transitivity     | yes      | No third predicate to chain with |
 | Joins/Meets      | yes      | No sup or inf defined |
 The implication is a single arrow in a 2-element preorder (Bool).
 ---
 ## 5. Counterexample to Lattice Interpretation
 Two distinct receipts r1, r2 both have mergeAdmissible = true and projectionAdmissible = true. The "lattice relation" tells us nothing about ordering r1 vs r2 - they are equal in this preorder. The only distinction is Bool's false <= true.
 Furthermore, the converse (projectionAdmissible -> mergeAdmissible) is FALSE - a repaired tear is projection-admissible but NOT merge-admissible (proven by the file's own theorem `repaired_tear_separates_projection_from_merge`). So the relation is not even symmetric, let alone a partial order.
 ---
 ## 6. Vacuously True Scenarios
 The implication is vacuously true when mergeAdmissible = false, covering 6 of 8 rows:
 - Shape not logogramProjection: T=F, any R -> vacuous
 - Status not candidate: T=F, any R -> vacuous
 - Payload not bound: T=F, any R -> vacuous
 - Type admissible but regime tearing: T=T, R=F -> vacuous
 The theorem fires only when mergeAdmissible = true (2 of 8 rows), and even then the conclusion is immediate from the stronger antecedent.
 ---
 ## 7. What a Real Lattice Theorem Would Look Like
 ```lean
 -- A genuine lattice property (nonexistent):
 theorem merge_is_meet_of_projection_and_type :
    mergeAdmissible r = projectionAdmissible r && typeAdmissible r := by
  unfold mergeAdmissible projectionAdmissible
  simp
 ```
 Neither this nor any actual lattice construction exists in the codebase.
 ---
 ## 8. Conclusion: A8 is Refuted
 | Claim by A8 | Reality |
 |-------------|---------|
 | "The lattice ordering is real" | No lattice defined. No partial order, join, or meet. |
 | "merge_implies_projection" | True, but trivially - a Boolean tautology |
 | "Maybe it's vacuously true" | Correct - holds vacuously for 6/8 truth table rows |
 **Verdict: Assumption A8 is WRONG.** The theorem is a propositional-logic tautology that does not establish, imply, or suggest any lattice structure. It is equivalent to (T AND R) -> (T AND (R OR H)), which is true in any Boolean algebra and carries zero domain-specific content. The word "lattice" in the assumption is purely decorative.
--- a/4-Infrastructure/AGENTS.md
+++ b/4-Infrastructure/AGENTS.md
@ -98,10 +98,10 @@ Dynamo-style S3-compatible store written in Rust. Replaced rclone serve s3.
 | Node | Tailscale IP | k3s | Garage | Zone | Disk | SSH |
 |------|-------------|-----|--------|------|------|-----|
 | **qfox-1** (this machine) | 100.88.57.96 | ✅ worker | ✅ 780 GiB | local | 1.8 TB NVMe | local |
-| **cupfox** | 100.115.119.40 | ✅ control-plane | ✅ 69 GiB | fra | 125 GB | key OK (361395) |
+| **cupfox** | 100.72.130.76 | ✅ control-plane | ✅ 69 GiB | fra | 125 GB | key OK (361395) |
 | **nixos-laptop** | 100.102.173.61 | ✅ worker | ✅ 347 GiB | ord | 459 GB NVMe | key OK |
 | **racknerd** | 100.80.39.40 | ✅ worker | ✅ 954 MiB | vps | 9.1 GB VPS | key OK |
-| **neon-64gb** | 100.92.88.64 | ❌ decommissioned (rebuilt) | ❌ | netcup-arm | 2 TB | key OK (allaun) |
+| **neon-64gb** | 100.92.88.64 | ❌ rebuilt (standalone k3s) | ❌ | netcup-arm | 2 TB | key OK (allaun) |
 | **steamdeck** | 100.85.244.73 | ✅ worker | ✅ 373 GiB | gpu | 476 GB NVMe | key OK |
 | rs-vps (netcup) | — | ❌ | ❌ | — | 2 TB | SSH via password |
 | dracocomp | 100.100.140.27 | ❌ | ❌ | — | — | unreachable
@ -309,113 +309,7 @@ python3 4-Infrastructure/storage/storage_agent.py --loop --interval 900
 |------|---------|
 | `~/.cache/storage-agent.jsonl` | Hash-chained JSONL receipt log |
 | `~/.cache/storage-agent.log` | Human-readable stdout/stderr from systemd and hook runs |
-## Authentik SSO Stack: k3s + Helm + Caddy
+| `s3://research-stack/agent-receipts/` | Durable S3 receipts (Garage) |
 Authentik is deployed on `cupfox` (`100.115.119.40`) inside a lightweight single-node `k3s` cluster using Helm, and integrated with the edge Caddy reverse proxies on `racknerd` (`100.80.39.40`).
 ### Node configuration (cupfox)
 - **K3s server**: Installed with `--disable traefik --disable servicelb` to conserve memory.
 - **Authentik chart**: Deployed into the `authentik` namespace with custom `authentik-values.yaml` secrets.
 - **Port forwarding**: Host port `9000` is forwarded to the `authentik-server` NodePort `30080` via `socat` systemd user service (`authentik-port-forward.service`).
 - **Firewall**: Port `9000/tcp` allowed on the Tailscale interface.
 ### Credentials & Agent Configuration
 - **API Token**: Stored securely at `/home/allaun/.config/ene/authentik.token` (`chmod 600`).
 - **Agent updates**: The Python orchestrator (`service_orchestrator.py`, `configure_vault_authentik.py`) and Rust `authentik_agent_manager` support loading the token from the file specified in `AUTHENTIK_TOKEN_FILE` env var.
 - **MCP server**: configured in `.mcp.json.full` with:
  ```json
  "env": {
    "AUTHENTIK_BASE_URL": "${AUTHENTIK_BASE:-http://100.115.119.40:9000}",
    "AUTHENTIK_TOKEN_FILE": "/home/allaun/.config/ene/authentik.token"
  }
  ```
 ### Configured Applications & Providers
 All Proxy Providers run in `forward_single` mode, with cookie domain `researchstack.info`, mapped to the embedded outpost (`2540112b-fb26-489d-92da-82ccccef8bbc`):
 | Application | Slug | External Host | Internal Backend |
 |-------------|------|---------------|------------------|
 | **Research Stack Vaultwarden** | `researchstack-vault` | `https://vault.researchstack.info` | `http://100.115.119.40:8080` |
 | **Research Stack Chat** | `research-stack-chat` | `https://chat.researchstack.info` | `http://100.85.244.73:9119` (Steam Deck) |
 | **Research Stack Auth** | `research-stack-auth` | `https://auth.researchstack.info` | `http://100.115.119.40:9000` |
 ### Caddy Integration (racknerd)
 Edge Caddy on `racknerd` intercepts traffic to protected subdomains and routes authorization checks:
 ```caddy
 forward_auth 100.115.119.40:9000 {
    uri /outpost.goauthentik.io/auth/caddy
    copy_headers Remote-User Remote-Name Remote-Email X-Authentik-Username X-Authentik-Name X-Authentik-Email
 }
 ```
 ## Fraction Rules
 All numeric thresholds are Q16_16 (UInt32, one = 0x00010000 = 65536).
 No Float arithmetic. Threshold constants defined at the top of the file.
 ### Q16_16 Fraction Types
 | Type | Description | Use Case |
 |------|-------------|----------|
 | `Q16_16` | 16.16 fixed-point | General computation |
 | `Q0_16` | 0.16 fixed-point | Values in [0, 1) |
 | `Q12_20` | 12.20 fixed-point | High precision fractions |
 | `Q20_12` | 20.12 fixed-point | Large integer + fraction |
 ### Fraction Construction Rules
 1. **Use canonical constructors only**
   ```python
   Q16_16.ofNat(n)      # for integers
   Q16_16.ofRatio(a,b)  # for rational numbers
   Q16_16.ofRawInt(x)   # for already-scaled integers
   ```
 2. **Never use `ofFloat` in compute paths**
   - Allowed only at external boundary (JSON parsing, sensor input)
   - Must be immediately bracketed: `ofFloat(x).toFixedPoint().compute()`
 ## Gauge Theory Research Program
 Gauge theory is the most rigorous framework for mapping out math because it forces explicit
 distinctions between theorems, conjectures, and empirical observations. Use it as a probe,
 not as a claim.
 ### What Gauge Theory Demands
 1. **Proven vs Conjectural**
   - If you claim a correspondence, you must prove it or label it an ansatz
   - Empirical correlations are data, not theorems
   - Gauge theory requires: "Is this a theorem or an ansatz?"
 2. **Dimensional Honesty**
   - Dimensional mismatches must be explicitly addressed, not papered over
 3. **Category/Type Correctness**
   - Frustration is boolean/Z₂
   - Wilson loop is real-valued (trace of holonomy)
   - Curvature is Lie-algebra-valued
   - Confusing these categories is a type error
 ### Recommended Framing
 Use gauge theory as a research program:
 ```
 "We investigate whether SilverSight can be derived from lattice gauge theory.
 We have proven X, observed Y empirically, and conjecture Z.
 Here are the falsification criteria."
 ```
 Never claim:
 ```
 "SilverSight IS gauge theory"
 ```
 ## Current Stack-Solidification Anchors
@ -474,15 +368,15 @@ Never claim:
 - `4-Infrastructure/shim/rrc_bosonic_tensor_gpu.py` — GPU-accelerated Bosonic Tensor Network Centrality: computes exp(-i*A*theta) using adaptive RK4 on GPU with `wgpu` (Vulkan) to scale N to 10000+ without CPU eigendecomposition bottleneck. Receipt: `rrc_bosonic_tensor_gpu_receipt.json`.
 - `4-Infrastructure/shim/rrc_bosonic_db_buffer.py` — Asynchronous database ingestion buffer: queues, batches, and flushes PostgreSQL inserts for bosonic tensor network receipts and metrics in thread-safe worker pools.
 - `4-Infrastructure/shim/pist_trace_classify_offline.py` — Offline, token-free trace classifier implementing Lean's `Semantics.PIST.Classify` color-space model and executing the local `rrc-watchdog` binary in the container.
- `4-Infrastructure/shim/lake_build_ingest.py` — Pure-I/O shim that runs `lake build <target>` and ingests the result into `ene.sessions`, `ene.packages`, `ene.receipts`, and `ene.ingest_events` on the canonical nixos-laptop Postgres (`100.102.173.61`). No admissibility logic, no Float arithmetic.
+- `4-Infrastructure/shim/lake_build_ingest.py` — Pure-I/O shim that runs `lake build <target>` and ingests the result into `ene.sessions`, `ene.packages`, `ene.receipts`, and `ene.ingest_events` on the canonical neon-64gb Postgres (`arxiv-pg` container). No admissibility logic, no Float arithmetic.
 - `4-Infrastructure/k3s-flake/tests/chat-verify.spec.ts` — E2E Playwright verification spec for Chat (Hermes) SSO login.
 - `4-Infrastructure/k3s-flake/tests/audiobookshelf-verify.spec.ts` — E2E Playwright verification spec for Audiobookshelf SSO login.
 ## Canonical database locations
- **Postgres (canonical):** PostgreSQL service on **nixos-laptop** (`100.102.173.61`). Databases: `arxiv` (arXiv papers + pgvector HNSW), `ene` (ENE memory substrate with full schema from `ene_substrate_schema.sql`).
+- **Postgres (canonical):** `arxiv-pg` podman container on **neon-64gb** (`100.92.88.64`). Databases: `arxiv` (arXiv papers + pgvector HNSW), `ene` (ENE memory substrate with full schema from `ene_substrate_schema.sql`).
 - **Gremlin (canonical):** Azure Cosmos DB endpoint in `.env.gremlin` (`mathblob.gremlin.cosmos.azure.com`). Current graph: 44,804 vertices, 29,466 edges.
- **Local qfox Postgres:** none. Do not spin up local Postgres containers on qfox for production data; they are not replicated to nixos-laptop and create confusion.
+- **Local qfox Postgres:** none. Do not spin up local Postgres containers on qfox for production data; they are not replicated to neon and create confusion.
 ## Compute Dispatch (WGSL → any substrate)
@ -549,7 +443,7 @@ blessed Compiler surface:
 - Command: `python3 "4-Infrastructure/shim/lake_build_ingest.py" Compiler --actor opencode`
 - Runs in background so `git commit` is not blocked
 - Log: `~/.cache/lake-build-ingest.log`
- Destination: `ene.sessions`, `ene.packages`, `ene.receipts`, `ene.ingest_events` on nixos-laptop (`100.102.173.61`)
+- Destination: `ene.sessions`, `ene.packages`, `ene.receipts`, `ene.ingest_events` on neon-64gb (`arxiv-pg` container)
 To reinstall the hook on a fresh clone, append the background invocation from
 `.git/hooks/post-commit` to the Git LFS post-commit hook.
--- a/4-Infrastructure/infra/ene-rds/systemd/ene-api-wrapper.sh
+++ b/4-Infrastructure/infra/ene-rds/systemd/ene-api-wrapper.sh
@ -14,7 +14,7 @@ if [[ ! -x "$BIN" ]]; then
  exit 127
 fi
-export RDS_HOST="${RDS_HOST:-100.102.173.61}"
+export RDS_HOST="${RDS_HOST:-100.92.88.64}"
 export RDS_PORT="${RDS_PORT:-5432}"
 export RDS_USER="${RDS_USER:-postgres}"
 export RDS_DB="${RDS_DB:-postgres}"
--- a/4-Infrastructure/infra/service-orchestrator/service_orchestrator.py
+++ b/4-Infrastructure/infra/service-orchestrator/service_orchestrator.py
@ -29,12 +29,6 @@ import httpx
 AUTHENTIK_BASE = os.getenv("AUTHENTIK_BASE", "http://localhost:9000")
 AUTHENTIK_TOKEN = os.getenv("AUTHENTIK_TOKEN")
 if not AUTHENTIK_TOKEN:
    token_file = os.getenv("AUTHENTIK_TOKEN_FILE")
    if token_file and os.path.exists(token_file):
        with open(token_file, "r") as f:
            AUTHENTIK_TOKEN = f.read().strip()
 CADDY_ADMIN = os.getenv("CADDY_ADMIN", "http://100.101.247.127:2019")
 CREDENTIAL_SERVER = os.getenv("CREDENTIAL_SERVER", "http://100.101.247.127:8444")
 AUTHORIZATION_FLOW = os.getenv(
--- a/4-Infrastructure/infra/vikunja_mcp.py
+++ b/4-Infrastructure/infra/vikunja_mcp.py
@ -19,7 +19,7 @@ from urllib.error import HTTPError
 SERVER_NAME = "vikunja-mcp"
 SERVER_VERSION = "0.1.0"
-VIKUNJA_URL = os.environ.get("VIKUNJA_URL", "http://100.102.173.61:3456")
+VIKUNJA_URL = os.environ.get("VIKUNJA_URL", "http://100.92.88.64:3456")
 _token_file = os.environ.get("VIKUNJA_TOKEN_FILE", "")
 VIKUNJA_TOKEN = os.environ.get("VIKUNJA_TOKEN", "")
 if not VIKUNJA_TOKEN and _token_file:
--- a/4-Infrastructure/rds_probe/src/db.rs
+++ b/4-Infrastructure/rds_probe/src/db.rs
@ -12,7 +12,7 @@ pub struct DbConfig {
 impl DbConfig {
    pub fn from_env() -> Self {
        let host = env::var("RDS_HOST")
-            .unwrap_or_else(|_| "100.102.173.61".to_string());
+            .unwrap_or_else(|_| "100.92.88.64".to_string());
        let user = env::var("RDS_USER").unwrap_or_else(|_| "postgres".to_string());
        let password = env::var("RDS_PASSWORD").unwrap_or_else(|_| "".to_string());
--- a/4-Infrastructure/shim/authentik_agent_manager/src/bin/mcp_server.rs
+++ b/4-Infrastructure/shim/authentik_agent_manager/src/bin/mcp_server.rs
@ -147,16 +147,8 @@ async fn main() -> anyhow::Result<()> {
        .with_writer(std::io::stderr)
        .init();
-    let token = if let Ok(t) = std::env::var("AUTHENTIK_TOKEN") {
+    let token = std::env::var("AUTHENTIK_TOKEN")
-        t
+        .map_err(|_| anyhow::anyhow!("AUTHENTIK_TOKEN environment variable not set"))?;
    } else if let Ok(path) = std::env::var("AUTHENTIK_TOKEN_FILE") {
        std::fs::read_to_string(path)
            .map_err(|e| anyhow::anyhow!("Failed to read AUTHENTIK_TOKEN_FILE: {}", e))?
            .trim()
            .to_string()
    } else {
        anyhow::bail!("AUTHENTIK_TOKEN or AUTHENTIK_TOKEN_FILE environment variable not set");
    };
    let base_url = std::env::var("AUTHENTIK_BASE_URL")
        .unwrap_or_else(|_| "https://researchstack.info".to_string());
--- a/4-Infrastructure/shim/authentik_agent_manager/src/main.rs
+++ b/4-Infrastructure/shim/authentik_agent_manager/src/main.rs
@ -82,7 +82,7 @@ const DEFAULT_BASE_URL: &str = "https://researchstack.info";
 struct Cli {
    /// Authentik API token (or set AUTHENTIK_TOKEN env var).
    #[arg(long)]
-    token: Option<String>,
+    token: String,
    /// Authentik base URL.
    #[arg(long, default_value = DEFAULT_BASE_URL)]
@ -143,22 +143,16 @@ enum Command {
 async fn main() -> anyhow::Result<()> {
    tracing_subscriber::fmt::init();
-    let cli = Cli::parse();
+    let mut cli = Cli::parse();
-    let mut resolved_token = cli.token.clone();
+    if cli.token.is_empty() {
    if resolved_token.is_none() {
        if let Ok(t) = std::env::var("AUTHENTIK_TOKEN") {
-            resolved_token = Some(t);
+            cli.token = t;
        } else if let Ok(path) = std::env::var("AUTHENTIK_TOKEN_FILE") {
            if let Ok(t) = std::fs::read_to_string(path) {
                resolved_token = Some(t.trim().to_string());
            }
        }
    }
-    let token = match resolved_token {
+    if cli.token.is_empty() {
-        Some(t) => t,
+        anyhow::bail!("Set --token or AUTHENTIK_TOKEN environment variable");
-        None => anyhow::bail!("Set --token, AUTHENTIK_TOKEN, or AUTHENTIK_TOKEN_FILE environment variable"),
+    }
-    };
+    let client = authentik::Client::new(&cli.base_url, &cli.token);
    let client = authentik::Client::new(&cli.base_url, &token);
    match cli.cmd {
        Command::Execute { plan } => {
--- a/4-Infrastructure/shim/batch_embed_artifacts.py
+++ b/4-Infrastructure/shim/batch_embed_artifacts.py
@ -19,7 +19,7 @@ from shim.utils import sha256_text, utc_now
 BATCH_SIZE = 50
 TOKEN_REFRESH_SEC = 600
-HOST = os.environ.get("RDS_HOST", "100.102.173.61")
+HOST = os.environ.get("RDS_HOST", "100.92.88.64")
 PORT = int(os.environ.get("RDS_PORT", "5432"))
 USER = os.environ.get("RDS_USER", "postgres")
 DB = os.environ.get("RDS_DB", os.environ.get("RDS_DBNAME", "postgres"))
--- a/4-Infrastructure/shim/chentsov_fusion.py
+++ b/4-Infrastructure/shim/chentsov_fusion.py
@ -50,7 +50,7 @@ ENDPOINTS = {
        "temperature": 0.1,
    },
    "neon-qwen": {
-        "url": "http://100.102.173.61:11434/v1/chat/completions",
+        "url": "http://100.92.88.64:11434/v1/chat/completions",
        "model": "hf.co/llmfan46/Qwen3.6-35B-A3B-uncensored-heretic-GGUF:Q4_K_M",
        "name": "Qwen3.6-35B-A3B (neon, CPU)",
        "timeout": 3600,
@ -58,7 +58,7 @@ ENDPOINTS = {
        "temperature": 0.1,
    },
    "neon-step": {
-        "url": "http://100.102.173.61:11434/v1/chat/completions",
+        "url": "http://100.92.88.64:11434/v1/chat/completions",
        "model": "step3.7-flash",
        "name": "Step-3.7-Flash (neon, CPU)",
        "timeout": 3600,
@ -68,7 +68,7 @@ ENDPOINTS = {
    # DeepSeek-Prover-V2-7B: purpose-built Lean 4 / math proof model (~4-5 GB Q4_K_M).
    # Best for hard construction sorries; trained on Lean proof search data.
    "neon-deepseek": {
-        "url": "http://100.102.173.61:11434/v1/chat/completions",
+        "url": "http://100.92.88.64:11434/v1/chat/completions",
        "model": "hf.co/irmma/DeepSeek-Prover-V2-7B-Q4_K_M-GGUF:latest",
        "name": "DeepSeek-Prover-V2-7B (neon, CPU)",
        "timeout": 3600,
--- a/4-Infrastructure/shim/configure_vault_authentik.py
+++ b/4-Infrastructure/shim/configure_vault_authentik.py
@ -4,18 +4,10 @@ import requests
 import json
 import sys
-TOKEN = os.environ.get("AUTHENTIK_TOKEN")
+TOKEN = os.environ.get("AUTHENTIK_TOKEN", "sLYSgzOsIO0elCJXVtpkYkTDtnkkIoGnu10CdbQxjQa6F7EO3QsRbZC3Pf0Z")
 if not TOKEN:
    token_file = os.environ.get("AUTHENTIK_TOKEN_FILE")
    if token_file and os.path.exists(token_file):
        with open(token_file, "r") as f:
            TOKEN = f.read().strip()
 if not TOKEN:
    TOKEN = "sLYSgzOsIO0elCJXVtpkYkTDtnkkIoGnu10CdbQxjQa6F7EO3QsRbZC3Pf0Z"
 BASE_URL = "https://auth.researchstack.info"
 OUTPOST_UUID = "1ceb9880-517e-4fe6-acb8-ecc1c8276bf4"
 headers = {
    "Authorization": f"Bearer {TOKEN}",
    "Content-Type": "application/json",
--- a/4-Infrastructure/shim/dataset_ingest_rds.py
+++ b/4-Infrastructure/shim/dataset_ingest_rds.py
@ -34,7 +34,7 @@ logging.basicConfig(level=logging.INFO, format="%(asctime)s %(levelname)s %(mess
 log = logging.getLogger("dataset_ingest_rds")
 # Config
-RDS_HOST = os.environ.get("RDS_HOST", "100.102.173.61")
+RDS_HOST = os.environ.get("RDS_HOST", "100.92.88.64")
 STACK_ROOT = Path(os.environ.get("STACK_ROOT", "/home/researcher/stack"))
 DATA_DIR = STACK_ROOT / "shared-data" / "data" / "ingested_datasets" / "2026-05-18"
--- a/4-Infrastructure/shim/gccl_transfer_pipeline.py
+++ b/4-Infrastructure/shim/gccl_transfer_pipeline.py
@ -30,7 +30,7 @@ except ImportError:
    sys.path.insert(0, os.getcwd())
    import gccl_waveprobe as gw
-DEFAULT_TARGET_HOST = "100.102.173.61"  # neon-64gb IP
+DEFAULT_TARGET_HOST = "100.92.88.64"  # neon-64gb IP
 # ── Manifest Generation ─────────────────────────────────────────────────────
--- a/4-Infrastructure/shim/gremlin_lean_report.py
+++ b/4-Infrastructure/shim/gremlin_lean_report.py
@ -215,12 +215,12 @@ def emit_markdown(report: dict, out_path: Path) -> None:
 def push_to_appflowy(report: dict) -> None:
    """Push top modules to AppFloyo Cloud workspace."""
-    url = os.environ.get("APPFLOWY_URL", "http://100.102.173.61:8000")
+    url = os.environ.get("APPFLOWY_URL", "http://100.92.88.64:8000")
    token = os.environ.get("APPFLOWY_TOKEN", "")
    # If no token, try to get one from GoTrue
    if not token:
-        gotrue_url = os.environ.get("GOTRUE_URL", "http://100.102.173.61:9999")
+        gotrue_url = os.environ.get("GOTRUE_URL", "http://100.92.88.64:9999")
        email = os.environ.get("GOTRUE_ADMIN_EMAIL", "admin@researchstack.info")
        password = os.environ.get("GOTRUE_ADMIN_PASSWORD", "admin123")
        try:
--- a/4-Infrastructure/shim/lake_build_ingest.py
+++ b/4-Infrastructure/shim/lake_build_ingest.py
@ -9,7 +9,7 @@ lake_build_ingest.py — Run `lake build` and ingest the result into ENE on neon
 This is a pure-I/O shim: it runs the build, parses the output, and writes rows to
 Postgres. It contains no admissibility logic and no Float arithmetic.
-Target database: arxiv-pg container on neon-64gb (Tailscale 100.102.173.61).
+Target database: arxiv-pg container on neon-64gb (Tailscale 100.92.88.64).
 Tables used:
  ene.sessions     — one row per build invocation
  ene.packages     — one row per build target/receipt
@ -46,7 +46,7 @@ from typing import Any
 ROOT = Path("/home/allaun/Research Stack")
 LEAN_DIR = ROOT / "0-Core-Formalism/lean/Semantics"
-NEON_HOST = "100.102.173.61"
+NEON_HOST = "100.92.88.64"
 CONTAINER = "arxiv-pg"
 DB = "ene"
 PIST_CLASSIFY = LEAN_DIR / ".lake" / "build" / "bin" / "pist-classify-trace"
--- a/4-Infrastructure/shim/rds_connect.py
+++ b/4-Infrastructure/shim/rds_connect.py
@ -28,7 +28,7 @@ def _resolve_params() -> dict:
                        params["sslmode"] = v
        return params
-    host = os.environ.get("RDS_HOST", os.environ.get("PGHOST", "100.102.173.61"))
+    host = os.environ.get("RDS_HOST", os.environ.get("PGHOST", "100.92.88.64"))
    port = int(os.environ.get("RDS_PORT", os.environ.get("PGPORT", "5432")))
    user = os.environ.get("RDS_USER", os.environ.get("PGUSER", "postgres"))
    dbname = os.environ.get("RDS_DB", os.environ.get("RDS_DBNAME", os.environ.get("PGDATABASE", "postgres")))
--- a/4-Infrastructure/shim/sync_wiki_to_rds.py
+++ b/4-Infrastructure/shim/sync_wiki_to_rds.py
@ -17,7 +17,7 @@ from shim.utils import sha256_text, utc_now
 STACK_ROOT = Path(os.environ.get("STACK_ROOT", "/home/allaun/Research Stack"))
 WIKI_ROOT = Path(os.environ.get("WIKI_ROOT", str(STACK_ROOT / "6-Documentation" / "wiki")))
-HOST = os.environ.get("RDS_HOST", "100.102.173.61")
+HOST = os.environ.get("RDS_HOST", "100.92.88.64")
 DB = os.environ.get("RDS_DB", os.environ.get("RDS_DBNAME", "postgres"))
--- a/4-Infrastructure/storage/cache-offload.sh
+++ b/4-Infrastructure/storage/cache-offload.sh
@ -32,7 +32,7 @@ TIER0_PGDUMP="/mnt/stackcache/pgdump"
 TIER2_REMOTE="gdrive:research-stack-offload"
 TIER1_THRESHOLD_GB=2
-RDS_HOST="${RDS_HOST:-100.102.173.61}"
+RDS_HOST="${RDS_HOST:-100.92.88.64}"
 RDS_PORT="${RDS_PORT:-5432}"
 RDS_USER="${RDS_USER:-postgres}"
 RDS_DB="${RDS_DB:-postgres}"
--- a/4-Infrastructure/storage/garage/db-consolidate.sh
+++ b/4-Infrastructure/storage/garage/db-consolidate.sh
@ -39,7 +39,7 @@ export AWS_ACCESS_KEY_ID AWS_SECRET_ACCESS_KEY
 export AWS_DEFAULT_REGION="${AWS_DEFAULT_REGION:-garage}"
 export AWS_ENDPOINT_URL="${AWS_ENDPOINT_URL:-http://localhost:3900}"
-RDS_HOST="${RDS_HOST:-100.102.173.61}"
+RDS_HOST="${RDS_HOST:-100.92.88.64}"
 RDS_PORT="${RDS_PORT:-5432}"
 RDS_USER="${RDS_USER:-postgres}"
 RDS_DB="${RDS_DB:-postgres}"
--- a/4-Infrastructure/storage/restic/backup.sh
+++ b/4-Infrastructure/storage/restic/backup.sh
@ -38,7 +38,7 @@ fi
 export AWS_ACCESS_KEY_ID AWS_SECRET_ACCESS_KEY AWS_DEFAULT_REGION
 export RESTIC_REPOSITORY RESTIC_PASSWORD_FILE
-RDS_HOST="${RDS_HOST:-100.102.173.61}"
+RDS_HOST="${RDS_HOST:-100.92.88.64}"
 RDS_PORT="${RDS_PORT:-5432}"
 RDS_USER="${RDS_USER:-postgres}"
 RDS_DB="${RDS_DB:-postgres}"
--- a/5-Applications/tools-scripts/llm/deepseek_v4_flash_lean_harness.py
+++ b/5-Applications/tools-scripts/llm/deepseek_v4_flash_lean_harness.py
@ -84,13 +84,13 @@ PROVIDERS: dict[str, dict] = {
        "notes": "OpenRouter, deepseek-v4-flash",
    },
    "neon-deepseek-prover": {
-        "api_base": "http://100.102.173.61:11434/v1",
+        "api_base": "http://100.92.88.64:11434/v1",
        "api_key": "",
        "model": "hf.co/irmma/DeepSeek-Prover-V2-7B-Q4_K_M-GGUF",
        "notes": "neon-64gb, DeepSeek-Prover-V2 7B Q4_K_M, 62GB RAM CPU-only",
    },
    "neon-goedel-prover": {
-        "api_base": "http://100.102.173.61:11434/v1",
+        "api_base": "http://100.92.88.64:11434/v1",
        "api_key": "",
        "model": "hf.co/mradermacher/Goedel-Prover-V2-8B-GGUF",
        "notes": "neon-64gb, Goedel-Prover-V2 8B GGUF, 62GB RAM CPU-only",
--- a/5-Applications/tools-scripts/mcp/cloud_bootstrap.sh
+++ b/5-Applications/tools-scripts/mcp/cloud_bootstrap.sh
@ -5,7 +5,7 @@
 #
 # Environment variables (set these in cloud env config):
 #   BUILD_SERVER_URL=http://100.88.57.96:8765
-#   NEON_OLLAMA_URL=http://100.102.173.61:11434
+#   NEON_OLLAMA_URL=http://100.92.88.64:11434
 #   LAKE_WORKDIR=/workspace/0-Core-Formalism/lean/Semantics
 set -e
@ -54,7 +54,7 @@ try:
    print('  build_server: UP')
 except: print('  build_server: DOWN (tailnet required)')
 try:
-    r = urllib.request.urlopen('${NEON_OLLAMA_URL:-http://100.102.173.61:11434}/api/tags', timeout=5)
+    r = urllib.request.urlopen('${NEON_OLLAMA_URL:-http://100.92.88.64:11434}/api/tags', timeout=5)
    print('  neon_ollama:   UP')
 except: print('  neon_ollama:   DOWN (tailnet required)')
 "
--- a/5-Applications/tools-scripts/mcp/token_saver_mcp.py
+++ b/5-Applications/tools-scripts/mcp/token_saver_mcp.py
@ -50,7 +50,7 @@ def _ensure_singleton() -> None:
 # ── Resource URLs (configurable via env) ────────────────────────────────
 BUILD_SERVER = os.environ.get("BUILD_SERVER_URL", "http://100.88.57.96:8765")
-NEON_OLLAMA   = os.environ.get("NEON_OLLAMA_URL", "http://100.102.173.61:11434")
+NEON_OLLAMA   = os.environ.get("NEON_OLLAMA_URL", "http://100.92.88.64:11434")
 NEON_MODEL    = os.environ.get("NEON_MODEL",
    "hf.co/irmma/DeepSeek-Prover-V2-7B-Q4_K_M-GGUF")
 LAKE_WORKDIR  = os.environ.get("LAKE_WORKDIR",
--- a/AGENTS.md
+++ b/AGENTS.md
@ -58,38 +58,6 @@ fully-local Hermes-3 model on qfox-1's RTX 4070. OpenClaw is decommissioned.
    api_key: "sk-local"
  ```
 ## Provider-nixos LLM Gateway (2026-07-03)
 `neon-rs1000` (Tailscale `100.79.14.103`, NixOS, 4 cores, 7.8Gi RAM) runs the
 FreeLLMAPI proxy + OpenCode server as the model inference gateway for the
 onklaud-5 pipeline.
 ### FreeLLMAPI (port 3001)
 - **Repo**: `tashfeenahmed/freellmapi`, cloned to `~/freellmapi`, production build
 - **Dashboard**: `http://100.79.14.103:3001` — admin: `admin@researchstack.info` / `admin123`
 - **Unified API key**: `freellmapi-ef5610fa456735f2bcb6205faf03f8725fe41265f129cd56`
 - **Base URL**: `http://100.79.14.103:3001/v1`
 - **Systemd user unit**: `freellmapi.service` — enabled, auto-restart
 - **20 provider keys installed** (Google, Groq, Cerebras, NVIDIA, Mistral, OpenRouter,
  GitHub, Cloudflare, Zhipu, Ollama Cloud, HuggingFace, OpenCode Zen, Kilo,
  Pollinations, OVH, LLM7, AI Horde, Agnes, Reka, SiliconFlow, Routeway, BazaarLink)
 - **~1.7B tokens/month aggregate**, 6.1K used (~99.99% remaining)
 ### OpenCode Server (port 4096)
 - **Version**: 1.17.9, installed via `nix profile install nixpkgs#opencode`
 - **Systemd user unit**: `opencode-serve.service` — enabled, auto-restart
 - **Provider**: FreeLLMAPI via `@ai-sdk/openai-compatible` (model: `freeapi/auto`)
 - **Config**: `~/.config/opencode/config.json`
 ### Onklaud-5 Pipeline
 - **Path**: `~/onklaud-5`
 - **council.py**: Patched to route through FreeLLMAPI (`localhost:3001/v1`) instead of
  OpenRouter directly. Both `KIMI_MODEL` and `GLM_MODEL` set to `auto`.
 - **Venv**: `~/onklaud-5/venv`, 31/32 tests pass
 ### Common failure modes
 - `500 Internal Error` from `chat.researchstack.info` after a model swap:
@ -123,11 +91,18 @@ workstation.
  failures and writes corrections to AGENTS.md. Requires `claude` CLI available
  for the analysis LLM.
-### DECOMMISSIONED — Neon proxy (2026-06-19)
+### Neon proxy (2026-06-19)
-[INACTIVE / DECOMMISSIONED] Headroom proxy previously ran on neon-64gb:
+Headroom proxy also runs on neon-64gb (netcup ARM64, NixOS) for remote agent
- **Tailscale endpoint**: `http://100.92.88.64:8787` (inactive)
+sessions:
- **Status**: Decommissioned. All remote/local LLM sessions route directly through qfox-1 or external providers. Do not route ANTHROPIC_BASE_URL to neon.
+
 - **Tailscale endpoint**: `http://100.92.88.64:8787` (also reachable as
  `http://neon-64gb:8787` via MagicDNS)
 - **Startup**: `/home/allaun/.headroom/headroom-proxy-start.sh` (wraps
  `LD_LIBRARY_PATH` for NixOS libstdc++ compatibility)
 - **Installed via**: Python venv at `~/headroom-venv/`
 - **Config**: `--memory --learn --port 8787 --host 0.0.0.0`
 - **Route through it**: `ANTHROPIC_BASE_URL=http://100.92.88.64:8787 claude`
 ### Common failure modes
@ -457,114 +432,6 @@ For files using PhysicsScalar.Q16_16:
 ### Migration Guide
 See `LEAD_Q16_16_MIGRATION_GUIDE.md` for detailed microsteps.
 ## Gauge Theory Research Program
 Gauge theory is the most rigorous framework for mapping out math because it forces explicit
 distinctions between theorems, conjectures, and empirical observations. Use it as a probe,
 not as a claim.
 ### What Gauge Theory Demands
 1. **Proven vs Conjectural**
   - If you claim a correspondence, you must prove it or label it an ansatz
   - Empirical correlations (r=0.41, r=-0.33, n=13, p>0.05) are data, not theorems
   - Gauge theory requires: "Is this a theorem or an ansatz?"
 2. **Dimensional Honesty**
   - AT model is 2D; gauge confinement requires 3+1D (or 2+1D for compact U(1))
   - Confinement in 2D gauge theory is trivial — this is a theorem
   - Dimensional mismatches must be explicitly addressed, not papered over
 3. **Category/Type Correctness**
   - Frustration is boolean/Z₂
   - Wilson loop is real-valued (trace of holonomy)
   - Curvature is Lie-algebra-valued
   - Confusing these categories is a type error
 ### What Gauge Theory Does NOT Give You
 1. **Derivation for Free** — The Baker-Hopf coupling is an ansatz, not derived from gauge principles
 2. **Uniqueness** — Other connections (arctan, Li₂, etc.) could satisfy similar constraints
 3. **Predictive Power** — Correlations computed because the hypothesis suggested them
 ### Success Criteria
 Success is NOT "SilverSight IS gauge theory."
 Success IS: "We attempted to derive SilverSight structures from gauge theory.
 We succeeded for X, failed for Y, and learned Z."
 Specifically:
 - **Attempt derivation for Baker-Hopf coupling** — proves it's gauge-theoretic or reveals it's something else
 - **Attempt derivation for frustration = Wilson loop** — proves the correspondence or reveals it's just a correlation
 - **Attempt derivation for Baker Λ = field strength** — proves the formal resemblance or reveals it's just a resemblance
 ### Failure Mode
 Failure is NOT "correspondences don't hold."
 Failure IS: "We didn't attempt the derivation, so we don't know what the structures actually are."
 ### Recommended Framing
 Use gauge theory as a research program:
 ```
 "We investigate whether SilverSight can be derived from lattice gauge theory.
 We have proven X, observed Y empirically, and conjecture Z.
 Here are the falsification criteria."
 ```
 Never claim:
 ```
 "SilverSight IS gauge theory"
 ```
 ## Fraction Rules
 The Research Stack operates on fixed-point arithmetic for mathematical rigor.
 Float (`ofFloat`) is forbidden in compute paths.
 ### Q16_16 Fraction Types
 | Type | Description | Use Case |
 |------|-------------|----------|
 | `Q16_16` | 16.16 fixed-point | General computation |
 | `Q0_16` | 0.16 fixed-point | Values in [0, 1) |
 | `Q12_20` | 12.20 fixed-point | High precision fractions |
 | `Q20_12` | 20.12 fixed-point | Large integer + fraction |
 ### Fraction Construction Rules
 1. **Use canonical constructors only**
   ```lean
   Q16_16.ofNat n      -- for integers
   Q16_16.ofRatio a b  -- for rational numbers
   Q16_16.ofRawInt x   -- for already-scaled integers
   ```
 2. **Never use `ofFloat` in compute paths**
   - Allowed only at external boundary (JSON parsing, sensor input)
   - Must be immediately bracketed: `ofFloat x |> toFixedPoint |> compute`
 3. **Bridge pattern for legacy code**
   ```lean
   import Semantics.PhysicsScalarBridge
   -- Use PhysicsScalarBridge.add, .gt, etc.
   -- Constants: PhysicsScalarBridge.one, .two, .three, .half, .quarter
   ```
 ### Fraction Comparison Pattern
 ```lean
 -- WRONG: direct comparison with Float
 if x > 0.5 then ...
 -- RIGHT: fixed-point comparison
 if x > Q16_16.half then ...
 ```
 ## Glossary (before reading further)
 These terms appear throughout all AGENTS.md files and the codebase:
--- a/atlas.json
+++ b/atlas.json
@ -1,11 +0,0 @@
 {
  "project_id": "b4390de5-14d9-46dc-8be7-9bb36291e0b4",
  "auto": {
    "enabled": true,
    "log": true,
    "web": "prefer_atlas",
    "capture": "suggest"
  },
  "privacy": "private",
  "source_ids": []
 }
--- a/shared-data/precomputed-math-data
+++ b/shared-data/precomputed-math-data
@ -1 +0,0 @@
 Subproject commit cf28838be713b7c93942be80382b43d3b81da898
		`@ -1 +0,0 @@`
			`Subproject commit cf28838be713b7c93942be80382b43d3b81da898`