PackMatches
plain-language theorem explainer
Component-wise equality of a bridge-side dimensionless pack against a universal dimensionless target at parameter φ. RecogSpec matching claims cite this as the atomic agreement predicate. It is a pure seven-way conjunction of field equalities (α, mass ratios, mixing angles, muon g−2, strong-CP neutrality, eight-tick minimality, Born rule), with no proof obligations of its own.
Claim. For $\varphi\in\mathbb{R}$, ledger $L$ with bridge $B$, dimensionless pack $P$ on $(L,B)$, and universal dimensionless target $U$ at $\varphi$, $P$ matches $U$ when $P$ and $U$ agree on all seven components: fine-structure constant, mass ratios, mixing angles, muon $g-2$, strong-CP neutrality, eight-tick minimality, and Born-rule status.
background
RecogSpec packages the dimensionless observables that a Recognition ledger-and-bridge pair is required to reproduce. A DimlessPack is the concrete, bridge-side record of those observables (α, mass ratios, CKM/PMNS-style mixing angles, muon anomalous moment, strong-CP neutrality flag, eight-tick minimality, Born rule). A UniversalDimless target is the corresponding φ-parameterized ideal record that the framework claims is forced.
Matching is deliberately component-wise rather than existential: each field of the pack must equal the corresponding field of the universal target. The fine-structure slot is the usual α; the eight-tick slot records the T7 octave constraint (period $2^3$); the Born slot records the two-outcome Born certificate. RS-native units ($c=1$, tick/voxel gauge) sit underneath but do not appear in the predicate itself.
Upstream constants such as alpha and the RS-native unit gauge supply the numeric and unit conventions that packs and targets are expected to share; this definition only asserts equality of already-formed records.
proof idea
Definitional, not a proved theorem. The body is the seven-fold conjunction of propositional equalities between corresponding fields of the pack $P$ and the universal target $U$. No tactics, no lemmas, no rewriting: inhabiting the Prop means exhibiting (or later proving) those seven equalities.
why it matters
This is the atomic matching relation for the RecogSpec layer. Downstream, MatchesEval specializes it to the designated evaluator dimlessPack_explicit, so that "the explicit pack matches $U$" is just PackMatches at that pack. The lemma matchesEval_explicit then discharges the specialized claim against UD_explicit by simp unfolding.
Architecturally it removes an existential "some pack matches" form: any future strengthening of the explicit pack automatically strengthens the match. Framework landmarks touched by the seven slots include the fine-structure band near $1/137$, the mass φ-ladder ratios, T7 eight-tick minimality, and the Born-rule certificate. It does not itself force φ or derive the constants; it only states what full dimensionless agreement means.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.