ticksPerPhase
ticksPerPhase returns the count of fundamental recognition ticks inside each 8-tick phase of a rotating device. Laboratory tests of information-limited gravity cite the quantity to confirm that dynamical timescales exceed the recognition scale by many orders of magnitude. The definition is realized as a direct division of phase duration by the tick interval.
claim$n = (T_ {rot}/8)/τ_0$, where $T_{rot}$ is the rotation period of the lab device and $τ_0$ is the fundamental recognition tick.
background
The Flight.GravityBridge module connects the ILG weight kernel $w_t(T_{dyn},τ_0)=1+C_{lag}((T_{dyn}/τ_0)^α-1)$ to rotating devices by setting the dynamical time equal to the rotation period. The eight-tick phase structure comes from EightTick.phase, which partitions any rotation into eight equal intervals; phaseDuration implements this partition as $T_{rot}/8$. The tick is the RS-native time quantum $τ_0=1$ in native units, with one octave defined as eight ticks.
proof idea
One-line wrapper that applies the phaseDuration definition and divides the result by the tick length $τ_0$.
why it matters in Recognition Science
The definition supplies the numerical argument to scheduleWellSeparated, which lab_schedule_well_separated invokes to verify that $n>64$ at typical lab periods of 0.06 s. This supports the null prediction that the weight factor remains unity at laboratory scales, consistent with the eight-tick octave (T7) and the separation of the recognition tick from macroscopic dynamics. The parent theorem lab_schedule_well_separated unfolds the definition to obtain the $10^{12}$ estimate.
scope and limits
- Does not incorporate relativistic corrections to the rotation period.
- Does not compute the ILG weight kernel itself.
- Assumes $T_{rot}$ and $τ_0$ are expressed in consistent units.
- Limits attention to the uniform 8-phase discretization.
- Does not address non-periodic or accelerated rotation.
Lean usage
theorem lab_example : scheduleWellSeparated typicalLabPeriod_seconds tau0_seconds := by unfold scheduleWellSeparated ticksPerPhase phaseDuration; norm_numformal statement (Lean)
106def ticksPerPhase (T_rot τ0 : ℝ) : ℝ := phaseDuration T_rot / τ0
proof body
Definition body.
107
108/-- The 8-tick schedule is well-separated from the recognition tick
109 when the number of recognition ticks per phase >> 8. -/