doc(periodic): update final overlap route gap#3272
Conversation
claude
Bot
added
formalization
|
PR cleanup
Conventions: CONTRIBUTING.md |
|
You have reached your Codex usage limits for code reviews. You can see your limits in the Codex usage dashboard. |
![claude[bot]](https://avatars.githubusercontent.com/in/1236702?s=60&v=4){kind=small}
There was a problem hiding this comment.
Review Summary
This is a clean, tightly-scoped documentation-only PR updating the periodic-overlap paper-gap note. All review categories pass.
Verified claims:
- The "single remaining leaf" claim is accurate:
rg -n sorryconfirmsCase3.leancontains exactly onesorry—repeatedBlocks_of_blockedSectorGaugePhase(line 638) - All newly-referenced Lean declarations (
PiTensorProductPhase.exists_kappa_of_piTensorProduct_eq_smul,PiTensorProductPhase.exists_kappa_product_one_of_piTensorProduct_eq_root_smul,exists_fin_complex_unit_cyclic_coboundary_shift_of_prod_eq_one) exist and are fully proved sectorGaugePhaseEquiv_succ_of_cyclicTransportandgaugePhaseEquiv_of_overlap_norm_tendsto_one_of_irreducible_TPhave complete proofs- The note adheres to
docs/paper-gaps/policy.tex: self-contained exposition, notation introduced before use, precise source citations,\leanidin footnotes, clear verdict
No issues found in any review category (proof integrity, proof correctness, style, type safety, performance, modularity, documentation, paper-gap policy).
APPROVED.
There was a problem hiding this comment.
Review: doc(periodic): update final overlap route gap
Verdict: APPROVE — no 🔴 or 🟡 issues found.
This is a documentation-only change to docs/paper-gaps/1708_periodic_overlap_route_alignment.tex, narrowing the recorded Case-3 obstruction from "two remaining leaf obligations" to one (repeatedBlocks_of_blockedSectorGaugePhase, issue #873). I verified every load-bearing claim against the codebase and the local source Papers/1708.00029/main.tex.
Faithfulness / proof-status claims — all confirmed:
- The "single remaining leaf" claim is accurate. There is exactly one
sorryacross all ofTNLean/MPS/Periodic/Overlap/and the cited support files — atCase3.lean:638, insiderepeatedBlocks_of_blockedSectorGaugePhase. The citedPiTensorProductPhase.exists_kappa_of_piTensorProduct_eq_smul,...exists_kappa_product_one_of_piTensorProduct_eq_root_smul, andexists_fin_complex_unit_cyclic_coboundary_shift_of_prod_eq_oneare allsorry-free, so "already isolated" is correct. - All
\leaniddeclarations cited in the changed text resolve to existing declarations.
Source citations — all accurate against Papers/1708.00029/main.tex:
eq:resultpropis labelled at line 1067; the Ω_u contraction ("Now consider the concatenation of tensors") begins at line 1041, so the new range 1041–1068 is correct, and the η bookkeeping (η_v defined line 1060) matches.- The normalization/gauge bullet maps precisely to lines 1073–1117: κ_v with ∏κ_v=1 (
eq:prodkappaprop, line 1079), |κ_v|=1 from ‖Σ A_u^{i†}A_u^i‖=1 (lines 1082–1083), θ_v=φ_v−φ_{v+1} (line 1095), and U=Σ_u e^{iφ_{u+q}}P_u U_{u+q}Q_{u+q} (line 1111).
Dropped "per-sector corner unitaries" bullet — justified: the leaf lemma repeatedBlocks_of_blockedSectorGaugePhase already takes the corner data as hypotheses (φA/φB, hA_letter/hB_letter, and the per-sector hBlockMatch gauge-phase equivalences from the formalized T^l + Theorem 2.10 staircase). Removing it from the remaining list is consistent with the actual signature; the open work is genuinely the contraction + normalization the note now describes.
Policy (docs/paper-gaps/policy.tex): the note stays a self-contained mathematical account — notation introduced, formal identifiers in footnotes, source cited by equation label and line range, and a clear verdict per section. The edit is a coherent status narrowing (§Revision), not a chronological log.
No code or proof logic changes; no proof-integrity, type-safety, performance, or modularity concerns apply.
There was a problem hiding this comment.
Review: doc(periodic): update final overlap route gap
Verdict: APPROVE — documentation-only update to a paper-gap note; all claims verified faithful.
This PR edits only docs/paper-gaps/1708_periodic_overlap_route_alignment.tex, narrowing the recorded Case-3 obstruction from "two remaining leaf obligations" to a single leaf and recording the already-isolated Lean inputs. I reviewed it against docs/paper-gaps/policy.tex and verified every factual claim against the formalization and the local source.
Verification
"Single remaining leaf" claim — accurate. TNLean/MPS/Periodic/Overlap/Case3.lean contains exactly one sorry (line 638), inside repeatedBlocks_of_blockedSectorGaugePhase (declared line 583). The note's statement that the sector-match argument is "proved modulo the single remaining leaf repeatedBlocks_of_blockedSectorGaugePhase" is correct.
Cited isolated Lean inputs — all exist and are proved (no sorry):
PiTensorProductPhase.exists_kappa_of_piTensorProduct_eq_smulandPiTensorProductPhase.exists_kappa_product_one_of_piTensorProduct_eq_root_smul—TNLean/Algebra/PiTensorProductPhase.lean(lines 50, 147; file has 0sorry), namespaceTNLean.Algebra.PiTensorProductPhase.exists_fin_complex_unit_cyclic_coboundary_shift_of_prod_eq_one—TNLean/Algebra/FiniteCycleCoboundary.leanline 122 (file has 0sorry).
New source citations — faithful to Papers/1708.00029/main.tex:
- The Ω_u contraction bullet cites "lines 1041–1068 …
eq:resultprop". The concatenation argument begins at line 1041 (right-inverse relationeq:Omegaupropat 1039), andeq:resultpropis labelled at line 1067 — inside the cited range. - The normalization/gauge bullet matches the source:
∏_v κ_v = 1(eq:prodkappaprop, line 1080),|κ_v|=1from‖∑_i A_u^{i†}A_u^i‖ = 1(lines 1082–1083; correctly paraphrased as the left-canonical normalization, consistent with theIsLeftCanonicalhypotheses on the lemma), andκ_v = e^{i(φ_v−φ_{v+1})}(lines 1094–1096). The global unitaryU = ∑_u e^{iφ_{u+q}} P_u U_{u+q} Q_{u+q}matches the source assembly.
Policy compliance (policy.tex)
The note remains a self-contained mathematical account: it introduces its notation, states the source assertion, isolates the remaining contraction-and-gauge obligation, compares source/blueprint/Lean, and gives an explicit verdict (route substitution + scope restriction, none unfaithful). Formal identifiers stay in footnotes; the wording change "phase assembly" → "phase construction" is purely cosmetic and does not affect the mathematics.
No proof-integrity, correctness, type-safety, or style concerns apply (no Lean code changed). No 🔴 or 🟡 issues found.
2 participants
Motivation
The periodic-overlap paper-gap note still said the Case 3 argument was proved modulo two remaining leaf obligations. Current
origin/mainhas narrowed the obstruction to the single private lemmarepeatedBlocks_of_blockedSectorGaugePhase, tracked by #873.Description
docs/paper-gaps/1708_periodic_overlap_route_alignment.texso it names the single remaining Case 3 leaf.Ω_ucontraction producingeq:resultprop, followed by the unit-modulus normalization, finite-cycle coboundary, and global gauge construction.Testing
git diff --checkpython3 scripts/check_reader_facing_prose.py --root . --diff-base origin/mainpython3 scripts/blueprint_lean_sync.py --root . --ciTEXINPUTS=.: latexmk -pdf -interaction=nonstopmode -halt-on-error -outdir=/tmp/tnlean-1708-gap-local 1708_periodic_overlap_route_alignment.texfromdocs/paper-gapsAddresses #873. Refs #81. Refs #619.
Note
Low Risk
Documentation-only edits to a paper-gap TeX note; no code or proof logic changes.
Overview
Aligns the periodic overlap paper-gap note with current formalization status for arXiv:1708.00029 Appendix A Case 3.
The note now states the sector-match argument is complete modulo a single leaf,
repeatedBlocks_of_blockedSectorGaugePhase(issue #873), instead of two. Wording shifts from "phase assembly" to "phase construction" in headings and load-bearing remarks.The remaining Case-3 work is reframed as two concrete steps: the cyclic Ω_u contraction to
eq:resultprop, then normalization and global gauge (κ extraction, unit modulus, finite-cycle coboundary, assembly ofU). It drops the older bullet about per-sector corner unitaries / compression upgrades.New text points to already-isolated Lean inputs (
PiTensorProductPhaseκ lemmas,exists_fin_complex_unit_cyclic_coboundary_shift_of_prod_eq_one) and notes one-step transport is closed via the cited overlap and primitivity theorems.Reviewed by Cursor Bugbot for commit cef8b1e. Bugbot is set up for automated code reviews on this repo. Configure here.