ControllerState
plain-language theorem explainer
ControllerState is the record type holding the minimal runtime variables for the recognition-load governor. Control theorists citing the critical-loading certificates would reference this structure when stating the inputs to the semantic condensation gate. The declaration is a plain structure definition carrying positivity hypotheses on area and demand.
Claim. A record whose fields are positive reals $a$ (area) and $d$ (demand), together with reals $S$ (entropy), $S_0$ (entropy floor), $A$ (attention), $s$ (signature), $s_0$ (signature minimum), $s_1$ (signature maximum), and $z$.
background
The module sketches a control theorem for the operating regime suggested by recognition bandwidth and the semantic condensation gate. The central control variable is the load ratio rho = R_dem / R_max, with healthy operation required to lie in the narrow band rho_min < rho < 1. The actuator runs on the native 8-tick cadence while stability is judged on the 360-tick supervisory horizon forced by lcm(8,45).
proof idea
This is a structure definition; the body consists solely of the listed fields and the two positivity hypotheses hArea and hDemand. No lemmas are applied.
why it matters
ControllerState supplies the state type for the downstream theorems criticalRecognitionLoading_certificate and forcedCriticalRecognitionLoading_certificate, which conclude subcriticality, attention bounded by phi^3, and z at least phi^45. It supplies the structural interface required by the control sketch in the module, linking the load-ratio band to the eight-tick octave and the SemanticCondensationGate predicate.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.