Cost Real Trace Root Larger Trace Of Diff Sq

The larger trace

For a real number t at least 2, consider the quadratic equation x² - t x + 1 = 0. Its two roots multiply to 1, so they are reciprocals. One root is at least 1, the other at most 1. The principal root, called the trace root, is the one at least 1, given by the formula (t + √(t² - 4)) / 2. This is a standard piece of algebra, no framework needed.

The classical background goes back to the hyperbolic cosine: cosh(y) satisfies cosh(2y) = 2 cosh²(y) - 1, and the trace root behaves like a discrete version of that doubling. If you set t = 2 cosh(y), then the trace root is e^y. The equation x² - t x + 1 = 0 is the characteristic equation of a 2-by-2 matrix with trace t and determinant 1, so its roots are the eigenvalues. The principal root is the larger eigenvalue, the one that dominates under repeated multiplication.

In Recognition Science, the framework models a ledger, a discrete record of recognition events, and proves that any cost function satisfying five plain conditions must equal J(x) = (x + 1/x)/2 - 1. A key step is showing that the cost function's values on products and quotients obey a multiplicative d'Alembert equation: T(x*y) + T(x/y) = T(x) * T(y), with T(1) = 2. The theorem larger_trace_of_diff_sq is the algebraic core of that step. It says: if u + v = a*b and (u - v)² = (a² - 4)(b² - 4), with v ≤ u, then u = (a*b + √(a² - 4)√(b² - 4)) / 2. In plain language, given the sum and the squared difference of two numbers, the larger one is forced to be exactly the principal trace root of the product a*b.

This is a pure algebra theorem, proved in the framework's machine-checked library of formal theorems. It does not by itself derive the cost function, nor does it prove the d'Alembert equation holds for any particular T. Those are separate steps. The theorem only resolves a uniqueness question: when two candidate values satisfy the sum and difference-square constraints, the larger one is pinned down. It is a lemma in a longer chain, not the chain itself.

The consequence is that the framework's cost function is not free to wander: the larger trace is uniquely determined by the product of two inputs. This is what makes the composition law forced rather than chosen. The reader can now see why the framework's central theorem has a chance of being unique: at each step, the algebra leaves no room for alternatives.

/-- Given `u + v = a b` and `(u - v)² = (a²−4)(b²−4)` with `v ≤ u`, the larger
trace is the cosh-addition value. -/
theorem larger_trace_of_diff_sq {a b u v : ℝ}
    (ha : 2 ≤ a) (hb : 2 ≤ b)
    (hsum : u + v = a * b)
    (hdiffsq : (u - v) ^ 2 = (a ^ 2 - 4) * (b ^ 2 - 4))
    (hulev : v ≤ u) :
    u = (a * b + Real.sqrt (a ^ 2 - 4) * Real.sqrt (b ^ 2 - 4)) / 2 := by
  have hnonnega : 0 ≤ a ^ 2 - 4 := realTraceRoot_sq_sub_four_nonneg ha
  have hprod_sqrt :
      Real.sqrt ((a ^ 2 - 4) * (b ^ 2 - 4)) =
        Real.sqrt (a ^ 2 - 4) * Real.sqrt (b ^ 2 - 4) :=
    Real.sqrt_mul hnonnega (b ^ 2 - 4)
  have huv : u - v = Real.sqrt (a ^ 2 - 4) * Real.sqrt (b ^ 2 - 4) := by
    have := congrArg Real.sqrt hdiffsq
    rwa [Real.sqrt_sq (sub_nonneg.mpr hulev), hprod_sqrt] at this
  linarith

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

What this page does not claim

This theorem does not prove the d'Alembert equation holds for any specific function T. This theorem does not derive the cost function J(x). This theorem does not establish any physical consequence about 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: