saturationAccel_pos
plain-language theorem explainer
Saturation acceleration is positive. Researchers modeling holographic bounds or emergent gravity would cite it to fix the transition scale separating Newtonian and ILG regimes. The proof is a term-mode one-liner that unfolds the definition and invokes positivity of pi together with the already-established positivity of k_R.
Claim. $0 < a_0$ where $a_0$ is the critical acceleration at which the demanded recognition rate equals the holographic bandwidth bound set by $k_R$.
background
The Bandwidth Saturation module treats the recognition operator as subject to a finite throughput limit arising from the holographic bound. When Newtonian dynamics would require more recognition events per unit time than this bound permits, the operator compensates by batching, which manifests as the ILG time kernel $w_t > 1$. The saturation acceleration $a_0$ is the unique positive scale at which the equality between demanded rate and available bandwidth holds, using the gravitational area and dynamical time expressions given in the module.
proof idea
The proof is a one-line term wrapper. It unfolds saturationAccel, then applies div_pos to Real.pi_pos and the product of a norm_num fact establishing 2 > 0 with the upstream lemma k_R_pos.
why it matters
The result is invoked directly by high_accel_newtonian (to show gravArea is smaller above saturation) and low_accel_saturated (to show gravArea is larger below saturation), as well as by saturationAccel_well_defined. It supplies the positivity anchor required for the regime-classification theorems that realize the module's claim that ILG gravity emerges from recognition throughput limits.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.