frobeniusNormSq
plain-language theorem explainer
Frobenius norm-squared of a pure two-qubit amplitude matrix: the double sum of entrywise |A_ij|². Anyone citing pure-state normalization or the reduced-density trace identity in Track 2.B uses this. It is a one-line definition via Complex.normSq, so the unit-norm condition stays algebraic over ℝ.
Claim. For a $2\times 2$ complex amplitude matrix $A$, the Frobenius norm-squared is $\|A\|_F^2 := \sum_{i,j}\lvert A_{ij}\rvert^2$, computed as the sum of `Complex.normSq` on each entry.
background
Track 2.B treats a pure two-qubit state through its amplitude matrix $A:\mathrm{Fin},2\times\mathrm{Fin},2\to\mathbb{C}$. Normalization means $\sum_{ij}\lvert A_{ij}\rvert^2=1$. The Wootters concurrence is $C(A)=2\lvert\det A\rvert$, and the first-qubit reduced density is $\rho_1=A A^\dagger$ (partial trace over the second qubit).
The Frobenius quantity is the natural real scalar that makes those statements algebraic: it is exactly the squared Hilbert–Schmidt norm of $A$. Sibling lemmas equate $\mathrm{tr}(\rho_1)$ to this norm-squared, so a normalized pure state has $\mathrm{tr}(\rho_1)=1$ without leaving the ring of real polynomials in the real and imaginary parts of the entries.
Related squared-norm helpers appear in the primitive recognition calculus (finite amplitude vectors and Hilbert displays). Those are the same idea on different carriers; here the carrier is the $2\times 2$ complex matrix of two-qubit amplitudes.
proof idea
Pure definition: unfold to the double finite sum $\sum_i\sum_j\mathrm{Complex.normSq}(A,i,j)$. No lemmas, no tactics. Downstream proofs simply rw or simp this unfold when they need $\mathrm{tr}(\rho_1)=|A|_F^2$.
why it matters
Locally it is the scalar that closes the reduced-density step of Track 2.B: siblings reducedDensity_trace_eq_frobenius and reducedDensity_trace_eq_one_of_normalized turn unit Frobenius norm into $\mathrm{tr}(\rho_1)=1$, which feeds the eigenvalue formula $(\lambda_\pm=(1\pm\sqrt{1-C^2})/2)$ and thence strict positivity of von Neumann entropy whenever $C>0$.
The module status is structural theorem, no new RS assumptions. The same Frobenius pattern appears on $4\times 4$ real matrices in the Regge/continuum TT analysis (preflight scale gates, axis normalizations equal to 2, exact-$J$ bridge to the EH face). Those are parallel definitions, not dependents of this one; the shared name records a common algebraic habit across quantum and gravity tracks.
No open scaffold: Track 2.B is marked closed once concurrence, reduced-density eigenvalues, and binary-entropy positivity are composed.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.