pulseTicks
plain-language theorem explainer
The definition fixes the native actuation period at eight ticks for the recognition controller. Researchers analyzing subcritical loading regimes cite it to anchor the actuator cadence before deriving the supervisory horizon as lcm(8,45). It is introduced as a direct numerical constant with no reduction steps or additional axioms.
Claim. The native actuation period is defined to be $8$ ticks.
background
The Critical Recognition Loading module defines the load ratio as rho = R_dem / R_max, where R_dem is the demanded recognition rate and R_max is the bandwidth of the active region. Healthy operation is required to satisfy rho_min < rho < 1, with the actuator running on the native 8-tick cadence while stability is judged over the 360-tick supervisory horizon obtained from lcm(8,45). This construction rests on the meta-realization structure from UniversalForcingSelfReference, which records the structural properties needed for orbit and step coherence axioms.
proof idea
The declaration is a direct constant definition that assigns the integer value 8. No lemmas are invoked; the constant is later unfolded in downstream results such as supervisoryTicks_is_lcm and pulse_divides_supervisory.
why it matters
This supplies the eight-tick period that anchors the actuator inside the critical recognition loading certificates. It is referenced by criticalRecognitionLoading_certificate and forcedCriticalRecognitionLoading_certificate, which establish subcriticality together with the bounds s.attention ≤ phi^3 and phi^45 ≤ s.z. The definition realizes the eight-tick octave (T7) from the forcing chain and enables the supervisory horizon via lcm with the barrier period. The module remains a theorem sketch for later runtime or physics deployment.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.