ControllerState
plain-language theorem explainer
ControllerState supplies the minimal runtime state record for the governor in the critical recognition loading control system. It collects positive area and demand with thermodynamic entropy, attention, signature bounds, and auxiliary z to support load-ratio stability checks. Control theorists working in recognition bandwidth models would reference this record when building certificates for subcritical operation. The declaration is a direct structure definition with embedded positivity hypotheses.
Claim. A record type consisting of positive real numbers for area and demand together with real numbers for entropy (proportional to total defect), entropy floor, attention, signature, signature minimum, signature maximum, and auxiliary variable 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 satisfy rho_min < rho < 1. The actuator runs on the native 8-tick cadence while the controller judges stability on the 360-tick supervisory horizon forced by lcm(8,45). This file is a theorem sketch proving structural lemmas for a fuller runtime or physics deployment theorem. Entropy of a configuration is proportional to its total defect with zero defect yielding zero entropy. Entropy is also given by S = k beta averageEnergy + k ln Z in the Boltzmann setting and by k_B (log Z + beta averageEnergy) in the partition-function setting.
proof idea
This is a structure definition that directly declares the nine real-valued fields and the two positivity hypotheses on area and demand.
why it matters
The structure is the common carrier for the downstream definitions IsCriticalRecognitionLoading and IsForcedCriticalRecognitionLoading, which in turn feed the certificates criticalRecognitionLoading_certificate and forcedCriticalRecognitionLoading_certificate. It supplies the concrete state object required by the control theorem sketched in the module, consistent with the eight-tick octave and the 360-tick supervisory horizon. It touches the open question of closing the sketch into a full runtime deployment theorem.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.