two_le_add_inv
plain-language theorem explainer
Any positive real plus its reciprocal is at least 2 (classical AM–GM). Holography cites it as the scalar engine that turns a positive delivered eigenvalue of a pairing-conserving transfer into a one-sided lower bound on the only audit invariant, the trace. The proof is a short nonlinear-arithmetic discharge from nonnegativity of (x−1)² together with x·x⁻¹=1.
Claim. For every real number $x>0$, one has $2\le x+x^{-1}$.
background
The ambient module types the R1–R4 residue of ConservingSeamPricing in its weakest honest form and shows that B2 (the deficit-free period $\beta=2\pi/\kappa$ as the unique zero of the per-cycle seam cost) survives a strict weakening of the fourth conjunct: the exact character-anomaly reading $\mathrm{Tr}(W)/2-1$ is not load-bearing for the B2 zero set.
The key new lemma in that program is a trace bound: a pairing-conserving $2\times 2$ transfer with a real positive eigenvalue $x$ satisfies $\mathrm{Tr},W=x+x^{-1}\ge 2$, with equality iff $x=1$. The present statement is the pure scalar AM–GM half of that argument; the matrix half (unimodularity from pair-form preservation, then Cayley–Hamilton balanced trace) lives upstream and is applied only at the next lemma.
No Recognition-cost $J$, no $\cosh$, and no anomaly normalization enter here: the inequality is ordinary real analysis on $\mathbb{R}_{>0}$.
proof idea
From $x>0$ obtain $x\cdot x^{-1}=1$. Feed that identity, the hypothesis $x>0$, and the square nonnegativity $(x-1)^2\ge 0$ into nonlinear arithmetic. Expanding the square against the product identity rearranges exactly to $x+x^{-1}\ge 2$. No case split and no named external lemma beyond the field inverse law.
why it matters
This is the scalar engine of the seam-ledger discharge. The immediate parent is the conserving-trace lower bound: any pairing-conserving transfer with positive delivered eigenvalue has trace at least the identity's, proved by rewriting the trace as $x+x^{-1}$ and applying the present inequality.
That bound is item (1) of the module's theorem list and feeds the forced-conditional B2 uniqueness under any calibrated faithful trace reading (item 2), and thence the bridge that recovers the full ConservingSeamPricing chain at the anomaly reading without re-proving it. In the Recognition forcing picture this is the elementary inequality that lets the unique-zero structure of B2 sit on ledger language alone, independent of the T5 $J$-cost shape until the anomaly bridge is invoked.
It does not touch the still-open B3 identification of $\kappa$ with the horizon clock, nor the physical claim that the actual seam cost satisfies LedgerClosurePricing.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.