Trace-Kernel Function Polarization
Abstract
A trace-zero matrix function with an ambient polynomial representative, mixed bidegree law and simultaneous special-unitary invariance admits a normalized coefficient polarization.
Theorem 1.1 (Mixed polarization on the trace kernel).
Proof. Machine-checked in Lean as D5/S3/Quantum/Algebra/TraceKernelFunctionPolarization.trace_kernel_function_polarization (✓ std3). ∎
Source. Repository-derived.
Commentary.
For each choice of m,n,N in the statement, the notation uses the full matrix space M, its trace-zero subtype K, the disjoint slot set J and the entry-variable set V. The superscript H denotes conjugate transpose; SU and UnitaryGroup denote the corresponding complex matrix groups. The map C embeds complex coefficients in the indicated polynomial ring; evalTwo is polynomial substitution. The symbol delta(i,j) is one when i=j and zero otherwise; identity(N) is the identity matrix. Writing a polynomial applied to an entry assignment means polynomial evaluation, and compose(T,x) sends each slot j to T(x(j)). The multi-index ones assigns exponent one to every slot, including the empty multi-index when both degrees vanish. The symbols t are the slot-polynomial variables. MultilinearMap(C,J,M,C) means complex multilinear maps with one full-matrix input per slot in J.
For every m,n ≥ 0 and N ≥ 1, an arbitrary ambient entry-polynomial representative of a trace-zero matrix function satisfying the stated mixed bidegree law and simultaneous SU(N) conjugation invariance yields a multilinear coefficient polarization on all matrix slots.
The squarefree coefficient is linear in each slot: the derivative chain rule removes one slot and expresses its coefficient as a linear sum of that slot’s entries. The two block factorials normalize the repeated inputs. The theorem recovers the original function on every repeated trace-zero pair, and records invariance under every linear map preserving the projected polynomial and under every unitary conjugation. It is a partial source bridge: the intrinsic representative correspondence and original source witness construction remain open.
The SU-circle reduction locally reuses the Tau Ceti contributors’ Apache 2.0 proof at revision d8fd630a6d98d0e5933f51cb0819ef09f28fa2b4. The full license, exact source provenance and retirement condition tied to this repository’s own Mathlib pin accompany the source.