pulse_divides_supervisory
plain-language theorem explainer
The theorem establishes that the native 8-tick actuation period divides the 360-tick supervisory horizon. Researchers modeling bounded recognition systems cite it to confirm exact alignment between actuation cadence and the lcm(8,45) integration window. The proof is a direct term-mode construction that supplies the multiplier 45, unfolds the constant definitions, and reduces the arithmetic via norm_num.
Claim. Let $p=8$ be the native actuation period and $s=360$ the supervisory horizon. Then $p$ divides $s$.
background
The Critical Recognition Loading module defines the load ratio as rho = R_dem / R_max and requires healthy operation inside the band rho_min < rho < 1. Actuation occurs on the native 8-tick cadence while stability is judged over the 360-tick supervisory horizon forced by lcm(8,45). Upstream, barrierTicks is defined as 360 with the explicit note that it spans exactly 45 octaves, pulseTicks is fixed at 8, and supervisoryTicks is set equal to barrierTicks.
proof idea
The proof exhibits the integer witness 45 for the divisibility relation. It unfolds pulseTicks, supervisoryTicks, and barrierTicks to expose the concrete values 8 and 360. norm_num then verifies the arithmetic identity 8 * 45 = 360.
why it matters
This divisibility supplies a structural prerequisite for the criticalRecognitionLoading_certificate theorem, which concludes that any state satisfying IsCriticalRecognitionLoading is subcritical with attention bounded by phi^3 and z at least phi^45. It anchors the alignment between the eight-tick octave and the 360-tick supervisory period inside the Recognition Science framework, ensuring that persistence checks integrate over an integer number of octaves.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.