diff --git a/LEAN_MIGRATION.md b/LEAN_MIGRATION.md
index fee90d8..9f99323 100644
--- a/LEAN_MIGRATION.md
+++ b/LEAN_MIGRATION.md
@@ -81,3 +81,35 @@ validate phase by phase.
 - [x] Phase 5
 - [x] Phase 6
 - [x] Phase 7
+
+All phases complete: `lake build` is green with zero warnings, zero `sorry`s
+and zero axioms, and `lake exe spa` prints output **byte-for-byte identical**
+to the compiled Agda `Main` (verified with `diff`). Per-file `Agda ↦ Lean`
+correspondence tables live in the header comment of each Lean file.
+
+## Wins from the migration
+
+- The four monotonicity **postulates** in `Analysis/Sign.agda` and
+  `Analysis/Constant.agda` are now proved theorems (via
+  `AboveBelow.le_cases`), so the Lean development is postulate-free.
+- ~2200 lines of map machinery (`Lattice/Map.agda`, `Lattice/MapSet.agda`,
+  much of `Lattice/FiniteMap.agda`) collapse into the spine-pinned
+  `FiniteMap` + `Finset`; the `IterProd` isomorphism no longer needs
+  `Unique ks` (the representation is canonical).
+- `Equivalence.agda`, `Chain.agda`, the `IsSemilattice`/`IsLattice`
+  hierarchy, and most of `Utils.agda` lift into mathlib.
+
+## Deviations & deferred items
+
+- `Lattice/Builder.agda`: not ported (nothing in the repo imports it).
+- `Lattice/ExtendBelow.agda`, `Lattice/Nat.agda`: not ported (unused by the
+  pipeline; `Nat`'s lattice is mathlib's, `ExtendBelow` would be `WithBot` +
+  a small height proof). Say the word if you want them for parity.
+- `Program.vars` lists variables in **sorted** order (`Finset.sort`, since
+  `Finset.toList` is noncomputable). For the test program this coincides
+  with the Agda MapSet order.
+- Chains are mathlib `LTSeries`, so chain-manipulating proofs
+  (`Prod` `unzip`, `AboveBelow`'s `isLongest` → a `rank`-based bound) are
+  restated against that API rather than pattern-matching a custom `Chain`
+  inductive.
+- `Trace`/`EndToEndTrace` are `Prop`-valued and destructured in proofs.