Cost Unit From Minimality Anchor Is Minimality Over Powers

The anchor theorem

The Recognition Science framework begins with a cost function, a measure of the price of distinguishing one positive real number from 1, and it asks which base number is cheapest to use as a unit. The framework's library, a machine-checked collection of formal theorems, proves that the answer is the number 1 itself. The theorem anchor_is_minimality_over_powers states this precisely: for any positive base b that is not 1, and any exponent n at least 1, the cost of b raised to the n-th power equals the cost of b if and only if n equals 1. In plainer words, no power of a base other than the first power is ever as cheap as the base itself.

The proof leans on a strict monotonicity property of the cost function. The library shows that for any base above 1, raising it to a higher power strictly increases cost; the same holds for bases below 1 by symmetry, since cost is blind to inversion. The theorem unit_is_selected_by_minimality_over_powers packages this as a universal statement: for every base x above 0 and not equal to 1, and every exponent n of at least 2, the cost of x is strictly less than the cost of x to the n-th power. The anchor theorem then converts this strict inequality into an equivalence, identifying the first power as the unique minimizer among all positive integer powers.

What the theorem does not claim is just as important. It does not say that the number 1 is the only base with zero cost; the library separately proves that the zero-th power of any base has zero cost, which would undercut the unit if allowed. The theorem therefore restricts attention to exponents of at least 1, excluding the degenerate zero-th power. It also does not extend to continuous exponents: the library shows that for real exponents, halving the exponent always reduces cost, so no least positive real exponent exists. The minimality result is a discrete phenomenon, holding for integer powers only, and the theorem states exactly that scope.

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

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

/-- Exponent zero is the degenerate member: it charges nothing at every ratio. It is least in
the enlarged family, and for a reason that has nothing to do with cost, which is exactly why
selection needs nondegeneracy rather than leastness alone. -/
theorem exponent_zero_charges_nothing (x : ℝ) : Jcost (x ^ (0 : ℕ)) = 0 := by
  rw [pow_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 theorem does not claim that the number 1 is the only base with zero cost. The theorem does not claim that minimality holds for continuous exponents. The theorem does not claim that any power other than the first is ever as cheap as the base itself.

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: