Foundation Jcost Geometry

The cost curve and its geometry

The cost function J(x) = (x + 1/x)/2 − 1 measures how far a ratio x is from 1. For x = 1 the cost is 0; for x = 2 it is 0.25; for x = 1/2 it is also 0.25, because the formula treats x and 1/x alike. This reciprocal symmetry is the first property that defines the cost. The function is nonnegative for all positive x, and it is zero only when x equals 1. A useful equivalent form is J(x) = (x − 1)²/(2x), which shows the cost grows quadratically near 1 but only linearly for large x.

The cost has a natural home in logarithmic coordinates. Writing x = e^ε, the cost becomes J(e^ε) = cosh(ε) − 1, a standard hyperbolic cosine shifted down by one. Near ε = 0, this behaves like ε²/2, with a cubic correction bounded by 2|ε|³ for small ε. This quadratic behavior means small deviations from 1 are cheap, while large deviations grow faster than linear. The same cost appears in a fundamental identity: for any nonzero x and y, J(xy) + J(x/y) = 2J(x)J(y) + 2J(x) + 2J(y). This identity is the algebraic engine behind the geometry.

When several neighbors are present, the total cost is the sum of individual costs J(v/n) for each neighbor n. A central result is that this total is minimized when v equals the geometric mean of the neighbors, not the arithmetic mean. For two unequal positive numbers, the geometric mean is always strictly less than the arithmetic mean, so simultaneous adjustment to the geometric mean differs from sequential adjustment to the arithmetic mean. This distinction is proved in the framework's machine-checked library of formal theorems.

In Recognition Science, the framework models recognition events as a ledger, a discrete record of events, and the cost of recognition is forced by five plain conditions. From this cost function, the framework derives the golden ratio φ = (1 + √5)/2 as the unique self-similar scaling, and it defines the jBit as log φ, a natural unit of information. The golden ratio satisfies φ² = φ + 1, a property that links the cost geometry to self-similar structure. The framework proves these results in its library, but the classical cost function itself is the starting point, not the conclusion.

The practical payoff is a precise language for balancing ratios. When a system must reconcile two quantities, the cost geometry says the optimal balance is the geometric mean, and the difference from the arithmetic mean is not a rounding error but a structural fact. This gives a concrete rule for when simultaneous adjustment beats sequential adjustment, and it explains why the golden ratio appears as a natural scale in the framework's derivations.

/-- **F1.1.3**: J(x) = 0 iff x = 1 (for x > 0) -/
theorem jcost_eq_zero_iff {x : ℝ} (hx : 0 < x) : Jcost x = 0 ↔ x = 1 := by
  constructor
  · intro h
    have hne : x ≠ 0 := ne_of_gt hx
    rw [Jcost_eq_sq hne] at h
    have hden : 0 < 2 * x := by positivity
    have hsq : (x - 1) ^ 2 = 0 := by
      by_contra hne'
      have : 0 < (x - 1) ^ 2 := by positivity
      have := div_pos this hden
      linarith
    have := sq_eq_zero_iff.mp hsq
    linarith
  · intro h; subst h; exact Jcost_unit0

/-- **F1.3.2 (two-element case)**: For two positive reals, the geometric mean
    minimizes the total J-cost. We prove the key fact: at the geometric mean,
    the J-cost is symmetric in the two neighbors. -/
