UD_explicit
plain-language theorem explainer
Explicit universal dimensionless target pack at a real parameter φ: fine-structure constant, lepton mass ratios, CKM mixing angles, muon g−2, strong-CP and eight-tick witnesses, plus Born-rule compliance, each with a φ-closedness certificate. Anyone stating RS inevitability of dimensionless observables cites this pack as the canonical target. Construction is a structure literal wiring default values and short PhiClosed proofs.
Claim. For any real $\varphi$, there is an explicit universal dimensionless pack whose components are the default $\varphi$-expressions for $\alpha$, the three lepton mass ratios, the three CKM mixing-angle magnitudes, and muon $g-2$, together with fixed strong-CP and eight-tick witnesses and a Born-rule compliance proposition, and such that each real component lies in the subfield generated by $\varphi$.
background
In RecogSpec, dimensionless RS targets are bundled as a UniversalDimless structure at a fixed real $\varphi$: fine-structure value, lepton inter-generation mass ratios $(\mu/e,\tau/e,\tau/\mu)$, CKM mixing-angle magnitudes $(V_{us},V_{cb},V_{ub})$, muon $g-2$, plus propositional slots for strong CP, the eight-tick octave, and Born-rule compliance.
PhiClosed $\varphi$ $x$ means $x$ lies in the subfield generated by $\varphi$ under field operations. The lemma PhiClosed.self records that $\varphi$ itself is closed. Payload helpers LeptonMassRatios.Forall and the CKM analogue assert a predicate on every component of those records.
The module assembles the explicit pack used by matching and inevitability predicates: every ledger/bridge is required to hit this same $\varphi$-closed target, not an arbitrary one.
proof idea
Structure literal, not a deep proof. Numeric slots are filled by the module defaults alphaDefault, massRatiosDefault, mixingAnglesDefault, and g2Default at $\varphi$. Propositional slots take the fixed witnesses kGateWitness, eightTickWitness, and bornHolds (the two-outcome Born certificate).
φ-closedness obligations: alpha0_isPhi is phiClosed_alphaDefault; g2Muon0_isPhi is phiClosed_one_div_pow φ 5. Mass-ratio closedness unfolds LeptonMassRatios.Forall on the default triple and supplies PhiClosed.self, phiClosed_one_div_pow _ 2, and phiClosed_one_div. Mixing-angle closedness likewise unfolds the CKM Forall and uses one-over and one-over-power closedness at exponents 1, 2, 3.
why it matters
This is the canonical dimensionless target that RS claims every calibrated bridge must match. Downstream, matchesEval_explicit is a one-line simp proof that every ledger/bridge matches this pack, and Inevitability_dimless is the conjunction of universal matching against UD_explicit with non-vacuity of the Prop fields (Born, eight-tick, strong CP).
It also feeds RecognitionClosureNonVacuityCert, which requires recognition closure to imply the non-vacuous inevitability statement, and appears in the anchor-uniqueness development via the same Spec layer. Framework landmarks touched: eight-tick octave (T7), Born-path weights, and the φ-ladder expressions for α-band and mass/mixing ratios. Without an explicit pack, inevitability would quantify over an unspecified target and become vacuous.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.