experimentalStatus
plain-language theorem explainer
Current data on fermion masses supports the φ-cascade derivation in Recognition Science. A physicist assessing beyond-Standard-Model hierarchies would cite this list when checking viability against LHC and precision data. The definition enumerates three experimental checks with their reported statuses in a direct list construction.
Claim. The experimental status is the list $[(``Fourth generation'', ``Excluded by LHC''), (``φ-cascade fit'', ``Works to ~10% for most particles''), (``Koide formula'', ``Exact to 0.01%'')]$, where each pair records a potential falsifier of the φ-hierarchy mass derivation and its current status.
background
The module SM-006 derives the fermion mass hierarchy from Recognition Science's φ-cascade: each generation differs by factors φ² or φ³, yielding m_n ~ m_0 × φ^(-αn) and spanning ratios up to 10^5 via the eight-tick structure. MassHierarchyFalsifier is the structure recording a falsification type (String) and its status (String), with the listed cases being discovery of a fourth generation, masses not fitting the cascade, Koide violation, or absence of φ in ratios. The upstream UniversalForcingSelfReference.for supplies the meta-realization context that embeds these checks into the self-reference axioms of the forcing chain.
proof idea
This is a direct definition that constructs the explicit list of three MassHierarchyFalsifier records. No lemmas or tactics are applied; the body is the literal enumeration of the pairs.
why it matters
This definition anchors the empirical support claim for the φ-hierarchy in the Recognition framework, directly feeding the mass formula (yardstick × φ^(rung-8+gap(Z))) and the T5-T8 forcing chain that forces D=3 and the phi-ladder. It fills the SM-006 paper proposition on deriving the hierarchy from first principles and touches the open question of whether the ~10% cascade fit can be tightened to sub-percent level without additional parameters.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.