`supervisoryTicks_eq`

proved

show as: view math explainer →

module: IndisputableMonolith.Unification.CriticalRecognitionLoading
domain: Unification
line: 49 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Unification.CriticalRecognitionLoading on GitHub at line 49.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

supervisoryTicks IndisputableMonolith.Unification.CriticalRecognitionLoading

formal source

  46/-- Supervisory horizon for persistence checks. -/
  47def supervisoryTicks : ℕ := barrierTicks
  48
  49theorem supervisoryTicks_eq : supervisoryTicks = 360 := by
  50  rfl
  51
  52theorem supervisoryTicks_is_lcm : supervisoryTicks = Nat.lcm pulseTicks 45 := by
  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. -/

papers checked against this theorem

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