saturated_or_sub
plain-language theorem explainer
The theorem asserts that any gravitating system with given boundary area, mass, and dynamical time falls into either the bandwidth-saturated regime or the sub-saturated regime. Workers modeling the Newtonian-to-ILG transition cite this dichotomy to partition parameter space without gaps. The proof unfolds the two predicates and applies trichotomy to the comparison of demanded rate against bandwidth, dispatching to the matching disjunct.
Claim. For any real numbers $A$, $M$, $T$, either the demanded recognition rate $M/T$ satisfies $M/T$ ≥ $A/(4ℓ_P² k_R · 8τ_0)$ or $M/T$ < $A/(4ℓ_P² k_R · 8τ_0)$, where the right-hand side is the recognition bandwidth of the region.
background
Recognition bandwidth is defined as the maximum ledger-event rate permitted by the holographic bound: $R_max(A) = A / (4ℓ_P² · ln(φ) · 8τ_0)$, with each recognition event costing $k_R = ln(φ)$ bits and the eight-tick cadence limiting throughput. Demanded rate is the Newtonian requirement $M/T_dyn$, where $T_dyn$ is the Keplerian dynamical time at the relevant radius. IsSaturated holds when demanded rate meets or exceeds bandwidth (ILG regime); IsSubSaturated holds when demand lies strictly below bandwidth (Newtonian regime). The module connects holographic capacity, per-bit recognition cost, and the eight-tick cadence to produce this hard ceiling on throughput.
proof idea
The proof unfolds IsSaturated and IsSubSaturated to expose the comparison between demandedRate and bandwidth, then applies le_or_lt to that real-number inequality and routes the resulting left or right case directly to the corresponding disjunct of the disjunction.
why it matters
The result supplies the exhaustive partition of regimes required by the Recognition Bandwidth module, ensuring every system is classified without remainder. It directly supports the activation condition for ILG modifications when holographic capacity is exceeded and rests on the five-element unification (holographic bound, $k_R$, ILG parameters, eight-tick cadence, consciousness boundary cost) stated in the module header. No downstream theorems are recorded yet, so the lemma remains available for any later saturation-threshold analysis.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.