diff --git a/0-Core-Formalism/lean/Semantics/Semantics/E8Sidon.lean b/0-Core-Formalism/lean/Semantics/Semantics/E8Sidon.lean
index d94d71fe..9dc041b4 100644
--- a/0-Core-Formalism/lean/Semantics/Semantics/E8Sidon.lean
+++ b/0-Core-Formalism/lean/Semantics/Semantics/E8Sidon.lean
@@ -417,7 +417,7 @@ theorem fiber_partition (S : Finset ℕ) (s : ℕ) :
 |------|------|--------|--------|
 | `e8_additive_completeness` | §10 | axiom | Open problem in additive combinatorics |
 
-### Sorry inventory (10 total, all with TODO(lean-port))
+### Sorry inventory (12 total, all with TODO(lean-port))
 
 | Item | Line | Blocked on |
 |------|------|------------|