IsSubcritical
plain-language theorem explainer
Subcritical systems satisfy a strict inequality between demanded recognition rate and the maximum bandwidth permitted by a region's area. Control theorists building stability arguments for recognition-based systems cite this predicate to bound operating regimes below saturation. The definition is a direct comparison imported from the bandwidth function without additional lemmas.
Claim. A system with area $A$ and demand $D$ is subcritical when $D < R_*(A)$, where $R_*(A)$ is the recognition bandwidth of the region.
background
The module develops structural lemmas for a control theorem on recognition loading. The load ratio is defined as rho = R_dem / R_max, with healthy regimes satisfying rho_min < rho < 1. Stability is assessed on the 360-tick supervisory horizon obtained from lcm(8,45), while the actuator follows the native 8-tick cadence. The bandwidth function, imported from RecognitionBandwidth, supplies the ceiling: R_max(A) equals A divided by four times Planck area, k_R = ln(phi), and the eight-tick cadence factor.
proof idea
The declaration is a definition that directly equates the predicate to the inequality demand < bandwidth area. No tactics or lemmas are applied beyond the unfolding of the imported bandwidth term.
why it matters
This predicate appears in the certificates criticalRecognitionLoading_certificate and forcedCriticalRecognitionLoading_certificate, which conjoin subcriticality with attention and zeta bounds. It supplies one of the structural lemmas required by the module's control theorem sketch, linking the load-ratio regime to the eight-tick cadence and phi-based constants of the Recognition Science framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.