boundaryArea_pos
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.
claimIf $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 in Recognition Science
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.
scope and limits
- Does not bound the magnitude of the area or relate it to J-cost.
- Applies only to the spherical definition given in the module.
- Does not treat non-Euclidean or higher-dimensional boundaries.
- Does not incorporate the 360-tick barrier period or phi-ladder scaling.
Lean usage
have hA : 0 < boundaryArea L := boundaryArea_pos hLformal statement (Lean)
86theorem boundaryArea_pos {L : ℝ} (hL : 0 < L) : 0 < boundaryArea L := by
proof body
Term-mode proof.
87 unfold boundaryArea
88 exact mul_pos (mul_pos (by linarith) Real.pi_pos) (sq_pos_of_pos hL)
89