energyScale
plain-language theorem explainer
Energy scale assigns the dimensionless values 1.0 to BCC and 0.917 to both FCC and HCP, encoding the inverse relation between packing efficiency and cohesive energy. Materials scientists comparing lattice stability inside the Recognition Science framework would cite these assignments when ordering crystal energies. The definition is a direct case split on the three constructors of the Structure type.
Claim. The energy scale function maps crystal structure types to real numbers by the rules $e(BCC) = 1.0$, $e(FCC) = 0.917$, and $e(HCP) = 0.917$, where the values are chosen to be inversely related to packing efficiency.
background
The module classifies crystal structures into the inductive type with constructors BCC (body-centered cubic), FCC (face-centered cubic), and HCP (hexagonal close-packed). RS principles link BCC to eight-tick coordination while FCC and HCP realize maximum packing efficiency of approximately 74 percent. The local setting states that packing efficiency relates directly to cohesive energy, with the ordering FCC ≈ HCP > BCC.
proof idea
Direct definition by exhaustive case analysis on the Structure inductive type; no lemmas or tactics are applied beyond the pattern match that returns the listed real constants.
why it matters
The definition supplies the concrete numbers required by the downstream theorem close_packed_lower_energy, which proves that both FCC and HCP have strictly lower energy scale than BCC. It realizes the energy-ordering prediction stated in the module doc-comment and connects to the eight-tick coordination and phi-stability landmarks of the Recognition Science framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.