Cost Unit From Minimality Cost Of The First Distinction

The cost of the first distinction

A ledger is a discrete record of events, each event separated from the next by a definite step. In the Recognition Science framework, the cost of recognizing a step is not chosen freely; it is forced by five plain conditions on how costs must behave. One of those conditions is that cost is blind to inversion: recognizing a step of size x costs the same as recognizing a step of size 1/x. Another is that a step of size 1, the unit step, costs nothing at all.

From these conditions, the framework proves a result about the smallest possible nonzero step. The theorem cost_of_the_first_distinction states that the cost of the step from 1 to 2, the first distinction away from the unit, is exactly one quarter. In symbols, J(2) = 1/4, where J is the cost function that the five conditions force to be J(x) = (x + 1/x)/2 - 1. The proof is a direct computation from that closed form, checked line by line in a machine-checked library of formal theorems.

The result is not an isolated curiosity. It is tied to a deeper structural fact about the ledger. The framework proves that among all positive integer powers of a base, the first power, the unit step itself, is the unique cheapest one. Any higher power, such as squaring or cubing the step, costs strictly more. This is the theorem unit_is_selected_by_minimality: for any base x other than 1, J(x) is less than J(x^n) for every integer n at least 2. The first distinction is not merely the smallest step; it is the step that the cost structure itself selects as the canonical unit.

The same minimality principle has a sharp edge. For odd powers, the framework proves that the first power is again the unique cheapest, and that no odd power beyond the first can tie it. But for continuous exponents, the situation reverses: the framework proves there is no least positive exponent at all. Halving the exponent always lowers the cost, so the cost can be driven arbitrarily close to zero without ever reaching a smallest positive value. This contrast, discrete floors versus continuous descent, is proved as a single theorem: discrete_gauge_has_a_floor_and_continuous_gauge_does_not.

What the declaration does not claim is just as important. It does not claim that the number 2 itself is special, only that the step from 1 to 2 is the first integer step and carries the cost one quarter. It does not claim that a step of size 2 is the only step with that cost; inversion symmetry means a step of size 1/2 costs the same. And it does not claim that the cost of the first distinction determines any physical constant. The value one quarter is a pure consequence of the cost function's form, with no empirical input.

/-- **The cost of the first distinction.** The composition law fixes the output scale of
the cost, since rescaling a solution breaks it. The only freedom left was the input scale,
and minimality has just removed it. So this number is now determined rather than
stipulated: telling one from two costs a quarter. -/
theorem cost_of_the_first_distinction : Jcost 2 = 1 / 4 := by
  norm_num [Jcost]

theorem unit_is_selected_by_minimality_over_powers :
    ∀ x : ℝ, 0 < x → x ≠ 1 → ∀ n : ℕ, 2 ≤ n → Jcost x < Jcost (x ^ n) :=
  fun x hx hx1 n hn => jcost_lt_pow x hx hx1 n hn

/-- **No cheapest cost exists on the continuum.** For every admissible scale there is a
strictly cheaper one, so the least-cost principle that fixes the unit on the countable
carrier has nothing to select here. -/
theorem no_least_gauge_member (x : ℝ) (hx : 0 < x) (hx1 : x ≠ 1) (l : ℝ) (hl : 0 < l) :
    Jcost (x ^ (l / 2)) < Jcost (x ^ l) := by
  rcases lt_trichotomy x 1 with hlt | heq | hgt
  · have hinv : 1 < x⁻¹ := one_lt_inv_iff₀.mpr ⟨hx, hlt⟩
    have h := gauge_halving_is_cheaper_of_one_lt x⁻¹ hinv l hl
    rwa [← jcost_rpow_inv x hx (l / 2), ← jcost_rpow_inv x hx l] at h
  · exact absurd heq hx1
  · exact gauge_halving_is_cheaper_of_one_lt x hgt l hl

/-- The two carriers, side by side. Least cost is a selection principle on the discrete
gauge and not on the continuous one, and completion to the real line is what turns the
first into the second.

The first clause is the countable carrier: `J` is strictly cheapest among the odd powers.
The second is the continuum: no scale is cheapest, because halving always undercuts. This
is a conjunction of the two facts, not a characterization of discreteness. -/
theorem discrete_gauge_has_a_floor_and_continuous_gauge_does_not :
    (∀ x : ℝ, 0 < x → x ≠ 1 → ∀ k : ℕ, 1 ≤ k → Jcost x < Jcost (x ^ (2 * k + 1)))
    ∧ (∀ x : ℝ, 0 < x → x ≠ 1 → ∀ l : ℝ, 0 < l → Jcost (x ^ (l / 2)) < Jcost (x ^ l)) :=
  ⟨fun x hx hx1 k hk => jcost_lt_odd_power x hx hx1 k hk,
   fun x hx hx1 l hl => no_least_gauge_member x hx hx1 l hl⟩

What this page does not claim

The number 2 is special; only the step from 1 to 2 is the first integer step. A step of size 2 is the only step with cost one quarter; inversion symmetry gives the same cost for a step of size 1/2. The value one quarter determines any physical constant or empirical quantity.

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/UnitFromMinimality.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: