UniversalDimless
plain-language theorem explainer
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.
Claim. Let φ 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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.