phaseDuration
plain-language theorem explainer
The phaseDuration definition supplies the duration of each of the eight recognition phases that partition a device's rotation period. Researchers working on the Flight-Gravity bridge would cite it when converting a lab rotation period into the dynamical timescale that enters the ILG weight kernel. The definition is a direct arithmetic division by eight, inheriting the eight-tick structure from the upstream EightTick.phase lemma.
Claim. Let $T_{rot}$ be the rotation period of a laboratory device. The phase duration is given by $T_{phase}=T_{rot}/8$.
background
In the Flight-Gravity Bridge module the 8-tick window discipline partitions any rotation into eight equal phases. The fundamental recognition tick $τ_0$ is imported from Constants.tick and equals one in RS-native units. Upstream, the EightTick.phase definition supplies the eight angular positions $kπ/4$ for $k=0,…,7$, establishing the periodic structure that phaseDuration discretizes in time.
proof idea
The definition is a one-line wrapper that applies the arithmetic division $T_{rot}/8$, directly implementing the eight-phase partition stated in the module documentation and consistent with the phase function from EightTick.
why it matters
This definition is required by the downstream theorems lab_schedule_well_separated and ticksPerPhase. The former shows that a typical lab period of 0.06 s yields approximately $10^{12}$ ticks per phase, far above the eight-tick threshold, confirming that the schedule remains well-separated from the recognition scale. It therefore supports the null-result prediction $w≈1$ at laboratory scales within the Recognition Science framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.