TauGatePredictions
plain-language theorem explainer
The structure bundles the tau-gate identity with predicted electron and muon timescales on the phi-ladder. Researchers testing Recognition Science lepton correspondences would cite these bundled predictions to check rung alignments for the lighter generations. It is realized as a structure definition that includes the identity record and rung deviation bounds for the two timescales.
Claim. If the tau-gate identity holds with time base $b$, then the structure asserts an electron timescale $t_e$ and muon timescale $t_μ$ such that the rung level of $t_e$ relative to $b$ lies within 0.5 of 2 and the rung level of $t_μ$ relative to $b$ lies within 0.5 of 13.
background
The module presents the tau-gate hypothesis that the tau lepton mass and a molecular gating timescale both occupy rung 19 on the phi-ladder, where the rung is the integer nearest to the base-phi logarithm of the ratio to a chosen base. The referenced identity structure encodes this shared rung 19 together with explicit mass and time bases and the two rung-proximity conditions. This predictions structure extends the hypothesis by adjoining real-valued timescales for the electron and muon generations together with their own rung-proximity conditions that reuse the same time base.
proof idea
This declaration is a structure definition with an empty proof body. It simply assembles the identity record, two real numbers for the timescales, and the two rung-proximity inequalities as fields.
why it matters
This definition renders the tau-gate hypothesis falsifiable by supplying concrete numerical predictions for the other lepton generations, directly supporting the three falsification criteria listed in the module documentation. It extends the phi-ladder rung correspondence (T6 self-similar fixed point) from the tau case to the full set of generations while leaving open whether the alignments are accidental or require a deeper mechanism from the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.