gravArea_inv_sq
plain-language theorem explainer
Gravitational area scales as the inverse square of acceleration. In the bandwidth saturation framework this identity follows from the area definition A proportional to (G_N M / a)^2 and is used when equating demanded recognition rate to holographic capacity. Researchers deriving the critical acceleration a_sat or the ILG time kernel cite the relation to rescale dynamical times consistently. The proof is a one-line algebraic reduction after unfolding the area definition.
Claim. Let $A(G_N, M, a)$ denote gravitational area. Then for positive real numbers $c$ and $a$, $A(G_N, M, c a) = A(G_N, M, a) / c^2$.
background
The BandwidthSaturation module shows how ILG gravity arises when Newtonian dynamics exceed recognition throughput. At saturation the demanded rate M / T_dyn equals the holographic bound A / (4 ℓ_P² k_R 8 τ_0), with T_dyn the Keplerian period and A the gravitational area at acceleration a. Gravitational area is the surface 4π(2 G_N M / a)^2 evaluated at the radius where acceleration equals a. The theorem uses the definition of gravArea together with real arithmetic; upstream constants include Time from RSNativeUnits and radius from CellularAutomata.
proof idea
The proof unfolds the definition of gravArea and applies the ring tactic to cancel terms in the resulting polynomial identity over the reals.
why it matters
The scaling supplies the algebraic step needed to solve the implicit saturation equation for a_sat inside the module. It feeds the derivations of saturationAccel, ilg_kernel_compensates and ilg_params_from_bandwidth listed in the module documentation. The identity is consistent with the eight-tick octave (T7) by preserving the relation between dynamical time and recognition cycles when accelerations are rescaled.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.