AdmissibleFamily
plain-language theorem explainer
An admissible family is a set of Standard Model fermions sharing one common Z-value from their charge indices and occupying a single residue class of rung numbers modulo 360. Model builders working on fermion mass hierarchies at the recognition anchor scale cite this structure to enforce the equal-Z degeneracy condition required for pure phi-power ratios. The definition is a direct packaging of two existential statements with no additional proof obligations.
Claim. A set $S$ of fermions is admissible if there exists an integer $Z_0$ such that the charge-derived index $Z(f)$ equals $Z_0$ for every $f$ in $S$, and there exists an integer $a$ such that the rung number of each $f$ in $S$ satisfies rung$(f) ≡ a$ (mod 360).
background
The RSBridge.Anchor module supplies the core mapping from recognition theory to the twelve Standard Model fermions. Fermion is the inductive type listing the six quarks, three charged leptons, and three neutrinos. ZOf(f) returns the integer $q^2 + q^4$ (plus 4 for quarks) where $q$ is the tilde-Q charge of the species. The local rung function assigns fixed integers to each fermion (for example 2 for the electron, 4 for up and down quarks, 11 for the second neutrino).
proof idea
This is a structure definition that directly encodes the two policy requirements as existential quantifiers: one for the constant Z-value across the set and one for the common rung residue class modulo 360.
why it matters
The structure packages the equal-Z plus rung-offset policy that supports single-anchor mass phenomenology. It is referenced by the AdmissibleFamily declaration in the parent RSBridge module, which in turn feeds the massAtAnchor and anchor_ratio constructions. Within the Recognition Science framework it supplies the rung-residue condition needed for the phi-ladder mass formula at the anchor scale.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.