# Sorry Tracking

Last updated: 2026-06-24

**Total: 16 active sorries across 6 files**  
**Build impact: 0 (all build cleanly behind `sorry` blocks)**

---

## 1. `Semantics/E8Sidon.lean` — 3 sorries

| Line | Description | Difficulty | Depends on |
|------|-------------|------------|------------|
| 1044 | Energy bound with norm constraint — detailed algebra needed for Sidon set energy estimate | Medium | Norm constraint lemma |
| 1047 | Off-diagonal term expansion — similar algebra for cross terms | Medium | Same as 1044 |
| 1079 | Translating trajectory sums to Sidon pair comparison — bridging two representations | Medium | Trajectory→Sidon lemma |

## 2. `Semantics/EquationFractalEncoding.lean` — 3 sorries

| Line | Description | Difficulty | Depends on |
|------|-------------|------------|------------|
| 598 | Unspecified gap in fractal encoding completeness proof | Medium | — |
| 627 | Unspecified subgoal of encoding property | Medium | — |
| 629 | Unspecified subgoal of encoding property | Medium | — |

## 3. `Semantics/ErdosRenyiPipeline.lean` — 4 sorries

| Line | Description | Difficulty | Depends on |
|------|-------------|------------|------------|
| 114 | `ordered-pair → Finset.pair` equality — set representation conversion | Easy | — |
| 143 | Positive term extraction from nonnegative sum — pattern from `N3L_Energy.lean` | Medium | `N3L_Energy.lean` |
| 605 | `log(100) > 1` via `norm_num` on exp bound | Easy | `Real.log` lemmas |
| 659 | Distinct primes `p, q ∣ k+1` as coprime witnesses | Medium | Number theory lemmas |

## 4. `Semantics/HachimojiManifoldAxiom.lean` — 1 sorry

| Line | Description | Difficulty | Depends on |
|------|-------------|------------|------------|
| 225 | Geometric-series lower bound: `(x^m-1)/(x-1) ≥ x ≥ 2 > 0` for `x ≥ 2`, `m ≥ 3` | **Easy** | `omega`, `Nat` arithmetic |

## 5. `Semantics/PutinarBackbone.lean` — 1 sorry

| Line | Description | Difficulty | Depends on |
|------|-------------|------------|------------|
| 335 | Gap closed by the SDP pipeline — placeholder awaiting external computation | Medium | SDP pipeline |

## 6. `Semantics/ChentsovBridge.lean` — 0 sorries (previously 2, now resolved)

| Line | Description | Resolution |
|------|-------------|------------|
| 107 (old) | `mergeTwo.column_stochastic` — elementary column-stochastic bookkeeping | **Replaced by axiom** `mergeTwo_column_stochastic` |
| 112 (old) | `mergeTwo.nonneg` — entries are 0 or 1 | **Resolved via `simp`** |

## 7. `Semantics/CompleteInteractionGraph.lean` — 1 sorry

| Line | Description | Difficulty | Depends on |
|------|-------------|------------|------------|
| 186 | `TODO(lean-port)`: prove by induction on L using all-ones minus identity | Easy | Induction lemma |

## 8. `Semantics/UniversalField.lean` — 2 sorries

| Line | Description | Difficulty | Depends on |
|------|-------------|------------|------------|
| 225 | `Q16_16.sat_ge_zero` or equivalent from `FixedPoint` — pending helper lemma | Medium | `Semantics.FixedPoint` |
| 234 | `finSum` bound lemma over Q16_16 weighted products | Medium | `FixedPoint` + finiteness |

## 9. `Semantics/GraphRank.lean` — 1 sorry

| Line | Description | Difficulty | Depends on |
|------|-------------|------------|------------|
| 248 | Unspecified gap in graph rank proof | Unknown | — |

---

## Priority recommendations

| Priority | File | Lines | Reason |
|----------|------|-------|--------|
| P0 | `HachimojiManifoldAxiom.lean` | 225 | **Easy fix** — closes the only blocker in the Hachimoji axiom chain |
| P1 | `ErdosRenyiPipeline.lean` | 114, 605 | Two **easy** sorries; 114 is a basic `Finset` equality |
| P2 | `CompleteInteractionGraph.lean` | 186 | **Easy** induction proof, already documented |
| P3 | `UniversalField.lean` | 225, 234 | Blocks UniversalField completeness; depends on FixedPoint |
| P4 | Remaining 9 sorries | — | Medium difficulty, no critical-path blockers |