realTraceRoot
plain-language theorem explainer
Principal real root of the reciprocal quadratic X² - tX + 1 = 0, chosen ≥ 1 for every t ≥ 2. Cited by anyone working real characters of ratio orbits, d'Alembert products on traces, or the real skeleton of J-cost. Definition is the closed-form half-sum of t and √(t² - 4).
Claim. For $t \in \mathbb{R}$, set $\rho(t) := \dfrac{t + \sqrt{t^2 - 4}}{2}$. When $t \ge 2$ this is the unique root of $X^2 - tX + 1 = 0$ satisfying $\rho(t) \ge 1$.
background
Recognition Science builds cost from the unique J obeying the Recognition Composition Law. On the reals the natural generators are reciprocal quadratics $X^2 - tX + 1$, whose roots form inverse pairs. The larger (principal) root is the coordinate in which multiplicative characters and d'Alembert composition identities become transparent.
This module isolates that principal branch as a single real function so later factorizations (anchor roots, native-cost ledgers) quote one closed form instead of re-deriving the quadratic formula. Companion lemmas then record positivity, the identity $\rho(t) + \rho(t)^{-1} = t$, and multiplicativity under the d'Alembert product of traces.
proof idea
Pure definition: the body is the standard closed-form expression for the larger root of $X^2 - tX + 1 = 0$. Noncomputable solely because real square root is noncomputable; no further proof obligations.
why it matters
Supplies the real-analytic skeleton for the local algebraic suite: value 1 at trace 2, lower bound ≥ 1, positivity, the inversion identity $\rho + \rho^{-1} = t$, and multiplicativity under the d'Alembert product of traces ≥ 2. Downstream, anchorRoot specializes the same formula at the distinguished positive-integer trace coming from a ratio-orbit endomorphism, and the primitive recognition calculus invokes it to show a cube-generated native cost is not canonical. The construction is the concrete real character underlying J-uniqueness (T5) when restricted to positive real traces.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.