phaseDuration

formal source

  98
  99/-- The 8-tick window discipline divides the rotation into 8 phases.
 100    Each phase has duration T_phase = T_rot / 8. -/
 101def phaseDuration (T_rot : ℝ) : ℝ := T_rot / 8
 102
 103/-- Number of recognition ticks per phase at lab scales.
 104    For T_rot = 0.06 s, T_phase = 7.5 ms, so n_ticks ≈ 10¹².
 105    This is far above the 8-tick threshold. -/
 106def ticksPerPhase (T_rot τ0 : ℝ) : ℝ := phaseDuration T_rot / τ0
 107
 108/-- The 8-tick schedule is well-separated from the recognition tick
 109    when the number of recognition ticks per phase >> 8. -/
 110def scheduleWellSeparated (T_rot τ0 : ℝ) : Prop :=
 111  ticksPerPhase T_rot τ0 > 64  -- At least 8² ticks per phase
 112
 113theorem lab_schedule_well_separated :
 114    scheduleWellSeparated typicalLabPeriod_seconds tau0_seconds := by
 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). -/
 123def nullHypothesis (P : LabScalePrediction) (tolerance : ℝ) : Prop :=
 124  |P.w_predicted - 1| < tolerance
 125
 126/-- If C_lag < tolerance / (ratio^α - 1), the null hypothesis holds. -/
 127theorem null_holds_if_C_lag_small (T_dyn τ0 α C_lag tolerance : ℝ)
 128    (hτ : 0 < τ0) (hT : τ0 < T_dyn)
 129    (hα : 0 < α) (hC : 0 ≤ C_lag)
 130    (hbound : C_lag * (Real.rpow (T_dyn / τ0) α - 1) < tolerance) :
 131    nullHypothesis (mkLabPrediction T_dyn τ0 α C_lag) tolerance := by