doc(MPS/Periodic): use 1708.00029 terminology for periodic bases

[LionSR]

Motivation

• arXiv:1708.00029 (De las Cuevas et al.) uses "non-repeated blocks" and "basis/bases of periodic tensors" in Section 3. The existing docstrings and blueprint entries used "non-repeating" and "periodic bases", which do not match the paper's terminology.
• Aligns reader-facing prose with the source-discipline requirement for arXiv:1708.00029 formalization (see Tracking: arXiv:1708.00029 periodic Fundamental Theorem of MPS #619).

Description

• TNLean/MPS/Periodic/FundamentalTheorem.lean: replaced "non-repeating" with "non-repeated" in docstrings for the periodic Fundamental Theorem results (Theorem 3.4 and equal-case matching/scalar statements); mathematical content and theorem names are unchanged.
• blueprint/src/chapter/ch22_periodic_ft.tex: retitled the conditional matching theorem to "Conditional matching of bases of periodic tensors"; updated proof text to say "bases of periodic tensors" instead of "periodic bases".
• No Lean proofs, definitions, or blueprint chapter visibility are modified; chapters 20--24 remain commented out in blueprint/src/content.tex.

Testing

• lake exe cache get
• lake build TNLean.MPS.Periodic.FundamentalTheorem -q
• python3 scripts/check_reader_facing_prose.py --root . --diff-base origin/main --ci
• python3 scripts/blueprint_lean_sync.py --root . --ci
• git diff --check

---

Refs #619

---

Note

Low Risk
Prose and LaTeX title tweaks only; no formal statements, proofs, or runtime behavior change.

Overview
Documentation-only terminology alignment with arXiv:1708.00029 Section 3 wording.

In TNLean/MPS/Periodic/FundamentalTheorem.lean, reader-facing docstrings for Theorem 3.4 and the equal-case matching/scalar statements now say non-repeated blocks instead of non-repeating; mathematical content and theorem names are unchanged.

In blueprint/src/chapter/ch22_periodic_ft.tex, the conditional matching theorem is retitled to Conditional matching of bases of periodic tensors, and its proof text refers to matching bases of periodic tensors rather than periodic bases.

No Lean proofs, definitions, or blueprint chapter visibility are modified.

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

[chatgpt-codex-connector]

You have reached your Codex usage limits for code reviews. You can see your limits in the Codex usage dashboard.

[claude]

PR cleanup

Field	Before	After
Title	doc(Periodic): use 1708 terminology for periodic tensors	doc(MPS/Periodic): use 1708.00029 terminology for periodic bases
Body	## Summary / ## Source / ## Validation headings	restructured to ### Motivation / ### Description / ### Testing template; Bugbot block preserved; Refs #619 footer retained
Labels	(none)	added: tracking, 1708.00029, documentation
Issue	linked to #619

Conventions: CONTRIBUTING.md

[claude]

Review: documentation-only terminology alignment

This PR changes reader-facing prose only — four docstrings in TNLean/MPS/Periodic/FundamentalTheorem.lean and a blueprint theorem title plus proof text in blueprint/src/chapter/ch22_periodic_ft.tex. No Lean proof, definition, theorem statement, signature, or \lean{}/\leanok/\uses{} tag is modified.

Faithfulness check (in scope)

The terminology changes match the cited source exactly. In Papers/1708.00029/main.tex:

• "non-repeated blocks" appears at lines 288 (non-repeated blocks, there is a permutation of the blocks), 409, 444, and 949 — the paper never uses "non-repeating". The docstring edits at lines 20, 277, 507, 530 of FundamentalTheorem.lean correctly adopt "non-repeated".
• The paper's Definition "Basis of periodic tensors" (lines 302–304: "Any set ${A_j}_{j\in J}$ of non-repeated periodic tensors … is called a basis of periodic tensors for $A$") and subsequent uses ("bases of periodic tensors", lines 579, 605, 614, 622, 626, 645) confirm "bases of periodic tensors" over the prior "periodic bases". The blueprint retitle of thm:periodic_equalcase_matching and its proof text (lines 469, 507) align with this.

So the change is a strict alignment to source terminology, not a divergence.

Consistency check

rg over TNLean/MPS/Periodic/ and ch22_periodic_ft.tex finds no surviving "non-repeating" or "periodic bases" referring to this concept — the rename is complete within the affected area, leaving no mixed vocabulary.

Categories not applicable

Proof integrity, proof correctness, type safety, and performance are N/A — no proof terms or statements changed. Mathlib naming/style is N/A — no declarations renamed. Prose quality and blueprint↔Lean sync are explicitly out of scope for this review (handled by the dedicated Blueprint Sync & Prose Review workflow); I evaluated only the source-faithfulness of the terminology, which is correct.

No 🔴 or 🟡 issues found. Approving.

[claude]

Blueprint ↔ Lean Equivalence and Prose Review

0 equivalence mismatches · 0 stale \leanok tags · 0 prose issues

---

Category A — Blueprint ↔ Lean equivalence and status

The only blueprint entry touched is thm:periodic_equalcase_matching, which receives a new title. The mathematical body (hypotheses + conclusion, lines 474–478) is unchanged. I verified all four checks:

A.1 — Mathematical equivalence. The blueprint states: irreducible form for both tensors (IsIrreducibleForm), no repeated pair of distinct basis elements (the hNonRepA/hNonRepB universally-quantified HetRepeatedBlocks negations), and the periodic-overlap hypothesis (PeriodicOverlapHypothesis) — yielding same cardinality plus a bijection with per-element HetRepeatedBlocks. The Lean signature of fundamentalTheorem_periodic_equalCase_matching matches on every axis: same hypotheses, same strength, same conclusion (PeriodicBlockMatchingWitness expands to exactly ∃ h : rA = rB, ∃ perm, ∀ j, HetRepeatedBlocks (A j) (B (perm j))). No mismatch.

A.2 — \leanok accuracy. Both \leanok tags (statement and proof) are pre-existing and unmodified by this PR. The statement tag is valid: \lean{MPSTensor.fundamentalTheorem_periodic_equalCase_matching} resolves and the signature matches. The proof tag is valid: the Lean proof is a one-liner calling fundamentalTheorem_periodic_proportional, which has a complete tactic proof (lines 315–366, no sorry or admit). The admitted portions documented in the file live inside PeriodicOverlapHypothesis.ofIsPeriodic, which constructs the structure from IsPeriodic data; fundamentalTheorem_periodic_proportional takes PeriodicOverlapHypothesis as an opaque hypothesis, so no sorry propagates into either proof. The second modified proof sketch (thm:periodic_equalcase_scalar_component) likewise bears a pre-existing \leanok; fundamentalTheorem_periodic_equalCase is fully proved at lines 568–594 with no sorry.

A.3/A.4 — No stale \notready, no missing tags, no renamed declarations. No \leanok or \lean{...} tags were added or removed. No Lean declaration was introduced, removed, or renamed.

---

Category B — Prose quality

The terminology changes ("non-repeated", "bases of periodic tensors") are source-faithful to arXiv:1708.00029 Section 3. No banned software-engineering or LLM terms appear in the changed lines. Backtick references in the Lean docstrings name declarations defined in the same file, which is the explicitly permitted use per §1 "Allowed in Lean docstrings". The blueprint proof sketch ("First use Theorem X to match the bases of periodic tensors. For each matched block, apply Theorem Y…") is a transparent two-step citation, not an overlap or tensor-network argument; no formula display is required.

[claude]

Review Summary

This is a clean, well-scoped documentation-only PR that aligns reader-facing terminology with arXiv:1708.00029 Section 3.

What changed:

• TNLean/MPS/Periodic/FundamentalTheorem.lean: 4 docstring replacements of "non-repeating" → "non-repeated" (paper uses "non-repeated blocks" at line 288, "non-repeated periodic tensors" at line 303).
• blueprint/src/chapter/ch22_periodic_ft.tex: 2 replacements of "periodic bases" → "bases of periodic tensors" (paper's Definition at line 302: "Basis of periodic tensors").

Paper verification:

• arXiv:1708.00029, line 288: "non-repeated blocks" ✅
• arXiv:1708.00029, lines 302–303: "basis of periodic tensors" ✅

No Lean code, proofs, theorem statements, \lean/\leanok tags, or chapter visibility changed. No 🔴 or 🟡 issues found.

Verdict: APPROVE.

[claude]

Auto-fix investigation: no code error found (transient CI infrastructure failure)

I investigated the failed CI run (run 27892423106) and found no Lean build error to fix.

Root cause

The attempt-1 failure was a network timeout while installing the Lean toolchain, before any compilation began:

info: downloading https://releases.lean-lang.org/lean4/v4.31.0/lean-4.31.0-linux.tar.zst
error: could not download file from 'https://releases.lean-lang.org/lean4/v4.31.0/lean-4.31.0-linux.tar.zst'
info: caused by: error during download
info: caused by: [28] Timeout was reached (Connection timed out after 30002 milliseconds)

This is a transient infrastructure issue (toolchain CDN timeout), not a code problem. CI attempt 2 is already re-running automatically and was in progress at the time of this investigation.

Verification

• This PR's only commit (0d2dafc) is doc-only: a docstring terminology change ("non-repeating" → "non-repeated") plus a blueprint .tex wording change. No proof or signature was touched.
• lake env lean TNLean/MPS/Periodic/FundamentalTheorem.lean compiles cleanly locally with zero errors.
• No sorry/admit placeholders in the file — the only rg hits are the words "admitted"/"admit" inside docstring prose.

Action taken

None. There is no defect to fix, so I did not push a no-op commit (per proof-integrity guidance, spurious commits should be avoided). If attempt 2 hits the same CDN timeout, simply re-running the workflow should resolve it.

🤖 Generated with Claude Code