MatchesEval
plain-language theorem explainer
Computed matching asserts that the explicit dimensionless pack built from a ledger and bridge equals a given universal dimensionless target at φ. Spec authors and inevitability proofs cite it to pin matching to one designated evaluator rather than an existential pack. The body is a one-line abbreviation of pack-matching against that evaluator.
Claim. For golden-ratio parameter $\varphi\in\mathbb{R}$, ledger $L$, bridge $B$ on $L$, and universal dimensionless target $U$ at $\varphi$, the designated explicit dimensionless pack of $(\varphi,L,B)$ matches $U$.
background
In RecogSpec, dimensionless physics is packaged as a universal target at the self-similar scale $\varphi$ (the fixed point forced in the RS chain). A ledger is a double-entry record of recognition events; a bridge is a commuting display/observe map from native ledger data to observables. Matching means the dimensionless invariants extracted from $(L,B)$ agree with the target $U$.
The older matching claim allowed any pack that fits. Here the pack is fixed: the designated evaluator builds one explicit dimensionless pack from $\varphi$, $L$, and $B$. RS-native units set $\tau_0=1$ tick, $\ell_0=1$ voxel, $c=1$, so the pack is already in the gauge used by the rest of the monolith.
Sibling predicates (band membership, unique calibration, anchor equivalence) sit nearby; this definition only records pack equality against $U$, not band widths or calibration uniqueness.
proof idea
Definitional abbreviation, not a proved theorem. The predicate is exactly pack-matching of the explicit dimensionless pack of $(\varphi,L,B)$ against the universal target $U$. Downstream, the lemma that the explicit universal target matches is a simp unfolding of this abbreviation together with the pack and target constructors.
why it matters
Inevitability of the dimensionless layer is stated as: every ledger/bridge matches the explicit universal target under this predicate, plus non-vacuity of the target's propositional fields. By routing through the designated evaluator, any future tightening of that evaluator automatically tightens inevitability, without rewriting existential pack hypotheses.
The companion lemma discharges the match for the explicit universal target by simplification. In the broader RS picture this sits under dimensionless closure toward the forced $\varphi$ ladder and the display of constants (including the fine-structure band), not under the geometric forcing steps T7–T8 themselves.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.