TauGateIdentity
plain-language theorem explainer
The TauGateIdentity structure packages the data for the claim that the tau lepton mass and a molecular gate timescale both occupy rung 19 on the phi-ladder. Researchers testing Recognition Science cross-domain predictions would cite it when examining whether particle masses and biological timescales share the same logarithmic scaling. The definition simply declares an integer rung, two real bases, and two inequalities that force the computed rungs to match within 0.5.
Claim. A structure consisting of an integer rung (default 19), real numbers massBase and timeBase, and the conditions $|computeRung(tauMassGeV, massBase) - rung| ≤ 0.5$ and $|computeRung(molecularGateSeconds, timeBase) - rung| ≤ 0.5$, where $computeRung(v, b) = ln(v/b)/ln φ$.
background
The phi-ladder assigns rungs via logarithmic scaling with the golden ratio φ, so that the rung of a quantity x relative to base b satisfies rung ≈ ln(x/b)/ln φ. This module imports PhiLadder to supply the computeRung function and the underlying φ arithmetic. The local theoretical setting is the RRF Hypotheses section, which treats the tau-gate coincidence as an explicit, falsifiable hypothesis rather than a derived theorem.
proof idea
This is a structure definition that directly declares the five fields and the two rung-matching predicates. No lemmas or tactics are invoked; the body is pure packaging of the hypothesis data.
why it matters
The structure supplies the core data bundle for the tau-gate hypothesis and is referenced by TauGatePredictions (to generate electron and muon timescale forecasts) and TauGateFalsifier (to record failed predictions or unnatural bases). It occupies the explicit-hypothesis slot in the RRF module, extending the phi-ladder (T5–T8) from particle masses into biological timescales and leaving open the question of whether the required base choices are natural.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.