psToSeconds
plain-language theorem explainer
psToSeconds converts a real number representing picoseconds into seconds via direct multiplication by 10^{-12}. It is cited by researchers stating the tau-gate hypothesis when they need the molecular gate timescale expressed in SI units. The definition is a one-line scalar multiplication with no lemmas, constants, or further computation.
Claim. The map sending a real number $ps$ (time in picoseconds) to seconds is given by $psToSeconds(ps) := ps × 10^{-12}$.
background
The TauGate module states the explicit hypothesis that the tau lepton (rung 19 on the particle-physics phi-ladder) and the molecular gate timescale (also rung 19 on the biological phi-ladder) share the same scaling. The module imports PhiLadder for the rung structure and Real.Basic for the reals. This definition supplies the unit conversion required to write the gate time in seconds so that the numerical correspondence can be checked directly.
proof idea
The declaration is a direct definition performing the multiplication by 1e-12. No lemmas or tactics are invoked; it is a one-line scaling operation.
why it matters
It is the immediate prerequisite for molecularGateSeconds, which in turn appears inside the TauGateIdentity statement that both the tau mass and the gate time sit at rung 19. The module presents the whole construction as an explicit hypothesis whose falsification criteria include accidental rung correspondence and unnatural base-scale choices. The conversion therefore closes the last syntactic gap between the phi-ladder prediction and an observable time in seconds.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.