pith. sign in
module module high

IndisputableMonolith.RRF.Hypotheses.TauGate

show as:
view Lean formalization →

TauGate module specifies the tau lepton mass in GeV within the RRF hypotheses. Particle physicists testing phi-ladder scale predictions for leptons would cite it. The module collects definitions, identities, predictions and falsifiers as explicit physical claims imported from the phi-ladder hypothesis.

claim$m_τ$ (in GeV) under the φ-ladder hypothesis

background

The module imports PhiLadder, whose doc states: physical scales are organized by powers of φ; this is an explicit hypothesis, not a definitional truth, generating prediction obligations that must be tested empirically. It also imports Mathlib.Data.Real.Basic for real-number arithmetic. The local setting is the RRF.Hypotheses umbrella, which collects physical claims that make specific predictions and carry explicit falsification criteria.

proof idea

this is a definition module, no proofs

why it matters in Recognition Science

This module feeds the parent RRF.Hypotheses umbrella file. It supplies the tau lepton mass hypothesis as one explicit physical claim in the Recognition framework, extending the phi-ladder organization of scales with supporting identities and falsification objects.

scope and limits

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (11)