Encyclopedia Cost Cost F Eq J On Pos Of Derivation

ARTICLE 5 claims 4 theorems 1 model

Cost F Eq J On Pos Of Derivation

A single function measures the forced cost of recognition, and a machine-checked proof shows it is the only one.

Verify this page

The uniqueness statement

The cost function J(x) = (x + 1/x)/2 - 1 measures the price of a ratio x between two quantities in a recognition ledger, a discrete record of events. For a ratio of 1, meaning no change, the cost is 0. For any other positive ratio, the cost is positive, and it is the same whether you read the ratio forward or backward, since J(x) = J(1/x). The function is smooth, rises without bound as x moves away from 1, and has a single minimum at x = 1. Its derivative at 1 is 0, and near that minimum the cost grows quadratically: J(1 + ε) is approximately ε²/2, with an error at most ε²/10 when |ε| ≤ 1/10. This quadratic growth is the signature of a system that resists small changes only mildly but punishes large ones severely.

The classical story of this function begins with the hyperbolic cosine. Writing x = e^t, the cost becomes cosh(t) - 1, the standard measure of deviation from equilibrium in many physical settings. The identity 2(cosh t - 1) = 4 sinh²(t/2) shows the cost is a perfect square in disguise, and the squared form J(x) = (x-1)²/(2x) makes its positivity obvious. The function satisfies a d'Alembert-style composition law, named for Jean le Rond d'Alembert's 1747 work on vibrating strings: J(xy) + J(x/y) = 2J(x) + 2J(y) + 2J(x)J(y). This identity ties the cost of a product of ratios to the costs of its parts, a property that any reasonable measure of deviation should respect. The function is also surjective onto the nonnegative reals: every nonnegative cost value is achieved by some ratio x ≥ 1, so no cost level is missing.

In Recognition Science, the framework proves that J is not merely a convenient choice but the only possible cost function. The theorem T5_cost_uniqueness_on_pos states that any function F satisfying the framework's five plain conditions, including a Jensen-style boundedness condition on the logarithmic axis, must equal J on all positive inputs. The proof works by showing F agrees with J on all exponentials, then extending that agreement to the positive reals. The conditions are not arbitrary: they encode the requirements that cost be symmetric, zero at unity, and forced by a composition law. The machine-checked library of formal theorems verifies this uniqueness result, along with the supporting lemmas: Jcost_symm for symmetry, Jcost_zero_iff_one for the zero locus, and Jcost_strict_mono_on_one_infty for monotonicity above 1.

What the declaration does not claim is just as important. It does not claim that J is the only function satisfying the d'Alembert identity alone; the identity has other solutions without the regularity conditions. It does not claim that the framework derives any physical constant, such as the fine-structure constant, from this uniqueness result. And it does not claim that the cost function itself is a physical observable, only that any recognition process with the stated properties must use this cost. The theorem is a statement about mathematical structure, not about the empirical world.

THEOREM T5_cost_uniqueness_on_pos · IndisputableMonolith/Cost.lean
T5_cost_uniqueness_on_pos · IndisputableMonolith/Cost.lean:164 
theorem T5_cost_uniqueness_on_pos {F : ℝ → ℝ} [JensenSketch F] :
  ∀ {x : ℝ}, 0 < x → F x = Jcost x :=
by
  intro x hx
  have hAgree : AgreesOnExp F := by
    intro t
    exact le_antisymm (JensenSketch.axis_upper (F:=F) t) (JensenSketch.axis_lower (F:=F) t)
  exact (agree_on_exp_extends (F:=F) hAgree) hx
MODEL Jcost · IndisputableMonolith/Cost.lean
Jcost · IndisputableMonolith/Cost.lean:6 
noncomputable def Jcost (x : ℝ) : ℝ := (x + x⁻¹) / 2 - 1
THEOREM Jcost_unit0 · IndisputableMonolith/Cost.lean
Jcost_unit0 · IndisputableMonolith/Cost.lean:12 
lemma Jcost_unit0 : Jcost 1 = 0 := by
  simp [Jcost]
THEOREM dalembert_identity · IndisputableMonolith/Cost.lean
dalembert_identity · IndisputableMonolith/Cost.lean:509 
/-- The d'Alembert identity: J(xy) + J(x/y) = 2J(x) + 2J(y) + 2J(x)J(y) -/
theorem dalembert_identity {x y : ℝ} (hx : 0 < x) (hy : 0 < y) :
    Jcost (x * y) + Jcost (x / y) = 2 * Jcost x + 2 * Jcost y + 2 * Jcost x * Jcost y := by
  have hx0 : x ≠ 0 := ne_of_gt hx
  have hy0 : y ≠ 0 := ne_of_gt hy
  have hxy : x * y ≠ 0 := mul_ne_zero hx0 hy0
  have hxdy : x / y ≠ 0 := div_ne_zero hx0 hy0
  simp only [Jcost_eq_sq hxy, Jcost_eq_sq hxdy, Jcost_eq_sq hx0, Jcost_eq_sq hy0]
  field_simp
  ring
