pulse_divides_supervisory

formal source

  53  unfold supervisoryTicks pulseTicks
  54  simpa using barrier_is_lcm
  55
  56theorem pulse_divides_supervisory : pulseTicks ∣ supervisoryTicks := by
  57  use 45
  58  unfold pulseTicks supervisoryTicks barrierTicks
  59  norm_num
  60
  61/-! ## §2. Load ratio and regimes -/
  62
  63/-- The runtime load ratio for a bounded recognition system. -/
  64def loadRatio (area demand : ℝ) : ℝ :=
  65  demand / bandwidth area
  66
  67/-- Underloaded systems do not reach the target condensation band. -/
  68def IsUnderloaded (rhoMin area demand : ℝ) : Prop :=
  69  loadRatio area demand ≤ rhoMin
  70
  71/-- Subcritical systems remain below the bandwidth ceiling. -/
  72def IsSubcritical (area demand : ℝ) : Prop :=
  73  demand < bandwidth area
  74
  75/-- Overloaded systems hit or exceed the bandwidth ceiling. -/
  76def IsOverloaded (area demand : ℝ) : Prop :=
  77  bandwidth area ≤ demand
  78
  79/-- The critical-loading band: close to saturation, but still below it. -/
  80def InCriticalBand (rhoMin area demand : ℝ) : Prop :=
  81  rhoMin < loadRatio area demand ∧ loadRatio area demand < 1
  82
  83/-- The forced lower edge of the control band from the phase-transition geometry. -/
  84abbrev rhoCriticalMin : ℝ := rhoBandLower
  85
  86theorem rhoCriticalMin_eq : rhoCriticalMin = phi⁻¹ ^ 2 :=