rung_sdgt_up
plain-language theorem explainer
The declaration supplies the SDGT rung table for up quarks, returning 4 for u, 17 for c, and 28 for t. Mass modelers working in the Recognition Science framework cite this table when constructing adjusted rung selectors for fermion mass predictions on the phi-ladder. The definition is realized by a direct pattern match on the quark name string with a zero default.
Claim. The SDGT up-quark rung function maps the up quark to rung value 4, the charm quark to 17, and the top quark to 28, returning 0 for any other input string.
background
In the AnchorPolicy module, rung selectors supply integer positions on the phi-ladder for mass calculations. The base rung function dispatches by sector to tables such as the RSBridge.Anchor definition, which assigns up quarks the values 4, 15, 21. The SDGT variant keeps the up-quark rung at 4 while shifting charm and top to 17 and 28. These tables support the mass formula that multiplies a yardstick by phi raised to (rung minus 8 plus gap(Z)). Upstream results include the sector-dispatch rung in AnchorPolicy and the default fermion tables in RSBridge.Anchor.
proof idea
The definition is a direct pattern match on the input string name. It returns the fixed integer 4 for u, 17 for c, and 28 for t, with 0 as the default case. No lemmas or tactics are invoked; the body is a pure data table.
why it matters
This definition supplies the up-quark case for the rung_sdgt selector, which is the immediate parent used in mass prediction routines. It adjusts the standard rungs from RSBridge.Anchor to support SDGT-specific calculations inside the Recognition Science mass ladder. The adjustment participates in the eight-tick octave and phi-ladder structure that underlies the T5 J-uniqueness and T6 phi fixed-point steps of the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.