UniversalDimless
plain-language theorem explainer
UniversalDimless φ packages the dimensionless observables (fine-structure constant, lepton mass ratios, CKM angles, muon g-2) together with three propositional flags that Recognition Science requires to lie inside the subfield generated by φ. A physicist stating the target values any ledger must reproduce cites this structure. The declaration is a plain structure definition with field-wise PhiClosed constraints and no proof obligations.
Claim. Let φ ∈ ℝ. UniversalDimless φ is the structure whose fields are α₀ ∈ ℝ, lepton mass ratios, CKM mixing angles, g-2 muon anomaly, plus three propositions (strong-CP phase, eight-tick octave, Born rule), each required to satisfy PhiClosed φ (i.e., membership in the subfield generated by φ under field operations).
background
PhiClosed φ x is the predicate x ∈ phiSubfield φ, the subfield of ℝ generated by φ. Bridge L is the trivial structure over a Ledger that carries units equivalence. RSNativeUnits.U fixes the native gauge τ₀ = 1 tick, ℓ₀ = 1 voxel, c = 1. ObservablePayloads supplies the concrete record types LeptonMassRatios, CkmMixingAngles and the Forall combinator that lifts a predicate over all three lepton ratios.
proof idea
The declaration is a structure definition; no lemmas or tactics are applied.
why it matters
Matches (downstream) uses UniversalDimless φ to express the proposition that a concrete Bridge reproduces the universal targets. The structure therefore supplies the φ-closed reference values that Recognition Science claims must be recovered from any ledger, directly supporting the dimensionless sector of the forcing chain (T5–T7).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.