AbsolutePack

formal source

  35  bornRule         : Prop
  36
  37/-- Absolute (SI) packaging for reference displays, distinct from dimensionless pack. -/
  38structure AbsolutePack (L : Ledger) (B : Bridge L) : Type where
  39  c_SI        : ℝ
  40  hbar_SI     : ℝ
  41  G_SI        : ℝ
  42  Lambda_SI   : ℝ
  43  masses_SI   : List ℝ
  44  energies_SI : List ℝ
  45
  46/-- Subfield generated by `φ`. -/
  47def phiSubfield (φ : ℝ) : Subfield ℝ :=
  48  Subfield.closure ({φ} : Set ℝ)
  49
  50/-- The value `x` is algebraic over the subfield generated by `φ` using field
  51operations. -/
  52def PhiClosed (φ x : ℝ) : Prop := x ∈ phiSubfield φ
  53
  54namespace PhiClosed
  55
  56variable {φ x y : ℝ}
  57
  58@[simp] lemma mem : PhiClosed φ x ↔ x ∈ phiSubfield φ := Iff.rfl
  59
  60lemma self (φ : ℝ) : PhiClosed φ φ := by
  61  change φ ∈ phiSubfield φ
  62  exact Subfield.subset_closure (by simp)
  63
  64lemma of_rat (φ : ℝ) (q : ℚ) : PhiClosed φ (q : ℝ) := by
  65  change ((algebraMap ℚ ℝ) q) ∈ phiSubfield φ
  66  simpa using (phiSubfield φ).algebraMap_mem q
  67
  68lemma zero (φ : ℝ) : PhiClosed φ (0 : ℝ) :=