module module

`IndisputableMonolith.Cosmology.PolarizedBirthInterfaceCount`

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.Cosmology.LatticeBallEdges module_import

depends on (4)

Lean names referenced from this declaration's body.

IndisputableMonolith.Cosmology.InterfaceComponentBound module_import
IndisputableMonolith.Cosmology.LatticeBallVolume module_import
IndisputableMonolith.Cosmology.PolarizedBirthDomains module_import
IndisputableMonolith.Cosmology.PolarizedBirthInterface module_import

declarations in this module (14)

def B L62
theorem interface_length_eq_card L68
theorem edge_structure L84
def idx L94
theorem idx_card L98
theorem memSpine L105
theorem memNbr L113
def edgeIndex L121
def edgeFromIndex L126
theorem interface_card_eq L136
theorem interface_length_eq L223
theorem interface_increment_const L232
theorem interface_total_growth L241
theorem interface_increment_linear L427