IndisputableMonolith.RecogSpec.Scales

   1import Mathlib
   2import IndisputableMonolith.Constants
   3
   4namespace IndisputableMonolith
   5namespace RecogSpec
   6
   7/-! Binary scales and φ-exponential wrappers -/
   8
   9/-- Binary scale factor `B = 2^k` as a real. -/
  10def B_of (k : Nat) : ℝ := (2 : ℝ) ^ k
  11
  12@[simp] lemma B_of_zero : B_of 0 = 1 := by simp [B_of]
  13
  14@[simp] lemma B_of_succ (k : Nat) : B_of (k+1) = 2 * B_of k := by
  15  simp [B_of, pow_succ, mul_comm]
  16
  17lemma B_of_pos (k : Nat) : 0 < B_of k := by
  18  have : 0 < (2:ℝ) := by norm_num
  19  simpa [B_of] using pow_pos this k
  20
  21@[simp] lemma B_of_one : B_of 1 = 2 := by simp [B_of]
  22
  23lemma one_le_B_of (k : Nat) : (1 : ℝ) ≤ B_of k := by
  24  induction k with
  25  | zero => simp [B_of]
  26  | succ k ih =>
  27      have hmul : (2 : ℝ) ≤ 2 * B_of k := by
  28        have : 2 * (1 : ℝ) ≤ 2 * B_of k := by
  29          have hnonneg : 0 ≤ (2 : ℝ) := by norm_num
  30          exact mul_le_mul_of_nonneg_left ih hnonneg
  31        simpa using this
  32      have h12 : (1 : ℝ) ≤ 2 := by norm_num
  33      have : (1 : ℝ) ≤ 2 * B_of k := le_trans h12 hmul
  34      simpa [B_of_succ, mul_comm] using this
  35
  36/-- Two to an integer power: 2^k for k ∈ ℤ. -/
  37noncomputable def twoPowZ (k : Int) : ℝ :=
  38  if 0 ≤ k then (2 : ℝ) ^ (Int.toNat k)
  39  else 1 / ((2 : ℝ) ^ (Int.toNat (-k)))
  40
  41@[simp] lemma twoPowZ_zero : twoPowZ 0 = 1 := by simp [twoPowZ]
  42@[simp] lemma twoPowZ_ofNat (k : Nat) : twoPowZ (Int.ofNat k) = (2 : ℝ) ^ k := by simp [twoPowZ]
  43@[simp] lemma twoPowZ_negSucc (k : Nat) : twoPowZ (Int.negSucc k) = 1 / ((2 : ℝ) ^ k.succ) := by
  44  simp [twoPowZ]
  45
  46/-- φ-power wrapper. -/
  47noncomputable def PhiPow (x : ℝ) : ℝ := Real.exp (Real.log (Constants.phi) * x)
  48
  49lemma PhiPow_add (x y : ℝ) : PhiPow (x + y) = PhiPow x * PhiPow y := by
  50  unfold PhiPow
  51  have hx : Real.log (Constants.phi) * (x + y)
  52        = Real.log (Constants.phi) * x + Real.log (Constants.phi) * y := by
  53    ring
  54  simp [hx, Real.exp_add]
  55
  56lemma PhiPow_sub (x y : ℝ) : PhiPow (x - y) = PhiPow x / PhiPow y := by
  57  unfold PhiPow
  58  have hx : Real.log (Constants.phi) * (x - y)
  59        = Real.log (Constants.phi) * x + Real.log (Constants.phi) * (-y) := by
  60    ring
  61  calc
  62    Real.exp (Real.log (Constants.phi) * (x - y))
  63        = Real.exp (Real.log (Constants.phi) * x + Real.log (Constants.phi) * (-y)) := by
  64              simp [hx]
  65    _   = Real.exp (Real.log (Constants.phi) * x)
  66            * Real.exp (Real.log (Constants.phi) * (-y)) := by
  67              simp [Real.exp_add]
  68    _   = Real.exp (Real.log (Constants.phi) * x)
  69            * (Real.exp (Real.log (Constants.phi) * y))⁻¹ := by
  70              simp [Real.exp_neg]
  71    _   = Real.exp (Real.log (Constants.phi) * x)
  72            / Real.exp (Real.log (Constants.phi) * y) := by
  73              simp [div_eq_mul_inv]
  74
  75@[simp] lemma PhiPow_zero : PhiPow 0 = 1 := by
  76  unfold PhiPow; simp
  77
  78@[simp] lemma PhiPow_one : PhiPow 1 = Constants.phi := by
  79  unfold PhiPow
  80  have hφ : 0 < Constants.phi := Constants.phi_pos
  81  simp [one_mul, Real.exp_log hφ]
  82
  83@[simp] lemma PhiPow_neg (y : ℝ) : PhiPow (-y) = 1 / PhiPow y := by
  84  have := PhiPow_sub 0 y
  85  simp [PhiPow_zero, sub_eq_add_neg] at this
  86  simpa using this
  87
  88@[simp] noncomputable def lambdaA : ℝ := Real.log Constants.phi
  89@[simp] noncomputable def kappaA  : ℝ := Constants.phi
  90
  91@[simp] noncomputable def F_ofZ (Z : ℤ) : ℝ := (Real.log (1 + (Z : ℝ) / kappaA)) / lambdaA
  92
  93@[simp] def Z_quark (Q : ℤ) : ℤ := 4 + (6 * Q) ^ (2 : Nat) + (6 * Q) ^ (4 : Nat)
  94@[simp] def Z_lepton (Q : ℤ) : ℤ := (6 * Q) ^ (2 : Nat) + (6 * Q) ^ (4 : Nat)
  95@[simp] def Z_neutrino : ℤ := 0
  96
  97lemma kappaA_pos : 0 < kappaA := by
  98  unfold kappaA; simpa using Constants.phi_pos
  99
 100lemma lambdaA_ne_zero : lambdaA ≠ 0 := by
 101  have hpos : 0 < Constants.phi := Constants.phi_pos
 102  have hne1 : Constants.phi ≠ 1 := Constants.phi_ne_one
 103  simpa [lambdaA] using Real.log_ne_zero_of_pos_of_ne_one hpos hne1
 104
 105lemma kappaA_ne_zero : kappaA ≠ 0 := by
 106  simpa [kappaA] using Constants.phi_ne_zero
 107
 108/-! Ledger units (δ subgroup) -/
 109namespace LedgerUnits
 110
 111/-- The subgroup of ℤ generated by δ. We specialize to δ = 1 for a clean order isomorphism. -/
 112def DeltaSub (δ : ℤ) := {x : ℤ // ∃ n : ℤ, x = n * δ}
 113
 114/-- Embed ℤ into the δ=1 subgroup. -/
 115def fromZ_one (n : ℤ) : DeltaSub 1 := ⟨n, by exact ⟨n, by simpa using (Int.mul_one n)⟩⟩
 116
 117/-- Project from the δ=1 subgroup back to ℤ by taking its value. -/
 118def toZ_one (p : DeltaSub 1) : ℤ := p.val
 119
 120@[simp] lemma toZ_fromZ_one (n : ℤ) : toZ_one (fromZ_one n) = n := rfl
 121
 122@[simp] lemma fromZ_toZ_one (p : DeltaSub 1) : fromZ_one (toZ_one p) = p := by
 123  cases p with
 124  | mk x hx =>
 125    apply Subtype.ext
 126    rfl
 127
 128/-- Explicit equivalence between the δ=1 subgroup and ℤ (mapping n·1 ↦ n). -/
 129def equiv_delta_one : DeltaSub 1 ≃ ℤ :=
 130{ toFun := toZ_one
 131, invFun := fromZ_one
 132, left_inv := fromZ_toZ_one
 133, right_inv := toZ_fromZ_one }
 134
 135end LedgerUnits
 136
 137/-! Affine maps for unit-to-scale projections -/
 138namespace Scales
 139
 140/-- Affine map from ℤ to ℝ: n ↦ slope·n + offset. -/
 141structure AffineMapZ where
 142  slope : ℝ
 143  offset : ℝ
 144
 145@[simp] def apply (f : AffineMapZ) (n : ℤ) : ℝ := f.slope * (n : ℝ) + f.offset
 146
 147/-- Map δ-subgroup to ℝ by composing an affine map with a provided projection to ℤ. -/
 148noncomputable def mapDelta (δ : ℤ) (hδ : δ ≠ 0)
 149  (toZ : {x : ℤ // ∃ n : ℤ, x = n * δ} → ℤ) (f : AffineMapZ) :
 150  {x : ℤ // ∃ n : ℤ, x = n * δ} → ℝ :=
 151  fun p => f.slope * ((toZ p) : ℝ) + f.offset
 152
 153/-- Context constructors: charge (quantum `qe`), time (τ0), and action (ħ). -/
 154@[simp] def chargeMap (qe : ℝ) : AffineMapZ := { slope := qe, offset := 0 }
 155@[simp] def timeMap (U : Constants.RSUnits) : AffineMapZ := { slope := U.tau0, offset := 0 }
 156-- actionMap omitted in minimal RSUnits (no `hbar` field)
 157
 158@[simp] lemma apply_chargeMap (qe : ℝ) (n : ℤ) :
 159  apply (chargeMap qe) n = qe * (n : ℝ) := by simp [apply, chargeMap]
 160
 161@[simp] lemma apply_timeMap (U : Constants.RSUnits) (n : ℤ) :
 162  apply (timeMap U) n = U.tau0 * (n : ℝ) := by simp [apply, timeMap]
 163
 164-- (no actionMap in minimal RSUnits)
 165
 166/-- Specialization of `mapDelta` to δ = 1 using the canonical projection. -/
 167noncomputable def mapDeltaOne
 168  (toZ : LedgerUnits.DeltaSub 1 → ℤ) (f : AffineMapZ) : LedgerUnits.DeltaSub 1 → ℝ :=
 169  fun p => f.slope * ((toZ p) : ℝ) + f.offset
 170
 171@[simp] lemma mapDeltaOne_fromZ_one
 172  (f : AffineMapZ) (n : ℤ) :
 173  mapDeltaOne LedgerUnits.toZ_one f (LedgerUnits.fromZ_one n)
 174    = f.slope * (n : ℝ) + f.offset := by
 175  simp [mapDeltaOne, LedgerUnits.toZ_one, LedgerUnits.fromZ_one]
 176
 177lemma mapDeltaOne_step (f : AffineMapZ) (n : ℤ) :
 178  mapDeltaOne LedgerUnits.toZ_one f (LedgerUnits.fromZ_one (n+1))
 179    - mapDeltaOne LedgerUnits.toZ_one f (LedgerUnits.fromZ_one n) = f.slope := by
 180  simp [mapDeltaOne, add_comm, add_left_comm, add_assoc, sub_eq_add_neg, mul_add]
 181
 182@[simp] lemma mapDeltaTime_fromZ_one
 183  (U : Constants.RSUnits) (n : ℤ) :
 184  mapDeltaOne LedgerUnits.toZ_one (timeMap U) (LedgerUnits.fromZ_one n)
 185    = U.tau0 * (n : ℝ) := by
 186  simp [mapDeltaOne, timeMap, add_comm]
 187
 188-- (no actionMap in minimal RSUnits)
 189
 190end Scales
 191
 192end RecogSpec
 193end IndisputableMonolith
 194