anchorRoot_ge_one
plain-language theorem explainer
Under the anchor-free native-cost hypotheses on a ratio-orbit map F, the principal real root extracted from the doubled trace at two is at least one. Cost and character-factorization arguments cite this as the nonnegativity floor for the anchor root. The proof is a one-line reduction: feed the trace-at-two lower bound into the real-trace-root inequality.
Claim. Let $F$ be a map on rational orbits satisfying the anchor-free native-cost pack (base-sans-two, sign-reversing, monotone, and zero-calibrated doubled trace). Then the principal real root of the doubled trace of $F$ at the distinguished positive integer two obeys $1 \le \mathrm{root}(F)$.
background
In the real-character factorization of native cost, one extracts a real scalar from the doubled trace evaluated on rational displays. The rational trace sends a rational $x$ to the real display of $F$ on the corresponding ratio orbit. The anchor root is the principal real root of that trace at the distinguished positive integer two: $\mathrm{anchorRoot}(F) := \mathrm{realTraceRoot}(\mathrm{rationalTrace}, F, 2)$.
The hypothesis pack SansAnchorHypotheses is the anchor-free structural pack matching the PRC native-cost hypotheses without an external anchor: base-sans-two, sign-reversing, monotone, and zero-calibrated doubled trace. Upstream, traceDisplay_two_ge_two already gives $2 \le \mathrm{traceDisplay}, F, \mathrm{two}$ under that pack. Independently, realTraceRoot_ge_one states that any real $t \ge 2$ has principal root at least one (via nonnegativity of $\sqrt{t^2-4}$ and a linear arithmetic close).
proof idea
One-line term wrapper. Apply realTraceRoot_ge_one to the real $t = \mathrm{rationalTrace}, F, 2$. The needed inequality $2 \le t$ is obtained by simpa [rationalTrace] from traceDisplay_two_ge_two hF, which itself is the positive-integer case of the display lower bound at two. No further case splits or algebraic expansion of the root formula appear here.
why it matters
The anchor root is the distinguished positive real that seeds the real-character factorization of native cost on ratio orbits. This non-strict lower bound is the first positivity fact in that chain: downstream, anchorRoot_gt_one upgrades it to a strict inequality under a nontriviality hypothesis on the trace at two, and anchorRoot_ne_zero immediately obtains nonzero by comparing with $0 < 1$. Together those facts keep the root inside the multiplicative group of positive reals, which is required before one can treat it as a genuine character base or ladder rung in the cost factorization. In the broader Recognition setting this sits inside the cost layer that supports J-uniqueness and the native-cost uniqueness path, not yet at the T5–T8 forcing steps themselves.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.