tauOf
plain-language theorem explainer
The tauOf definition supplies integer tau offsets for the three generator classes in the mass kernel: zero for the first class, eleven for the second, and seventeen for the third. Mass spectrum calculations in the Recognition Science framework cite this mapping to adjust rung positions on the phi-ladder. The implementation consists of a direct case distinction on the inductive type with three constructors.
Claim. The offset function on generator classes satisfies $g_1$ maps to 0, $g_2$ maps to 11, and $g_3$ maps to 17.
background
The module introduces an inductive type consisting of three generator classes. These classes label distinct kernel types whose offsets enter rung calculations for the mass formula. The upstream inductive definition of the generator classes supplies the exhaustive cases used by this mapping.
proof idea
The definition is given by pattern matching on each of the three constructors of the generator class type and returns the fixed integer associated with that class.
why it matters
This mapping is used directly by the rungOf definition to compute the integer rung as the ell component plus the tau offset. It contributes to the discrete mass formula by fixing the class-dependent shift in the exponent of phi. The values align with the Z_cf threshold near phi^5 in the Recognition Science constants.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.