info_per_voxel
plain-language theorem explainer
Each boundary voxel in the RS ledger on ℤ³ carries exactly one unit of information. Derivations of the Bekenstein-Hawking entropy bound from ledger capacity cite this normalization. The assignment follows directly from the unit choice in RS-native units where Gℏ = 1, making total accessible information equal to boundary area divided by 4.
Claim. The information capacity per boundary voxel is defined to be $1$ ledger unit.
background
The module derives the Bekenstein-Hawking bound S = A/(4Gℏ) from the RS ledger structure on ℤ³, closing Gap G3 in the brain holography proof. The ledger lives on ℤ³ with D = 3 forced by the eight-tick octave. Each voxel is the fundamental length quantum, set to length 1 in native units. Entropy of a configuration is proportional to its total defect, with zero defect corresponding to minimum entropy. The active edge count A per fundamental tick equals 1. Upstream, the ledger factorization structures (ℝ₊, ×) with J-cost calibration, and nuclear densities occupy discrete φ-tiers.
proof idea
Direct definition that assigns the constant value 1. No lemmas are applied; the assignment normalizes the information unit so that boundary information equals A/4 in units where Gℏ = 1.
why it matters
This definition supplies the normalization for information accessible through a boundary of area A, yielding S_BH = A/4. It closes the ledger capacity step in the brain holography proof by linking boundary voxel count to the standard Bekenstein-Hawking formula. It relies on G_hbar_product_eq_one and feeds area_not_volume_certificate and bekenstein_hawking_from_rs.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.