Cost Geometric Root Jcost Chain Excess Identity

The chaining identity

The cost function J(x) = (x+1/x)/2 - 1 measures the price of a recognition event, where x is the ratio between two quantities being compared. The identity in question states that when you chain two events, the total cost is not simply the sum of the individual costs. There is an extra term, a positive excess that depends on the magnitudes of the steps being chained.

In symbols, the identity reads J(e^(a+b)) = J(e^a) + J(e^b) + J(e^a)·J(e^b) + sinh(a)·sinh(b). The first three terms on the right are what you would get from a simple multiplicative composition. The final term, sinh(a)·sinh(b), is the excess. When a and b have the same sign, this excess is nonnegative, and it is strictly positive when both are nonzero. Chaining two distinctions always costs strictly more than the sum of its parts.

This excess has a direct consequence. If you try to split a fixed distinction into arbitrarily fine micro-steps, the total cost of all those micro-steps tends to zero. The identity shows that a ledger, a discrete record of events, that could be infinitely refined would not be able to sustain any positive cost floor. Contrapositively, a ledger with an irreducible cost floor is forced to forbid refinement beyond a certain finite number of steps. Discreteness is not assumed; it is a consequence of having a positive cost at all.

In Recognition Science, this identity is a proved theorem in a machine-checked library of formal theorems. It is part of a chain that aims to show that the golden ratio emerges as the unique self-similar scaling. However, the identity itself does not complete that chain. The final step, deriving the closure condition of a geometric ladder from this excess, remains an open research leg. The identity establishes the excess and its consequences, but it does not, by itself, force the golden ratio.

/-- **The chaining identity.** The cost of a chained distinction exceeds the
sum of its parts by an exactly computable excess:
`J(e^{a+b}) = J(e^a) + J(e^b) + J(e^a)·J(e^b) + sinh a·sinh b`. -/
theorem jcost_chain_excess_identity (a b : ℝ) :
    Jcost (Real.exp (a + b))
      = Jcost (Real.exp a) + Jcost (Real.exp b)
        + Jcost (Real.exp a) * Jcost (Real.exp b) + Real.sinh a * Real.sinh b := by
  have h1 : Jcost (Real.exp (a + b)) = Real.cosh (a + b) - 1 := by
    have h := FunctionalEquation.Jcost_G_eq_cosh_sub_one (a + b)
    simpa [FunctionalEquation.G] using h
  have h2 : Jcost (Real.exp a) = Real.cosh a - 1 := by
    have h := FunctionalEquation.Jcost_G_eq_cosh_sub_one a
    simpa [FunctionalEquation.G] using h
  have h3 : Jcost (Real.exp b) = Real.cosh b - 1 := by
    have h := FunctionalEquation.Jcost_G_eq_cosh_sub_one b
    simpa [FunctionalEquation.G] using h
  rw [h1, h2, h3, Real.cosh_add]
  ring

/-- **Strict superadditivity.** For same-sign nonzero `a, b`, chaining two
distinctions costs strictly more than the sum of the parts: the excess
`J(e^a)J(e^b) + sinh a sinh b` is positive. -/
theorem jcost_superadd_strict_same_sign {a b : ℝ} (h : 0 < a * b) :
    Jcost (Real.exp a) + Jcost (Real.exp b) < Jcost (Real.exp (a + b)) := by
  rw [jcost_chain_excess_identity]
  have hJa : 0 < Jcost (Real.exp a) := jcost_exp_pos (fun ha => by
    rw [ha] at h
    simp at h)
  have hJb : 0 < Jcost (Real.exp b) := jcost_exp_pos (fun hb => by
    rw [hb] at h
    simp at h)
  have hsinh : 0 < Real.sinh a * Real.sinh b := by
    rcases mul_pos_iff.mp h with ⟨ha, hb⟩ | ⟨ha, hb⟩
    · exact mul_pos (sinh_pos_of_pos ha) (sinh_pos_of_pos hb)
    · have h1 : Real.sinh a = - Real.sinh (-a) := by
        rw [Real.sinh_neg a]
        ring
      have h2 : Real.sinh b = - Real.sinh (-b) := by
        rw [Real.sinh_neg b]
        ring
      rw [h1, h2, neg_mul_neg]
      exact mul_pos (sinh_pos_of_pos (neg_pos.mpr ha)) (sinh_pos_of_pos (neg_pos.mpr hb))
  have h3 : 0 < Jcost (Real.exp a) * Jcost (Real.exp b) := mul_pos hJa hJb
  linarith [h3, hsinh]

/-- **Subdivision trivializes.** The total cost of `n` equal micro-steps
spanning a fixed distinction of log-size `ε` tends to zero:
`n · J(e^{ε/n}) → 0`. A continuum (infinitely refinable) ledger prices every
finite chain arbitrarily low. -/
theorem jcost_subdivision_trivializes (ε : ℝ) :
    Filter.Tendsto (fun n : ℕ => (n : ℝ) * Jcost (Real.exp (ε / n)))
      Filter.atTop (nhds 0) := by
  have hC : Filter.Tendsto (fun n : ℕ => ε ^ 2 * Real.cosh ε / (2 * (n : ℝ)))
      Filter.atTop (nhds 0) := by
    have h := tendsto_const_div_atTop_nhds_zero_nat (ε ^ 2 * Real.cosh ε / 2)
    exact h.congr (fun n => by rw [div_div])
  exact squeeze_zero (subdivision_cost_nonneg ε) (subdivision_cost_bound ε) hC

What this page does not claim

The identity alone does not force the golden ratio; the closure condition remains an assumption. The identity does not specify what the cost function J measures in any particular physical context. The identity does not imply that all recognition events must have a strictly positive cost.

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/GeometricRoot.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: