Rectangular attainment
Abstract
Attaining orthonormal pairs for finite rectangular Ky Fan sums.
Theorem 1.1 (Attaining orthonormal pair).
Lean statement: D5/S3/Quantum/Entanglement/Rectangular/FiniteSectorRectangularAttainment.exists_orthonormal_re_sum_inner_map_eq_ky_fan_sum
Proof. Machine-checked in Lean as D5/S3/Quantum/Entanglement/Rectangular/FiniteSectorRectangularAttainment.exists_orthonormal_re_sum_inner_map_eq_ky_fan_sum (✓ std3). ∎
Citation. Jon Crall, Claude Fable 5, Claude Opus 4.8, GPT-5.6 Thinking, and GPT-5.6 High (2026). Formal rectangular singular-value variational bounds. URL: https://github.com/AIQ-Kitware/aiq-dkps-formalization/tree/64e234954217f3ca907ac980c8cbde2900109a66/ForTauCeti/Analysis/InnerProductSpace.
Commentary.
For a real or complex finite-dimensional linear map between possibly unequal dimensions, every natural k at most both dimensions admits orthonormal source and target k-families attaining the real paired trace. The original Gram eigenbasis provides the source family; normalization on the positive singular directions and orthonormal extension provide the target family. The empty family remains legal. This is the original attainment argument used by sector_pair, with no additional completeness or nontriviality assumptions.