`LabScalePrediction`

definition

show as: view math explainer →

module: IndisputableMonolith.Flight.GravityBridge
domain: Flight
line: 80 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.Flight.GravityBridge on GitHub at line 80.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

open explainer

depends on

used by

formal source

  77
  78    This is a TESTABLE prediction if C_lag is not too small.
  79-/
  80structure LabScalePrediction where
  81  T_dyn : ℝ           -- Rotation period
  82  τ0 : ℝ              -- Recognition tick
  83  α : ℝ               -- ILG exponent
  84  C_lag : ℝ           -- Coupling constant
  85  w_predicted : ℝ     -- Predicted weight
  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 :=

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.