MPS/Periodic: m-factor cyclic contraction for blocked sector gauges

[LionSR]

Context

This is the focused Case 3 proof obligation for the periodic-overlap dichotomy.

The live target on current main is the private lemma

TNLean/MPS/Periodic/Overlap/Case3.lean
private lemma repeatedBlocks_of_blockedSectorGaugePhase

It feeds

lemma sectorTensor_proportional_of_blockedMatch
theorem periodicOverlap_gaugeEquiv_of_sector_match

and hence the Case 3 branch of Proposition 3.3.

Source Passage

The source is arXiv:1708.00029, Appendix A, lines 1023--1117. In the local LaTeX source this is the passage beginning with the sector-restricted tensors

A_u^i := P_u A^i P_{u+1},
B_v^i := U_v Q_v B^i Q_{v+1} U_{v+1}^{\dagger}

and continuing through the equations labelled eq:Fu, eq:Omegauprop, eq:resultprop, eq:thetaACprop, eq:prodkappaprop, and eq:result.

Current Lean State

The one-step sector propagation and the phase endpoints are no longer the central missing pieces.

• Sector propagation is formalized through sectorMatch_propagation and the public overlap-transport theorem.

• The finite-cycle phase choice in Appendix A, lines 1093--1102, is isolated in TNLean.Algebra.exists_fin_complex_unit_cyclic_coboundary_of_prod_eq_one.

• The shifted form needed for the propagated sector match (u, u + q) is isolated in TNLean.Algebra.exists_fin_complex_unit_cyclic_coboundary_shift_of_prod_eq_one.

• The final algebraic conversion from a unit-modulus gauge-phase relation to RepeatedBlocks is isolated in TNLean.MPS.Periodic.Overlap.repeatedBlocks_of_gaugePhaseData_norm_one.

• The propagated per-sector gauge-phase data now gives per-sector RepeatedBlocks after dimension cast, via sectorRepeatedBlocks_of_blockedMatch.

• The block-word right inverse corresponding to the Appendix A maps \Omega_u is available as TNLean.MPS.Chain.blockDecompositionMap, with existence packaged by IsNBlkInjective.exists_rightInverse. Its linear-combination defining identity is blockDecompositionMap_spec, and its explicit finite-sum form is blockDecompositionMap_sum.

• The finite-family common-length step is formalized as exists_common_isNBlkInjective_of_isNormal_leftCanonical: positive-dimensional left-canonical normal sector blocks admit one common positive exact block-injectivity length.

• Case 3 now packages the corresponding common sector right inverses as exists_common_sectorDecompositionMaps_of_isNormal_leftCanonical. After PR feat(periodic): expose sector omega sum form #3004, the witness hΩ has the explicit form

  ∑ σ : Fin L → Fin d,
    (Ω k X σ) • evalWord (blocks k) (List.ofFn σ) = X

  matching the sum identity in eq:Omegauprop.

• The remaining source passage is the m-factor cyclic contraction using these \Omega_u maps and the global gauge assembly. Per-sector RepeatedBlocks is not enough: the proof must still assemble the sector gauges into one global gauge for A and B.

Concrete Target

Given per-sector blocked gauge-phase data

hBlockMatch : ∀ u : Fin m,
  ∃ hdim : dimA u = dimB (u + q),
    GaugePhaseEquiv
      (cast (congr_arg (MPSTensor (blockPhysDim d m)) hdim) (blocksA u))
      (blocksB (u + q))

prove RepeatedBlocks A B by following Appendix A:

1. Starting from the already chosen common length L and right inverses Ω u satisfying the sum-form identity hΩ, apply the Ω_u inverses to the repeated cyclic concatenation to obtain the tensor-product identity eq:resultprop.
2. Extract per-site proportionality with phases \kappa_v, prove \prod_v \kappa_v = 1, and prove |\kappa_v| = 1 from the left-canonical normalization.
3. Apply the finite-cycle coboundary lemma, in its shifted form, for the \kappa/\theta/\phi phase telescoping.
4. Assemble the global gauge
   U = \sum_u e^{i\phi_{u+q}} P_u U_{u+q} Q_{u+q}
   and conclude A^i = e^{i\xi} U B^i U†.

