IsCriticalRecognitionLoading
plain-language theorem explainer
IsCriticalRecognitionLoading defines the full critical-loading condition as the conjunction of the load ratio lying in (rhoMin, 1) and the semantic condensation gate on entropy, attention, and signature fields of a controller state. Recognition-bandwidth control theorists cite it when specifying the narrow sub-saturation operating regime. It is realized as a direct conjunction of the two sibling predicates InCriticalBand and SemanticCondensationGate.
Claim. The predicate holds for minimum load ratio $rho_min$ and controller state $s$ precisely when $rho_min < demand/area < 1$ and the semantic condensation gate is satisfied: entropyFloor < entropy, signatureMin ≤ signature ≤ signatureMax, attention ≤ $phi^3$, together with the remaining gate conditions on $z$.
background
The module sketches a control theorem for the operating regime of recognition bandwidth. The central variable is the load ratio rho = demand / area, with healthy operation asserted in the open interval (rhoMin, 1). The 8-tick actuator cadence is judged on the 360-tick supervisory horizon given by lcm(8,45). ControllerState packages the minimal runtime variables: area, demand, entropy, entropyFloor, attention, signature, signatureMin, signatureMax, z.
proof idea
The definition is a direct conjunction of InCriticalBand rhoMin s.area s.demand with SemanticCondensationGate applied to the entropy, attention, signature, and z components of s.
why it matters
This supplies the central predicate for the critical recognition loading control theorem. It is invoked by criticalRecognitionLoading_certificate (which extracts subcriticality, attention ≤ phi^3, and z ≥ phi^45) and by IsForcedCriticalRecognitionLoading (which specializes to rhoCriticalMin). It fills the structural lemma slot in the module sketch of the 8-tick cadence controller, consistent with the eight-tick octave (T7) of the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.