matchesEval_explicit
plain-language theorem explainer
For any real scale φ, ledger L, and bridge B, the explicit universal dimensionless pack equals the pack computed by the designated evaluator on (L,B). Spec and inevitability authors cite it to discharge the matching half of dimensionless inevitability without existential choice. The proof is a one-shot simp unfolding of MatchesEval, PackMatches, and the two explicit pack constructors.
Claim. For every real $\varphi$, every ledger $L$, and every bridge $B$ on $L$, the designated dimensionless pack extracted from $(L,B)$ matches the explicit universal dimensionless data $U_{\mathrm{explicit}}(\varphi)$ (fine-structure default, mass ratios, mixing angles, muon $g-2$, strong-CP gate, eight-tick witness, and Born compliance).
background
RecogSpec packages Recognition Science predictions as dimensionless packs: fine-structure $\alpha$, mass ratios, mixing angles, muon $g-2$, a strong-CP gate, the eight-tick octave witness, and Born-rule compliance. A ledger is a double-entry list of recognition events; a bridge is a commuting display/observe triple from native ledger data to observables.
MatchesEval is the non-existential matching predicate: the fixed evaluator dimlessPack_explicit applied to $(\varphi,L,B)$ must agree with a given universal pack $U$. The companion pack UD_explicit $\varphi$ hard-wires the RS defaults (phi-closed $\alpha$, default mass and mixing ladders, $k$-gate strong CP, eight-tick, and the two-outcome Born certificate).
This sits in the RecogSpec layer that turns foundation forcing (J-cost uniqueness, $\varphi$ fixed point, eight-tick period $2^3$) into checkable dimensionless claims against anchors and bands.
proof idea
Term-mode proof by a single simp on the four definitional equalities MatchesEval, PackMatches, dimlessPack_explicit, and UD_explicit. After unfolding, both sides are the same constructor fields, so the match goal reduces to reflexivity. No arithmetic or external lemmas are required.
why it matters
Feeds the first conjunct of inevitability_dimless_holds: for every ledger and bridge, the explicit pack matches under the designated evaluator. That theorem is the scaffold entry point for dimensionless inevitability in RecogSpec.
By pinning match to the concrete evaluator rather than an existential pack, any future strengthening of dimlessPack_explicit automatically tightens the inevitability claim. The pack itself carries framework landmarks: eight-tick octave (T7), Born compliance via the two-outcome certificate, and phi-closed $\alpha$ in the RS band. It does not itself prove band membership or calibration uniqueness; those are sibling predicates (MeetsBands, UniqueCalibration) used elsewhere in the scaffold.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.