Foundation Jcost Geometry Jcost Ratio Zero Iff

The zero-cost condition

The function J(x) = (x + 1/x)/2 − 1 is a measure of how far a positive number x sits from 1. It is zero at x = 1, positive everywhere else, and symmetric in the sense that J(x) = J(1/x). The declaration jcost_ratio_zero_iff proves a sharper statement: for any two positive real numbers v and n, the cost J(v/n) is zero if and only if v = n. In plain language, the cost of comparing two quantities vanishes exactly when the quantities are identical.

The proof is a short chain of existing facts. Since v and n are positive, the ratio v/n is positive, so the theorem jcost_eq_zero_iff applies: J(v/n) = 0 forces v/n = 1. Multiplying through gives v = n. The converse is immediate from J(1) = 0. The declaration thus packages a one-line argument into a reusable lemma, stated in the framework's native terms of recognition, the discrete record of events that the framework uses as its starting point.

What the declaration does not claim is just as important. It does not say that equality is the only way to achieve zero total cost across a collection; that is a separate statement about sums, not ratios. It does not assert anything about the magnitude of J when v and n differ, only that the cost is positive. And it does not derive the framework's central uniqueness theorem for J itself; that result lives in a different module and rests on the five forcing conditions, not on this ratio test.

The practical payoff is a clean criterion: within the framework's model, a perfect match between an expected value and an observed value is the unique zero-cost state. This makes the ratio test a building block for the framework's claims about geometric-mean optimality, where the total cost over a set of neighbors is minimized at the geometric mean. The theorem itself is small, but it is the kind of precise, reusable fact that lets the framework's larger results stand on checked ground.

/-- **F1.2.1**: J(v/n) = 0 ↔ v = n for v, n > 0 -/
theorem jcost_ratio_zero_iff {v n : ℝ} (hv : 0 < v) (hn : 0 < n) :
    Jcost (v / n) = 0 ↔ v = n := by
  have hvn : 0 < v / n := div_pos hv hn
  rw [jcost_eq_zero_iff hvn]
  exact div_eq_one_iff_eq (ne_of_gt hn)

/-- **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.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.4**: J(x) = J(1/x) for x > 0 -/
theorem jcost_reciprocal {x : ℝ} (hx : 0 < x) : Jcost x = Jcost x⁻¹ :=
  Jcost_symm hx

What this page does not claim

This declaration does not prove that equality is the only zero-cost state for a sum of costs. This declaration does not derive the uniqueness of the cost function J from the five forcing conditions. This declaration says nothing about the magnitude of the cost when v and n differ, only that it is positive.

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: