Encyclopedia Cost Cost Jcost Surjective On Nonneg

ARTICLE 4 claims 4 theorems

Cost Jcost Surjective On Nonneg

The recognition cost function J(x) hits every non-negative number exactly once, a fact that anchors the framework's later claims about scales and dimensions.

Verify this page

The cost function's reach

The function J(x) = (x + 1/x)/2 - 1, defined for positive real numbers x, is the cost of a recognition event: the price, in the framework's ledger, of mistaking one state for another. The cost is zero when x equals 1, meaning no price is paid for recognizing a state as itself. For any other positive x, the cost is positive, and it grows without bound as x moves away from 1 in either direction. The function is symmetric in a precise sense: J(x) equals J(1/x), so the cost of mistaking x for 1/x is the same as the cost of the reverse mistake.

The classical fact about J is its range. The theorem Jcost_surjective_on_nonneg, proved in the framework's machine-checked library of formal theorems, states that for every non-negative real number y, there exists an x greater than or equal to 1 such that J(x) = y. In plain language, the cost function covers the entire non-negative half of the real line: no non-negative cost is too large or too small to be realized by some positive input. Because J is strictly increasing on the interval from 1 to infinity, that input x is unique for each y. The function therefore provides a one-to-one correspondence between the set of non-negative costs and the half-line of inputs from 1 upward.

This surjectivity is not an isolated curiosity. It is what makes the cost function a usable measuring stick within the framework. If some physical quantity, such as a ratio of masses or lengths, is assigned a cost, the theorem guarantees that the cost can always be inverted to recover a unique underlying ratio. The framework's later results, which force the golden ratio, an eight-tick cycle, and three spatial dimensions, all depend on the cost function being able to represent every possible non-negative value. The theorem is a foundational guarantee that the ledger never runs out of entries.

What the theorem does not claim is just as important. It does not say that every positive x is needed to cover the costs; in fact, the input x can always be chosen to be at least 1, so the half-line below 1 is redundant. It does not say that J is surjective onto all real numbers, only onto the non-negative ones; negative costs are never realized. And it does not assign any physical meaning to the input x itself. The theorem is a statement about the function's mathematical range, not about which physical states actually occur. The framework's later steps, not this theorem, supply that physical interpretation.

