IndisputableMonolith.Foundation.LogicAsFunctionalEquation.PositiveRatioForcing

   1import Mathlib
   2import IndisputableMonolith.Foundation.LogicAsFunctionalEquation.FiniteLogicalComparison
   3
   4/-!
   5# Positive ratios as forced comparison coordinates
   6
   7Scale-invariant comparison on positive magnitudes factors through the ratio
   8`x / y`.  This module packages that fact as a reusable universal property.
   9-/
  10
  11namespace IndisputableMonolith
  12namespace Foundation
  13namespace LogicAsFunctionalEquation
  14
  15/-- The ratio-derived cost of a two-argument comparison. -/
  16@[simp] def ratioCost (C : ComparisonOperator) : ℝ → ℝ :=
  17  fun r => C r 1
  18
  19/-- Scale-invariant comparison factors through the positive ratio `x / y`. -/
  20theorem scale_free_comparison_factors_through_ratio
  21    (C : ComparisonOperator)
  22    (hScale : ScaleInvariant C) :
  23    ∃ F : ℝ → ℝ, ∀ x y : ℝ, 0 < x → 0 < y → C x y = F (x / y) := by
  24  refine ⟨ratioCost C, ?_⟩
  25  intro x y hx hy
  26  unfold ratioCost
  27  have hy_inv_pos : 0 < y⁻¹ := inv_pos.mpr hy
  28  have hscale := hScale x y y⁻¹ hx hy hy_inv_pos
  29  have hleft : y⁻¹ * x = x / y := by
  30    rw [div_eq_mul_inv, mul_comm]
  31  have hright : y⁻¹ * y = 1 := by
  32    exact inv_mul_cancel₀ (ne_of_gt hy)
  33  calc
  34    C x y = C (y⁻¹ * x) (y⁻¹ * y) := hscale.symm
  35    _ = C (x / y) 1 := by rw [hleft, hright]
  36
  37/-- The ratio factor is unique on positive ratios. -/
  38theorem ratio_factor_unique
  39    (C : ComparisonOperator) (F G : ℝ → ℝ)
  40    (hF : ∀ x y : ℝ, 0 < x → 0 < y → C x y = F (x / y))
  41    (hG : ∀ x y : ℝ, 0 < x → 0 < y → C x y = G (x / y)) :
  42    ∀ r : ℝ, 0 < r → F r = G r := by
  43  intro r hr
  44  have hF' := hF r 1 hr one_pos
  45  have hG' := hG r 1 hr one_pos
  46  simpa using hF'.symm.trans hG'
  47
  48/-- The canonical factor obtained from scale invariance is exactly
  49`derivedCost`. -/
  50theorem ratioCost_eq_derivedCost (C : ComparisonOperator) :
  51    ratioCost C = derivedCost C := by
  52  rfl
  53
  54/-- Searchable alias: positive ratios are forced by scale-free comparison. -/
  55theorem positive_ratio_is_forced_by_scale_free_comparison
  56    (C : ComparisonOperator)
  57    (hScale : ScaleInvariant C) :
  58    ∃ F : ℝ → ℝ, ∀ x y : ℝ, 0 < x → 0 < y → C x y = F (x / y) :=
  59  scale_free_comparison_factors_through_ratio C hScale
  60
  61end LogicAsFunctionalEquation
  62end Foundation
  63end IndisputableMonolith
  64