Cost Real Trace Root

The trace root

The cost real trace root is a function that takes a real number t and returns the larger solution of the quadratic equation X² - tX + 1 = 0. For any t at least 2, the formula is (t + √(t² - 4)) / 2. At t = 2 the root equals 1, and for larger t it grows smoothly. The name comes from linear algebra: for a 2x2 matrix with trace t and determinant 1, this root is the larger eigenvalue, the one that dominates under repeated multiplication.

This object appears throughout classical mathematics. The equation X² - tX + 1 = 0 is the characteristic equation of a hyperbolic rotation, and its roots are the eigenvalues e^±θ where t = 2cosh(θ). The root itself is then e^θ, the expansion factor of the rotation. When t = 3, the root is (3 + √5)/2 ≈ 2.618, the square of the golden ratio. When t = φ + 1/φ = √5, the root is φ itself, the golden ratio, which solves X² - X - 1 = 0. These connections tie the trace root to the geometry of pentagons and to continued fractions.

The framework's library proves three structural facts about this root. First, the root is always at least 1 for t ≥ 2, so it picks the principal branch. Second, the root satisfies the identity r + 1/r = t, which is just the original equation rearranged. Third, and most importantly, the root turns multiplication of traces into multiplication of roots: if u is built from a and b by the formula u = (ab + √(a²-4)√(b²-4))/2, then the root of u equals the product of the roots of a and b. This is the cosh addition formula in disguise, and it is what makes the trace root a natural unit for composing costs.

In Recognition Science, the ledger, a discrete record of recognition events, assigns a cost to each event, and the cost function must satisfy a forced composition law. The library shows that the trace root is the right coordinate for that law. A separate theorem proves that any function g satisfying g(xy) + g(x/y) = 2g(x)g(y) with g(1) = 1 must obey the duplication identity g(x²) = 2g(x)² - 1. From this, the library derives that the quantity (g(x) - g(1/x))² equals 4(g(x)² - 1)(g(1/x)² - 1), exactly the difference-square identity that the trace root satisfies. In doubled-trace units, where T(1) = 2, the same identity reads (T(xy) - T(x/y))² = (T(x)² - 4)(T(y)² - 4).

What this establishes is that the trace root is not an arbitrary convenience. It is the unique coordinate in which the composition law becomes multiplication, the same way logarithms turn multiplication into addition. The machine-checked library proves these identities from the composition law alone, with no extra assumptions about the cost function. This means the trace root is the natural language for describing how costs combine, and it is the reason the framework's later results, such as the golden ratio as the unique self-similar scaling, can be derived at all.

/-- The principal (≥ 1) root of `X² - t X + 1 = 0`, for `t ≥ 2`. -/
noncomputable def realTraceRoot (t : ℝ) : ℝ :=
  (t + Real.sqrt (t ^ 2 - 4)) / 2

theorem realTraceRoot_ge_one {t : ℝ} (ht : 2 ≤ t) : 1 ≤ realTraceRoot t := by
  have hs : 0 ≤ Real.sqrt (t ^ 2 - 4) := Real.sqrt_nonneg _
  simp only [realTraceRoot]
  linarith

theorem realTraceRoot_add_inv {t : ℝ} (ht : 2 ≤ t) :
    realTraceRoot t + (realTraceRoot t)⁻¹ = t := by
  have hsq : Real.sqrt (t ^ 2 - 4) ^ 2 = t ^ 2 - 4 :=
    Real.sq_sqrt (realTraceRoot_sq_sub_four_nonneg ht)
  have hne : realTraceRoot t ≠ 0 := ne_of_gt (realTraceRoot_pos ht)
  have hinv : (realTraceRoot t)⁻¹ = (t - Real.sqrt (t ^ 2 - 4)) / 2 := by
    have hprod :
        realTraceRoot t * ((t - Real.sqrt (t ^ 2 - 4)) / 2) = 1 := by
      simp only [realTraceRoot]
      field_simp
      nlinarith [hsq]
    have := congrArg (fun z : ℝ => z / realTraceRoot t) hprod
    field_simp [hne] at this ⊢
    linarith
  rw [hinv]
  simp only [realTraceRoot]
  ring

/-- **Multiplication of principal branches.** If `a, b ≥ 2` and
`u = (a b + √(a²−4)√(b²−4))/2`, then
`realTraceRoot u = realTraceRoot a * realTraceRoot b`. -/
theorem realTraceRoot_mul {a b : ℝ} (ha : 2 ≤ a) (hb : 2 ≤ b) :
    realTraceRoot ((a * b + Real.sqrt (a ^ 2 - 4) * Real.sqrt (b ^ 2 - 4)) / 2) =
      realTraceRoot a * realTraceRoot b := by
  set sa := Real.sqrt (a ^ 2 - 4)
  set sb := Real.sqrt (b ^ 2 - 4)
  have hsa : 0 ≤ sa := Real.sqrt_nonneg _
  have hsb : 0 ≤ sb := Real.sqrt_nonneg _
  have hsqa : sa ^ 2 = a ^ 2 - 4 := by
    simpa [sa] using Real.sq_sqrt (realTraceRoot_sq_sub_four_nonneg ha)
  have hsqb : sb ^ 2 = b ^ 2 - 4 := by
    simpa [sb] using Real.sq_sqrt (realTraceRoot_sq_sub_four_nonneg hb)
  set u := (a * b + sa * sb) / 2
  -- √(u² − 4) = (a sb + b sa) / 2
  have hdisc : u ^ 2 - 4 = ((a * sb + b * sa) / 2) ^ 2 := by
    have h : 4 * (u ^ 2 - 4) = (a * sb + b * sa) ^ 2 := by
      simp only [u]
      nlinarith [hsqa, hsqb]
    have h4 : (4 : ℝ) ≠ 0 := by norm_num
    calc
      u ^ 2 - 4 = (4 * (u ^ 2 - 4)) / 4 := by ring
      _ = (a * sb + b * sa) ^ 2 / 4 := by rw [h]
      _ = ((a * sb + b * sa) / 2) ^ 2 := by ring
  have hsqrt : Real.sqrt (u ^ 2 - 4) = (a * sb + b * sa) / 2 := by
    have hnn : 0 ≤ (a * sb + b * sa) / 2 := by positivity
    rw [hdisc]
    exact Real.sqrt_sq hnn
  -- both sides equal (ab + a sb + b sa + sa sb) / 4
  simp only [realTraceRoot, hsqrt, u, sa, sb]
  field_simp
  ring

/-- **Multiplicative duplication.** From the product law at `(x, x)` with `g 1 = 1`. -/
theorem mulDAlembert_duplication {g : ℝ → ℝ}
    (hd : ∀ x y, x ≠ 0 → y ≠ 0 → g (x * y) + g (x / y) = 2 * g x * g y)
    (h1 : g 1 = 1) :
    ∀ x, x ≠ 0 → g (x * x) = 2 * (g x) ^ 2 - 1 := by
  intro x hx
  have h := hd x x hx hx
  rw [div_self hx, h1] at h
  linarith

What this page does not claim

The trace root is not claimed to be the cost function itself, only a coordinate for composing costs. The duplication identity does not by itself force the golden ratio; it is one step in a longer chain. No claim is made that the trace root is derived from the five cost conditions; it is defined independently and shown to satisfy the composition identities.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Cost/RealTraceRoot.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: