AdmissibleFamily
A set S of fermions is admissible when all members share one common Z value under ZOf and their rung numbers fall into a single congruence class modulo 360. Model builders working on anchor-scale mass hierarchies cite this structure to select degenerate families for pure phi-power ratios. The definition is a direct structure encoding of the two policy predicates with no auxiliary lemmas.
claimA set $S$ of fermions is admissible if there exists an integer $Z_0$ such that $Z(f)=Z_0$ for every $f$ in $S$, and there exists an integer $a$ such that rung$(f) ≡ a$ (mod 360) for every $f$ in $S$, where $Z(f)$ denotes the charge-indexed integer produced by ZOf.
background
The RSBridge.Anchor module supplies the interface between Recognition Science and the Standard Model by introducing the inductive type Fermion (12 species: six quarks, three charged leptons, three neutrinos) together with the map ZOf that returns the integer $Z = q̃^2 + q̃^4$ (plus 4 for quarks). The companion function rung assigns an integer label to each species (for example 2 for the electron, 4 for the up quark, 0 for the first neutrino). The gap function $F(Z) = ln(1 + Z/φ)/ln(φ)$ is declared to be the closed-form value of the integrated RG residue at the anchor scale μ*.
proof idea
The declaration is a structure definition whose two fields directly assert the required existence statements: a constant Z0 shared by ZOf on S, and a common residue a modulo 360 for the rung values on S. No lemmas or tactics are invoked; the structure itself packages the equal-Z plus rung-offset policy.
why it matters in Recognition Science
AdmissibleFamily supplies the predicate used to isolate families that obey the equal-Z degeneracy and rung-offset rules at μ*, thereby licensing the anchor_ratio claim that mass ratios within such families are pure powers of φ. It sits inside the Single Anchor Phenomenology package that equates the integrated RG residue to gap(ZOf) with tolerance ~1e-6. The construction touches the phi-ladder mass formula and the self-similar fixed point of the forcing chain, though it does not invoke any numbered T-step directly.
scope and limits
- Does not verify that any concrete set of fermions meets the two conditions.
- Does not compute or bound physical masses.
- Does not incorporate the gap function or RG transport integrals.
- Does not distinguish neutrino versus quark sector behavior beyond the definition of ZOf.
formal statement (Lean)
181structure AdmissibleFamily (S : Set Fermion) : Prop where
182 equalZ_const : ∃ Z0 : ℤ, ∀ {f}, f ∈ S → ZOf f = Z0
183 rung_residue : ∃ a : ℤ, ∀ {f}, f ∈ S → Int.ModEq (360 : ℤ) (rung f) a
184
185
186end RSBridge
187end IndisputableMonolith