gravArea_pos
gravArea_pos establishes that the effective gravitational area A(a) = 4π(G_N M / a)^2 is strictly positive for positive real parameters G_N, M, and a. Researchers modeling ILG gravity from recognition bandwidth limits cite it to keep the holographic area term well-defined in saturation threshold derivations. The proof is a direct term-mode reduction that unfolds the explicit formula and chains mul_pos with sq_pos_of_pos.
claimIf $G_N > 0$, $M > 0$, and $a > 0$, then the gravitational area $A = 4π (G_N M / a)^2$ satisfies $A > 0$.
background
The BandwidthSaturation module models how recognition throughput limits induce ILG gravity by batching dynamical effects over 8-tick cycles when Newtonian demands exceed the holographic bound. The gravArea function computes the effective area of the sphere where Newtonian acceleration equals a given value a, entering the rate comparison that defines the critical saturation acceleration a_sat. The upstream definition of G_N supplies Newton's constant in SI units from entanglement entropy calculations, while the Recognition and Cycle3 structures supply the discrete recognition operator M underlying the continuum bridge.
proof idea
The term-mode proof unfolds gravArea to the product 4 * π * (G_N * M / a)^2. It applies mul_pos to separate the constant factor (positive by linarith on 4 and Real.pi_pos) from the squared quotient. The squared term is then shown positive by sq_pos_of_pos applied to the positive ratio obtained via mul_pos on hG and hM divided by ha.
why it matters in Recognition Science
This lemma secures positivity of the area term required for the saturation acceleration equation in the module, where demanded recognition rate equals bandwidth at a_sat. It supports sibling results such as saturationAccel_pos and ilg_kernel_compensates that derive the ILG time kernel w_t > 1. In the Recognition Science framework it anchors the Newtonian-to-saturated transition at the holographic bound, consistent with the eight-tick octave and phi-ladder scaling.
scope and limits
- Does not establish the numerical value of the saturation acceleration a_sat.
- Does not incorporate discrete recognition events or phi-ladder corrections.
- Does not address non-positive values of G_N, M, or a.
- Does not prove stability or convergence of the resulting ILG dynamics.
formal statement (Lean)
52theorem gravArea_pos {G_N M a : ℝ} (hG : 0 < G_N) (hM : 0 < M) (ha : 0 < a) :
53 0 < gravArea G_N M a := by
proof body
Term-mode proof.
54 unfold gravArea
55 apply mul_pos
56 · exact mul_pos (by linarith) Real.pi_pos
57 · exact sq_pos_of_pos (div_pos (mul_pos hG hM) ha)
58
59/-- Gravitational area scales as 1/a². -/