lab_schedule_well_separated
plain-language theorem explainer
The theorem shows that a typical laboratory rotation period of 0.06 s and recognition tick of 7.3 fs yield more than 64 recognition ticks per phase in the eight-tick schedule. Experimental physicists checking Information-Limited Gravity null results at lab scales would cite this to confirm separation from the recognition threshold. The proof is a direct unfolding of the phase and tick definitions followed by numerical normalization.
Claim. Let $T=0.06$ be a typical laboratory rotation period in seconds and $τ_0=7.3×10^{-15}$ the recognition tick. Then the number of recognition ticks per phase satisfies $(T/8)/τ_0>64$.
background
The Flight-Gravity Bridge module connects the ILG weight kernel $w_t(T_{dyn},τ_0)=1+C_{lag}((T_{dyn}/τ_0)^α-1)$ with $α≈0.191$ to rotating lab devices. It formalizes the prediction that $w≈1$ at laboratory scales where dynamical times exceed the recognition tick by many orders of magnitude, using the eight-tick schedule to discretize rotation phases.
proof idea
The proof unfolds scheduleWellSeparated, ticksPerPhase, phaseDuration, typicalLabPeriod_seconds, and tau0_seconds. It then applies norm_num to evaluate the resulting numerical inequality directly.
why it matters
This result verifies the separation condition required for the null hypothesis that ILG deviations remain negligible at lab scales. It supports the eight-tick octave structure (T7) in the forcing chain and closes a concrete step from RS constants to experimental falsifiability for rotating devices.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.