IsForcedCriticalRecognitionLoading
plain-language theorem explainer
The definition asserts that a controller state satisfies the critical recognition loading condition when evaluated at the minimal forced rho threshold. Control theorists modeling recognition bandwidth would cite it to anchor stability certificates in the sub-saturation regime. It is realized as a direct one-line instantiation of the full critical loading predicate using the precomputed rhoCriticalMin value.
Claim. Let $s$ be a controller state with components area, demand, entropy, entropyFloor, attention, signature, signatureMin, signatureMax, and $z$. Then $s$ satisfies forced critical recognition loading if it lies in the critical band above $rho_{crit,min}$ and obeys the semantic condensation gate on its entropy, attention, and signature fields.
background
The module develops control lemmas for recognition systems under the load ratio $rho = R_{dem}/R_{max}$. Healthy regimes require $rho_{min} < rho < 1$, with stability judged over the 360-tick supervisory horizon from lcm(8,45). ControllerState is the minimal structure holding area, demand, entropy, entropyFloor, attention, signature, signatureMin, signatureMax, and $z$ for the governor.
proof idea
This is a one-line wrapper that applies IsCriticalRecognitionLoading to the fixed rhoCriticalMin value on the input state $s$.
why it matters
This definition supplies the non-parameterized form of the critical loading condition invoked by the forcedCriticalRecognitionLoading_certificate theorem. The certificate extracts subcriticality, attention bounds by $phi^3$, and lower bounds on $z$ by $phi^{45}$. It closes the structural gap between recognition bandwidth geometry and the supervisory control layer, consistent with the eight-tick octave cadence.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.