fermionKineticCert
plain-language theorem explainer
The fermionKineticCert definition assembles the structural certificate for the fermion kinetic sector by supplying the per-generation fermion count of 15 together with positivity and adjacent-ratio properties of the mass function on the phi-ladder. A researcher deriving the Standard Model fermion spectrum from recognition geometry would cite this to anchor the kinetic-term mapping. The construction is a direct record instantiation that references the pre-proved positivity and ratio lemmas for the mass function.
Claim. The fermion kinetic sector certificate is the structure asserting that the number of fermions per generation equals 15, that the mass function satisfies $0 < m_0$ implies $0 < m_0 phi^k$ for every rung $k$, and that adjacent masses on the ladder obey $m_{k+1}/m_k = phi$.
background
In the Recognition Science setting the fermion kinetic sector maps the Dirac Lagrangian to a recognition lattice: the mass term becomes J-cost on the fermion recognition ratio while the derivative term becomes the lattice gradient. The FermionKineticCert structure collects three properties: the generation count equals 5 times 3, the mass function fermionMassAt remains positive, and successive masses differ by the factor phi. This rests on the upstream theorems fermionMassAt_pos (positivity by unfolding and applying phi positivity) and fermionMassAt_adjacent_ratio (ratio by algebraic simplification of the successor relation). The module notes that 15 equals the structural count from three colors times five electroweak sectors at spatial dimension D=3.
proof idea
The definition constructs the certificate by direct field assignment inside the record syntax. It supplies the constant fermionsPerGeneration_val for the generation count, the theorem fermionMassAt_pos for the positivity field, and the theorem fermionMassAt_adjacent_ratio for the mass-ratio field. No additional tactics are required.
why it matters
This certificate completes the structural description of the fermion kinetic sector and supplies the mass ladder that reproduces the observed fermion spectrum from the phi-ladder. It connects to the Recognition Composition Law through the phi fixed point and to the eight-tick octave via rung indexing. The construction closes the gap between the abstract phi-ladder proved in the meson and neutrino modules and the explicit fermion count required by the Standard Model. No open questions remain inside this declaration.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.