high_accel_newtonian
plain-language theorem explainer
Above saturation acceleration, gravitational area decreases strictly with rising acceleration, so Newtonian gravity suffices without recognition batching. An astrophysicist modeling high-acceleration orbits or binaries would cite this to bound the classical regime inside the Recognition Science unification. The tactic proof unfolds the area definition, compares the quotients via division monotonicity, then invokes monotonicity of squaring on the positive reals.
Claim. Let $a > a_0$ with $G_N > 0$ and $M > 0$. Then the gravitational area satisfies $4π (G_N M / a)^2 < 4π (G_N M / a_0)^2$.
background
The Bandwidth Saturation module derives ILG gravity from holographic recognition throughput limits. Saturation acceleration $a_0$ is the threshold at which demanded recognition rate $M/T_ dyn$ equals the bound set by gravitational area over Planck area, recognition constant, and eight-tick cycle. Gravitational area is the quantity $4π(G_N M / a)^2$ that enters the rate comparison. The module imports positivity of $a_0$ and arithmetic comparison lemmas to separate the Newtonian and saturated regimes.
proof idea
Tactic proof begins by importing positivity of saturation acceleration and of $a$ via the upstream positivity lemma and lt_trans. It forms the product $G_N M > 0$ by mul_pos, unfolds the area definition, and obtains the strict quotient inequality by div_lt_div_iff₀ followed by nlinarith. Non-negativity of the quotient is immediate from div_pos. The square comparison is finished by mul_lt_mul_of_pos_left applied to the self-product inequality produced by nlinarith.
why it matters
The result supplies the high-acceleration half of the bandwidth saturation dichotomy stated in the module doc-comment, confirming that Newtonian dynamics hold once gravitational area drops below the holographic limit. It pairs with the companion low-acceleration theorem that activates the ILG kernel. In the broader framework it anchors the transition at the eight-tick octave scale (T7) where recognition throughput first saturates, without invoking extra hypotheses.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.