loadRatio
plain-language theorem explainer
The load ratio is the demanded recognition rate divided by the maximum bandwidth permitted by the holographic bound on a region of given area. Control theorems for operating regimes in bounded recognition systems cite this ratio to delineate underloaded, critical, and overloaded states. The definition is a direct quotient by the bandwidth function.
Claim. For a region of area $A$ and recognition demand $D$, the load ratio is defined by $rho = D / R_{max}(A)$, where $R_{max}(A)$ denotes the recognition bandwidth of the region.
background
The Critical Recognition Loading module introduces the load ratio as the central control variable rho = R_dem / R_max for a bounded recognition system. Healthy operation is claimed to lie in the narrow band rho_min < rho < 1, with the actuator operating on the native 8-tick cadence while stability is judged on the 360-tick supervisory horizon given by lcm(8,45). The module supplies structural lemmas that a fuller runtime or physics deployment theorem can build upon.
proof idea
One-line definition that directly returns demand divided by the bandwidth of the supplied area.
why it matters
This definition supplies the core quantity used by InCriticalBand, IsUnderloaded, loadPenalty, and the theorems criticalBand_implies_subcritical and loadPenalty_zero_of_critical. It therefore anchors the control-band analysis that connects recognition bandwidth to the sub-saturation regime required by the Recognition Science framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.