THEOREM Jcost_surjective_on_nonneg · IndisputableMonolith/Cost.lean
Jcost_surjective_on_nonneg · IndisputableMonolith/Cost.lean:257 
/-- **THEOREM**: Jcost is surjective onto [0, ∞). -/
theorem Jcost_surjective_on_nonneg : ∀ y : ℝ, 0 ≤ y → ∃ x : ℝ, 1 ≤ x ∧ Jcost x = y := by
  intro y hy
  -- J(x) = (x + 1/x)/2 - 1
  -- Solve (x + 1/x)/2 - 1 = y => x + 1/x = 2(y+1)
  -- x^2 - 2(y+1)x + 1 = 0
  -- x = [(2(y+1)) + sqrt(4(y+1)^2 - 4)] / 2 = (y+1) + sqrt((y+1)^2 - 1)
  let x := (y + 1) + Real.sqrt ((y + 1) ^ 2 - 1)
  use x
  have h_y1_ge_1 : 1 ≤ y + 1 := by linarith
  have h_sq_ge_0 : 0 ≤ (y + 1) ^ 2 - 1 := by nlinarith
  constructor
  · have : 0 ≤ Real.sqrt ((y + 1) ^ 2 - 1) := Real.sqrt_nonneg _
    linarith
  · unfold Jcost
    have hx_pos : 0 < x := by
      have : 0 ≤ Real.sqrt ((y + 1) ^ 2 - 1) := Real.sqrt_nonneg _
      linarith
    field_simp [hx_pos.ne']
    -- Goal after field_simp: x^2 + 1 - x*2 = x*2*y
    -- Since x = y+1 + sqrt((y+1)^2 - 1), we have x^2 - 2(y+1)x + 1 = 0
    -- Thus x^2 + 1 = 2(y+1)x = 2x + 2xy, so x^2 + 1 - 2x = 2xy
    let s := Real.sqrt ((y + 1) ^ 2 - 1)
    have hs_sq : s ^ 2 = (y + 1) ^ 2 - 1 := Real.sq_sqrt h_sq_ge_0
    have hx_eq : x = y + 1 + s := rfl
    -- Key equation: x^2 - 2(y+1)x + 1 = 0
    have h_quad : x ^ 2 - 2 * (y + 1) * x + 1 = 0 := by
      have h1 : x ^ 2 = (y + 1 + s) ^ 2 := by rw [hx_eq]
      have h2 : (y + 1 + s) ^ 2 = (y + 1) ^ 2 + 2 * (y + 1) * s + s ^ 2 := by ring
      have h3 : s ^ 2 = (y + 1) ^ 2 - 1 := hs_sq
      calc x ^ 2 - 2 * (y + 1) * x + 1
          = (y + 1 + s) ^ 2 - 2 * (y + 1) * (y + 1 + s) + 1 := by simp only [hx_eq]
        _ = ((y + 1) ^ 2 + 2 * (y + 1) * s + s ^ 2) - 2 * (y + 1) * (y + 1 + s) + 1 := by rw [h2]
        _ = ((y + 1) ^ 2 + 2 * (y + 1) * s + ((y + 1) ^ 2 - 1)) - 2 * (y + 1) * (y + 1 + s) + 1 := by rw [h3]
        _ = 0 := by ring
    -- From h_quad: x^2 + 1 = 2(y+1)x = 2x(y+1) = 2x + 2xy
    -- So: x^2 + 1 - 2x = 2xy
    linarith [h_quad]
THEOREM Jcost_unit0 · IndisputableMonolith/Cost.lean
Jcost_unit0 · IndisputableMonolith/Cost.lean:12 
lemma Jcost_unit0 : Jcost 1 = 0 := by
  simp [Jcost]
THEOREM Jcost_symm · IndisputableMonolith/Cost.lean
Jcost_symm · IndisputableMonolith/Cost.lean:22 
lemma Jcost_symm {x : ℝ} (hx : 0 < x) : Jcost x = Jcost x⁻¹ := by
  have hx0 : x ≠ 0 := ne_of_gt hx
  rw [Jcost_eq_sq hx0, Jcost_eq_sq (inv_ne_zero hx0)]
  field_simp [hx0]
  ring
THEOREM Jcost_strict_mono_on_one_infty · IndisputableMonolith/Cost.lean
Jcost_strict_mono_on_one_infty · IndisputableMonolith/Cost.lean:649 
/-- J-cost is strictly increasing on `[1, ∞)`.

This root-module copy keeps downstream files from importing both
`IndisputableMonolith.Cost` and `IndisputableMonolith.Cost.JcostCore`, which
define overlapping names in the same namespace. -/
lemma Jcost_strict_mono_on_one_infty (x y : ℝ) (hx : 0 < x) (hy : 0 < y)
    (hx1 : 1 ≤ x) (hxy : x < y) :
    Jcost x < Jcost y := by
  have hx0 : x ≠ 0 := ne_of_gt hx
  have hy0 : y ≠ 0 := ne_of_gt hy
  rw [Jcost_eq_sq hx0, Jcost_eq_sq hy0]
  have h2x : 0 < 2 * x := by linarith
  have h2y : 0 < 2 * y := by linarith
  rw [div_lt_div_iff₀ h2x h2y]
  have hmain : (x - 1) ^ 2 * (2 * y) < (y - 1) ^ 2 * (2 * x) := by
    let f : ℝ → ℝ := fun t => (t - 1) ^ 2 / t
    have hf_mono : ∀ a b : ℝ, 1 ≤ a → a < b → f a < f b := by
      intro a b ha hab
      simp only [f]
      have ha0 : (0 : ℝ) < a := by linarith
      have hb0 : (0 : ℝ) < b := by linarith
      rw [div_lt_div_iff₀ ha0 hb0]
      have : (a - 1) ^ 2 * b - (b - 1) ^ 2 * a < 0 := by
        have hcalc : (a - 1) ^ 2 * b - (b - 1) ^ 2 * a = (a - b) * (a * b - 1) := by
          ring
        rw [hcalc]
        have h1 : a - b < 0 := by linarith
        have h2 : a * b - 1 > 0 := by nlinarith
        nlinarith
      linarith
    have := hf_mono x y hx1 hxy
    simp only [f] at this
    rw [div_lt_div_iff₀ hx hy] at this
    calc
      (x - 1) ^ 2 * (2 * y) = 2 * ((x - 1) ^ 2 * y) := by ring
      _ < 2 * ((y - 1) ^ 2 * x) := by nlinarith
      _ = (y - 1) ^ 2 * (2 * x) := by ring
  exact hmain

What this page does not claim

The theorem does not assign physical meaning to the input x. The theorem does not claim J is surjective onto negative real numbers. The theorem does not say every positive x is needed to represent all costs.

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