Validation

• lake env lean TNLean/MPS/Periodic/Overlap/Case3.lean
• no new sorry, admit, axiom, native_decide, or proof-integrity workaround
• if blueprint entries or \leanok tags change, run lake build followed by cd blueprint && leanblueprint checkdecls

Refs #450 #81 #619

[LionSR]

@claude auto fix

Please pick this up from the issue body and open a focused PR from main for #873.

Keep the PR scoped to this issue, reference #873 in the PR body, and avoid introducing any new sorry, admit, axiom, native_decide, or proof-integrity workaround. If the statement is false or blocked by a dependency that is not yet on main, make the smallest useful preparatory PR or report the precise Lean-level blocker instead of adding placeholder proofs.

Use the repository conventions in docs/pr_review_management.md, docs/style.md, docs/doc.md, and the relevant blueprint style guide. Run targeted lake build checks for touched Lean modules, and run cd blueprint && leanblueprint checkdecls whenever blueprint declarations or tags are changed.

[claude]

Claude finished @LionSR's task in 5m 33s —— View job

---

Blocker report for #873

After reading TNLean/MPS/Periodic/Overlap/Case3.lean, the Appendix A proof in Papers/1708.00029/main.tex, and the currently exposed chain / sector infrastructure, I do not open a PR: the target sorry cannot be discharged on current main without adding substantial new infrastructure, and I am following the issue's instruction to avoid placeholder proofs. A precise report follows.

• Read Case3.lean around the target sorry (L324) and its two downstream dependents (L386, L442).
• Survey supporting infrastructure: RepeatedBlocks, GaugePhaseEquiv, IsNormal, IsCyclicSectorDecomp, decompositionMap / exists_rightInverse, tensor_proportional.
• Cross-check Appendix A of arXiv:1708.00029 (paper Papers/1708.00029/main.tex, L952-L1117) against the Lean statement.
• Conclude that the statement requires new infrastructure, not just a local proof script.

What the target sorry asks for

repeatedBlocks_of_blockedSectorGaugePhase (Case3.lean:284-324) must upgrade per-sector blocked data

hBlockMatch : ∀ u : Fin m, ∃ (hdim : dimA u = dimB (u + q)),
  GaugePhaseEquiv (cast _ (blocksA u)) (blocksB (u + q))

to a global RepeatedBlocks A B, i.e. ∃ ξ Y, ‖ξ‖ = 1 ∧ ∀ i, A i = ξ • Y * B i * Y⁻¹.

The hypothesis lives at the blocked sector level (MPSTensor (blockPhysDim d m) (dimA u)); the conclusion lives at the original unblocked level (MPSTensor d D). The paper executes the bridge in Eqs. A.14-A.18 (Papers/1708.00029/main.tex, L1012-L1117).

Precise Lean-level gaps on current main

The docstring at TNLean/MPS/Periodic/Overlap/Case3.lean:267-283 already flags the core gap. I confirm three distinct pieces of infrastructure are absent:

1. Corner-transition tensors A_u^i := P_u A^i P_{u+1} as a Lean definition.
   The paper's Eq. A.12-A.13 introduce A_u^i, B_v^i; the corresponding Lean API (exists_compressedTensor_of_supported_projection and its one-site variant) does not yet expose these one-site corner transitions. Without them, there is no way to turn the blocked-sector gauge-phase data into the m-fold product identity Eq. A.13 that the contraction argument starts from. This is the same gap that blocks sectorGaugePhaseEquiv_succ_of_cyclicTransport (Case3.lean:87-128).

