mkLabPrediction

formal source

  86  h_w : w_predicted = 1 + C_lag * (Real.rpow (T_dyn / τ0) α - 1)
  87
  88/-- Construct a lab-scale prediction for a given device. -/
  89def mkLabPrediction (T_dyn τ0 α C_lag : ℝ) : LabScalePrediction where
  90  T_dyn := T_dyn
  91  τ0 := τ0
  92  α := α
  93  C_lag := C_lag
  94  w_predicted := 1 + C_lag * (Real.rpow (T_dyn / τ0) α - 1)
  95  h_w := rfl
  96
  97/-! ## Connection to 8-Tick Schedule -/
  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