tauGateFalsified
plain-language theorem explainer
This definition encodes the falsification criteria for the tau-gate hypothesis linking the tau lepton mass to molecular gating timescales on the phi-ladder. Researchers testing Recognition Science predictions would reference it to determine if the rung-19 alignment holds or if lepton generations are inconsistent. It is defined directly as a disjunction of two conditions derived from rung computations and the lepton structure hypothesis.
Claim. The tau-gate hypothesis is falsified if no positive real bases $b_1, b_2$ exist such that the rung of the tau mass (1.77686 GeV) relative to $b_1$ lies within 0.5 of 19 and the rung of the molecular gate time (in seconds) relative to $b_2$ lies within 0.5 of 19, or if the lepton generation rungs structure is uninhabited.
background
In the RRF module, local recognition fields are modeled as maps from four-dimensional indices to reals. The phi-ladder computation uses the formula log(x / b) / log phi to assign rung numbers. The tau-gate hypothesis asserts that both the tau mass and the molecular gate timescale occupy rung 19 relative to suitable bases, with the lepton generations expected to fit integer rungs on the same ladder. The upstream RRF abbreviation provides the non-sealed metric interface, while computeRung implements the logarithmic rung finder. LeptonGenerationRungs structures the requirement for a common base and integer rungs for electron and muon (with tau implied). This setting follows the module's explicit hypothesis that the correspondence is striking but requires falsification criteria for naturalness.
proof idea
The definition is constructed as a direct disjunction in the Prop type. The first disjunct asserts that for all positive bases the rung deviation exceeds 0.5 for at least one of the two quantities. The second disjunct states that the LeptonGenerationRungs structure is uninhabited.
why it matters
This supplies the explicit falsifier for the tau-gate identity, the most striking claim in the phi-ladder theory connecting particle masses to biological gating. It operationalizes the falsification criteria listed in the module documentation and stands as a check within the RRF hypotheses. It touches the open question of whether the rung alignment is accidental or forced by the self-similar properties of phi.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.