IndisputableMonolith.Cost.RealTraceRoot
Defines the principal real root ≥ 1 of X² - tX + 1 = 0 for traces t ≥ 2, plus positivity, inversion, and d'Alembert product identities. Cost and real-character arguments cite it to lift a trace to a unique multiplicative coordinate. Development is definition-first with short algebraic lemmas on the closed-form root.
claimFor $t \geq 2$, let $\rho(t) \geq 1$ be the unique real solution of $X^2 - t X + 1 = 0$ (equivalently $\rho(t) = (t + \sqrt{t^2-4})/2$). The module records $\rho(t) + \rho(t)^{-1} = t$, $\rho(t) > 0$, multiplicativity under trace products, and related d'Alembert duplication and difference-square identities.
background
In the Cost layer, real traces arise as $t = x + x^{-1}$ for $x > 0$. Recovering the larger factor $x \geq 1$ is exactly solving $X^2 - tX + 1 = 0$. The discriminant $t^2 - 4$ is nonnegative precisely when $t \geq 2$, so a real principal root exists on that ray.
The module names that root realTraceRoot and packages the elementary calculus around it: square-minus-four nonnegativity, the normalization $\rho(2) = 1$, positivity and $\rho \geq 1$, the inversion identity $\rho + \rho^{-1} = t$, and multiplicative d'Alembert formulas that turn products and differences of traces back into traces. These are the standard Chebyshev/SL(2) relations written in root form.
Only Mathlib is imported; the consumer is the real-character factorization module.
proof idea
Definition module centered on the closed-form larger root $(t + \sqrt{t^2-4})/2$. Lemmas are short algebraic checks: discriminant nonnegativity for $t \geq 2$, direct substitution for the sum-with-inverse identity, and ring/nlinarith-style verifications of the d'Alembert product, duplication, and difference-square formulas. No deep induction or analysis; each sibling is a one- or few-line identity on the explicit radical.
why it matters in Recognition Science
Supplies the canonical multiplicative lift used by RealCharacterFactorization (the sole direct importer). In the RS cost stack that lift converts additive trace data into a coordinate compatible with character factorization and, downstream, with ladder and J-cost constructions. Without a fixed principal root $\geq 1$, real characters would lack a unique positive real factor, blocking unique factorization statements that feed mass and rung formulas.
scope and limits
- Does not treat the reciprocal root in (0,1] as a separate object.
- Does not define or analyze complex traces or |t| < 2.
- Does not itself mention J-cost, phi, or the forcing chain.
- Does not prove character identities; only the scalar root calculus.
- Does not address numerical approximation or floating-point roots.
used by (1)
declarations in this module (12)
-
def
realTraceRoot -
theorem
realTraceRoot_sq_sub_four_nonneg -
theorem
realTraceRoot_one -
theorem
realTraceRoot_ge_one -
theorem
realTraceRoot_pos -
theorem
realTraceRoot_add_inv -
theorem
realTraceRoot_mul -
theorem
larger_trace_of_diff_sq -
theorem
mulDAlembert_duplication -
theorem
mulDAlembert_prod -
theorem
mulDAlembert_diff_sq -
theorem
mulDAlembert_diff_sq_trace