Two involutions and homogeneous word rank
Abstract
Homogeneous operator words in two involutions with a four-dimensional relative-product space.
Theorem 1.1 (Exact rank at every length).
Proof. Machine-checked in Lean as D5/S3/Quantum/QuantumChannels/TwoInvolutionWordRank.homogeneous_word_rank (✓ std3). ∎
Source. Repository-derived.
Commentary.
A is a finite-dimensional complex algebra, with no commutativity assumption. Products(u,v,0) is {1}; Products(u,v,n+1) consists of u and v multiplied on the left of every exact length-n product. W is its complex linear span. P is the span of 1, uv, (uv)^2 and (uv)^3. The two closure hypotheses are left multiplication by uv and vu on every member of P.
The proof places even and odd word spaces in P and uP. Invertible multiplication exhibits one, two, three and four independent words at lengths zero through three. Rank monotonicity and the invariant space give every later length. This theorem concerns terminal operator spans and supplies no measured history, physical implementation or independent coherent archive.
Theorem 1.2 (Nonzero generator scaling).
Proof. Machine-checked in Lean as D5/S3/Quantum/QuantumChannels/TwoInvolutionWordRank.wordSpace_scale (✓ std3). ∎
Source. Repository-derived.
Commentary.
Independent nonzero complex weights preserve each homogeneous span. The lifted balanced five-mode rank follows after removing these weights.
Theorem 1.3 (Exact algebra transport).
Proof. Machine-checked in Lean as D5/S3/Quantum/QuantumChannels/TwoInvolutionWordRank.wordSpace_map (✓ std3). ∎
Source. Repository-derived.
Commentary.
A unital complex algebra homomorphism maps the entire exact-length product set, including the empty product. In the lifted balanced five-mode rank formula, injectivity is needed there to preserve dimension.