m_tau_pos
plain-language theorem explainer
The theorem proves the tau mass in RS units is strictly positive. Researchers deriving lepton masses on the phi-ladder would cite it to confirm the sign of the tau entry before forming ratios. The proof is a one-line wrapper that unfolds m_tau_rs to the mass_on_rung expression and invokes positivity.
Claim. $0 < m_τ^{RS}$ where $m_τ^{RS} := E_{coh} φ^{19}$.
background
In Recognition Science, lepton masses sit on the phi-ladder. The function mass_on_rung(r) returns Anchor.E_coh ⋅ φ^r for integer rung r. The tau is placed at rung 19, so its RS mass is defined directly as mass_on_rung 19. The module P-011 records the full ladder: electron at rung 2, muon at rung 13, tau at rung 19, producing the ratio m_τ/m_e ≈ φ^17.
proof idea
The proof is a one-line wrapper. It unfolds the definitions of m_tau_rs and mass_on_rung to expose E_coh ⋅ φ^19, then applies the positivity tactic. The tactic succeeds because E_coh > 0 and φ > 1.
why it matters
The result anchors the tau entry in the lepton mass ladder of P-011. It supports the mass hierarchy theorems that follow in the same module and aligns with the phi-forcing chain (T6) that fixes φ as the self-similar point. No downstream uses are recorded, but the positivity guarantee is presupposed by any ratio or numerical comparison involving m_tau_rs.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.