Cost Real Trace Root Real Trace Root Ge One

The lower bound

The real trace root is the larger solution to the quadratic equation X² - t X + 1 = 0, where t is a real number at least 2. The formula for this principal root is (t + sqrt(t² - 4)) / 2. The theorem realTraceRoot_ge_one proves that for every such t, this root is greater than or equal to 1. The proof is a short algebraic argument: the square root term is nonnegative, and adding it to t before dividing by 2 cannot push the result below 1.

This bound is the first rung on a ladder of results about the root. A companion theorem shows the root is strictly positive, and another shows that the root plus its reciprocal equals t, a property reminiscent of hyperbolic cosine addition. These facts support a multiplication law: for two parameters a and b, the root of a certain product expression equals the product of the individual roots. That law, in turn, feeds the multiplicative d'Alembert algebra, a structure built around the functional equation g(x*y) + g(x/y) = 2*g(x)*g(y) with g(1) = 1.

In Recognition Science, this root appears as the cost of a recognition event. The framework models recognition as a forced expense, and the cost function J(x) = (x + 1/x)/2 - 1 is proved unique under five plain conditions. The real trace root is the value x that makes the trace x + 1/x equal to a given t. The theorem realTraceRoot_ge_one then states that this cost never falls below 1, a floor that anchors the framework's scale and connects to the golden ratio as the unique self-similar point.

The theorem does not claim that the cost is always exactly 1; it only establishes a lower bound. It does not identify which t values occur in physical situations, nor does it assert that the root is rational or irrational for any particular t. The result is a pure inequality about a real-valued function, proved in the machine-checked library of formal theorems, and it stands independently of any physical interpretation.

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_pos {t : ℝ} (ht : 2 ≤ t) : 0 < realTraceRoot t :=
  lt_of_lt_of_le zero_lt_one (realTraceRoot_ge_one ht)

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

What this page does not claim

The theorem does not claim the root equals 1 for any t other than t = 2. The theorem does not claim anything about the rationality or irrationality of the root. The theorem does not identify which t values occur in physical recognition events.

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: