UniversalDimless
UniversalDimless packages the dimensionless observables that must lie in the subfield generated by φ. Researchers matching RS predictions to SM parameters cite it to fix the target values for alpha, lepton mass ratios, CKM angles, and muon g-2. The declaration is a direct structure definition that attaches PhiClosed conditions to each component.
claimLet φ be real. The structure UniversalDimless(φ) consists of a real α₀, lepton mass ratios, CKM mixing angles, a real g_{2μ,0}, and propositions for strong CP violation, the eight-tick octave, and the Born rule, together with the assertions that α₀, each mass ratio, each mixing angle, and g_{2μ,0} all lie in the subfield generated by φ.
background
PhiClosed φ x is the predicate that x belongs to the subfield of ℝ generated by φ under addition, multiplication, and inversion. The module RecogSpec.Core works with dimensionless packs over bridges on ledgers, using observable structures such as LeptonMassRatios and CkmMixingAngles. Upstream, RSNativeUnits.U fixes the native gauge with τ₀ = 1 tick and ℓ₀ = 1 voxel while Recognition.U supplies the structural equality used for recognition relations.
proof idea
Direct structure definition. The declaration lists the observable fields and attaches the PhiClosed conditions as field requirements; no tactics or lemmas are applied.
why it matters in Recognition Science
The structure supplies the universal target values consumed by the Matches predicate, which checks whether a concrete Bridge over a Ledger reproduces the listed phi-closed observables. It encodes the requirement that the fine-structure constant, mass ratios, and mixing angles are forced into the phi-subfield by the Recognition Composition Law and the eight-tick octave step in the T0-T8 chain. It leaves open the derivation of the precise numerical values from the phi-ladder.
scope and limits
- Does not assign numerical values to any observable.
- Does not prove that the listed quantities satisfy PhiClosed.
- Does not instantiate a specific Ledger or Bridge.
- Does not impose PhiClosed on the strongCP0, eightTick0, or born0 propositions.
formal statement (Lean)
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). -/