TFPT scientific source excerpt
Original repository path: experiments/theory-contracts/seam-source-character-search-20261015/source_reconstruction/PROOF.txt
Original file SHA-256: 424e2f8eaf021cae575e479ccca4fcd2b8a34df1e5d5410371a86144f07ddb5d
Inclusive original lines: 51-67
Line numbers below refer to the original source.
This bounded excerpt is source evidence; it is not a new proof/checker run.
Conversation metadata and personal execution details are omitted where indicated.

000051 | 3. The first operator identity, before any spectrum fitting
000052 | 
000053 | Let C be an orthogonal projection, U a unitary on the same Hilbert space,
000054 | and S=C U C restricted to C H. Direct multiplication gives
000055 | 
000056 |  C-S* S = C U* (1-C) U C = ((1-C) U C)* ((1-C) U C).
000057 | 
000058 | Thus S is an isometry precisely when (1-C) U C=0. This says that the
000059 | actual seam action leaves the positive Cauchy-data subspace invariant.
000060 | It is a relation between two operators, stronger than a winding number.
000061 | Lean proves the algebraic corner identity and the equivalence S*S=C iff
000062 | the leakage expression vanishes. Hilbert positivity and the norm-zero
000063 | implication are the elementary analytic argument above, not Lean output.
000064 | 
000065 | Fredholm index -1 determines dim ker S - dim ker S* = -1 only. Once S is
000066 | known to be an isometry, it implies dim ker S*=1. It does not itself prove
000067 | isometry or exclude a unitary summand in the Wold decomposition.