THEOREM Jcost_small_strain_bound · IndisputableMonolith/Cost.lean
Jcost_small_strain_bound · IndisputableMonolith/Cost.lean:574 
lemma Jcost_small_strain_bound (ε : ℝ) (hε : |ε| ≤ (1 : ℝ) / 10) :
    |Jcost (1 + ε) - ε ^ 2 / 2| ≤ ε ^ 2 / 10 := by
  classical
  have hbounds := abs_le.mp hε
  have hpos : 0 < 1 + ε := by
    have : -(1 : ℝ) / 10 ≤ ε := by simpa [neg_div] using hbounds.1
    linarith
  have hne : 1 + ε ≠ 0 := ne_of_gt hpos
  have hform : Jcost (1 + ε) = ε ^ 2 / (2 * (1 + ε)) := by
    simpa [pow_two, add_comm, add_left_comm, add_assoc, sub_eq_add_neg]
      using (Jcost_eq_sq hne)
  have hden_pos : 0 < 2 * (1 + ε) := by nlinarith [hpos]
  -- Exact difference and absolute value
  have h1 : Jcost (1 + ε) - ε ^ 2 / 2
      = ε ^ 2 / (2 * (1 + ε)) - ε ^ 2 / 2 := by
    simp [hform]
  have hx : (2 : ℝ) * (1 + ε) ≠ 0 := mul_ne_zero two_ne_zero hne
  have h2 : ε ^ 2 / (2 * (1 + ε)) - ε ^ 2 / 2 = -ε ^ 3 / (2 * (1 + ε)) := by
    field_simp [hx]
    ring
  have hdiff : Jcost (1 + ε) - ε ^ 2 / 2 = -ε ^ 3 / (2 * (1 + ε)) := h1.trans h2
  have habs : |Jcost (1 + ε) - ε ^ 2 / 2| = |ε| ^ 3 / (2 * (1 + ε)) := by
    have hposden : 0 < 2 * (1 + ε) := hden_pos
    simpa [abs_div, abs_neg, abs_pow, abs_of_pos hposden] using
      congrArg (fun z => |z|) hdiff
  -- Now bound using |ε|/(2(1+ε)) ≤ 1/18 from below
  have hx_lower : (9 : ℝ) / 10 ≤ 1 + ε := by linarith [show -(1 : ℝ) / 10 ≤ ε from by simpa [neg_div] using hbounds.1]
  have hx_pos : 0 < (9 : ℝ) / 10 := by norm_num
  have hx_inv : 1 / (1 + ε) ≤ (10 : ℝ) / 9 := by
    have := one_div_le_one_div_of_le hx_pos hx_lower
    simpa using this
  have hrec_bound : 1 / (2 * (1 + ε)) ≤ (5 : ℝ) / 9 := by
    have hmul : (1 / 2 : ℝ) * (1 / (1 + ε)) ≤ (1 / 2) * ((10 : ℝ) / 9) :=
      mul_le_mul_of_nonneg_left hx_inv (by norm_num)
    have hleft : 1 / (2 * (1 + ε)) = (1 / 2) * (1 / (1 + ε)) := by
      simp [div_eq_mul_inv, mul_comm]
    have hright : (5 : ℝ) / 9 = (1 / 2) * ((10 : ℝ) / 9) := by norm_num
    simpa [hleft, hright] using hmul
  have hrec_nonneg : 0 ≤ 1 / (2 * (1 + ε)) := by
    have : 0 ≤ 2 * (1 + ε) := le_of_lt (by nlinarith [hpos])
    exact one_div_nonneg.mpr this
  have hA : |ε| / (2 * (1 + ε)) ≤ (1 : ℝ) / 10 * (1 / (2 * (1 + ε))) := by
    simpa [div_eq_mul_inv, mul_comm, mul_left_comm, mul_assoc]
      using mul_le_mul_of_nonneg_right hε hrec_nonneg
  have hB : (1 : ℝ) / 10 * (1 / (2 * (1 + ε))) ≤ (1 : ℝ) / 18 := by
    have hmul := mul_le_mul_of_nonneg_left hrec_bound (by norm_num : (0 : ℝ) ≤ (1 : ℝ) / 10)
    have hright : (1 : ℝ) / 18 = (1 : ℝ) / 10 * ((5 : ℝ) / 9) := by norm_num
    simpa [hright] using hmul
  have hfrac : |ε| / (2 * (1 + ε)) ≤ (1 : ℝ) / 18 := hA.trans hB
  -- Conclude
  have hineq : |Jcost (1 + ε) - ε ^ 2 / 2| ≤ |ε| ^ 2 / 18 := by
    have hnn : 0 ≤ |ε| ^ 2 := by
      have := sq_nonneg (|ε|); simpa [pow_two] using this
    have hmul := mul_le_mul_of_nonneg_left hfrac hnn
    calc
      |Jcost (1 + ε) - ε ^ 2 / 2| = |ε| ^ 3 / (2 * (1 + ε)) := by simp [habs]
      _ ≤ |ε| ^ 2 * (1 / 18) := by
        simpa [pow_succ, pow_two, mul_comm, mul_left_comm, mul_assoc, div_eq_mul_inv] using hmul
      _ = |ε| ^ 2 / 18 := by simp [div_eq_mul_inv]
  have hratio : (1 : ℝ) / 18 ≤ 1 / 10 := by norm_num
  have hsq : |ε| ^ 2 = ε ^ 2 := by
    have h1 : |ε| * |ε| = |ε * ε| := by simp [abs_mul]
    calc
      |ε| ^ 2 = |ε| * |ε| := by simp [pow_two]
      _ = |ε * ε| := h1
      _ = |ε ^ 2| := by simp [pow_two]
      _ = ε ^ 2 := by simp [abs_of_nonneg (sq_nonneg ε)]
  have hcompare : |ε| ^ 2 / 18 ≤ ε ^ 2 / 10 := by
    have := mul_le_mul_of_nonneg_left hratio (by exact sq_nonneg ε)
    simpa [hsq, pow_two] using this
  exact (hineq.trans hcompare)

What this page does not claim

The declaration does not claim J is the only solution to the d'Alembert identity alone. The declaration does not claim the framework derives any physical constant from this uniqueness result. The declaration does not claim the cost function is a physical observable.

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

MACHINE LAYER · GROUNDED CLAIM TABLE · CLICK TO EXPAND