module module

`IndisputableMonolith.Chemistry.CrystalStructure`

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.Chemistry.CrystalSymmetry module_import

depends on (1)

Lean names referenced from this declaration's body.

IndisputableMonolith.Constants module_import

declarations in this module (21)

inductive Structure L41
def coordination L48
def packingEfficiency L54
def packingEfficiencyApprox L60
theorem bcc_is_8_tick L66
theorem close_packed_coordination L69
theorem bcc_packing_lt_fcc L73
theorem fcc_hcp_same_packing L78
def idealHCPRatio L83
theorem ideal_hcp_ratio_value L86
theorem hcp_ratio_near_phi L104
def energyScale L124
theorem close_packed_lower_energy L130
def eightTickCoherence L140
theorem bcc_max_8tick_coherence L146
def stabilityScore L153
theorem stability_tradeoff L159
def prefersBCC L174
def prefersFCC L177
def prefersHCP L180
theorem alkali_prefer_bcc L183