supervisoryTicks_eq
plain-language theorem explainer
supervisoryTicks_eq fixes the supervisory horizon at 360 ticks for persistence checks in load-ratio control. Recognition bandwidth modelers cite it to set the monitoring interval that aligns the 8-tick actuator with the 45-tick gate. The proof is a single reflexivity step on the barrierTicks definition.
Claim. The supervisory horizon for persistence checks equals 360 ticks.
background
The Critical Recognition Loading module defines the load ratio as demanded recognition rate divided by maximum bandwidth of the active region. Healthy regimes lie in the open interval between a minimum threshold and saturation. The actuator operates on the native 8-tick cadence while stability judgments use the supervisory horizon forced by lcm(8,45). The upstream definition states that supervisoryTicks is barrierTicks and supplies the doc-comment 'Supervisory horizon for persistence checks.'
proof idea
The proof applies reflexivity directly to the definition of supervisoryTicks as barrierTicks, which evaluates to the constant 360.
why it matters
This declaration anchors the 360-tick supervisory horizon required by the module's control sketch for sub-saturation operation. It supplies the structural constant that any fuller runtime or physics deployment theorem would invoke when monitoring load ratio between rho_min and 1. The module presents it as one of the lemmas supporting the eight-tick octave alignment in the Recognition Science framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.