Cost Geometric Root Jcost Superadd Strict Same Sign

The strict chaining inequality

In the Recognition Science framework, a ledger (a discrete record of events) assigns a cost to each distinction it records. The cost function, written Jcost, is not chosen freely; it is forced by five plain conditions and takes the exact form Jcost(x) = (x-1)^2/(2x) for a positive ratio x. This is the chordal form of the cost, and it is a proved theorem in the framework's machine-checked library of formal theorems.

The strict chaining inequality concerns what happens when a ledger records two distinctions in the same direction. Write the two distinctions as exponential steps, e^a and e^b, where a and b are real numbers. The theorem jcost_superadd_strict_same_sign states that if the product a·b is positive, meaning a and b have the same sign, then Jcost(e^a) + Jcost(e^b) < Jcost(e^(a+b)). In plain language: chaining two distinctions that point the same way always costs strictly more than the sum of their separate costs. The proof is an exact identity: Jcost(e^(a+b)) equals Jcost(e^a) + Jcost(e^b) + Jcost(e^a)·Jcost(e^b) + sinh a · sinh b. The last two terms are the excess, and for same-sign steps they are strictly positive whenever both steps are nonzero.

This strictness is the mechanical heart of a larger argument. The framework uses the chaining inequality to show that subdivision trivializes: splitting a fixed distinction into arbitrarily fine micro-steps makes its total cost arbitrarily small. A ledger that could refine without limit could not sustain any positive cost floor, so a ledger with an irreducible cost floor is forced to forbid refinement past a finite bound. That discreteness, in turn, is what forces the golden ratio as the unique self-similar scaling in the framework's account. The strict inequality is the engine that makes the ledger discrete, not continuous.

What the declaration does not claim is equally precise. The strict inequality holds only for same-sign steps; for opposite signs the excess can vanish or reverse, and the inequality does not apply. The theorem also does not derive the closure condition that completes the golden-ratio argument: the framework still assumes a geometric ladder, not deriving it from the chaining excess. That derivation remains open. The strict inequality is a proved lemma, not the whole forcing chain.

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

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

/-- **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 strict inequality does not hold for steps of opposite signs. The declaration does not derive the closure condition that forces the golden ratio. The theorem does not say that any discrete ledger must use this exact cost function.

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: