anchorRoot
plain-language theorem explainer
Principal real root (≥ 1) of X² − tX + 1 = 0, where t is the doubled trace of a ratio-orbit map F at the distinguished integer 2. Cited by anyone factoring real characters of cost maps or classifying gauge orbits via integer exponents. One-line composition of the principal-root extractor with the rational doubled-trace display at 2.
Claim. For a map $F$ on ratio orbits, the anchor root is the principal real number $\ge 1$ solving $X^2 - t X + 1 = 0$, where $t$ is the doubled trace of $F$ evaluated at the rational display of $2$. Explicitly, $\mathrm{anchorRoot}(F) = \bigl(t + \sqrt{t^2-4}\bigr)/2$ with $t = \mathrm{rationalTrace}(F,2)$.
background
Ratio orbits are the primitive rational displays of Recognition Calculus: an integer numerator over a nonzero distinction-denominator. The distinguished orbit two is the ratio orbit of the positive integer 2. Cost maps act on these orbits; their doubled trace at a rational display is the honest real-valued function rationalTrace F x, obtained by pushing the rational through the orbit embedding and reading the trace display.
When that trace value $t$ satisfies $t \ge 2$, the quadratic $X^2 - t X + 1 = 0$ has two real roots reciprocal to each other. The principal root extractor realTraceRoot selects the one that is at least 1: $(t + \sqrt{t^2-4})/2$. This is the classical Chebyshev/cosh generator for multiplicative characters on the positive reals (the same algebraic seed that underlies the J-cost fixed-point structure and the Recognition Composition Law).
The local module builds a real-character factorization of cost maps that obey the sans-anchor hypotheses (RCL-type identities without presupposing a preferred base). The anchor root is the nondegenerate symbolic extraction of that seed from the trace at two.
proof idea
Pure definitional composition, no proof obligations. Evaluate the doubled rational trace of $F$ at the integer 2, then feed that real number into the principal-root constructor for $X^2 - tX + 1 = 0$. The body is exactly realTraceRoot (rationalTrace F 2).
why it matters
This is the numerical seed that turns a cost map's trace data into a genuine multiplicative character. Downstream lemmas immediately record the basic algebraic facts: the root is ≥ 1 (and > 1 when the trace is nontrivially larger than 2), nonzero, satisfies root + 1/root = trace-at-two, and has square-minus-one nonzero under nondegeneracy.
Those facts feed nontrivialCharacterValue and, crucially, exists_nat_exponent in GaugeOrbitClassification: Howe supplies a real exponent, the anchor root forces positivity, and the six-exponentials input upgrades it to a positive integer. That integer-exponent theorem is the only place the six-exponentials import is used, so the anchor root is the bridge from continuous character data to discrete rung structure on the phi-ladder. It sits inside the cost-uniqueness stream that ultimately supports T5 J-uniqueness and the native cost factorization.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.