feat(algebra): assemble the skew-unitary congruence

[LionSR]

What changed

• formalize the explicit paired-projector construction in the skew branch of CPSV17:
  [
  S=e^{-i\pi/4}\sum_E e^{-iE/2}(P_E+P_E^T),
  \qquad
  \widetilde\Lambda=i\sum_E(P_E-P_E^T)
  ]
• prove $S$ is symmetric and unitary, $\widetilde\Lambda$ is entrywise real, skew-symmetric, and unitary, and
  [
  x=S^T\widetilde\Lambda S
  ]
• add reusable multiplication and unitarity lemmas for weighted complete orthogonal-projector sums
• keep the projector-label type independent of the ambient matrix index, so spectral projectors may have arbitrary multiplicity
• add a checked Chapter 28 supplied-projector lemma while leaving spectral-pair extraction (Extract paired spectral projectors from a skew-symmetric unitary #7587), determinant one (Real skew-unitary matrices have determinant one #7588), and the full skew theorem \notready

The proof follows CPSV17 lines 1066-1082 and retains the source phase $e^{-i\pi/4}$. It makes no rank-one projector assumption and no continuity claim.

Validation

• lake build TNLean.Algebra.UnitaryCongruence (2980/2980 on exact hot-main cache)
• independent source/mathematical review and simplifier review
• full pre-publication build (10451/10451 before final unrelated-main rebase)
• repository style and proof-integrity checks
• Blueprint synchronization (7305/7305 theorem-like entries after rebase)
• strict declaration checks
• double LuaLaTeX, zero undefined cross-references
• diagnostics clean
• git diff --check

Closes #7586
Advances #7580
Advances #7572

[chatgpt-codex-connector]

Codex Review Summary

This comment shows the latest Codex review activity on this pull request.

Review	Status	Commit	Review trigger
📝 Code Review	✅ Completed 2026-09-01T10:21:43.743564Z	f83526b	New commits

ℹ️ About Codex in GitHub

Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you

• Open a pull request for review
• Mark a draft as ready
• Comment "@codex review" or "@codex security review".

Codex reacts with 👀 while any review is running, comments if it has suggestions, and reacts with 👍 once all reviews finish with no findings.

[Copilot]

🟢 Approval recommended

The Lean implementation and Blueprint sync appear consistent with the stated CPSV17 construction, with only a minor documentation-header mismatch noted.

Pull request overview

This PR extends TNLean.Algebra.UnitaryCongruence to cover the skew-symmetric branch of the CPSV17 paired-projector construction, adding reusable lemmas for weighted sums of orthogonal projectors and synchronizing the corresponding Blueprint lemma in Chapter 28.

Changes:

• Add reusable multiplication and unitarity lemmas for weighted sums over mutually orthogonal Hermitian idempotents.
• Formalize the CPSV17 paired-projector assembly in the skew branch, producing symmetric unitary S, real skew-symmetric unitary Λ, and the factorization x = Sᵀ * Λ * S.
• Add a Blueprint lemma entry (\leanok) for the paired-projector skew congruence and wire it into the dependency graph of the (still \notready) full normal-form lemma.

File summaries

File	Description
TNLean/Algebra/UnitaryCongruence.lean	Adds weighted-sum infrastructure and proves the skew paired-projector congruence assembly theorem.
blueprint/src/chapter/ch28_mpu.tex	Adds/marks the paired-projector skew congruence lemma as checked and updates \uses dependencies accordingly.

Review details

• Files reviewed: 2/2 changed files
• Comments generated: 1
• Review effort level: Lite

---

💡 Add a code-review agent skill or configure MCP servers for context-aware, tailored reviews. Learn more in the docs.

[LionSR]

Addressed the Copilot documentation finding in 0f5e653c0: the module heading now names both symmetric and skew-symmetric unitary congruence factorizations. The review thread is resolved.

[chatgpt-codex-connector]

💡 Codex Review

Here are some automated review suggestions for this pull request.

Reviewed commit: 0f5e653c0d

ℹ️ About Codex in GitHub

Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you

• Open a pull request for review
• Mark a draft as ready
• Comment "@codex review".

If Codex has suggestions, it will comment; otherwise it will react with 👍.

Codex can also answer questions or update the PR. Try commenting "@codex address that feedback".

[LionSR]

Addressed the Codex source-citation finding by adding a reader-visible CPSV17 lemma citation in blueprint/src/chapter/ch28_mpu.tex. The thread is resolved.

[claude]

Reviewed for (A) blueprint ↔ Lean equivalence/status and (B) prose quality only, per the scoped mandate.

Category A — equivalence and status

• New lemma lem:mpu_skew_unitary_paired_projectors ↔ Matrix.exists_skew_unitary_congruence_of_paired_projectors checked hypothesis-by-hypothesis: finite index sets (K→κ, I→m), Hermitian P k (hPstar), the combined orthogonal-idempotent family over Sum κ κ (hPmul) capturing "family {P_k, P_k^T} mutually orthogonal projectors," and the identity resolution (hPsum) capturing "sums to the identity." Conclusion formulas for x, S, Λ match the paper phases (e^{-iπ/4}, e^{-iE_k/2}, i) term-for-term, and the five asserted properties (S^T=S, S unitary, Λ real, Λ^T=-Λ, Λ unitary, x=S^TΛS) match the Lean conjuncts one-to-one. No hypothesis strengthening/weakening found.
• \leanok on both the statement and proof is valid: the declaration resolves, the signature matches per above, and grep -n 'sorry|admit|axiom|native_decide' TNLean/Algebra/UnitaryCongruence.lean is empty.
• \notready on lemma:conjclass-normalform-continuous remains correct — it still has no \lean{} counterpart and depends on the not-yet-formalized spectral-pair extraction (#7587); the added \uses{lem:mpu_skew_unitary_paired_projectors} edge is accurate given the new lemma's role.
• Module docstring header was updated to cover both branches (this also resolves the earlier copilot-pull-request-reviewer thread on the stale header — left that thread's resolution to a maintainer since I don't own it).
• The two new helper lemmas (weighted_sum_mul_weighted_sum, weighted_sum_mem_unitaryGroup) are reusable technical building blocks, not paper-level statements, so no blueprint entry is expected for them (consistent with existing ledger entries of the same kind).

Category B — prose quality

• New blueprint lemma/proof text is pure mathematics, no Lean identifiers or banned software/LLM phrasing.
• The proof sketch is formula-driven as required: it displays the weight identity (e^{-iπ/4}e^{-iE_k/2})^2 i = e^{-iE_k} rather than describing the phase cancellation in words only.
• No banned-term or Lean-jargon hits in the changed docstring/blueprint text.

No new findings in either category — 0 equivalence mismatches, 0 stale \leanok/\notready, 0 prose issues.

Note: the existing unresolved chatgpt-codex-connector thread (visible citation for the new lemma's source) is still open and not fixed by this diff, but it falls outside my A/B mandate (citation-formatting practice, not a math-equivalence or banned-language issue), so I neither duplicated nor resolved it.

[claude]

Summary

Reviewed TNLean/Algebra/UnitaryCongruence.lean and blueprint/src/chapter/ch28_mpu.tex against CPSV17 (Papers/1703.09188/paper_v2.tex, lines 1054–1082) and the Lean development.

Mathematical faithfulness. Matrix.exists_skew_unitary_congruence_of_paired_projectors (UnitaryCongruence.lean:189) matches the skew branch of lemma:conjclass-normalform-continuous (paper lines 1066–1082): given a paired family {P_k, P_k^T} of Hermitian orthogonal idempotents summing to 1, it produces S = e^{-iπ/4}∑ e^{-iE_k/2}(P_k+P_k^T) and Λ̃ = i∑(P_k-P_k^T), and shows S^T = S, S unitary, Λ̃ real and skew-symmetric and unitary, and x = S^T Λ̃ S. I checked the phase algebra by hand: (e^{-iπ/4}e^{-iE_k/2})² · i = e^{-iπ/2}e^{-iE_k}·i = (-i)(i)e^{-iE_k} = e^{-iE_k} for the P_k term, and (e^{-iπ/4}e^{-iE_k/2})²·(-i) = -e^{-iE_k} for the P_k^T term — this reproduces x = ∑ e^{-iE_k}(P_k - P_k^T) exactly as in the paper (hphase/hphase_neg, lines ~336–360).

The Hermiticity hypothesis hPstar on P is not a smuggled restriction: the paper's own proof of 𝑃̄_E = P_E^\dagger (used to derive Λ̃ real) implicitly relies on the same fact, since "orthogonal projector" in this source means self-adjoint idempotent throughout. The lemma is honestly scoped as a new blueprint entry (lem:mpu_skew_unitary_paired_projectors) feeding into the still-\notready lemma:conjclass-normalform-continuous via \uses{...} — it is not mislabeled as the full source theorem, so no paper-gap note is required for the "projectors are given rather than derived from a spectral decomposition" gap (spectral-pair extraction is correctly deferred to #7587).

Proof integrity. No sorry/admit/axiom/native_decide in the changed file. The two new general-purpose lemmas (weighted_sum_mul_weighted_sum, weighted_sum_mem_unitaryGroup) are reusable and correctly generalize over an arbitrary orthogonal-idempotent family, not hardcoded to Sum κ κ.

Prior review threads. Both the Copilot module-header finding and the Codex citation finding are addressed in the diff (module docstring now names both branches at UnitaryCongruence.lean:13; the new lemma carries \cite[Lemma~\texttt{lemma:conjclass-normalform-continuous}]{Cirac2017MPU} inline, matching the style of the preceding symmetric-branch entry) and are already marked resolved on GitHub — no action needed.

Style/docs. Docstrings present on all three new declarations; naming follows convention (exists_..., weighted_sum_...); Cirac2017MPU is a valid, already-used bib key.

No 🔴 blockers or 🟡 requires-changes issues found. Approving.

[LionSR]

Post-merge verification on exact origin/main d1bd82b6d: warm hot-main full lake build passed 10452/10452 jobs.

[claude]

Scope: blueprint↔Lean equivalence/status (A) and prose quality (B) only.

Category A — blueprint ↔ Lean equivalence

Checked the new lemma lem:mpu_skew_unitary_paired_projectors (blueprint) against Matrix.exists_skew_unitary_congruence_of_paired_projectors (Lean):

• Hypotheses. Blueprint's "$P_k$ Hermitian projectors" + "${P_k,P_k^T}$ mutually orthogonal, sums to the identity" corresponds exactly to hPstar (Hermitian on $P_k$; Hermiticity of $P_k^T$ is a correct derived fact, not smuggled in) + hPmul (idempotency at $a=b$, pairwise orthogonality at $a\neq b$, including the same-$k$ cross term $P_k P_k^T=0$) + hPsum (sum over Sum κ κ = 1). No silent strengthening or weakening.
• Conclusion. Formulas for $x$, $S$, $\widetilde\Lambda$ match term-by-term (phases, sums, transposes). $S^T=S$, $\overline{\widetilde\Lambda}=\widetilde\Lambda$ (entrywise conjugate, matching Matrix.map (starRingEnd ℂ), not conjugate-transpose), $\widetilde\Lambda^T=-\widetilde\Lambda$, both unitary, and $x=S^T\widetilde\Lambda S$ all line up with the Lean conjunctions. The existential/let-bound Lean phrasing is a standard restatement of "the matrix given by this formula has these properties," not a weaker claim.
• \leanok accuracy. Both the statement and proof \leanok are valid: Matrix.exists_skew_unitary_congruence_of_paired_projectors resolves, and rg -n "sorry|admit|axiom" TNLean/Algebra/UnitaryCongruence.lean is empty.
• \notready accuracy. lemma:conjclass-normalform-continuous correctly stays \notready — this PR supplies only the projectors-given branch; spectral-pair extraction and $\det=1$ remain open (per PR body, tracked as #7587/#7588). The added \uses{..., lem:mpu_skew_unitary_paired_projectors} on that parent entry is accurate.
• Both prior bot review threads (module header mismatch, invisible-only citation) are already fixed in the current diff and marked resolved — nothing outstanding there.

No equivalence mismatches found.

Category B — prose quality

The new blueprint lemma and proof sketch are formula-driven throughout (explicit sums, phases, and the key identity $(e^{-i\pi/4}e^{-iE_k/2})^2 i = e^{-iE_k}$ is displayed rather than asserted in words). No banned software/LLM phrasing or Lean jargon found in the changed blueprint prose or Lean docstrings.

Summary: 0 equivalence mismatches, 0 stale \leanok/\notready, 0 prose issues.

[claude]

Reviewed against the cited source (Papers/1703.09188/paper_v2.tex, lines 1066–1084) and the blueprint. This PR is already merged; filing this review for the record since CI just completed on the merge commit.

Source fidelity

Lines 1066–1084 of paper_v2.tex state the skew branch of lemma:conjclass-normalform-continuous: for $x=-x^T$ unitary, $x=\sum_E e^{-iE}(P_E-P_E^T)$ with ${P_E,P_E^T}$ a complete mutually-orthogonal family, $S=e^{-i\pi/4}\sum_E e^{-iE/2}(P_E+P_E^T)$, $\widetilde\Lambda=i\sum_E(P_E-P_E^T)$, giving $S$ unitary/symmetric, $\widetilde\Lambda$ real/skew-symmetric, and $x=S^T\widetilde\Lambda S$. The new blueprint entry lem:mpu_skew_unitary_paired_projectors (blueprint/src/chapter/ch28_mpu.tex:6708) restates exactly this, with the domain of $E_k$ widened from $[0,\pi)$ to all of $\mathbb R$ — a legitimate generalization (proving more, not assuming less), not a faithfulness gap. The parent lemma lemma:conjclass-normalform-continuous correctly stays \notready (det $=1$ and the spectral-pair extraction from an arbitrary skew-unitary $x$ are deferred to #7587/#7588 per the PR body), so nothing is overclaimed against the source.

Proof correctness (TNLean/Algebra/UnitaryCongruence.lean)

• weighted_sum_mul_weighted_sum / weighted_sum_mem_unitaryGroup: correctly generalize "sum of unit-modulus-weighted mutually-orthogonal Hermitian idempotents summing to 1 is unitary." Stated over a generic ι, not hard-coded to Sum κ κ — appropriately reusable, and I didn't find a pre-existing equivalent in Mathlib or .lake/packages/qiclean (checked QICLean/Algebra/{OrthogonalProjection,EigenvectorProjection}.lean).
• exists_skew_unitary_congruence_of_paired_projectors: hand-checked the algebra. hPmul over Sum κ κ correctly encodes orthogonality of all pairs, including $P_k\cdot P_k^T=0$ for every $k$ (since inl k ≠ inr k always), matching "the family ${P_k,P_k^T}$ ... mutually orthogonal" in the blueprint. The phase identity in hphase/hphase_neg is exactly $(e^{-i\pi/4}e^{-iE_k/2})^2\cdot i=e^{-iE_k}$ and $(e^{-i\pi/4}e^{-iE_k/2})^2\cdot(-i)=-e^{-iE_k}$, which are the two coefficients needed for $S^T\Lambda S$ to reassemble $x=\sum_k e^{-iE_k}(P_k-P_k^T)$ — verified against hquarter's $e^{-i\pi/2}=-i$ and hhalf. hΛ_real/hΛ_transpose correctly derive $\overline\Lambda=\Lambda$, $\Lambda^T=-\Lambda$ from hPstar via hPmap/hPtransposeMap. No sorry/axiom/native_decide.

Prior review threads

Confirmed via GraphQL that both bot threads are resolved and the fixes are present in the final diff: the module docstring now reads "Congruence factorizations of symmetric and skew-symmetric unitary matrices" (Copilot's finding), and the new lemma carries a visible \cite[Lemma~\texttt{lemma:conjclass-normalform-continuous}]{Cirac2017MPU} in the rendered blueprint text, not just the LaTeX % Source lines comment (Codex's P1 finding).

Advisory (non-blocking)

hphase/hphase_neg (lines ~313–359) go through a manual show ... by ring rewrite before applying hquarter/hhalf; this works but is more verbose than necessary — likely shrinkable with ring_nf plus the two exponential facts. Not required before merge (it already merged), just a candidate for docs/tactic_patterns.md/proof-shrink follow-up if this pattern recurs.

No blocking or must-fix issues found.