ControllerState
ControllerState supplies the minimal record of runtime variables for the recognition governor: real scalars for area, demand, entropy, entropy floor, attention, signature with its bounds, and auxiliary z, plus positivity constraints on area and demand. Control theorists in the Recognition Science setting cite it when stating the state space for critical-loading predicates. The declaration is a direct structure definition with no further computation or proof obligations.
claimA record consisting of real numbers for spatial area, demanded recognition rate, entropy, entropy floor, attention level, signature value with its minimum and maximum, and auxiliary variable z, subject only to the positivity constraints that area and demand are strictly positive.
background
The module sketches a control theorem for the operating regime suggested by recognition bandwidth and the semantic condensation gate. The central variable is the load ratio rho equal to demanded recognition rate over maximum bandwidth, with healthy operation restricted to the narrow sub-saturation interval rho_min less than rho less than 1. The actuator runs on the native eight-tick cadence while stability is judged on the 360-tick supervisory horizon given by lcm(8,45). Upstream entropy definitions are used: entropy of a configuration is proportional to its total defect (zero defect yields minimum entropy), entropy equals k beta times average energy plus k ln Z in the Boltzmann setting, and entropy equals k_B times (ln Z plus beta times average energy) in the partition-function setting.
proof idea
Direct structure definition that introduces the nine real fields together with the two positivity hypotheses on area and demand. No lemmas are applied; the declaration simply packages the variables required by the downstream predicates IsCriticalRecognitionLoading and IsForcedCriticalRecognitionLoading.
why it matters in Recognition Science
This definition supplies the state space for the criticalRecognitionLoading_certificate and forcedCriticalRecognitionLoading_certificate theorems, which conclude subcriticality, attention bounded by phi to the third power, and z at least phi to the 45th. It fills the structural prerequisite in the control theorem for the eight-tick octave with 360-tick supervisory horizon. The declaration touches the open question of a full runtime or physics deployment theorem that would discharge the remaining scaffolding in the module.
scope and limits
- Does not compute or constrain the load ratio rho itself.
- Does not enforce membership in the critical band or the semantic condensation gate.
- Does not relate the fields to the phi-ladder mass formula or Berry creation threshold.
- Does not include any dynamics or evolution equations for the state variables.
formal statement (Lean)
171structure ControllerState where
172 area : ℝ
173 demand : ℝ
174 entropy : ℝ
175 entropyFloor : ℝ
176 attention : ℝ
177 signature : ℝ
178 signatureMin : ℝ
179 signatureMax : ℝ
180 z : ℝ
181 hArea : 0 < area
182 hDemand : 0 < demand
183
184/-- The full critical-loading condition. -/