SMVerificationCert
plain-language theorem explainer
The SMVerificationCert structure bundles three properties of the Recognition Science mass law applied to Standard Model fermions: strict positivity of every predicted mass, exact multiplicative scaling by phi under unit rung increase, and the enumeration of exactly nine fermion species. Researchers checking zero-parameter derivations of lepton and quark masses would cite this certificate when confirming consistency with the phi-ladder construction. The declaration is a plain structure definition that packages the three statements as fields, to
Claim. A structure asserting that every fermion mass prediction satisfies $m(f)>0$, that the master mass law obeys $m(s,r+1,z)=phicdot m(s,r,z)$ for all sectors $s$, rungs $r$ and charge parameters $z$, and that the set of fermion species has cardinality nine, where $m$ denotes the yardstick times $phi$ to the power of the adjusted rung.
background
The module states RS mass predictions for Standard Model particles via the formula $m=$ yardstick(Sector) $times phi^{r-8+gap(Z)}$, derived from three-dimensional cube geometry with zero free parameters. Fermion is the inductive type listing the nine charged species (electron, muon, tauon, up, charm, top, down, strange, bottom). Sector classifies particles into Lepton, UpQuark, DownQuark and Electroweak categories, each carrying its own yardstick constant.
proof idea
The declaration is a structure definition whose three fields are independent statements. The positivity field is supplied by the upstream fermionMass positivity lemma. The scaling field follows directly from the exponential definition of predict_mass in MassLaw, since incrementing the rung by one multiplies the result by phi. The cardinality field is the Fintype instance for the nine-constructor inductive type.
why it matters
The structure is instantiated by sm_verification_cert to supply a single object carrying the verified mass-law properties for fermions. It supports the claim that RS derives all SM masses from the phi fixed point and the eight-tick octave without free parameters, consistent with D=3 and the Recognition Composition Law. It leaves open the numerical interval-arithmetic comparison against PDG 2024 values.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.