LeptonGenerationRungs
plain-language theorem explainer
The LeptonGenerationRungs structure encodes the hypothesis that electron, muon, and tau masses occupy distinct integer rungs on a shared real mass base under the phi-ladder. A researcher examining Recognition Science mass spectra would cite it when checking whether the tau rung-19 correspondence extends consistently to lighter leptons. The definition assembles four field conditions that enforce rung proximity within 0.5 and pairwise distinctness.
Claim. A structure with real mass base $m_b$, integers $r_e$, $r_μ$, $r_τ=19$, such that $|$computeRung(electron mass in GeV, $m_b) - r_e| ≤ 0.5$, and analogously for muon and tau masses, together with the requirement that $r_e$, $r_μ$, $r_τ$ are pairwise distinct.
background
The TauGate module formulates the explicit hypothesis that the tau lepton mass and a biological molecular gate timescale both occupy rung 19 on the same phi-ladder. The phi-ladder is realized by computeRung, which returns the integer closest to the logarithmic distance of a given mass from the supplied base in units of phi. Upstream rung assignments from RSBridge.Anchor fix electron at 2, muon at 13, and tau at 19; Anchor.tau supplies the generation torsion values 0, 11, 17.
proof idea
This is a structure definition whose fields directly state the three rung-proximity conditions via computeRung together with the explicit distinctness predicate. No lemmas or tactics are applied; the body is the conjunction of the four field assertions.
why it matters
The structure supplies the hypothesis object consumed by tauGateFalsified, which declares the tau-gate identity falsified precisely when no base satisfies the rung conditions or when the structure is empty. It operationalizes the module claim that the rung-19 tau correspondence is non-accidental only if the lighter leptons fit the same ladder, connecting to the phi-ladder mass formula and the eight-tick octave. It leaves open whether a natural base exists without fine-tuning.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.