scheduleWellSeparated
plain-language theorem explainer
scheduleWellSeparated encodes the separation condition between the eight-tick phase schedule and the recognition tick scale by requiring more than 64 recognition ticks per phase. Researchers modeling ILG gravity corrections for rotating lab devices cite this predicate to confirm that dynamical timescales remain in the Newtonian regime. The definition reduces directly to an inequality on the ticksPerPhase function.
Claim. The predicate holds for rotation period $T_{rot}$ and recognition tick duration $τ_0$ precisely when the number of recognition ticks per phase exceeds 64, i.e., phaseDuration$(T_{rot})/τ_0 > 64$.
background
The Flight.GravityBridge module connects the ILG weight kernel $w_t(T_{dyn}, τ_0) = 1 + C_{lag}((T_{dyn}/τ_0)^α - 1)$ to flight and propulsion models, with $τ_0 ≈ 7.3$ fs and $α ≈ 0.191$. It addresses whether the eight-tick schedule interacts with ILG predictions at laboratory scales where $T_{rot} ≫ τ_0$ by 10–15 orders of magnitude, predicting $w ≈ 1$ (null result).
proof idea
One-line definition that applies the ticksPerPhase function and requires its value to exceed 64.
why it matters
This predicate supplies the separation criterion used by the downstream theorem lab_schedule_well_separated, which verifies the condition for typical laboratory periods (0.06 s) against $τ_0$. It closes the loop on the eight-tick octave (T7) by confirming laboratory dynamical times lie well above the recognition threshold, supporting the null ILG prediction at lab scales.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.