module module

`IndisputableMonolith.Constants.SolidAngleExclusivity`

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

depends on (2)

Lean names referenced from this declaration's body.

IndisputableMonolith.Constants module_import
IndisputableMonolith.Constants.AlphaDerivation module_import

declarations in this module (11)

def unitSphereSurface L47
theorem unitSphereSurface_D3 L51
theorem unitSphereSurface_D2 L91
theorem isotropic_measure_unique_principle L107
def solidAngle L116
theorem solidAngle_is_sphere_area L119
theorem two_pi_not_D3 L126
theorem eight_pi_not_unit L135
theorem four_pi_unique_for_D3 L146
theorem geometric_seed_eq_solidAngle_times_11 L156
theorem eleven_is_passive_edges L168