IndisputableMonolith.Foundation.LogicRealConstants

   1import Mathlib
   2import IndisputableMonolith.Constants
   3import IndisputableMonolith.Constants.Alpha
   4import IndisputableMonolith.Verification.EMAlphaCert
   5import IndisputableMonolith.Foundation.LogicRealTranscendentals
   6
   7/-!
   8  LogicRealConstants.lean
   9
  10  Recognition Science constants mirrored on the recovered real line.
  11
  12  The definitions are expressed in `LogicReal`; each theorem proves that
  13  transport through `LogicReal.toReal` recovers the existing real-valued
  14  constant from `IndisputableMonolith.Constants`.
  15-/
  16
  17namespace IndisputableMonolith
  18namespace Foundation
  19namespace LogicRealConstants
  20
  21open RealsFromLogic RealsFromLogic.LogicReal
  22open LogicRealTranscendentals
  23
  24noncomputable section
  25
  26/-- Recovered golden ratio. -/
  27def phiL : LogicReal :=
  28  (fromReal 1 + sqrtL (fromReal 5)) / fromReal 2
  29
  30/-- Recovered tick unit. -/
  31def tickL : LogicReal := fromReal Constants.tick
  32
  33/-- Recovered octave. -/
  34def octaveL : LogicReal := fromReal Constants.octave
  35
  36/-- Recovered J-bit constant. -/
  37def JbitL : LogicReal := logL phiL
  38
  39/-- Recovered coherence scale. -/
  40def EcohL : LogicReal := fromReal Constants.E_coh
  41
  42/-- Recovered hbar. -/
  43def hbarL : LogicReal := rpowL phiL (fromReal (-(5 : ℝ)))
  44
  45/-- Recovered Newton constant in RS-native units. -/
  46def gravL : LogicReal := fromReal Constants.G
  47
  48/-- Recovered Einstein coupling. -/
  49def kappaEinsteinL : LogicReal := fromReal Constants.kappa_einstein
  50
  51/-- Recovered inverse fine-structure constant. -/
  52def alphaInvL : LogicReal := fromReal Constants.alphaInv
  53
  54@[simp] theorem toReal_phiL : toReal phiL = Constants.phi := by
  55  simp [phiL, Constants.phi, toReal_fromReal]
  56
  57@[simp] theorem toReal_tickL : toReal tickL = Constants.tick := toReal_fromReal _
  58
  59@[simp] theorem toReal_octaveL : toReal octaveL = Constants.octave := toReal_fromReal _
  60
  61@[simp] theorem toReal_JbitL : toReal JbitL = Constants.J_bit := by
  62  simp [JbitL, Constants.J_bit]
  63
  64@[simp] theorem toReal_EcohL : toReal EcohL = Constants.E_coh := toReal_fromReal _
  65
  66@[simp] theorem toReal_hbarL : toReal hbarL = Constants.hbar := by
  67  rw [Constants.hbar_eq_phi_inv_fifth]
  68  simp [hbarL, toReal_phiL, toReal_fromReal]
  69
  70@[simp] theorem toReal_gravL : toReal gravL = Constants.G := toReal_fromReal _
  71
  72@[simp] theorem toReal_kappaEinsteinL :
  73    toReal kappaEinsteinL = Constants.kappa_einstein := toReal_fromReal _
  74
  75@[simp] theorem toReal_alphaInvL : toReal alphaInvL = Constants.alphaInv := toReal_fromReal _
  76
  77/-- Positivity of recovered φ. -/
  78theorem phiL_pos : (0 : LogicReal) < phiL := by
  79  rw [lt_iff_toReal_lt, toReal_zero, toReal_phiL]
  80  exact Constants.phi_pos
  81
  82/-- Recovered φ exceeds 1. -/
  83theorem phiL_gt_one : (1 : LogicReal) < phiL := by
  84  rw [lt_iff_toReal_lt, toReal_one, toReal_phiL]
  85  exact Constants.phi_gt_one
  86
  87/-- Recovered lower numerical φ bound. -/
  88theorem phiL_gt_onePointFive : fromReal (1.5 : ℝ) < phiL := by
  89  rw [lt_iff_toReal_lt, toReal_fromReal, toReal_phiL]
  90  exact Constants.phi_gt_onePointFive
  91
  92/-- Recovered upper numerical φ bound. -/
  93theorem phiL_lt_onePointSixTwo : phiL < fromReal (1.62 : ℝ) := by
  94  rw [lt_iff_toReal_lt, toReal_fromReal, toReal_phiL]
  95  exact Constants.phi_lt_onePointSixTwo
  96
  97/-- Recovered hbar identity. -/
  98theorem hbarL_eq_phi_inv_fifth : hbarL = rpowL phiL (fromReal (-(5 : ℝ))) := rfl
  99
 100/-- Recovered hbar numerical bounds. -/
 101theorem hbarL_bounds : fromReal (0.088 : ℝ) < hbarL ∧ hbarL < fromReal (0.093 : ℝ) := by
 102  constructor
 103  · rw [lt_iff_toReal_lt, toReal_fromReal, toReal_hbarL]
 104    exact Constants.hbar_bounds.1
 105  · rw [lt_iff_toReal_lt, toReal_fromReal, toReal_hbarL]
 106    exact Constants.hbar_bounds.2
 107
 108/-- Recovered alpha inverse has the verified EM range. -/
 109theorem alphaInvL_bounds : fromReal (137.030 : ℝ) < alphaInvL ∧
 110    alphaInvL < fromReal (137.039 : ℝ) := by
 111  have h := (Verification.EMAlpha.EMAlphaCert.verified_any ⟨⟩).2.2.2
 112  constructor
 113  · rw [lt_iff_toReal_lt, toReal_fromReal, toReal_alphaInvL]
 114    exact h.1
 115  · rw [lt_iff_toReal_lt, toReal_fromReal, toReal_alphaInvL]
 116    exact h.2
 117
 118end
 119
 120end LogicRealConstants
 121end Foundation
 122end IndisputableMonolith
 123