FermionKineticCert
plain-language theorem explainer
FermionKineticCert packages the count of 15 Weyl fermions per generation with the positivity and consecutive phi-ratio properties of the mass function on the recognition ladder. A physicist modeling the standard-model spectrum inside the recognition framework would cite the certificate when confirming that the fermion kinetic sector reproduces the phi-ladder already forced by the composition law. The declaration is a structure definition that directly records the generation count from the module constant and the mass properties proved in the ph
Claim. A certificate asserting that the number of Weyl fermions per generation equals 15, that the mass at rung $k$ given by $m_0 phi^k$ is positive whenever $m_0 > 0$, and that consecutive masses on the ladder satisfy $m_{k+1}/m_k = phi$ for every $k$.
background
The module maps the standard-model fermion kinetic Lagrangian to the recognition picture: the mass term is J-cost on the recognition ratio while the derivative term is the lattice operator on $H_{RS}$. The mass function is defined by $m_k := m_0 phi^k$. The generation count is fixed at 15, obtained structurally as five electroweak sectors each containing three color copies. Upstream mass-positivity and mass-ratio theorems from the meson spectrum module supply the corresponding facts for the phi-ladder and are reused verbatim for fermions.
proof idea
This declaration is a structure definition. Its three fields directly encode the generation count taken from the module constant, the positivity statement for the mass function, and the adjacent-ratio statement equal to phi. No tactics or lemmas are invoked inside the definition; the properties are asserted as the certificate content.
why it matters
The certificate is instantiated by fermionKineticCert to supply the structural properties required for the recognition fermion kinetic sector. It confirms that the SM fermion counting and mass spectrum arise from the phi-ladder forced by the recognition composition law and the eight-tick octave. It connects to the D=3 spatial dimensions that produce the 5 times 3 equals 15 counting. The declaration remains a packaging step and does not close any open question in the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.