2. m-factor generalization of tensor_proportional.
   TNLean/MPS/Chain/TensorEquality.lean:81-185 proves proportionality for two injective tensors. The full-cycle contraction (paper Eqs. A.15-A.17) needs the cyclic m-factor version: given m injective normal tensors A_u with A_u^{i_1} ⋯ A_{u+m-1}^{i_m} = e^{iλ_v} B_v^{i_1} ⋯ B_{v+m-1}^{i_m}, conclude A_u^i = κ_v e^{iη/m} B_v^i with ∏ κ_v = 1. None of MPS/Chain/*.lean provides this. It is the "reusable m-factor cyclic contraction theorem built from decompositionMap" that the existing docstring names.

3. Cyclic phase telescoping and global-gauge reassembly.
   Even once (1) and (2) are in place, the paper's step from Eq. A.17 to Eq. A.18 requires (a) a pure real-analysis lemma: θ : Fin m → ℝ with ∑ θ_v ≡ 0 (mod 2π) yields φ : Fin m → ℝ with θ_v = φ_v - φ_{v+1} (mod 2π); (b) reassembly U := ∑_u e^{iφ_{u+q}} P_u U_{u+q} Q_{u+q} into a single GL (Fin D) ℂ, using the sector projections from IsCyclicSectorDecomp and the per-sector unitaries U_v = P_u U_v Q_v. Neither the Mathlib-level telescoping lemma nor the corner-gauge assembly is present.

Additionally, ‖ξ‖ = 1 (where ξ = η/m) in the conclusion relies on normalization of the left-canonical sums ∑ (A_u^i)ᴴ A_u^i = 1 transported through the corner bridge — also not currently exposed.

Why a placeholder / partial implementation is not appropriate here

• Any attempt to close the sorry with only two-site tensor_proportional would either (i) require an unproven helper stated as a fresh sorry / axiom (forbidden by docs/PROOF_INTEGRITY.md), or (ii) silently strengthen hypotheses (e.g. assume m = 1 or drop ‖ξ‖ = 1) and break callers.
• A "smallest useful preparatory PR" would have to land at least item (1) or (2) above in isolation. Item (2) alone is comparable in size to TNLean/MPS/Chain/TensorEquality.lean and meaningfully touches API shared with VirtualInsertion.lean; item (1) requires extending IsCyclicSectorDecomp with per-site corner-transition data. Either belongs in its own scoped issue/PR rather than being bundled here, and the issue body explicitly lists both as existing, separate dependencies.
• No commits were made; current origin/main is unchanged.

Suggested path forward (scoping suggestion, not a commitment)

Three tightly scoped follow-up issues/PRs, any of which can land independently of the others:

1. MPS/Chain/TensorEqualityCyclic.lean: state and prove the m-factor cyclic analogue of tensor_proportional, using decompositionMap applied to F_u in Eq. A.18 exactly as the paper does (Notes Papers/1708.00029/main.tex L1025-L1068). No dependency on periodic / sector code.
2. Extend IsCyclicSectorDecomp with the one-site corner-transition tensors A_u^i := P_u A^i P_{u+1} and their m-fold product identification with blocksA u i₁ ⋯ i_m. This simultaneously unblocks sectorGaugePhaseEquiv_succ_of_cyclicTransport (Case3.lean:128).
3. Cyclic phase telescoping lemma on Fin m + global-gauge assembly from per-sector U_v and projections P_u, Q_v. These can live in TNLean/Algebra/ and TNLean/MPS/Periodic/CornerTransition.lean respectively.

Once (1)-(3) are on main, repeatedBlocks_of_blockedSectorGaugePhase becomes a relatively short composition of those lemmas with the IsLeftCanonical normalization, and sectorTensor_proportional_of_blockedMatch + periodicOverlap_gaugeEquiv_of_sector_match discharge immediately.

No changes committed

No files in this repository were modified; no new sorry / axiom / admit / native_decide introduced. Blueprint entries at blueprint/src/chapter/ch11b_periodic_ft.tex:540-556 already carry \notready, which correctly reflects the current state, so no blueprint update is warranted for this no-op outcome.
 |  branch: claude/issue-873-formalizationmpsperiodic-prove-m-factor-cyclic-contraction (no new commits)

[LionSR]

Heads up: the file this targets (TNLean/MPS/Periodic/Overlap/Case3.lean) is now orphaned — it still exists on disk but was dropped from TNLean.lean in #1740 because it depends on the retired one-copy Full/ chain. See #1741 for the retarget-or-delete decision on the periodic-overlap family. Whether this specific full-cycle contraction sorry should be discharged depends on which resolution #1741 picks. (Audit on branch claude/audit-open-issues-G9xMg.)

---

Generated by Claude Code