IndisputableMonolith.Cost.JcostLogic

   1import Mathlib
   2import IndisputableMonolith.Cost.FunctionalEquation
   3import IndisputableMonolith.Foundation.LogicRealConstants
   4
   5/-!
   6  JcostLogic.lean
   7
   8  The canonical reciprocal cost on recovered reals.
   9
  10  This is a transport mirror of `Cost.JcostCore`: definitions live on
  11  `LogicReal`, while theorem proofs reduce to the already-verified real
  12  theorem surface through `LogicReal.toReal`.
  13-/
  14
  15namespace IndisputableMonolith
  16namespace Cost
  17namespace JcostLogic
  18
  19open Foundation.RealsFromLogic
  20open Foundation.RealsFromLogic.LogicReal
  21
  22noncomputable section
  23
  24/-- Canonical reciprocal cost on recovered reals. -/
  25def JcostL (x : LogicReal) : LogicReal :=
  26  (x + x⁻¹) / fromReal 2 - fromReal 1
  27
  28@[simp] theorem toReal_JcostL (x : LogicReal) :
  29    toReal (JcostL x) = Jcost (toReal x) := by
  30  simp [JcostL, Jcost, toReal_fromReal]
  31
  32theorem JcostL_unit0 : JcostL (fromReal 1) = fromReal 0 := by
  33  rw [eq_iff_toReal_eq, toReal_JcostL, toReal_fromReal, toReal_fromReal]
  34  exact Jcost_unit0
  35
  36theorem JcostL_symm {x : LogicReal} (hx : (0 : LogicReal) < x) :
  37    JcostL x = JcostL x⁻¹ := by
  38  rw [eq_iff_toReal_eq, toReal_JcostL, toReal_JcostL, toReal_inv]
  39  have hx' : 0 < toReal x := by simpa [lt_iff_toReal_lt] using hx
  40  exact Jcost_symm hx'
  41
  42theorem JcostL_nonneg {x : LogicReal} (hx : (0 : LogicReal) < x) :
  43    (0 : LogicReal) ≤ JcostL x := by
  44  rw [le_iff_toReal_le, toReal_zero, toReal_JcostL]
  45  have hx' : 0 < toReal x := by simpa [lt_iff_toReal_lt] using hx
  46  exact Jcost_nonneg hx'
  47
  48theorem JcostL_eq_sq {x : LogicReal} (hx : toReal x ≠ 0) :
  49    JcostL x = (x - fromReal 1) * (x - fromReal 1) / (fromReal 2 * x) := by
  50  rw [eq_iff_toReal_eq]
  51  simp [toReal_JcostL, toReal_fromReal]
  52  simpa [pow_two] using Jcost_eq_sq hx
  53
  54theorem JcostL_zero_iff {x : LogicReal} (hx : (0 : LogicReal) < x) :
  55    JcostL x = fromReal 0 ↔ x = fromReal 1 := by
  56  constructor
  57  · intro h
  58    rw [eq_iff_toReal_eq]
  59    have hx' : 0 < toReal x := by simpa [lt_iff_toReal_lt] using hx
  60    have hx0 : toReal x ≠ 0 := ne_of_gt hx'
  61    have hreal : Jcost (toReal x) = 0 := by
  62      have := congrArg toReal h
  63      rwa [toReal_JcostL, toReal_fromReal] at this
  64    rw [Jcost_eq_sq hx0] at hreal
  65    have hden : (0 : ℝ) < 2 * toReal x := by nlinarith
  66    have hsq : (toReal x - 1) ^ 2 = 0 := by
  67      have := congrArg (fun y : ℝ => y * (2 * toReal x)) hreal
  68      field_simp [ne_of_gt hden] at this
  69      simpa using this
  70    have hsub : toReal x - 1 = 0 := sq_eq_zero_iff.mp hsq
  71    rw [toReal_fromReal]
  72    linarith
  73  · intro h
  74    rw [h, JcostL_unit0]
  75
  76/-- Recognition Composition Law on recovered reals for a cost function. -/
  77def SatisfiesCompositionLawL (F : LogicReal → LogicReal) : Prop :=
  78  ∀ x y : LogicReal, (0 : LogicReal) < x → (0 : LogicReal) < y →
  79    F (x * y) + F (x / y)
  80      = fromReal 2 * F x * F y + fromReal 2 * F x + fromReal 2 * F y
  81
  82/-- A recovered-real function transported to a real function. -/
  83def transportCost (F : LogicReal → LogicReal) : ℝ → ℝ :=
  84  fun x => toReal (F (fromReal x))
  85
  86/-- Transported RCL: a recovered-real composition law becomes the existing
  87real composition law under `toReal`. -/
  88theorem compositionLawL_to_real {F : LogicReal → LogicReal}
  89    (hF : SatisfiesCompositionLawL F) :
  90    Cost.FunctionalEquation.SatisfiesCompositionLaw (transportCost F) := by
  91  intro x y hx hy
  92  unfold transportCost
  93  have hxL : (0 : LogicReal) < fromReal x := by
  94    rw [lt_iff_toReal_lt, toReal_zero, toReal_fromReal]; exact hx
  95  have hyL : (0 : LogicReal) < fromReal y := by
  96    rw [lt_iff_toReal_lt, toReal_zero, toReal_fromReal]; exact hy
  97  have hxy : fromReal x * fromReal y = fromReal (x * y) := by
  98    rw [eq_iff_toReal_eq]
  99    simp [toReal_fromReal]
 100  have hdiv : fromReal x / fromReal y = fromReal (x / y) := by
 101    rw [eq_iff_toReal_eq]
 102    simp [toReal_fromReal]
 103  have hL := hF (fromReal x) (fromReal y) hxL hyL
 104  rw [hxy, hdiv] at hL
 105  have h := congrArg toReal hL
 106  simpa [toReal_add, toReal_mul, toReal_div, toReal_fromReal] using h
 107
 108end
 109
 110end JcostLogic
 111end Cost
 112end IndisputableMonolith
 113