r_tau
plain-language theorem explainer
The declaration fixes the tau lepton at rung 19 on the phi-ladder. Researchers deriving lepton mass ratios from the Recognition Science phi-ladder would reference this rung assignment. The proof extracts the value directly from the precomputed r_lepton_values structure.
Claim. The rung for the tau lepton satisfies $r_τ = 19$.
background
The module formalizes the fermion mass hierarchy (P-002) by assigning each lepton an integer rung on the phi-ladder. Mass scales as the base coherence energy times phi to the rung power, with the electron fixed at rung 2 from the proton-electron mass ratio work. The tau rung at 19 follows from adding the generation spacing of 17, which traces to the cube geometry in the forcing chain. This setting relies on the phi-forcing derived results and the ledger factorization for the J-cost function that enforces the self-similar scaling. Upstream, the rung function from compatibility constants supplies the integer labels, while nucleosynthesis tiers provide the discrete tier structure for physical quantities.
proof idea
The proof is a one-line wrapper that applies the third component of the r_lepton_values tuple to establish the tau rung.
why it matters
This rung assignment completes the inputs for the lepton_hierarchy_geometric theorem, which resolves P-002 by proving the muon-to-electron ratio equals phi to the eleventh and the tau-to-muon ratio equals phi to the sixth. It removes all free Yukawa parameters from the mass hierarchy, consistent with the self-similar fixed point phi forced at T6 and the eight-tick octave structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.