boundaryArea_pos
plain-language theorem explainer
The positivity of the spherical boundary area 4πL² for positive extent L follows immediately from real-number arithmetic. Researchers modeling holographic information budgets in Recognition Science cite it to guarantee positive capacity in consciousness constraints. The proof is a one-line term-mode application of mul_pos after unfolding the definition, using linarith, Real.pi_pos, and sq_pos_of_pos.
Claim. If $L > 0$, then $4πL^2 > 0$.
background
In the ConsciousnessBandwidth module the boundary area enters the holographic capacity formula S_holo = L² / (4ℓ_P²) that limits maintenance events over the 360-tick barrier. The definition boundaryArea L := 4 * Real.pi * L ^ 2 supplies the geometric factor for any spherical extent L. The module imports Ledger L from Recognition and Cycle3, but the present theorem depends only on the boundaryArea definition together with standard positivity facts for reals.
proof idea
Unfold boundaryArea to expose the product 4 * Real.pi * L^2. Apply mul_pos twice: the first factor 4 is obtained by linarith, the second by Real.pi_pos, and the final L^2 factor by sq_pos_of_pos hL.
why it matters
The result is invoked directly by maintenanceBudget_pos to obtain a positive maintenance budget, which in turn supports the module's claims that a critical extent L_crit exists and that bandwidth constrains conscious extent. It supplies the required positivity for the holographic area that appears in the information-budget comparison with J-cost demand, consistent with the framework's use of positive quantities throughout the phi-ladder and recognition events.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.