Foundation Jcost Geometry Jcost Pos Away From One

The cost of mismatch

The cost function J(x) = ½(x + x⁻¹) − 1 measures the price of a mismatch between two positive quantities, such as a value and its neighbor in a ledger. The function is zero only when x = 1, meaning the two quantities are equal. The theorem jcost_pos_away_from_one states that for any positive x not equal to 1, the cost is strictly greater than zero. This is a proved result in the framework's machine-checked library of formal theorems, and it holds for every positive real number except 1.

The classical picture is simple. For x = 2, the cost is ½(2 + 0.5) − 1 = 0.25. For x = 0.5, the cost is the same, 0.25, because the function is symmetric under x → 1/x. The cost rises as x moves away from 1 in either direction. This matches the squared form J(x) = (x − 1)² / (2x), which is always nonnegative and zero only at x = 1. The theorem is a direct consequence of this form, and it is one of the core identities in the JCostGeometry module.

The theorem does not say that the cost is large or small in any absolute sense; it only says the cost is positive. It does not say that a particular value of x is optimal or that any specific ratio is preferred. It also does not claim that the cost function is the only possible one; that uniqueness is a separate result. The theorem is a local fact about the shape of J, not a global statement about what the universe must do.

In the framework, this positivity is what makes the cost function useful as a ledger: any deviation from equality registers as a positive cost, so the ledger cannot silently ignore a mismatch. The theorem is a building block for the larger result that the geometric mean minimizes total cost, and it is cited in the foundation paper F1. For a reader, the practical takeaway is that the cost function has a single minimum at 1, and every other positive input carries a positive price.

/-- **F1.1.5**: J''(x) = x⁻³ > 0 for x > 0 (strict convexity witness).
    We prove the consequence: J is strictly positive away from 1. -/
theorem jcost_pos_away_from_one {x : ℝ} (hx : 0 < x) (hne : x ≠ 1) :
    0 < Jcost x := Jcost_pos_of_ne_one x hx hne

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

What this page does not claim

The theorem does not say the cost is large or small in absolute terms, only that it is positive. The theorem does not claim that J is the only possible cost function; that uniqueness is a separate result. The theorem does not state that any particular ratio is optimal or preferred.

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: