supervisoryTicks_is_lcm
plain-language theorem explainer
The supervisory horizon equals the least common multiple of the native pulse period and 45. Control theorists working on recognition bandwidth would cite this to fix the 360-tick supervisory window from the 8-tick actuation cadence. The proof is a one-line wrapper that unfolds the two definitions and invokes the barrier period lemma.
Claim. The supervisory horizon equals the least common multiple of the actuation pulse period and 45.
background
pulseTicks is defined as the native actuation period of 8 ticks. supervisoryTicks is defined as barrierTicks, the supervisory horizon for persistence checks. The upstream barrier_is_lcm result states that barrierTicks equals the least common multiple of 8 and 45, yielding the 360-tick interval quoted in the module doc-comment as '360 = lcm(8, 45).'
proof idea
The proof unfolds supervisoryTicks and pulseTicks, then applies simpa to barrier_is_lcm. It is a one-line wrapper that reduces the equality directly to the established barrier period identity.
why it matters
This lemma anchors the supervisory horizon to lcm(pulseTicks, 45) inside the critical recognition loading module, supporting the structural claims for the 360-tick control window. It aligns with the eight-tick octave of the forcing chain and the load-ratio stability band rho_min < rho < 1. No downstream uses appear yet, so its role in fuller runtime theorems remains open.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.