IsSaturated
plain-language theorem explainer
A gravitating system is bandwidth-saturated when the recognition rate demanded by its Newtonian dynamics exceeds the holographic bandwidth limit set by its boundary area. Researchers modeling the transition to modified gravity or ILG regimes would cite this predicate to flag activation thresholds. The definition is a direct inequality between the pre-defined demandedRate and bandwidth functions.
Claim. A system with boundary area $A$, mass $m$, and dynamical time $t_d$ is bandwidth-saturated when the demanded recognition rate satisfies demandedRate$(m, t_d) ≥ bandwidth(A)$, where bandwidth$(A)$ equals the holographic maximum $A / (4 ℓ_P² · ln φ · 8 τ_0)$.
background
The RecognitionBandwidth module connects five previously separate Recognition Science elements: the holographic bound on information content, the per-bit recognition cost $k_R = ln φ$, ILG parameters $C_lag = φ^{-5}$ and $α = (1-1/φ)/2$, the eight-tick cadence of the recognition operator, and the consciousness boundary cost. Recognition bandwidth is the resulting hard ceiling on ledger throughput: $R_max = A / (4 ℓ_P² · ln φ · 8 τ_0)$. demandedRate is the rate implied by Newtonian dynamics for the given mass and dynamical time. Upstream, A denotes the active edge count per fundamental tick (IntegrationGap.A and Masses.Anchor.A), while the eight-tick structure appears in the module's cadence definitions.
proof idea
The definition is a one-line wrapper that applies the comparison demandedRate mass dynamicalTime ≥ bandwidth area, using the functions already introduced in the module.
why it matters
This predicate is the left disjunct in the downstream theorem saturated_or_sub, which partitions every system into saturated or sub-saturated regimes by excluded middle. It supplies the precise threshold at which ILG must activate, thereby linking the holographic bound, the recognition cost ln φ, and the eight-tick octave (T7) to gravitational dynamics. The module documentation lists this connection as one of the five previously unlinked elements now formally joined.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.