audit: canonical form reduction proof completeness report

[Copilot]

Audit of whether the full canonical form reduction from general MPS has been completely proved in both Lean and the blueprint.

Lean Code Status

• TNLean/MPS/CanonicalForm/ — ✅ 100% proved, 12/12 files, 0 sorry. Full 7-stage pipeline (irreducible decomposition → PF normalization → periodicity removal → cyclic sector decomp → equal-norm handling → BNT assembly → normal canonical form) is complete.

• TNLean/MPS/BNT/ — ✅ 100% proved, 5/5 files, 0 sorry. Includes cross_overlap_tendsto_zero, both permutation rigidity theorems, coeff_ratio_tendsto, Newton–Girard, and power-sum uniqueness.

• TNLean/MPS/Structure/ — ✅ 100% proved, 4/4 files, 0 sorry.

• TNLean/MPS/FundamentalTheorem/ — ⚠️ 13/14 files fully proved. One file incomplete:

  PeriodicOverlap.lean — ❌ 8 sorry statements (Prop. 3.3 of arXiv:1708.00029):

  Line	Theorem
  183	periodicSelfOverlap_tendsto
  207	periodicOverlap_tendsto_zero_of_ne_period
  240	sectorBlocked_isNormal_of_isPeriodic
  280	periodicOverlap_tendsto_zero_of_no_sector_match
  324	sectorMatch_propagation
  374	sectorTensor_proportional_of_blockedMatch
  401	periodicOverlap_gaugeEquiv_of_sector_match
  456	periodicOverlapDichotomy ← main theorem

  Root cause: statements are still phrased for ambient tensors; the live API in CyclicSectors.lean / Assembly.lean uses compressed sector tensors. The file header explicitly marks this as a skeleton pending API reformulation.

Blueprint Annotation Status

Chapter	\leanok coverage	Notes
ch10_bnt.tex	✅ 7/7 (100%)	Fully aligned
ch11_assembly.tex	⚠️ 11/26 (42%)	Periodic section correctly marked \notready
ch08_canonical.tex	⚠️ 2/66 (3%)	Annotation backlog — proofs exist in Lean but \leanok tags are absent

Recommended Actions

1. Close PeriodicOverlap.lean: re-state the 8 theorems against the compressed-sector API already in CyclicSectors.lean, then fill the proofs.
2. Update ch08_canonical.tex: add \leanok to ~64 proved theorems; run leanblueprint checkdecls.
3. Update ch11_assembly.tex: add \leanok to ~15 proved assembly theorems; keep \notready block until (1) is resolved.

Testing

• Grepped all relevant files: rg -n "sorry" TNLean/MPS/CanonicalForm/ TNLean/MPS/BNT/ TNLean/MPS/Structure/ → 0 matches.
• rg -n "sorry" TNLean/MPS/FundamentalTheorem/PeriodicOverlap.lean → 8 matches at lines 183, 207, 240, 280, 324, 374, 401, 456.
• Blueprint cross-checked by inspecting \leanok / \lean{ tags in blueprint/src/chapter/ch08_canonical.tex, ch10_bnt.tex, ch11_assembly.tex.

---

Note

Low Risk
Low risk because there are no repository changes; review is limited to metadata/context only.

Overview
No repository files are modified in this PR (the provided diff is empty), so there is no functional or proof-state change to review.

^{Reviewed by Cursor Bugbot for commit ade4b5e. Bugbot is set up for automated code reviews on this repo. Configure here.}

[LionSR]

needs to be addressed

[Copilot]

Copilot wasn't able to review any files in this pull request.

---

💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.

[LionSR]

Closing: empty diff (audit report in PR body only, findings already tracked in issue comments on #317-#335).