phi_conjugate_neg
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.
claimLet $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 in Recognition Science
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.
scope and limits
- Does not claim any bound on the magnitude of the conjugate.
- Does not connect the sign result to physical constants or spatial dimensions.
- Does not address other roots of higher-degree equations.
formal statement (Lean)
48theorem phi_conjugate_neg : φ_conjugate < 0 := by
proof body
Tactic-mode proof.
49 unfold φ_conjugate
50 have h : Real.sqrt 5 > 1 := by
51 have h1 : Real.sqrt 5 ^ 2 = 5 := Real.sq_sqrt (by norm_num : (5 : ℝ) ≥ 0)
52 nlinarith [Real.sqrt_nonneg 5, sq_nonneg (Real.sqrt 5 - 1)]
53 linarith
54
55/-! ## Uniqueness of φ -/
56
57/-- **THEOREM**: φ is the unique positive solution to r² = r + 1. -/