area_not_volume_certificate
plain-language theorem explainer
area_not_volume_certificate assembles the five conjuncts that confirm information in the RS ledger on Z^3 scales with boundary area rather than enclosed volume. A physicist closing the holographic gap in brain models or deriving the Bekenstein-Hawking bound from ledger capacity would cite it. The proof is a single exact term that packages boundary_dimension, boundary_exponent, G_hbar_product_eq_one, bekenstein_hawking_from_rs, and info_scales_subvolume.
Claim. With spatial dimension forced to three, the boundary of any region is two-dimensional, the scaling exponent equals 2/3, the product of the RS gravitational constant and reduced Planck constant equals one, the entropy bound reduces to boundary area over four for any positive area, and surface area grows slower than volume for lengths exceeding six.
background
The module derives the Bekenstein-Hawking bound from the RS ledger on the integer lattice Z^3, closing Gap G3 in the brain holography proof. D is defined as three by the forcing chain T8. G_rs equals phi to the fifth and hbar_rs equals phi to the minus fifth, so their product is one. Each voxel carries one unit of ledger information and accessible information flows only through the boundary. The key upstream result bekenstein_hawking_from_rs shows that in these units the entropy is exactly A/4.
proof idea
The proof is a term-mode exact constructor that directly supplies the five conjuncts from sibling lemmas: boundary_dimension for D minus one equals two, boundary_exponent for the two-thirds ratio, G_hbar_product_eq_one for the unit product, the lambda abstraction applying bekenstein_hawking_from_rs to obtain the entropy simplification, and another applying info_scales_subvolume for the surface-volume inequality.
why it matters
This certificate completes the derivation chain that closes Gap G3 by showing information scales with area, not volume, in the RS ledger on Z^3. It feeds the holographic bound used in brain holography arguments. It directly instantiates T8 (D equals three) and the natural-unit relation G hbar equals one from the phi-ladder. The module doc states it confirms S equals A over four where A is the boundary count.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.