theorem totalJcost_at_geomean_symmetric {n₁ n₂ : ℝ} (hn₁ : 0 < n₁) (hn₂ : 0 < n₂) :
    let gm := Real.sqrt (n₁ * n₂)
    Jcost (gm / n₁) = Jcost (gm / n₂) := by
  simp only
  have hprod : 0 < n₁ * n₂ := mul_pos hn₁ hn₂
  have hgm : 0 < Real.sqrt (n₁ * n₂) := Real.sqrt_pos.mpr hprod
  -- gm/n₁ = √(n₂/n₁) and gm/n₂ = √(n₁/n₂) = (√(n₂/n₁))⁻¹
  -- Since J(x) = J(1/x), these are equal
  have hgm_sq : Real.sqrt (n₁ * n₂) ^ 2 = n₁ * n₂ :=
    Real.sq_sqrt (le_of_lt hprod)
  -- Use reciprocal symmetry: J(gm/n₁) = J(n₂/gm) = J(gm/n₂) by J(x)=J(1/x)
  -- Actually: gm/n₁ = √(n₂/n₁) and gm/n₂ = √(n₁/n₂), and these are reciprocals
  have hn₁ne : n₁ ≠ 0 := ne_of_gt hn₁
  have hn₂ne : n₂ ≠ 0 := ne_of_gt hn₂
  have hgmne : Real.sqrt (n₁ * n₂) ≠ 0 := ne_of_gt hgm
  -- Both sides equal J(√(n₂/n₁)) by direct computation.
  -- Instead, use the simpler route: both ratios have the same J-value
  -- because J depends only on (x - 1)²/(2x), and we can show the
  -- squared-form representations are equal.
  have hn₁ne : n₁ ≠ 0 := ne_of_gt hn₁
  have hn₂ne : n₂ ≠ 0 := ne_of_gt hn₂
  have hgmne : Real.sqrt (n₁ * n₂) ≠ 0 := ne_of_gt hgm
  have hd1 : Real.sqrt (n₁ * n₂) / n₁ ≠ 0 := div_ne_zero hgmne hn₁ne
  have hd2 : Real.sqrt (n₁ * n₂) / n₂ ≠ 0 := div_ne_zero hgmne hn₂ne
  rw [Jcost_eq_sq hd1, Jcost_eq_sq hd2]
  -- Both equal (gm/n₁ - 1)²/(2·gm/n₁) vs (gm/n₂ - 1)²/(2·gm/n₂)
  -- Use that gm² = n₁·n₂
  have hsq : Real.sqrt (n₁ * n₂) * Real.sqrt (n₁ * n₂) = n₁ * n₂ :=
    Real.mul_self_sqrt (le_of_lt (mul_pos hn₁ hn₂))
  field_simp
  nlinarith [hsq, sq_nonneg (Real.sqrt (n₁ * n₂) - n₁),
             sq_nonneg (Real.sqrt (n₁ * n₂) - n₂)]

/-- **F1.4.3**: For distinct positive reals, the geometric mean differs
    from the arithmetic mean (AM-GM strict inequality). -/
theorem geometric_ne_arithmetic {n₁ n₂ : ℝ} (hn₁ : 0 < n₁) (hn₂ : 0 < n₂)
    (hne : n₁ ≠ n₂) :
    Real.sqrt (n₁ * n₂) ≠ (n₁ + n₂) / 2 := by
  intro h
  -- If √(n₁n₂) = (n₁+n₂)/2, squaring gives n₁n₂ = (n₁+n₂)²/4
  -- i.e. 4n₁n₂ = (n₁+n₂)² = n₁² + 2n₁n₂ + n₂²
  -- i.e. 0 = n₁² - 2n₁n₂ + n₂² = (n₁-n₂)²
  -- contradicting n₁ ≠ n₂
  have hprod : 0 ≤ n₁ * n₂ := le_of_lt (mul_pos hn₁ hn₂)
  have hsum_pos : 0 < (n₁ + n₂) / 2 := by linarith
  have hsq : n₁ * n₂ = ((n₁ + n₂) / 2) ^ 2 := by
    have h2 : Real.sqrt (n₁ * n₂) ^ 2 = n₁ * n₂ := Real.sq_sqrt hprod
    rw [← h2, h]
  have : (n₁ - n₂) ^ 2 = 0 := by nlinarith [hsq]
  have : n₁ - n₂ = 0 := by
    exact_mod_cast sq_eq_zero_iff.mp this
  exact hne (by linarith)

/-- phi satisfies φ² = φ + 1 -/
theorem phi_sq : phi ^ 2 = phi + 1 := by
  unfold phi
  have h5 : (0 : ℝ) ≤ 5 := by norm_num
  have hsq : Real.sqrt 5 ^ 2 = 5 := Real.sq_sqrt h5
  nlinarith [hsq]

What this page does not claim

The framework does not derive the fine-structure constant from this cost function. The cost function's uniqueness is not proved in this module alone. The golden ratio's appearance here does not imply it is the only self-similar scaling in all contexts.

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/Foundation/JCostGeometry.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: