def
definition
pulseTicks
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.Unification.CriticalRecognitionLoading on GitHub at line 44.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
41/-! ## §1. Native control geometry -/
42
43/-- Native actuation period. -/
44def pulseTicks : ℕ := 8
45
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