info_scales_subvolume
plain-language theorem explainer
In three dimensions the information accessible from a spatial region scales with its surface area rather than its volume. Holographic derivations cite this scaling to establish that bulk degrees of freedom exceed boundary encoding capacity. The short tactic proof reduces the cubic inequality to non-negative squares via nlinarith after a positivity step.
Claim. For every real number $L > 6$, the inequality $6L^2 < L^3$ holds.
background
The module derives the Bekenstein-Hawking bound from the RS ledger on the integer lattice in three dimensions. D is fixed at three by the forcing chain T8. Each voxel stores one unit of ledger information and information exchange occurs only across the boundary whose dimension is two. The surface-to-volume ratio therefore vanishes for large regions, enforcing holographic scaling.
proof idea
The tactic proof first establishes positivity of L by linear arithmetic. It then invokes nlinarith on the squares of L minus six and of L itself to conclude the strict inequality between the cubic volume and the quadratic surface term.
why it matters
This supplies the concrete surface-volume comparison inside the area-not-volume certificate. That certificate assembles the full chain from D equals three through G hbar equals one to the entropy bound S equals A over four. It directly supports the claim that information scales with area, closing the gap in the brain holography argument.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.