dimlessPack_explicit
plain-language theorem explainer
Explicit constructor for the bridge-side dimensionless observables pack: fine-structure value, mass ratios, mixing angles, muon g-2, strong-CP neutrality, eight-tick minimality, and Born-rule status, all keyed by a real scale φ. Spec and verification authors cite it as the designated evaluator that MatchesEval and PackMatches compare to the universal target. The body is a pure record fill from φ-defaults and fixed witnesses; ledger and bridge are unused parameters.
Claim. Given a real scale $\varphi$, a ledger $L$, and a bridge $B$ on $L$, form the dimensionless pack whose components are the default $\varphi$-formulas for $\alpha$, mass ratios, mixing angles, and muon $g-2$, together with the fixed witnesses for strong-CP neutrality, eight-tick minimality, and the Born rule.
background
RecogSpec packages Recognition Science predictions as dimensionless packs attached to a ledger (double-entry recognition events) and a bridge (comparison structure from ledger to observables). A DimlessPack holds the bridge-side values that should match a universal target at scale $\varphi$: electromagnetic $\alpha$, mass ratios on the $\varphi$-ladder, mixing angles, muon $g-2$, plus boolean-style witnesses for strong-CP neutrality, eight-tick minimality (the $2^3$ octave from the forcing chain), and Born-rule behavior.
The module treats this definition as the designated evaluator: matching claims are stated against this concrete pack rather than an existential choice of pack. Upstream constants supply $\alpha$ formulas and related anchors; the ledger and bridge types come from the foundation layer. Downstream honesty certificates already record that the present evaluator does not inspect $L$ or $B$.
proof idea
Not a proof: a noncomputable structure literal. Each field is assigned a named default or witness depending only on $\varphi$ (or on nothing): alphaDefault, massRatiosDefault, mixingAnglesDefault, g2Default, plus kGateWitness, eightTickWitness, and bornHolds. No lemmas are applied; the ledger and bridge arguments are ignored in the body.
why it matters
This is the fixed evaluator that turns universal dimensionless targets into checkable equalities. PackMatches and MatchesEval compare it component-wise to UniversalDimless; matchesEval_explicit discharges the match against the explicit universal pack by simp unfolding. Inevitability predicates and anchor-uniqueness results in the same module route through it. Framework landmarks touched: $\alpha$ in the RS band, mass ratios on the $\varphi$-ladder, the eight-tick octave (T7), and Born-rule certification.
HonestClosureCert explicitly flags the open gap: a true structural derivation must use $L$ and $B$. Until then, inevitability witnesses built on this placeholder sit outside the certified surface.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.