Cost Unit From Minimality Discrete Gauge Has A Floor And Continuous Gauge Does N

A floor for discrete gauges

A gauge fixes the unit of measurement. In Recognition Science, the cost of recognizing a ratio x is J(x) = (x + 1/x)/2 - 1, a number that grows as x moves away from 1. The question is whether some scales are cheaper than others, and whether a cheapest scale exists at all.

The framework's machine-checked library proves a sharp split. For discrete exponents, meaning integer powers of a base, the cost is strictly minimized at the first power: for any base x not equal to 1 and any integer n at least 2, J(x) is strictly less than J(x^n). The theorem discrete_gauge_has_a_floor_and_continuous_gauge_does_not packages this as a single statement: the discrete case has a floor, the continuous case does not.

The continuous half says something stronger. For any positive real exponent l, halving it always lowers the cost: J(x^(l/2)) is strictly less than J(x^l). Repeated halving drives the cost toward zero without ever reaching it, so no positive real exponent is cheapest. The continuous gauge has no least member, while the discrete gauge selects the first power as its unique minimum.

The proof rests on the strict monotonicity of J on the interval above 1, together with a reciprocity that lets every statement about bases below 1 be proved by inverting. The discrete case uses the fact that for integer n at least 2, x^n is strictly larger than x, so its cost is larger. The continuous case uses the same monotonicity on the halved exponent, which is always strictly between 0 and l.

What the declaration does not claim is equally precise. It does not say that the zero exponent is excluded from consideration; in fact, the zero exponent costs exactly zero and undercuts every positive exponent. It does not say that the discrete floor is unique across all possible bases, only that for each fixed base the first power is cheapest. And it does not say that the continuous gauge has a minimum at some negative exponent; the halving argument applies to every positive l, and the zero exponent remains the only point where cost reaches zero.

/-- **The unit is the cheapest member of the enlarged family.** For any base other than the
unit, `J` charges strictly less than the cost generated by any exponent above one. This is
`jcost_lt_odd_power` with the parity restriction removed, which is what the corrected
classification requires. -/
theorem jcost_lt_pow (x : ℝ) (hx : 0 < x) (hx1 : x ≠ 1) (n : ℕ) (hn : 2 ≤ n) :
    Jcost x < Jcost (x ^ n) := by
  rcases lt_trichotomy x 1 with hlt | heq | hgt
  · have hinv : 1 < x⁻¹ := one_lt_inv_iff₀.mpr ⟨hx, hlt⟩
    have h := jcost_lt_pow_of_one_lt x⁻¹ hinv n hn
    rwa [← Jcost_symm hx, ← jcost_pow_inv x hx n] at h
  · exact absurd heq hx1
  · exact jcost_lt_pow_of_one_lt x hgt 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 zero exponent is excluded from the minimization; it costs exactly zero and undercuts every positive exponent. The discrete floor is unique across all possible bases; it is unique only for each fixed base. The continuous gauge has a minimum at some negative exponent; the halving argument applies to every positive l.

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: