match_down_b
plain-language theorem explainer
The rung constructor assigns value 21 to the bottom quark fermion. Mass spectrum modelers in Recognition Science cite it to fix the third-generation down quark on the phi-ladder. The proof succeeds by direct reflexivity against the pre-anchored integer.
Claim. The rung constructor applied to the bottom quark fermion yields the integer 21.
background
The rung constructor is the legacy function in RungConstructor.Motif that maps a Species (here a fermion) to an integer rung via sector and generation lookup. Upstream anchors in RSBridge.Anchor and AnchorPolicy supply the explicit table values, including 21 for the b quark, while PhiLadderLattice supplies the lattice structure that these rungs populate. The module supplies verification theorems that the constructor reproduces the expected table entries for fermions.
proof idea
The proof is a one-line term-mode reflexivity that directly equates the constructor output for the bottom fermion to the constant 21.
why it matters
This verification anchors the bottom quark rung inside the mass formula yardstick times phi to the power of (rung minus 8 plus gap), consistent with the eight-tick octave and D equals 3. It supports the overall forcing chain from T5 J-uniqueness through T6 phi fixed point by confirming ladder placement for third-generation down quarks.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.