structure
definition
UniversalDimless
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.RecogSpec.Core on GitHub at line 118.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
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
136 ∧ P.mixingAngles = U.mixingAngles0
137 ∧ P.g2Muon = U.g2Muon0
138 ∧ P.strongCPNeutral = U.strongCP0
139 ∧ P.eightTickMinimal = U.eightTick0
140 ∧ P.bornRule = U.born0
141
142end
143
144end RecogSpec
145end IndisputableMonolith