IndisputableMonolith.Cost.RealTraceRoot
Defines the principal real root (≥ 1) of the monic reciprocal quadratic X² − t X + 1 = 0 for real t ≥ 2, together with its elementary algebraic identities. Cost and character-factorization developments cite it whenever a positive real with product-one conjugate is needed. The module is mostly definitional plus short positivity and multiplicative lemmas.
claimFor each real $t \ge 2$, let $\rho(t)$ be the unique root of $X^2 - t X + 1 = 0$ satisfying $\rho(t) \ge 1$. Then $\rho(t) = \frac{t + \sqrt{t^2 - 4}}{2}$, $\rho(t) + \rho(t)^{-1} = t$, $\rho(t) \rho(t)^{-1} = 1$, and $\rho$ is multiplicative on the corresponding d'Alembert (trace) product.
background
In the Cost layer, many identities are written in terms of a real trace parameter $t = x + x^{-1}$ with $x > 0$. The quadratic $X^2 - t X + 1 = 0$ is the minimal monic reciprocal equation whose roots are exactly that pair ${x, x^{-1}}$. When $t \ge 2$ the discriminant $t^2 - 4$ is nonnegative and the larger root is at least 1.
The module therefore packages that larger root as a single real-valued function (the principal trace root) and records the elementary consequences: square of the root minus four is nonnegative, the value at $t = 2$ is 1, positivity, the sum-with-inverse identity, and the multiplicative law that corresponds to the d'Alembert / Chebyshev addition formula for traces.
These facts sit upstream of real character factorizations used later in the cost calculus; they do not yet invoke the J-cost functional or the forcing chain, only the reciprocal quadratic geometry.
proof idea
Definition module. The root is introduced by the closed-form expression involving the nonnegative square root of $t^2 - 4$. Subsequent lemmas are short algebraic verifications: direct substitution into the quadratic, discriminant nonnegativity for $t \ge 2$, evaluation at the boundary $t = 2$, comparison with 1, and the multiplicative identities obtained by expanding products of roots (or equivalently by the d'Alembert duplication and product formulae for the trace).
why it matters in Recognition Science
Supplies the canonical positive real lift from a trace $t \ge 2$ back to a principal factor $\ge 1$. The immediate consumer is the RealCharacterFactorization module, which imports this file to factor real characters or cost expressions into reciprocal pairs. In the broader Recognition Science cost calculus such factorizations keep J-cost identities and composition-law arguments on the positive ray, consistent with the self-similar $\phi$-ladder geometry, without yet committing to the full T5–T8 forcing chain.
scope and limits
- Does not define or use the J-cost functional itself.
- Does not treat complex or |t| < 2 traces.
- Does not prove uniqueness of factorizations beyond the quadratic root.
- Does not connect the root to the golden ratio or eight-tick structure.
- Does not address discrete rung or mass-ladder applications.
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