energyScale
plain-language theorem explainer
The energyScale definition assigns dimensionless real values to the three crystal structure types, fixing BCC at 1.0 while setting both FCC and HCP to 0.917 to encode their higher packing efficiency. Material scientists applying RS-derived stability arguments would cite these numbers when ranking cohesive energies of lattices. The definition is realized by exhaustive case distinction on the Structure inductive type.
Claim. Let $E$ map crystal structures to reals by $E$(BCC) = 1.0, $E$(FCC) = 0.917, $E$(HCP) = 0.917, where the values are chosen inversely proportional to packing fraction so that close-packed lattices receive the lower scale.
background
The Structure inductive type enumerates the three lattices: BCC (body-centered cubic), FCC (face-centered cubic), and HCP (hexagonal close-packed). Module context ties BCC coordination 8 directly to the eight-tick ledger period, while FCC and HCP reach maximum packing efficiency ≈74% with coordination 12; the ideal HCP c/a ratio is noted as ≈φ. The upstream scale definition supplies noncomputable powers of phi for cosmological lengths, but energyScale uses fixed numerical ratios derived from the 68/74 packing comparison.
proof idea
Direct definition by pattern matching on the three constructors of Structure, returning the listed real constants with no further reduction or lemma application.
why it matters
Supplies the concrete coefficients required by the downstream close_packed_lower_energy theorem, which proves FCC and HCP energy scales are strictly smaller than BCC. It implements the module's energy-ordering prediction (FCC ≈ HCP > BCC) and connects the 8-tick coordination mechanism to observed metallic preferences. The 0.917 factor approximates the packing-efficiency ratio while remaining consistent with the phi-stability and eight-tick octave landmarks of the framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.