conserving_trace_eq_two_iff
plain-language theorem explainer
For a pairing-conserving real 2×2 transfer with positive real eigenvalue x, the trace equals 2 exactly when x = 1. This is the equality case that isolates the deficit-free seam period on the audit invariant alone. Anyone discharging B2 under weak ledger-closure pricing cites it. Proof: rewrite the trace as x + x⁻¹, then apply the elementary two-sided AM–GM equality criterion.
Claim. Let $W$ be a $2\times 2$ real matrix that preserves the bilinear pairing form under left action, and let $x>0$ be a real eigenvalue of $W$. Then $\operatorname{Tr} W = 2$ if and only if $x = 1$.
background
In the seam-ledger setting a transfer $W:\mathbb{R}^2\to\mathbb{R}^2$ is pairing-conserving when it leaves the fixed bilinear form invariant: $\mathrm{pairForm}(Wu,Wv)=\mathrm{pairForm}(u,v)$ for all vectors. Ledger conservation of that pairing is equivalent to unimodularity ($\det W=1$). For such $W$ with a positive real eigenvalue $x$, Cayley–Hamilton forces the companion eigenvalue to be $x^{-1}$, so the trace is the balanced sum $x+x^{-1}$.
This module weakens the fourth conjunct of ConservingSeamPricing: the exact character-anomaly reading $\operatorname{Tr}(W)/2-1$ is not load-bearing for the B2 zero set. Only the audit invariant $\operatorname{Tr} W$ is needed, once it is known when that invariant hits the calibration value 2.
Upstream, the elementary identity $x+x^{-1}=2\Leftrightarrow x=1$ (for $x>0$) is already available as a pure real-analysis fact; the conserving-trace identity supplies the bridge from matrix data to that scalar criterion.
proof idea
Two-step rewrite. First apply the sibling identity that any pairing-conserving $W$ with positive real eigenvalue $x$ has $\operatorname{Tr} W=x+x^{-1}$. The goal collapses to $x+x^{-1}=2\Leftrightarrow x=1$. Discharge that by the elementary lemma add_inv_eq_two_iff at the positivity hypothesis on $x$. No further matrix algebra is required.
why it matters
Doc-comment frames this as the entire zero-set content of B2, expressed on the audit invariant alone: the trace hits 2 exactly at unit delivery. It is packaged into the bundled key lemma conserving_trace_bound (trace identity, lower bound $\ge 2$, and this iff), which is what lets the discharge run on any calibrated faithful trace reading, not just the character anomaly.
Downstream, b2_unique_zero_of_ledgerClosure uses the bound: off the deficit-free period the turn ratio differs from 1, so the trace is strictly above 2 and faithfulness forbids a zero; at the period the ratio is 1, the trace is exactly 2, and calibration fires. That is the forced-conditional B2 statement under the weak residue LedgerClosurePricing.
Within the Recognition holography chain this closes the R1–R4 typing of ConservingSeamPricing without re-proving the older anomaly route. B3 (identifying $\kappa$ with the horizon clock) and physical instantiation of LedgerClosurePricing remain open; this lemma does not touch them.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.