F_ofZ

formal source

  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