LatticeType
plain-language theorem explainer
LatticeType enumerates the three metallic crystal structures employed in Recognition Science derivations of bonding and conductivity. Researchers computing coordination numbers or packing fractions from electron delocalization would reference it to index the 8-tick and 12-fold cases. The declaration is a plain inductive type whose constructors serve as the domain for two immediate sibling definitions.
Claim. The type of metallic lattice structures is the inductive type generated by the three constructors BCC (body-centered cubic), FCC (face-centered cubic), and HCP (hexagonal close-packed).
background
The MetallicBond module derives metallic bonding from electron delocalization that minimizes recognition cost (J-cost) while satisfying an 8-tick collective rhythm. LatticeType supplies the discrete domain needed to assign coordination numbers that realize this rhythm. The upstream coordination definition from CrystalStructure already maps BCC to 8 and both FCC and HCP to 12; the present inductive type simply reifies those three cases inside the metallic-bonding context.
proof idea
The declaration is an inductive definition that introduces exactly three constructors and derives Repr and DecidableEq; no lemmas are applied.
why it matters
LatticeType supplies the input type for coordinationNumber and packingEfficiency, which quantify how lattice geometry supports the delocalized electron sea required by the metallic-bonding derivation (CH-011). It directly instantiates the eight-tick octave (T7) landmark inside chemistry. The supplied material records no open questions attached to this definition.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.