IsOverloaded
plain-language theorem explainer
IsOverloaded holds precisely when demanded recognition rate meets or exceeds the bandwidth ceiling fixed by boundary area. Control theorists analyzing saturation in semantic systems cite it to mark the upper edge of the stable operating regime. The definition is a direct one-line inequality that invokes the precomputed bandwidth function without further reduction.
Claim. A recognition process with boundary area $A$ and demand rate $D$ is overloaded when $D$ meets or exceeds the maximum recognition events per unit time permitted by the holographic bound on $A$.
background
The module sketches a control theorem for recognition systems whose load ratio is defined as rho = demand / bandwidth(area). Healthy regimes are required to satisfy rho_min < rho < 1, with the actuator operating on the native 8-tick cadence while stability is judged over the 360-tick supervisory horizon. Bandwidth itself is the upstream definition R_max(A) = A / (4 * planckArea * k_R * eightTickCadence), the maximum event rate allowed by the holographic bound given k_R = ln(phi) bits per event.
proof idea
One-line definition that directly sets IsOverloaded area demand to the inequality bandwidth area ≤ demand.
why it matters
The definition supplies the upper boundary predicate used by the downstream theorem criticalBand_not_overloaded, which proves that any state inside the critical band remains strictly below overload. It completes one structural piece of the module's control sketch for sub-saturation operation, tying directly to the 8-tick cadence and recognition bandwidth landmarks of the Recognition Science framework. The sketch remains open on full runtime or physics deployment of the stability controller.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.