Foundation Jcost Geometry Jcost Squared Form

The squared form

The central object of Recognition Science is a cost, a real number that measures how far a recognition event's outcome, a ratio x, sits from the perfect match where x equals 1. The framework's foundational theorem proves that any cost function meeting five plain conditions must equal J(x) = ½(x + x⁻¹) − 1. The declaration jcost_squared_form establishes that this same function has an equivalent, more transparent shape: J(x) = (x − 1)² / (2x), valid for any nonzero x.

This squared form is not a new cost; it is the same function in a different dress, and the machine-checked library of formal theorems proves the two expressions are identical. Written this way, the cost's behavior becomes plain. The numerator (x − 1)² is a perfect square, so it is never negative, and the denominator 2x is positive whenever x is positive. The cost therefore bottoms out at zero exactly when x equals 1, the point of perfect recognition, and it climbs symmetrically as x moves away from 1 in either direction. The squared form also exposes the local geometry: near x = 1, writing x = 1 + ε, the cost behaves like ε²/2, a quadratic penalty that grows with the square of the small error ε.

In Recognition Science, this identity does real work. The framework models a ledger, a discrete record of recognition events, and sums costs over pairs of neighboring values. The squared form turns each summand into a ratio of squares, which makes the total cost's nonnegativity immediate and sharpens the analysis of how the total behaves. A companion theorem in the same module proves that the total cost over a list of neighbors is minimized when the value v sits at the geometric mean of those neighbors, not the arithmetic mean; the squared form is the algebraic engine behind that result.

What jcost_squared_form does not claim is just as important. It does not assert anything about the physical world; it is a theorem about a real-valued function, proved in the framework's machine-checked library. It does not say that recognition events actually occur, nor that the cost function is the one nature uses. Those are separate claims, grounded in other parts of the framework. The identity itself is unconditional algebra: for any nonzero real x, the two expressions are equal, with no hidden regularity assumptions and no appeal to empirical data.

/-- **F1.1.8**: The squared form J(x) = (x−1)²/(2x) -/
theorem jcost_squared_form {x : ℝ} (hx : x ≠ 0) :
    Jcost x = (x - 1) ^ 2 / (2 * x) := Jcost_eq_sq hx

/-- **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.1.6**: J(1) = 0 and the second derivative at 1 gives unit curvature.
    We state this via the quadratic approximation. -/
theorem jcost_unit_curvature (ε : ℝ) (hε : |ε| ≤ 1/2) :
    ∃ c : ℝ, Jcost (1 + ε) = ε ^ 2 / 2 + c * ε ^ 3 ∧ |c| ≤ 2 :=
  Jcost_one_plus_eps_quadratic ε hε

/-- **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₂)]

What this page does not claim

The theorem does not claim that recognition events occur in the physical world. The theorem does not claim that the cost function is the one nature uses. The theorem does not claim anything about the fine-structure constant or any other measured physical constant.

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: