diff --git a/.cursorrules b/.cursorrules
index d1e7c8b6..27730822 100644
--- a/.cursorrules
+++ b/.cursorrules
@@ -18,12 +18,13 @@ v0.4.74
 
 ## Research Stack — Current Project State (2026-05-28)
 
-**Build:** `lake build` — 3571 jobs, 0 errors
+**Build:** `lake build` — 3573 jobs, 0 errors (reverified 2026-06-15)
 **Python tests:** 68/68 pass
-**Sorry inventory:** 8 total (all with `TODO(lean-port)` documentation)
+**Sorry inventory:** 20 total (all with `TODO(lean-port)` documentation)
   - `AdjugateMatrix`: 3 sorries
   - `FourPrimitiveErdosRenyi`: 4 sorries
   - `HyperbolicStateSurface`: 1 sorry
+  - `E8Sidon`: 12 sorries (Eisenstein/Sidon, blocked on Mathlib valence formula)
 
 ### Key Architecture Decisions
 - **Q16_16 fixed-point arithmetic** throughout — no Float in hot paths (AGENTS.md §1.4 compliant)
@@ -32,7 +33,8 @@ v0.4.74
 - **Golden ratio unit separation** formalized in Lean
 
 ### New Lean Modules
-`AdjugateMatrix`, `OptimizedRoute`, `GoldenRatioSeparation`, `BraidBitwiseODE`
+`AdjugateMatrix`, `OptimizedRoute`, `GoldenRatioSeparation`, `BraidBitwiseODE`,
+`E8Sidon`, `FixedPointBoundary`
 
 ### New Python Modules
 `qubo_highs.py`, `alphaproof_loop.py`, `scale_space_solver.py`
diff --git a/0-Core-Formalism/lean/Semantics/AGENTS.md b/0-Core-Formalism/lean/Semantics/AGENTS.md
index 441baed0..9a3b4b99 100644
--- a/0-Core-Formalism/lean/Semantics/AGENTS.md
+++ b/0-Core-Formalism/lean/Semantics/AGENTS.md
@@ -113,6 +113,44 @@ Full workspace: **3573 jobs, 0 errors** (`lake build`, reverified 2026-06-15).
 PistSimulation: **3309 jobs, 0 errors** (`lake build Semantics.PistSimulation`, commit `778b78d3`, reverified 2026-05-27).
 EmergencyBoot: **3302 jobs, 0 errors** (`lake build Semantics.Hardware.EmergencyBootTypes Semantics.Hardware.EmergencyBootState Semantics.Hardware.EmergencyBootShell`, reverified 2026-05-27).
 
+### Float-Free FixedPoint Architecture (as of 2026-06-15)
+
+`FixedPoint.lean` (968 lines) is now fully Float-free. Core compute functions
+use integer-only algorithms:
+
+| Function | Algorithm | Location |
+|----------|-----------|----------|
+| `natLog2` | Fuel-based bit-shift loop (64 steps) | `FixedPoint.lean:30` |
+| `intSqrt` | Integer Newton's method (64 iterations) | `FixedPoint.lean:43` |
+| `Q16_16.sqrt` | `intSqrt(q.raw * 65536)` | `FixedPoint.lean:316` |
+| `Q16_16.log2` | Bit extraction + linear interpolation (94548 = 1/ln2 in Q16.16) | `FixedPoint.lean:324` |
+| `Q16_16.expNeg` | 7-segment piecewise-linear, max error ~0.02 | `FixedPoint.lean:336` |
+| `Q0_16.log2` | Bit extraction (47274 = 1/ln2 in Q0.16) | `FixedPoint.lean:130` |
+
+Removed from core: `ofFloat`, `toFloat`, `ln`, `pow`, `sin`, `log` (Q16_16);
+`toFloat`, `ofFloat` (Q0_16); `q0_64ScaleFloat`, `ofFloat`, `toFloat` (Q0_64).
+
+`FixedPointBoundary.lean` (89 lines) quarantines Float conversions at the I/O
+boundary. 14 downstream files import it for display/JSON purposes:
+`FuzzyAssociation`, `Autobalance`, `ProvenanceSource`, `Tape`,
+`Q16_16Numerics`, `CGAVersorAddress`, `EfficiencyAnalysis`,
+`Functions/BracketedCalculus`, `LocalDerivative`, `NUVMATH`, `QFactor`,
+`SLUG3`, `SubagentOrchestrator`, `ExtensionScaffold/Compression/SignalPolicy`,
+`LawfulLoss`.
+
+### E8Sidon Module (as of 2026-06-15)
+
+`E8Sidon.lean` (438 lines) formalizes the Eisenstein coefficient identity
+and Sidon set infrastructure:
+
+- `sigma3`, `sigma7`, `convolutionLHS` — divisor sum definitions with 13 `#eval` witnesses
+- `bernoulli_four`, `bernoulli_eight` — B4 = B8 = -1/30 via `native_decide`
+- `E4_normalization`, `E8_normalization` — -(2k/Bk) = 240, 480
+- `E4_sq_eq_E8_coeff` — theorem (1 sorry, blocked on Mathlib valence formula)
+- `IsSidonSet`, `sidon8` (card=8), Sidon energy bounds, greedy extraction
+- 12 sorries total, all with `TODO(lean-port)` + proof sketches
+- 1 axiom (`e8_additive_completeness`) — open problem in additive combinatorics
+
 ### BraidDiatCodec — chirality/MMR/braid residual codec
 
 New codec module (`Semantics.BraidDiatCodec`) layers the mountains-on-mountain stack into a compact binary format:
@@ -273,7 +311,9 @@ after narrowly compiling the file under a scratch target.
 - `Q16_16` is a Subtype `{ x : Int // q16MinRaw ≤ x ∧ x ≤ q16MaxRaw }`.
   Safe constructors: `Q16_16.ofRawInt (n : Int)`, `Q16_16.ofBits (u : UInt32)`,
   `Q16_16.ofNat`, `Q16_16.ofRatio`. No struct literals `{ val := N }`.
-- `Q0_16` has `add`/`sub` (no `addSat`/`subSat`).
+  Float constructors (`ofFloat`/`toFloat`) are only in `FixedPointBoundary.lean`.
+- `Q0_16` has `add`/`sub` (no `addSat`/`subSat`). `log2` is integer-only
+  (bit extraction). Float conversions are in `FixedPointBoundary.lean`.
 - `List.get?` does not exist — use `list[i]?` subscript syntax.
 - `liftMetaM` is the correct combinator for `MetaM → TacticM` in `mapM`.
 - `MVarId.toNat` does not exist — use `g.name.toString`.