Matches
plain-language theorem explainer
Matches defines the predicate that a bridge over a given ledger aligns with a set of universal dimensionless targets parameterized by a real number φ. Cosmologists and particle physicists in the Recognition Science program cite it to verify consistency of derived quantities such as the fine-structure constant, lepton mass ratios, and eight-tick minimality against φ-closed values. The definition is realized directly as an existential claim over a dimensionless pack whose fields are required to equal the corresponding universal targets componentw
Claim. Given a real number $φ$, a ledger $L$, a bridge $B$ over $L$, and universal dimensionless targets $U$ for $φ$, the predicate holds if there exists a dimensionless pack $P$ such that the fine-structure constant of $P$ equals the $α_0$ component of $U$, the lepton mass ratios of $P$ equal those of $U$, the CKM mixing angles match, the muon $g-2$ value matches, the strong CP phase is neutral as specified in $U$, the eight-tick minimality condition holds, and the Born rule is satisfied as in $U$.
background
Recognition Science employs ledgers as basic carriers equipped with an optional state and tick function for bookkeeping downstream projections. Bridges over ledgers supply a minimal structural interface consisting of a unit dummy. UniversalDimless collects the forced target values for dimensionless observables that the framework requires to be φ-closed, including α₀, lepton mass ratios, CKM mixing angles, muon g-2, strong CP neutrality, eight-tick minimality, and the Born rule, each carrying explicit PhiClosed constraints.
proof idea
The definition is a direct existential quantification over a dimensionless pack whose fields are set equal to the universal targets componentwise for alpha, mass ratios, mixing angles, g2Muon, strongCPNeutral, eightTickMinimal, and bornRule.
why it matters
This definition supplies the matching interface between ledger bridges and universal dimensionless targets. It feeds downstream results on neutron-proton ratios and lithium insights in cosmology, J-cost nonnegativity in cost analysis, phi-power intervals in numerics, and experimental status checks in QFT and thermodynamics. It supports verification against the eight-tick octave and D=3 forcing steps while remaining compatible with the alpha inverse band (137.030, 137.039).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.