InCriticalBand
plain-language theorem explainer
The definition InCriticalBand specifies the operating regime for recognition systems where the load ratio lies strictly between a minimum threshold and full saturation. Researchers working on control theorems in Recognition Science would cite this when establishing stability conditions for semantic condensation. The definition is a direct conjunction of two inequalities on the load ratio.
Claim. The critical band condition holds when $rhoMin < loadRatio(area, demand) < 1$, with $loadRatio(area, demand)$ the ratio of demanded recognition rate to maximum bandwidth of the region.
background
The module introduces the load ratio $rho = R_dem / R_max$ as the central control variable, with healthy operation confined to the narrow sub-saturation interval $rho_min < rho < 1$. The actuator follows the native 8-tick cadence while stability is judged on the 360-tick supervisory horizon. Upstream results supply the 8-tick phase definition (periodic with period $2pi$), the J-cost structure from PhiForcingDerived, and the band operation on stable states from PreLogicalCost.
proof idea
Direct definition consisting of the conjunction of the lower-bound inequality and the strict upper bound on loadRatio.
why it matters
This definition supplies the predicate used by the downstream theorems criticalBand_implies_subcritical, criticalBand_not_overloaded, InForcedCriticalBand, IsCriticalRecognitionLoading, and loadPenalty_zero_of_critical. It fills the control-band slot in the unification sketch, tying the recognition bandwidth to the eight-tick octave and the semantic condensation gate.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.