Cost Unit From Minimality Unit Is Selected By Minimality

The unit by minimality

In the Recognition Science framework, a ledger (a discrete record of events) assigns a cost to every positive real number, a cost that measures how far that number is from being the neutral element 1. The framework's central theorem proves that this cost function must take the form J(x) = (x + 1/x)/2 - 1, which is zero exactly at x = 1 and grows as x moves away from 1 in either direction. The declaration unit_is_selected_by_minimality asks a sharper question: if you take any positive base x other than 1 and raise it to an odd power, is the cost of that power always larger than the cost of the base itself? The theorem answers yes, for every such base and every odd exponent 3, 5, 7, and so on. In other words, the base 1 is the unique point that cannot be made cheaper by exponentiating it to a higher odd power.

The proof runs through a short chain of lemmas. For bases above 1, the cost function is strictly increasing, so raising the base to a larger exponent always increases the cost. For bases below 1, the framework uses a symmetry: the cost is blind to inverting the base, so J(x) equals J(1/x). This lets the proof invert a base below 1, apply the increasing argument to the inverted base, and then invert back. The same symmetry handles the even-power case through a separate theorem, unit_is_selected_by_minimality_over_powers, which covers all exponents 2 and above. A closely related result, anchor_is_minimality, states the converse: if a power of b has the same cost as b itself, then that power must be the first power, the exponent 1. So the unit is not merely cheap; it is the unique base for which no higher power is equally cheap.

The distinction between odd and even powers matters. For odd powers, the theorem holds for every positive base except 1. For even powers, the same conclusion follows, but the proof is separate because the symmetry argument must be applied differently. The framework also proves a limiting case: as the exponent tends to zero, the cost tends to zero as well, so the zero exponent is always the cheapest of all. This is why the framework insists on exponents 2 and above when asking which base is minimal: the zero exponent would trivially win every comparison, and the theorem excludes it.

What the declaration does not claim is just as important. It does not say that the cost function itself is minimal at 1 in any absolute sense; the zero function, which assigns cost zero to everything, is also admissible under the framework's axioms. The theorem only compares powers of a fixed base against that same base, not against other bases. It also does not address continuous exponents: for real exponents, the framework shows there is no least member, because halving a positive exponent always produces a smaller cost. The discrete case, with its odd powers, is where the unit emerges as the unique minimal base.

/-- Packaging: on the discrete gauge, least cost is a selection principle. Every gauge
member other than `J` is strictly more expensive at every base that is not the unit. -/
theorem unit_is_selected_by_minimality :
    ∀ x : ℝ, 0 < x → x ≠ 1 → ∀ k : ℕ, 1 ≤ k → Jcost x < Jcost (x ^ (2 * k + 1)) :=
  fun x hx hx1 k hk => jcost_lt_odd_power x hx hx1 k hk

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

/-- **The anchor is the leastness condition, over the whole nondegenerate family.** Same
statement as `anchor_is_minimality` with the parity restriction removed, so it now covers
every exponent the corrected classification admits. -/
theorem anchor_is_minimality_over_powers (b : ℝ) (hb : 0 < b) (hb1 : b ≠ 1) (n : ℕ)
    (hn : 1 ≤ n) :
    (Jcost (b ^ n) = Jcost b) ↔ IsLeastPowerCost n := by
  rw [anchorPower_iff_canonical b hb hb1 n hn, isLeastPower_iff_canonical n hn]

/-- **The limit of the descent is admissible, not excluded.** The scale zero gives the
identically zero function, and that function satisfies the composition law, reciprocity
and normalization. So the descent of `no_least_gauge_member` does not run off the edge of
the admissible class; it runs to a member of it. Ruling the zero cost out takes a
nondegeneracy condition that the stated hypotheses do not contain, which is a further
reason a bare least-cost principle cannot fix a unit on the line. -/
theorem zero_cost_is_admissible :
    FunctionalEquation.IsReciprocalCost (fun _ => 0)
    ∧ FunctionalEquation.IsNormalized (fun _ => 0)
    ∧ FunctionalEquation.SatisfiesCompositionLaw (fun _ => 0)
    ∧ ContinuousOn (fun _ : ℝ => (0 : ℝ)) (Set.Ioi 0)
    ∧ (∀ x : ℝ, 0 < x → Jcost (x ^ (0 : ℝ)) = 0) := by
  refine ⟨fun _ _ => rfl, rfl, fun _ _ _ _ => by norm_num,
    continuousOn_const, fun x _ => ?_⟩
  rw [Real.rpow_zero]
  exact Jcost_unit0

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

What this page does not claim

The cost function itself is minimal at 1 in any absolute sense; the zero function is also admissible. The theorem compares powers of a fixed base against other bases. The discrete case extends to continuous exponents, where no least member exists.

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: