Cost Geometric Root

The geometric root

The cost function at the center of Recognition Science is J(x) = (x + 1/x)/2 - 1, which measures the price of distinguishing a state x from a reference state 1. The geometric root is the observation that this algebraic formula is secretly a distance in hyperbolic geometry. For any positive x, the cost equals cosh(log x) - 1, and in the upper half-plane model of hyperbolic space, cosh(distance) - 1 equals the squared chordal distance between two points. The cost is not an arbitrary penalty; it is the hyperbolic distance from the reference point, expressed in a form that stays finite as x approaches 1.

The first theorem is an exact identity: J(x) = (x-1)^2 / (2x). This chordal form makes the geometry explicit. The second theorem is a chaining identity: J(e^(a+b)) = J(e^a) + J(e^b) + J(e^a)·J(e^b) + sinh a·sinh b. When a and b have the same sign, the last term is positive, so the cost of chaining two distinctions is strictly greater than the sum of their individual costs. This is the superadditivity property: in this geometry, combining two steps always costs more than taking them separately.

The third theorem is the one that forces structure. It shows that splitting a fixed distinction into n finer micro-steps makes the total cost n·J(e^(ε/n)) tend to 0 as n grows. A ledger that could be subdivided without limit would have no positive cost floor for any chain. Therefore, any ledger with an irreducible cost floor c > 0 must forbid refinement beyond a bound: n ≤ ε²·cosh ε / (2c). This is discreteness as a consequence, not an assumption. The module then assembles these results with a closure condition on a geometric ladder to derive r = φ, the golden ratio.

In Recognition Science, the framework models reality as a discrete ledger of recognition events, where each event has a forced cost. The geometric root shows that this cost is not an arbitrary choice but a hyperbolic distance, and that the discreteness of the ledger is forced by the cost structure itself. The golden ratio emerges as the unique self-similar scaling of this discrete ladder, a result that the framework's machine-checked library of formal theorems proves from the cost identity and the superadditivity inequality.

The honest status is that the closure condition, that the ladder's levels satisfy levels 2 = levels 1 + levels 0, is still assumed, not derived. The research leg that remains open is to derive this closure from the superadditivity excess itself, without assuming a geometric ladder. If that derivation succeeds, the golden ratio would be forced, not conditional, and the naming panel's reversal condition would fire.

/-- In the additive coordinate `x = e^t`, `J = cosh t - 1` exactly.
This is the banked theorem restated through `log`. -/
theorem jcost_eq_cosh_log_sub_one {x : ℝ} (hx : 0 < x) :
    Jcost x = Real.cosh (Real.log x) - 1 := by
  have h := FunctionalEquation.Jcost_G_eq_cosh_sub_one (Real.log x)
  simpa [FunctionalEquation.G, Real.exp_log hx] using h

/-- The chordal form: `J(x) = (x-1)^2/(2x)`. On the upper half-plane this is
`cosh d(i, ix) - 1` with `d` the hyperbolic distance, via
`cosh d(z,w) - 1 = |z-w|^2/(2 Im z Im w)`. The geometric reading is the
docstring; the arithmetic content is this identity. -/
theorem jcost_eq_chordal {x : ℝ} (hx : 0 < x) :
    Jcost x = (x - 1) ^ 2 / (2 * x) := by
  unfold Jcost
  field_simp [hx.ne']
  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

/-- The geometric-root chain, assembled. Three kernel-checked components:
the tick is forced (subdivision trivializes), chaining is superadditive, and
on a closed geometric ladder the ratio is φ (banked). The closure hypothesis
of the third component is the remaining research leg; see module docstring. -/
theorem geometric_root_assembly :
    (∀ ε : ℝ, Filter.Tendsto (fun n : ℕ => (n : ℝ) * Jcost (Real.exp (ε / n)))
        Filter.atTop (nhds 0))
    ∧ (∀ x y : ℝ, 1 ≤ x → 1 ≤ y → Jcost x + Jcost y ≤ Jcost (x * y))
    ∧ (∀ S : Foundation.PhiForcingDerived.GeometricScaleSequence,
        S.isClosed → S.ratio = Constants.phi) :=
  ⟨jcost_subdivision_trivializes,
   fun x y hx hy => @jcost_superadd_ratio x y hx hy,
   fun S h => Foundation.PhiForcingDerived.closed_ratio_is_phi S h⟩

What this page does not claim

The closure condition is derived, not assumed; it remains a hypothesis. The golden ratio is unconditionally forced; the derivation is conditional on the closure hypothesis. The cost function is the only possible one; the uniqueness theorem is separate and not proved in this module.

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: