lab_schedule_well_separated

formal source

 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
 132  unfold nullHypothesis mkLabPrediction
 133  simp only
 134  have hratio_pos : 0 < T_dyn / τ0 := div_pos (lt_trans hτ hT) hτ
 135  have hpow_ge_one : 1 ≤ Real.rpow (T_dyn / τ0) α := by
 136    have hge1 : 1 ≤ T_dyn / τ0 := by
 137      rw [one_le_div hτ]
 138      exact le_of_lt hT
 139    exact Real.one_le_rpow hge1 (le_of_lt hα)
 140  have hdiff_nonneg : 0 ≤ Real.rpow (T_dyn / τ0) α - 1 := sub_nonneg.mpr hpow_ge_one
 141  have hprod_nonneg : 0 ≤ C_lag * (Real.rpow (T_dyn / τ0) α - 1) :=
 142    mul_nonneg hC hdiff_nonneg
 143  -- Simplify |1 + x - 1| = |x| = x (since x ≥ 0)