low_accel_saturated
plain-language theorem explainer
The theorem establishes that gravitational area evaluated at saturationAccel is strictly smaller than the area at any lower positive acceleration a, given positive G_N and M. Modified-gravity and cosmology researchers cite it to confirm that sub-saturation regimes exceed holographic bandwidth and therefore activate the ILG time kernel. The tactic proof unfolds the area definition, derives the reciprocal inequality on G_N M over acceleration via div_lt_div_iff₀, squares both sides with mul_self_lt_mul_self, and scales the result by positive π.
Claim. Assume $0 < a < a_{sat}$, $G_N > 0$, $M > 0$. Then $A(G_N, M, a_{sat}) < A(G_N, M, a)$, where $A(G_N, M, a) := π (G_N M / a)^2$ and $a_{sat}$ denotes the saturation acceleration.
background
The Bandwidth Saturation module formalizes ILG gravity as compensation for recognition throughput limits. Saturation acceleration $a_{sat}$ is the critical value at which demanded recognition rate equals available holographic bandwidth, using the 8-tick octave and fundamental tick $τ_0 = 1$. Gravitational area $A(G_N, M, a)$ measures the effective surface requiring recognition events for Newtonian parameters at acceleration $a$; it grows as $a$ decreases, forcing batching that appears as the ILG kernel $w_t > 1$ (ratio of demanded rate to bandwidth).
proof idea
The tactic proof first obtains $0 < G_N M$ and $0 < saturationAccel$ from the supplied positivity hypotheses and the sibling saturationAccel_pos. After unfolding gravArea it proves the key comparison $G_N M / saturationAccel < G_N M / a$ by rewriting with div_lt_div_iff₀ and applying nlinarith. It records non-negativity of the left-hand side, then applies mul_lt_mul_of_pos_left to the squared comparison (via mul_self_lt_mul_self) scaled by the positive factor π.
why it matters
This proved statement supplies the inequality direction required to conclude that $a < a_{sat}$ places the system in the bandwidth-saturated regime where ILG activates. It directly supports the module's key results on saturation implying ILG activity and feeds the construction of the ILG time kernel $w_t$ together with ilg_params_from_bandwidth. Within Recognition Science it realizes the compensation step that follows T7 (eight-tick octave) once the holographic bound is imposed, linking J-uniqueness (T5) and phi-forcing to low-acceleration phenomenology.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.