module module

`IndisputableMonolith.Cosmology.PolarizedBirthDomains`

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 (3)

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

IndisputableMonolith.Cosmology.LatticeBallEdges module_import
IndisputableMonolith.Cosmology.PolarizedBirthInterface module_import
IndisputableMonolith.Cosmology.PolarizedBirthInterfaceCount module_import

depends on (2)

Lean names referenced from this declaration's body.

IndisputableMonolith.Cosmology.InterfaceComponentBound module_import
IndisputableMonolith.Cosmology.LatticeBallVolume module_import

declarations in this module (14)

theorem clos_someRoot_of_descent L51
theorem comp_le_of_roots L77
theorem clos_mono_charge L98
theorem three_le_comp_of_three_charges L111
def polarized L147
def Fmono L151
def hgt L156
theorem mem_Fmono L160
def roots L166
theorem hzero L172
theorem hdesc L194
theorem polarized_components_le_three L240
theorem polarized_components_eq_three L254
theorem polarized_carried_subextensive L268