module module

`IndisputableMonolith.Papers.GCIC.BekensteinFromLedger`

show as: view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

IndisputableMonolith.Papers.GCIC.BrainHolography module_import

depends on (2)

Lean names referenced from this declaration's body.

IndisputableMonolith.Constants module_import
IndisputableMonolith.Cost module_import

declarations in this module (17)

def D L42
theorem boundary_dimension L45
theorem boundary_exponent L49
theorem cube_volume_surface L53
theorem cube_sv_ratio L61
theorem cube_isoperimetric L67
def G_rs L79
def hbar_rs L82
theorem G_hbar_product_eq_one L86
theorem G_rs_pos L93
theorem hbar_rs_pos L98
def info_per_voxel L105
theorem bekenstein_hawking_from_rs L114
theorem bekenstein_positive L121
theorem info_scales_subvolume L135
theorem sv_ratio_decreasing L145
theorem area_not_volume_certificate L159