lab_schedule_well_separated
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.
claimLet $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 in Recognition Science
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.
scope and limits
- Does not compute the ILG weight value itself.
- Does not apply outside laboratory rotation periods.
- Does not bound the coupling constant C_lag.
- Does not incorporate quantum or relativistic corrections.
formal statement (Lean)
113theorem lab_schedule_well_separated :
114 scheduleWellSeparated typicalLabPeriod_seconds tau0_seconds := by
proof body
Term-mode proof.
115 unfold scheduleWellSeparated ticksPerPhase phaseDuration
116 unfold typicalLabPeriod_seconds tau0_seconds
117 -- 0.06 / 8 / 7.3e-15 = 0.0075 / 7.3e-15 ≈ 10¹² >> 64
118 norm_num
119
120/-! ## Null Hypothesis and Falsifiers -/
121
122/-- The null hypothesis: at lab scales, w ≈ 1 (no ILG deviation). -/