IndisputableMonolith.Cost.UnitFromMinimality

   1/-
   2  Cost/UnitFromMinimality.lean
   3
   4  THE UNIT OF COST, SELECTED BY COST.
   5
   6  Background. The composition law forces the FORM of the recognition cost but not its
   7  scale: the admissible costs come in a gauge family `x ↦ J (x ^ l)`, and picking `l = 1`
   8  has been done by calibration (`G''(0) = 1` on the continuum, an anchor at orbit two on
   9  the countable carrier). Calibration is a stipulation, so the standing honest wording has
  10  been "parameter-free up to a choice of unit", and whether the unit is forced or
  11  conventional has been open since `Delta_Cost_Form_Forced_Unit_Gauge` (May 2026).
  12
  13  What this file adds. A selection principle that needs no calibration: among admissible
  14  costs, take the cheapest. Whether that works turns entirely on whether the gauge is
  15  discrete or continuous, and the two carriers differ exactly there.
  16
  17  * On the countable carrier the gauge members proved to inhabit the anchor-free ledger
  18    form a discrete family indexed by an integer exponent, and `J` is their STRICT
  19    POINTWISE MINIMUM among the nondegenerate ones (`jcost_lt_pow`, with the earlier
  20    odd-power-only form `jcost_lt_odd_power`). Least cost therefore selects the unit
  21    outright, with no anchor: `unit_is_selected_by_minimality_over_powers`.
  22  * On the continuum the gauge is a continuum, the family is totally ordered with no
  23    least member (`no_least_gauge_member`), and its pointwise infimum is the zero cost
  24    (`gauge_tendsto_zero`). So no least-cost principle can fix a unit there; it
  25    degenerates to charging nothing for everything.
  26
  27  Reading. The freedom that forces calibration is not a feature of cost. It is introduced
  28  by completing to the real line, and it destroys the selection principle that would
  29  otherwise fix the unit for free. Combined with the standing result that the completion
  30  is a genuine purchase, the unit is a convention on the reals and a theorem on the
  31  carrier.
  32
  33  Scope, so this is not over-read. Minimality selects `J` from the power family, every
  34  member of which is proved to inhabit the anchor-free ledger. Two things are still needed
  35  for the unqualified reading. The reverse inclusion, that the ledger admits nothing
  36  outside that family, is OPEN (the Alaoglu-Erdos / six-exponentials wall). And exponent
  37  zero, the sign cost, does inhabit the ledger and charges nothing, so it undercuts `J`
  38  and is excluded by nondegeneracy rather than by cost
  39  (`exponent_zero_undercuts_everything`). So the selection theorems here are
  40  unconditional about the power family and the full "no anchor is needed" reading is
  41  conditional on the classification plus nondegeneracy. This file states the conditional
  42  explicitly rather than blurring it.
  43
  44  No project-local axioms. No sorry.
  45-/
  46
  47import Mathlib
  48import IndisputableMonolith.Cost
  49import IndisputableMonolith.Cost.FunctionalEquation
  50
  51namespace IndisputableMonolith
  52namespace Cost
  53namespace UnitFromMinimality
  54
  55/-! ## Reciprocity lets every statement be proved above one -/
  56
  57/-- Cost is blind to inversion of the base, so a gauge statement need only be proved for
  58bases above one. Stated for real exponents since the continuum half needs it. -/
  59lemma jcost_rpow_inv (x : ℝ) (hx : 0 < x) (l : ℝ) :
  60    Jcost (x ^ l) = Jcost ((x⁻¹) ^ l) := by
  61  have hpos : 0 < x ^ l := Real.rpow_pos_of_pos hx l
  62  rw [Real.inv_rpow hx.le l]
  63  exact Jcost_symm hpos
  64
  65/-- The same, for the natural-number powers the discrete gauge uses. -/
  66lemma jcost_pow_inv (x : ℝ) (hx : 0 < x) (n : ℕ) :
  67    Jcost (x ^ n) = Jcost ((x⁻¹) ^ n) := by
  68  have hpos : 0 < x ^ n := pow_pos hx n
  69  rw [inv_pow]
  70  exact Jcost_symm hpos
  71
  72/-! ## The countable carrier: a discrete gauge has a least member, and it is `J` -/
  73
  74/-- Above one, every higher odd power costs strictly more. -/
  75lemma jcost_lt_odd_power_of_one_lt (x : ℝ) (hx : 1 < x) (k : ℕ) (hk : 1 ≤ k) :
  76    Jcost x < Jcost (x ^ (2 * k + 1)) := by
  77  have hx0 : 0 < x := lt_trans zero_lt_one hx
  78  have hlt : x < x ^ (2 * k + 1) := by
  79    have h1 : (1 : ℕ) < 2 * k + 1 := by omega
  80    calc x = x ^ 1 := (pow_one x).symm
  81    _ < x ^ (2 * k + 1) := pow_lt_pow_right₀ hx h1
  82  exact Jcost_strict_mono_on_one_infty x (x ^ (2 * k + 1)) hx0
  83    (lt_trans hx0 hlt) hx.le hlt
  84
  85/-- **The unit is the cheapest gauge member.** For any base other than the unit, the
  86canonical cost `J` charges strictly less than every higher odd power of the gauge. Since
  87those odd powers are exactly the members proved to inhabit the anchor-free ledger on the
  88countable carrier, least cost picks out `J` with no calibration and no anchor. -/
  89theorem jcost_lt_odd_power (x : ℝ) (hx : 0 < x) (hx1 : x ≠ 1) (k : ℕ) (hk : 1 ≤ k) :
  90    Jcost x < Jcost (x ^ (2 * k + 1)) := by
  91  rcases lt_trichotomy x 1 with hlt | heq | hgt
  92  · -- Below one: invert and reuse the case above one.
  93    have hinv : 1 < x⁻¹ := one_lt_inv_iff₀.mpr ⟨hx, hlt⟩
  94    have h := jcost_lt_odd_power_of_one_lt x⁻¹ hinv k hk
  95    rwa [← Jcost_symm hx, ← jcost_pow_inv x hx (2 * k + 1)] at h
  96  · exact absurd heq hx1
  97  · exact jcost_lt_odd_power_of_one_lt x hgt k hk
  98
  99/-- Packaging: on the discrete gauge, least cost is a selection principle. Every gauge
 100member other than `J` is strictly more expensive at every base that is not the unit. -/
 101theorem unit_is_selected_by_minimality :
 102    ∀ x : ℝ, 0 < x → x ≠ 1 → ∀ k : ℕ, 1 ≤ k → Jcost x < Jcost (x ^ (2 * k + 1)) :=
 103  fun x hx hx1 k hk => jcost_lt_odd_power x hx hx1 k hk
 104
 105/-! ### Leastness, quantified over the family and not against a designated member
 106
 107The condition below makes no reference to the canonical cost. It says only that the
 108`k`-th member is nowhere more expensive than **any** member of the family, which is what
 109"least element of the pointwise order" means. Stating it against `J` instead would smuggle
 110in the answer, so it is stated properly and the characterization is derived. -/
 111
 112/-- The `k`-th gauge member is a least element of the odd-power family under the pointwise
 113order: it charges no more than any member, at every ratio other than the unit. -/
 114def IsLeastOddPowerCost (k : ℕ) : Prop :=
 115  ∀ j : ℕ, ∀ x : ℝ, 0 < x → x ≠ 1 →
 116    Jcost (x ^ (2 * k + 1)) ≤ Jcost (x ^ (2 * j + 1))
 117
 118/-- **The canonical cost is the unique least element of the gauge family.** No reference
 119to `J` appears in `IsLeastOddPowerCost`; leastness is quantified over the family alone,
 120and it happens to hold of exactly one member. -/
 121theorem isLeast_iff_canonical (k : ℕ) : IsLeastOddPowerCost k ↔ k = 0 := by
 122  constructor
 123  · intro h
 124    by_contra hk
 125    have hk1 : 1 ≤ k := Nat.one_le_iff_ne_zero.mpr hk
 126    have hle := h 0 2 (by norm_num) (by norm_num)
 127    have hlt := jcost_lt_odd_power (2 : ℝ) (by norm_num) (by norm_num) k hk1
 128    simp only [Nat.mul_zero, Nat.zero_add, pow_one] at hle
 129    exact absurd hle (not_le.mpr hlt)
 130  · rintro rfl
 131    intro j x hx hx1
 132    simp only [Nat.mul_zero, Nat.zero_add, pow_one]
 133    rcases Nat.eq_zero_or_pos j with rfl | hj
 134    · simp
 135    · exact le_of_lt (jcost_lt_odd_power x hx hx1 j hj)
 136
 137/-! ### The family is larger than the odd powers, and leastness survives the enlargement
 138
 139The classification of anchor-free inhabitants was corrected twice on 2026-07-25. The
 140inhabited set is not the odd powers. The sign cost inhabits it at exponent zero, and the
 141sign-extended character `x ↦ x·|x|^m` inhabits it at exponent `m+1` of either parity, so
 142every nonnegative integer exponent occurs (`Cost/GaugeOrbitFromRealCharacter.lean`:
 143`signGaugeNativeCost_sansAnchor`, `signedPowerNativeCost_sansAnchor`). Restricted to the
 144positive ratios, where the pointwise order is decided, that whole family is `x ↦ J (x ^ n)`
 145for `n : ℕ`. Since 2026-07-26 that is also the complete list: no other inhabitant exists
 146(`Cost.GaugeOrbitClassification.GaugeOrbitIsSignedPowerFamily_of_sixExponentials`, on the
 147six exponentials input), so the leastness statements below now range over exactly the
 148ledger's inhabitants rather than over a family known only to be contained in it.
 149
 150Leastness therefore has to be re-proved over the enlarged family, or the selection claim
 151covers less than the ledger contains. It goes through with the parity deleted: nothing in
 152the argument used it, only that the exponent exceeds one. Exponent zero charges nothing
 153anywhere and is least for the wrong reason, which is what the nondegeneracy hypothesis in
 154the companion argument excludes. -/
 155
 156/-- Above one, every higher power costs strictly more, at either parity of the exponent. -/
 157lemma jcost_lt_pow_of_one_lt (x : ℝ) (hx : 1 < x) (n : ℕ) (hn : 2 ≤ n) :
 158    Jcost x < Jcost (x ^ n) := by
 159  have hx0 : 0 < x := lt_trans zero_lt_one hx
 160  have hlt : x < x ^ n := by
 161    have h1 : (1 : ℕ) < n := by omega
 162    calc x = x ^ 1 := (pow_one x).symm
 163    _ < x ^ n := pow_lt_pow_right₀ hx h1
 164  exact Jcost_strict_mono_on_one_infty x (x ^ n) hx0 (lt_trans hx0 hlt) hx.le hlt
 165
 166/-- **The unit is the cheapest member of the enlarged family.** For any base other than the
 167unit, `J` charges strictly less than the cost generated by any exponent above one. This is
 168`jcost_lt_odd_power` with the parity restriction removed, which is what the corrected
 169classification requires. -/
 170theorem jcost_lt_pow (x : ℝ) (hx : 0 < x) (hx1 : x ≠ 1) (n : ℕ) (hn : 2 ≤ n) :
 171    Jcost x < Jcost (x ^ n) := by
 172  rcases lt_trichotomy x 1 with hlt | heq | hgt
 173  · have hinv : 1 < x⁻¹ := one_lt_inv_iff₀.mpr ⟨hx, hlt⟩
 174    have h := jcost_lt_pow_of_one_lt x⁻¹ hinv n hn
 175    rwa [← Jcost_symm hx, ← jcost_pow_inv x hx n] at h
 176  · exact absurd heq hx1
 177  · exact jcost_lt_pow_of_one_lt x hgt n hn
 178
 179theorem unit_is_selected_by_minimality_over_powers :
 180    ∀ x : ℝ, 0 < x → x ≠ 1 → ∀ n : ℕ, 2 ≤ n → Jcost x < Jcost (x ^ n) :=
 181  fun x hx hx1 n hn => jcost_lt_pow x hx hx1 n hn
 182
 183/-- The exponent-`n` member is a least element of the nondegenerate power family under the
 184pointwise order. Nondegeneracy is the restriction `1 ≤ m` on the competitors: exponent zero
 185is the identically zero cost. -/
 186def IsLeastPowerCost (n : ℕ) : Prop :=
 187  ∀ m : ℕ, 1 ≤ m → ∀ x : ℝ, 0 < x → x ≠ 1 → Jcost (x ^ n) ≤ Jcost (x ^ m)
 188
 189/-- **The canonical cost is the unique least nondegenerate member, at every exponent and not
 190merely the odd ones.** As before, the condition never names `J`. -/
 191theorem isLeastPower_iff_canonical (n : ℕ) (hn : 1 ≤ n) :
 192    IsLeastPowerCost n ↔ n = 1 := by
 193  constructor
 194  · intro h
 195    by_contra hne
 196    have hn2 : 2 ≤ n := by omega
 197    have hle := h 1 (le_refl 1) 2 (by norm_num) (by norm_num)
 198    have hlt := jcost_lt_pow (2 : ℝ) (by norm_num) (by norm_num) n hn2
 199    rw [pow_one] at hle
 200    exact absurd hle (not_le.mpr hlt)
 201  · rintro rfl
 202    intro m hm x hx hx1
 203    rw [pow_one]
 204    rcases Nat.lt_or_ge m 2 with hm2 | hm2
 205    · have hm1 : m = 1 := by omega
 206      subst hm1
 207      simp
 208    · exact le_of_lt (jcost_lt_pow x hx hx1 m hm2)
 209
 210/-- Exponent zero is the degenerate member: it charges nothing at every ratio. It is least in
 211the enlarged family, and for a reason that has nothing to do with cost, which is exactly why
 212selection needs nondegeneracy rather than leastness alone. -/
 213theorem exponent_zero_charges_nothing (x : ℝ) : Jcost (x ^ (0 : ℕ)) = 0 := by
 214  rw [pow_zero]
 215  exact Jcost_unit0
 216
 217theorem exponent_zero_undercuts_everything (n : ℕ) (x : ℝ) (hx : 0 < x) :
 218    Jcost (x ^ (0 : ℕ)) ≤ Jcost (x ^ n) := by
 219  rw [exponent_zero_charges_nothing]
 220  exact Jcost_nonneg (pow_pos hx n)
 221
 222/-! ### The anchor was minimality all along
 223
 224The structural ledger's surviving stipulation is the anchor at orbit two: the requirement
 225that the cost charge `J 2 = 1/4` there. The next two results show that this stipulation
 226and the minimality condition cut the gauge family at exactly the same place, so the
 227anchor is not an arbitrary numeric convention. It is the cheapest-cost condition, written
 228at one point. -/
 229
 230/-- The anchor selects the canonical member and nothing else, and it does so **at every
 231base**. The choice of orbit two as the anchor point is therefore immaterial: any single
 232ratio other than the unit pins the same member. What looked like two arbitrary choices,
 233where to anchor and what value to give it, is one determination with no freedom in it. -/
 234theorem anchor_iff_canonical (b : ℝ) (hb : 0 < b) (hb1 : b ≠ 1) (k : ℕ) :
 235    Jcost (b ^ (2 * k + 1)) = Jcost b ↔ k = 0 := by
 236  constructor
 237  · intro h
 238    by_contra hk
 239    have hk1 : 1 ≤ k := Nat.one_le_iff_ne_zero.mpr hk
 240    exact absurd h (ne_of_gt (jcost_lt_odd_power b hb hb1 k hk1))
 241  · rintro rfl
 242    norm_num
 243
 244/-- **The anchor is the leastness condition.** On the gauge family the stipulated anchor
 245value and genuine leastness over the family hold of exactly the same member, for any
 246anchor base. So the one surviving stipulation in the structural ledger is not a convention
 247about a number; it is least cost, evaluated at a point, and the point may be any point.
 248
 249Note what is and is not shown. Leastness here is over the odd-power family, which is the
 250part of the anchor-free ledger proved to be inhabited. Leastness over the whole ledger
 251needs the classification discussed in the accompanying paper. -/
 252theorem anchor_is_minimality (b : ℝ) (hb : 0 < b) (hb1 : b ≠ 1) (k : ℕ) :
 253    (Jcost (b ^ (2 * k + 1)) = Jcost b) ↔ IsLeastOddPowerCost k := by
 254  rw [anchor_iff_canonical b hb hb1, isLeast_iff_canonical]
 255
 256/-- The anchor characterization over the enlarged family: any single base other than the unit
 257pins the exponent to one, at either parity. -/
 258theorem anchorPower_iff_canonical (b : ℝ) (hb : 0 < b) (hb1 : b ≠ 1) (n : ℕ) (hn : 1 ≤ n) :
 259    Jcost (b ^ n) = Jcost b ↔ n = 1 := by
 260  constructor
 261  · intro h
 262    by_contra hne
 263    have hn2 : 2 ≤ n := by omega
 264    exact absurd h (ne_of_gt (jcost_lt_pow b hb hb1 n hn2))
 265  · rintro rfl
 266    rw [pow_one]
 267
 268/-- **The anchor is the leastness condition, over the whole nondegenerate family.** Same
 269statement as `anchor_is_minimality` with the parity restriction removed, so it now covers
 270every exponent the corrected classification admits. -/
 271theorem anchor_is_minimality_over_powers (b : ℝ) (hb : 0 < b) (hb1 : b ≠ 1) (n : ℕ)
 272    (hn : 1 ≤ n) :
 273    (Jcost (b ^ n) = Jcost b) ↔ IsLeastPowerCost n := by
 274  rw [anchorPower_iff_canonical b hb hb1 n hn, isLeastPower_iff_canonical n hn]
 275
 276/-- **The cost of the first distinction.** The composition law fixes the output scale of
 277the cost, since rescaling a solution breaks it. The only freedom left was the input scale,
 278and minimality has just removed it. So this number is now determined rather than
 279stipulated: telling one from two costs a quarter. -/
 280theorem cost_of_the_first_distinction : Jcost 2 = 1 / 4 := by
 281  norm_num [Jcost]
 282
 283/-! ## The continuum: a continuous gauge has no least member -/
 284
 285/-- Above one, halving the exponent is strictly cheaper. -/
 286lemma gauge_halving_is_cheaper_of_one_lt (x : ℝ) (hx : 1 < x) (l : ℝ) (hl : 0 < l) :
 287    Jcost (x ^ (l / 2)) < Jcost (x ^ l) := by
 288  have hx0 : 0 < x := lt_trans zero_lt_one hx
 289  have hhalf : 0 < l / 2 := by linarith
 290  have hone : 1 < x ^ (l / 2) := Real.one_lt_rpow_iff_of_pos hx0 |>.mpr (Or.inl ⟨hx, hhalf⟩)
 291  have hlt : x ^ (l / 2) < x ^ l := by
 292    exact Real.rpow_lt_rpow_left_iff hx |>.mpr (by linarith)
 293  exact Jcost_strict_mono_on_one_infty _ _ (lt_trans zero_lt_one hone)
 294    (lt_trans (lt_trans zero_lt_one hone) hlt) hone.le hlt
 295
 296/-- **No cheapest cost exists on the continuum.** For every admissible scale there is a
 297strictly cheaper one, so the least-cost principle that fixes the unit on the countable
 298carrier has nothing to select here. -/
 299theorem no_least_gauge_member (x : ℝ) (hx : 0 < x) (hx1 : x ≠ 1) (l : ℝ) (hl : 0 < l) :
 300    Jcost (x ^ (l / 2)) < Jcost (x ^ l) := by
 301  rcases lt_trichotomy x 1 with hlt | heq | hgt
 302  · have hinv : 1 < x⁻¹ := one_lt_inv_iff₀.mpr ⟨hx, hlt⟩
 303    have h := gauge_halving_is_cheaper_of_one_lt x⁻¹ hinv l hl
 304    rwa [← jcost_rpow_inv x hx (l / 2), ← jcost_rpow_inv x hx l] at h
 305  · exact absurd heq hx1
 306  · exact gauge_halving_is_cheaper_of_one_lt x hgt l hl
 307
 308/-- And the descent runs all the way to nothing: the gauge family's pointwise limit as
 309the scale vanishes is the zero cost. So the infimum is not merely unattained, it is the
 310degenerate cost that charges nothing for anything. -/
 311theorem gauge_tendsto_zero (x : ℝ) (hx : 0 < x) :
 312    Filter.Tendsto (fun l : ℝ => Jcost (x ^ l)) (nhds 0) (nhds 0) := by
 313  have hrw : (fun l : ℝ => Jcost (x ^ l))
 314      = fun l : ℝ => Real.cosh (Real.log x * l) - 1 := by
 315    funext l
 316    rw [Real.rpow_def_of_pos hx, Jcost_exp_cosh]
 317  rw [hrw]
 318  have hcont : Continuous (fun l : ℝ => Real.cosh (Real.log x * l) - 1) := by
 319    fun_prop
 320  have h0 : Real.cosh (Real.log x * (0 : ℝ)) - 1 = 0 := by simp
 321  simpa [h0] using hcont.tendsto (0 : ℝ)
 322
 323/-- **The limit of the descent is admissible, not excluded.** The scale zero gives the
 324identically zero function, and that function satisfies the composition law, reciprocity
 325and normalization. So the descent of `no_least_gauge_member` does not run off the edge of
 326the admissible class; it runs to a member of it. Ruling the zero cost out takes a
 327nondegeneracy condition that the stated hypotheses do not contain, which is a further
 328reason a bare least-cost principle cannot fix a unit on the line. -/
 329theorem zero_cost_is_admissible :
 330    FunctionalEquation.IsReciprocalCost (fun _ => 0)
 331    ∧ FunctionalEquation.IsNormalized (fun _ => 0)
 332    ∧ FunctionalEquation.SatisfiesCompositionLaw (fun _ => 0)
 333    ∧ ContinuousOn (fun _ : ℝ => (0 : ℝ)) (Set.Ioi 0)
 334    ∧ (∀ x : ℝ, 0 < x → Jcost (x ^ (0 : ℝ)) = 0) := by
 335  refine ⟨fun _ _ => rfl, rfl, fun _ _ _ _ => by norm_num,
 336    continuousOn_const, fun x _ => ?_⟩
 337  rw [Real.rpow_zero]
 338  exact Jcost_unit0
 339
 340/-! ## The contrast, in one statement -/
 341
 342/-- The two carriers, side by side. Least cost is a selection principle on the discrete
 343gauge and not on the continuous one, and completion to the real line is what turns the
 344first into the second.
 345
 346The first clause is the countable carrier: `J` is strictly cheapest among the odd powers.
 347The second is the continuum: no scale is cheapest, because halving always undercuts. This
 348is a conjunction of the two facts, not a characterization of discreteness. -/
 349theorem discrete_gauge_has_a_floor_and_continuous_gauge_does_not :
 350    (∀ x : ℝ, 0 < x → x ≠ 1 → ∀ k : ℕ, 1 ≤ k → Jcost x < Jcost (x ^ (2 * k + 1)))
 351    ∧ (∀ x : ℝ, 0 < x → x ≠ 1 → ∀ l : ℝ, 0 < l → Jcost (x ^ (l / 2)) < Jcost (x ^ l)) :=
 352  ⟨fun x hx hx1 k hk => jcost_lt_odd_power x hx hx1 k hk,
 353   fun x hx hx1 l hl => no_least_gauge_member x hx hx1 l hl⟩
 354
 355/-! ## Audits -/
 356
 357#print axioms jcost_lt_odd_power
 358#print axioms isLeast_iff_canonical
 359#print axioms anchor_is_minimality
 360#print axioms jcost_lt_pow
 361#print axioms isLeastPower_iff_canonical
 362#print axioms anchor_is_minimality_over_powers
 363#print axioms exponent_zero_undercuts_everything
 364#print axioms cost_of_the_first_distinction
 365#print axioms no_least_gauge_member
 366#print axioms gauge_tendsto_zero
 367#print axioms zero_cost_is_admissible
 368#print axioms discrete_gauge_has_a_floor_and_continuous_gauge_does_not
 369
 370end UnitFromMinimality
 371end Cost
 372end IndisputableMonolith
 373