conserving_trace_ge_two
plain-language theorem explainer
Any 2×2 real transfer that preserves the pairing form and admits a positive real eigenvalue x has matrix trace at least 2. Holography and seam-ledger arguments cite this as the inequality half of the conserving-trace bound that separates deficit-free delivery from mismatch. The proof rewrites the trace as x + x⁻¹ via the conserving-trace identity, then applies the elementary AM–GM lower bound on that sum.
Claim. Let $W$ be a $2\times 2$ real matrix that preserves the pairing form: $\mathrm{pair}(Wu,Wv)=\mathrm{pair}(u,v)$ for all vectors $u,v$. If $W$ has a real eigenvalue $x>0$, then $\mathrm{Tr}\,W\ge 2$.
background
This module types the R1–R4 seam-ledger residue in its weakest honest form and shows that B2 (uniqueness of the deficit-free period as the unique zero of per-cycle seam cost) survives without loading the exact character-anomaly reading $\mathrm{Tr}(W)/2-1$. The key algebraic fact is that pairing conservation forces unimodularity, so a conserving transfer with positive real eigenvalue has trace equal to $x+x^{-1}$.
The pairing form is the bilinear form on $\mathbb{R}^2$ that the seam transfer is required to preserve (ledger conservation). HasRealEigen asserts that $x$ is a genuine real eigenvalue of $W$. Upstream, the sibling identity equates the conserving trace to $x+x^{-1}$; the elementary bound $x+x^{-1}\ge 2$ for $x>0$ is the classical AM–GM (or $(x-1)^2\ge 0$) fact used here.
Locally this sits under Holography.SeamLedgerDischarge: the inequality is the half of the bundled conserving-trace bound that lets any calibrated faithful trace reading, not only the anomaly normalization, separate unit delivery from mismatch.
proof idea
One-line rewrite plus a pure inequality. First apply the sibling identity that any pairing-conserving $W$ with positive real eigenvalue $x$ satisfies $\mathrm{Tr},W=x+x^{-1}$. Then discharge the goal by the elementary lemma $2\le x+x^{-1}$ for $x>0$ (AM–GM / expansion of $(x-1)^2\ge 0$). No matrix algebra beyond that identity is reopened in this proof.
why it matters
This is the inequality half of the module's key new lemma. Downstream, conserving_trace_bound packages it with the equality $\mathrm{Tr},W=x+x^{-1}$ and the equality case $\mathrm{Tr},W=2\Leftrightarrow x=1$, which is what lets B2 discharge on any calibrated faithful trace reading rather than only the character anomaly.
The parent uniqueness theorem uses the bound explicitly: off the deficit-free period the turn ratio is not 1, so the conserving trace is strictly above 2 and faithfulness forbids a cost zero; at the period the trace hits 2 and calibration fires. That is the forced-conditional B2 statement under LedgerClosurePricing.
In the Recognition chain this supports the seam-cost zero-set without invoking J or cosh in the weak premise, while the bridge back to ConservingSeamPricing recovers the full $C=J(\mathrm{turnRatio})$ route. B3 (identifying $\kappa$ with the horizon clock) and physical instantiation of LedgerClosurePricing remain open; this lemma does not touch those.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.