phi_conjugate_neg
plain-language theorem explainer
The theorem establishes that the algebraic conjugate of the golden ratio is strictly negative. Researchers deriving the uniqueness of the positive self-similar fixed point in the Recognition Science forcing chain cite this fact to select the appropriate root for the phi-ladder. The short tactic proof unfolds the explicit quadratic definition and applies elementary real inequalities on the square root of five.
Claim. Let $r$ satisfy the fixed-point equation $r^2 = r + 1$. The secondary root satisfies $r < 0$.
background
The PhiEmergence module derives the golden ratio from J-cost minimization under the Recognition Composition Law. The conjugate is the secondary root of the quadratic $r^2 = r + 1$ that arises once J-uniqueness fixes the self-similar solution. Upstream structures supply the J-cost definition in PhiForcingDerived and the ledger factorization in DAlembert.LedgerFactorization that calibrate the underlying functional equation.
proof idea
The proof unfolds the conjugate definition, establishes sqrt(5) > 1 by squaring and applying nlinarith to nonnegativity and square inequalities, then concludes negativity by linarith.
why it matters
This algebraic sign fact supports the uniqueness theorem for the positive solution to the fixed-point equation, which is required before constructing the phi-ladder and mass formulas. It closes a basic prerequisite in the T5-T6 segment of the forcing chain so that only the positive root enters self-similarity and dimension derivations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.