diff --git a/.gitignore b/.gitignore
index fb56da5..076ae53 100644
--- a/.gitignore
+++ b/.gitignore
@@ -5,3 +5,4 @@ __pycache__/
 dist/
 build/
 .venv/
+freellmapi-setup/
diff --git a/AGENTS.md b/AGENTS.md
index 80094d3..ab16fe7 100644
--- a/AGENTS.md
+++ b/AGENTS.md
@@ -13,8 +13,9 @@ for Adleman/Lipton-style DNA computing.  The Φ mapping has 4 layers:
 ## Ground Rules
 
 - **Decision logic is in Lean** — BioSight shims are Python I/O only.
-  If any logic here starts making admissibility or routing decisions,
-  port it to SilverSight's `Semantics.RRC.*` modules.
+  Any Python path making an admissibility or routing decision without a
+  SilverSight receipt is **drift**. File it immediately as a pending
+  SilverSight gate.
 - **No floats in compute paths** — `phi.charclass` and `phi.embed`
   use integer arithmetic for all core encoding.  Only `phi.output`
   uses math.acos (for Fisher distance in Adleman graph building).
@@ -23,6 +24,39 @@ for Adleman/Lipton-style DNA computing.  The Φ mapping has 4 layers:
 - **Reproducibility** — two invocations on the same equation must
   produce identical DNA sequences (deterministic byte-class and
   AST order).
+- **Rotation trigger** — any time `phi.consistency` makes an
+  ADMIT/QUARANTINE call, check whether a SilverSight receipt backs it.
+  If not, that check is the next SilverSight gate to formalize.
+- **τ/δ mirror rule** — the Lean proof structure for any gate must
+  mirror BioSight's τ (topology) and δ (depth) values for that equation.
+  High δ → WF-recursive Lean definitions. High τ diversity → wider
+  typeclass hierarchy in SilverSight.
+
+## Anti-Drift Multi-Pass
+
+Every decision — no matter how minor — must survive all four passes:
+
+| Pass | Layer | Authority |
+|------|-------|-----------|
+| 1 | Python (`phi.*`) | I/O encoding only — no decisions |
+| 2 | Lean (SilverSight gate) | Formal authority — closes the decision |
+| 3 | RRC pipeline (`rigour_pipeline.py`) | Cross-repo alignment |
+| 4 | Research Stack (`~/Research Stack`, read-only) | Regression oracle |
+
+**Session start:** run `python3 -m py_compile phi/*.py equation_dna_encoder.py` and
+confirm phi.encode is deterministic before any new encoding work.
+
+## N=8 Root Dependency
+
+BioSight's entire 8-base alphabet choice depends on the SilverSight theorem:
+
+```
+N = 8 = min { N : Nyquist(N) ∧ Q16_16(N) ∧ DNA-subset(N) }
+```
+
+Target: `formal/SilverSight/HachimojiN8.lean` in the SilverSight repo.
+Until that theorem is closed with zero sorrys, the alphabet choice is
+documented justification only, not formal proof.
 
 ## Core Modules
 
@@ -67,6 +101,13 @@ python3 -c "import phi; print(phi.encode_phi('x + 1 = 2'))"
 
 ## SilverSight Relationship
 
-BioSight is the DNA-computing branch of the Research Stack ecosystem.
+BioSight is the first domain instance of the SilverSight framework.
 SilverSight (`/home/allaun/SilverSight`) owns all formal Lean logic.
-If BioSight needs a new theorem or receipt, it requests it from SilverSight.
+
+- BioSight **imports** SilverSight receipts; it never contains formal proofs.
+- BioSight **feeds** (τ, δ) distributions back to SilverSight as the work queue
+  for new gates (high-δ equations → WF-recursive gate; high-τ → wider typeclass).
+- If BioSight needs a new theorem or receipt, open a pending gate entry in
+  `dag/graph.md` and implement the gate in `formal/SilverSight/` first.
+- `~/Research\ Stack` is read-only archive — consult it only as a regression
+  oracle; never reference it as an active dependency.
diff --git a/python/phi/test_verified_units.py b/python/phi/test_verified_units.py
index 9d3c847..44b3969 100644
--- a/python/phi/test_verified_units.py
+++ b/python/phi/test_verified_units.py
@@ -8,23 +8,56 @@ sys.path.insert(0, os.path.dirname(os.path.dirname(os.path.abspath(__file__))))
 from phi.charclass import classify_char
 from phi.consistency import check_consistency
 
-# Helper functions for Q16_16 math in Python matching Lean's FixedPoint behavior
+# Helper functions for Q16_16 math in Python matching Lean's FixedPoint behavior.
+#
+# V4 MITIGATION — Lean 4 Int.div uses EUCLIDEAN division:
+#   - The remainder is always non-negative: a = q*b + r, r >= 0
+#   - For POSITIVE divisor: ediv == Python's // (floor division)
+#   - For NEGATIVE divisor: ediv != Python's //
+#     Example: Lean:   65536 / (-3) = -21845  (rem 1)
+#              Python: 65536 // (-3) = -21846  (rem -2, floor)
+#
+# Since q16_mul always divides by 65536 (positive), Python's // is safe there.
+# q16_div divides by an arbitrary b which may be negative, so we use _ediv.
+
+def _ediv(a, b):
+    """Euclidean division matching Lean 4's Int.div.
+    Guarantees: a = _ediv(a,b)*b + _emod(a,b) and _emod(a,b) >= 0."""
+    if b == 0:
+        return 0
+    # Python's divmod gives floor division (q, r) with r same sign as b.
+    # Euclidean requires r >= 0 always.
+    q, r = divmod(a, b)
+    if r < 0:
+        # This happens when b < 0 (Python's divmod gives r with sign of b)
+        q += 1
+        # r -= b  (but we don't need r for the return)
+    return q
+
 def q16_mul(a, b):
+    # Divisor is always 65536 (positive), so Python // matches Lean ediv.
     return (a * b) // 65536
 
 def q16_div(a, b):
-    return (a * 65536) // b
+    if b == 0:
+        return 2147483647  # Q16_16 infinity sentinel
+    # b may be negative, so we must use Euclidean division.
+    return _ediv(a * 65536, b)
 
 def int_sqrt(n):
+    """Integer square root via Newton's method (floor(√n)).
+    Uses floor division intentionally here because we want floor(√n),
+    not truncation — the Newton iteration converges correctly with
+    floor division on non-negative integers."""
     if n < 0:
         raise ValueError("Square root of negative number")
     if n == 0:
         return 0
     x = n
-    y = (x + 1) // 2
+    y = (x + 1) // 2  # floor div is correct here (n ≥ 0)
     while y < x:
         x = y
-        y = (x + n // x) // 2
+        y = (x + n // x) // 2  # floor div is correct here (both operands ≥ 0)
     return x
 
 def q16_sqrt(q_raw):