structural_dominance_holds
plain-language theorem explainer
The declaration defines the proposition that structural dominance holds for fermion f when its geometric residue differs from supplied rg_val and recognition strength exceeds 100. Researchers formalizing mass hierarchies under the zero-parameter hypothesis would cite it to separate geometric lock-in from perturbative corrections. The definition is a direct conjunction of the two conditions using the geometric_residue and recognition_strength functions.
Claim. For fermion $f$ and real $r$, structural dominance holds when geometric residue $F(f) ≠ r$ and recognition strength $g(f,r) > 100$, where $F(f)$ is the structure gap and $g(f,r) = F(f)/r$.
background
The RecognitionCoupling module addresses the gap between geometric mass predictions and perturbative RG transport. Geometric residue is defined as gap(ZOf f), the large exponent F(Z) required by the phi-ladder formula m_i = m_struct * φ^(F(Z)). Recognition strength is the ratio geometric_residue f / rg_val, measuring how far the geometric structure exceeds the small perturbative residue f_RG (typically 0.05 for electrons). The module documentation notes that geometric F(Z) values range from 5.74 to 13.95 while perturbative integrals remain below 1, motivating the ratio as a strength measure.
proof idea
The definition is a direct conjunction of geometric_residue f ≠ rg_val and recognition_strength f rg_val > 100. It applies the upstream definitions of geometric_residue (gap on ZOf f) and recognition_strength (direct division) with no additional lemmas or tactics.
why it matters
This definition encodes the zero-parameter hypothesis that masses follow geometric structure m_i = m_struct * φ^(F(Z)) rather than standard RG running m = m_struct * φ^(f_RG). It supports the Recognition Science mass formula and the replacement of perturbative residues by stronger geometric lock-in, consistent with T5 J-uniqueness and the eight-tick octave. No downstream uses appear yet, leaving open its integration into full spectrum derivations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.