charAnomaly
plain-language theorem explainer
The character anomaly of a 2×2 real transfer matrix is half its trace minus one. It is the conjugation-invariant scalar of a seam-closure holonomy, normalized to vanish at the identity. Downstream theorems identify it with the T5 J-cost on balanced transfers and with phase cost on rotations. The body is a one-line arithmetic definition.
Claim. For a real $2\times 2$ matrix $W$, the character anomaly is $\mathrm{Tr}(W)/2 - 1$.
background
SeamTransferCore implements LEG-B Phase B of the Scale-Holonomy Trace Core: the per-closure recognition cost of a seam crossing is read from the transfer $W$ that one closure induces on the seam's double-entry pair fiber. The panel rule is never to posit $W=\mathrm{diag}(x,x^{-1})$; only a delivered-leg scaling and balance are assumed.
Balance means $\det W=1$. For a balanced transfer with a real eigenvalue $x\neq 0$, the other eigenvalue is forced to be $x^{-1}$ (product of eigenvalues equals the determinant). Cayley–Hamilton on the characteristic polynomial $\lambda^2-(\mathrm{Tr},W)\lambda+\det W$ then forces $\mathrm{Tr},W=x+x^{-1}$.
The T5 cost is $J(x)=(x+x^{-1})/2-1$ (equivalently $\cosh(\log x)-1$). The character anomaly is the same algebraic combination of the trace, written before any identification with $J$.
proof idea
Pure definition: evaluate $\mathrm{Tr}(W)/2-1$ on a $2\times 2$ real matrix. No lemmas, no tactics. Downstream equalities unfold this abbreviation and rewrite the trace via balance and Cayley–Hamilton.
why it matters
This scalar is the named per-closure cost in the Phase-B program. The theorem charAnomaly_eq_J shows that on any balanced transfer with delivered eigenvalue $x>0$ it equals $J(x)$, so $J$ emerges from determinant-one plus one real eigenvalue rather than being inserted by hand (T5 uniqueness of the cost).
It feeds ConservingSeamPricing and SeamTransferPricing, which reduce census pricing to checkable seam structure (pair-form conservation, delivered-leg eigenvalue, anomaly reading) without naming $J$ in the premise. charAnomaly_rotation identifies the elliptic class with the kernel's phase-branch cost, explaining why that branch cannot carry a genuine mismatch. Ledger discharge uses the same reading to bridge weak premises to conserving seam pricing and to witness non-vacuity via hyperbolic transfers.
It is the numeric hinge of panel Live Bet 2: n-fold retrace surpluses pair to $J(n)$ once the cost is this anomaly.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.