match_up_c
plain-language theorem explainer
The declaration fixes the rung number for the charm quark at 15 under the legacy constructor. Modelers of the Recognition Science mass spectrum would cite it when anchoring the second-generation up-type quark on the phi-ladder. The proof is a direct reflexivity check against the definition of the rung function.
Claim. The legacy rung constructor assigns rung number 15 to the charm quark fermion.
background
The compute_rung definition builds rung integers for any species by first extracting its sector and generation index. For fermions it routes through sectorOf and the generation value supplied by RSBridge.genOf. The module supplies a family of match theorems that record the concrete integers the constructor produces for each named particle. The upstream definition states it is correct for leptons and neutrinos but recommends the sdgt variant for quarks.
proof idea
The proof is a one-line reflexivity tactic that matches the left-hand side directly against the definition of compute_rung for the charm fermion case.
why it matters
This anchors the charm quark at rung 15 inside the mass formula yardstick * phi^(rung - 8 + gap(Z)). It supplies one concrete data point for the second-generation up-type quark in the phi-ladder construction. No downstream theorems currently depend on it.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.