res_charm_eq_neg45
plain-language theorem explainer
The theorem states that the charm quark rung position equals exactly -4.5 on the real line. Workers deriving quark masses from the quarter-ladder hypothesis cite it to fix the charm sector before mass bounds are computed. The proof reduces the definition -18/4 by direct simplification and rational normalization.
Claim. The charm quark topological position on the phi-ladder satisfies $R = -4.5$, where the position is the quarter-integer value $-18/4$.
background
The module develops T12 quark masses under the Quarter-Ladder Hypothesis. Quarks occupy the same structural base mass as leptons but sit at quarter-integer rungs on the phi-ladder. Charm is placed at rung -4.50, written -18/4. The upstream definition in the RRF submodule sets res_charm directly to -18/4, while the sibling module defines it via subtraction from the bottom rung.
proof idea
The term proof is a one-line wrapper. It unfolds the definition of the rung position as -18/4, then applies numerical normalization to obtain equality with -4.5.
why it matters
The result supplies the exact rung value required by the downstream charm mass bounds theorem, which combines the structural mass interval with phi-power bounds at rung -45 to obtain 1245 < predicted mass < 1247. It completes the charm entry in the T12 quarter-ladder chain and aligns with the phi self-similar fixed point and eight-tick octave structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.