cube_volume_surface
plain-language theorem explainer
The theorem asserts that for any positive integer L the surface area 6L squared and volume L cubed of a cube are both strictly positive. It would be cited in derivations of the Bekenstein-Hawking bound from the Recognition Science ledger on the integer lattice in three dimensions. The proof is a term-mode wrapper that splits the conjunction and invokes the positivity tactic on each factor.
Claim. For every positive integer $L$, both $6L^2 > 0$ and $L^3 > 0$.
background
The module derives the Bekenstein-Hawking entropy bound from the Recognition Science ledger structure on ℤ³. In this setting each voxel carries one unit of ledger information and the boundary of a region scales as volume to the power (D-1)/D. For D = 3 this yields surface area scaling as L² when volume scales as L³. Upstream results include the volume definition as the cardinality of the set of vertices and the forcing of exactly three spatial dimensions from the T0-T8 chain.
proof idea
The proof is a term-mode wrapper. It applies the constructor tactic to split the conjunction into two goals and then invokes the positivity tactic on each goal separately.
why it matters
The result supplies the elementary positivity fact required for the geometric terms in the Bekenstein-Hawking derivation from the ledger. It supports the module's main claims that information scales with boundary count rather than volume and that S_BH equals boundary area over 4 in natural units where Gℏ = 1. It closes a basic step toward Gap G3 in the brain holography argument.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.