IsSubSaturated
plain-language theorem explainer
A definition classifying a system as sub-saturated in the Newtonian regime precisely when its demanded recognition rate lies strictly below the holographic bandwidth set by boundary area. Modelers of information throughput in bounded regions or derivations of classical limits from the recognition framework would invoke this predicate to partition regimes. The definition consists of a direct inequality between the demanded-rate function of mass and dynamical time and the bandwidth function of area.
Claim. A system with boundary area $A$, mass $m$, and dynamical time $t$ is sub-saturated when the demanded recognition rate $r(m,t)$ satisfies $r(m,t) < B(A)$, where $B(A)$ denotes recognition bandwidth.
background
Recognition bandwidth is the maximum rate of recognition events that can be processed inside a holographically bounded region, expressed as $R_max = A/(4 ell_P^2 ln phi * 8 tau_0)$. The module assembles five previously unconnected Recognition Science elements: the holographic bound on information content, the per-bit recognition cost $k_R = ln phi$, ILG parameters, the eight-tick cadence of the recognition operator, and consciousness-boundary cost. Demanded rate is the recognition-event requirement generated by a given mass and dynamical time.
proof idea
Direct definition: the predicate holds exactly when demanded rate is strictly less than bandwidth. No lemmas or tactics are invoked; the body is the primitive inequality that partitions the state space for later case analysis.
why it matters
The definition supplies one arm of the dichotomy proved in saturated_or_sub, which asserts every system is either saturated or sub-saturated by excluded middle. It operationalizes the Newtonian regime inside the Recognition Science framework, where demand remains below the ceiling fixed by the holographic bound and eight-tick periodicity. The parent theorem saturated_or_sub thereby closes the exhaustive classification of systems under the bandwidth model.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.