Cost Real Trace Root Real Trace Root Add Inv

The trace root identity

The declaration realTraceRoot_add_inv proves a clean algebraic fact about a specific square-root expression. For any real number t at least 2, define the principal root of the equation X² - t X + 1 = 0, meaning the larger solution. That root is (t + √(t² - 4)) / 2. The theorem states that this root plus its reciprocal equals t. In symbols: if r = (t + √(t² - 4)) / 2, then r + 1/r = t. This is a direct consequence of the quadratic formula, and the proof in the library is a short chain of algebraic manipulations.

The identity matters because it is the bridge between the root expression and the trace of a 2x2 matrix. In the framework's ledger, a discrete record of recognition events, the cost of a recognition step is built from such traces. The theorem shows that the root r and its reciprocal always sum to the parameter t, which is exactly the trace condition that the framework's cost function must satisfy. This is not a physical claim; it is a purely mathematical lemma that the framework's library uses as a stepping stone.

The library also proves related properties: the root is at least 1 when t ≥ 2, it equals 1 when t = 2, and it is always positive. A separate theorem shows that the root of a product of two such parameters equals the product of the individual roots, under a specific formula for the product parameter. These are all classical algebraic facts, verified in the machine-checked library of formal theorems, and they support the framework's derivation of the cost function J(x) = (x + 1/x)/2 - 1.

What the declaration does not claim is anything about physics or measurement. It does not assert that any physical quantity equals this root, nor does it assign a numerical value to t. The theorem is conditional: it holds for any real t ≥ 2, and it says nothing about which t, if any, nature chooses. The framework's later steps, which connect this algebra to the golden ratio and to physical constants, are separate claims with their own evidence. This lemma is just the algebraic foundation, not the physical conclusion.

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

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_one : realTraceRoot 2 = 1 := by
  simp [realTraceRoot, show (2 : ℝ) ^ 2 - 4 = 0 by norm_num, Real.sqrt_zero]

theorem realTraceRoot_pos {t : ℝ} (ht : 2 ≤ t) : 0 < realTraceRoot t :=
  lt_of_lt_of_le zero_lt_one (realTraceRoot_ge_one ht)

/-- **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

What this page does not claim

This declaration does not assign any physical meaning or numerical value to the parameter t. This declaration does not assert that any measured physical quantity equals the trace root. This declaration does not by itself derive the golden ratio or any physical constant.

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: