inv_pow_self

formal source

 102lemma inv_self (φ : ℝ) : PhiClosed φ (φ⁻¹) :=
 103  inv (self φ)
 104
 105lemma inv_pow_self (φ : ℝ) (n : ℕ) : PhiClosed φ ((φ ^ n)⁻¹) :=
 106  inv (pow_self φ n)
 107
 108lemma of_nat (φ : ℝ) (n : ℕ) : PhiClosed φ (n : ℝ) := by
 109  simpa using of_rat φ n
 110
 111lemma half (φ : ℝ) : PhiClosed φ (1 / (2 : ℝ)) := by
 112  have htwo : PhiClosed φ ((2 : ℚ) : ℝ) := of_rat φ 2
 113  simpa using inv htwo
 114
 115end PhiClosed
 116
 117/-- Universal φ-closed targets RS claims are forced to take. -/
 118structure UniversalDimless (φ : ℝ) : Type where
 119  alpha0        : ℝ
 120  massRatios0   : LeptonMassRatios
 121  mixingAngles0 : CkmMixingAngles
 122  g2Muon0       : ℝ
 123  strongCP0     : Prop
 124  eightTick0    : Prop
 125  born0         : Prop
 126  alpha0_isPhi        : PhiClosed φ alpha0
 127  massRatios0_isPhi   : massRatios0.Forall (PhiClosed φ)
 128  mixingAngles0_isPhi : mixingAngles0.Forall (PhiClosed φ)
 129  g2Muon0_isPhi       : PhiClosed φ g2Muon0
 130
 131/-- "Bridge B matches universal U" (pure proposition). -/
 132def Matches (φ : ℝ) (L : Ledger) (B : Bridge L) (U : UniversalDimless φ) : Prop :=
 133  ∃ (P : DimlessPack L B),
 134    P.alpha = U.alpha0
 135      ∧ P.massRatios = U.massRatios0