prefersHCP
The definition enumerates atomic numbers of metals that favor HCP crystal structures under Recognition Science rules. A condensed matter physicist would cite it when mapping element preferences to eight-tick coherence and phi-ratio stability. It is implemented as a direct list assignment with no computation or lemmas applied.
claimThe atomic numbers of metals preferring hexagonal close-packed crystal structures are $12$ (Mg), $30$ (Zn), $22$ (Ti), and $40$ (Zr).
background
Crystal structures emerge from RS principles in this module. BCC aligns with coordination number 8 from the eight-tick ledger period. Close-packed FCC and HCP reach maximum packing efficiency with coordination 12, while HCP is further distinguished by its ideal c/a ratio approximating phi. Energy ordering places FCC and HCP above BCC in cohesive energy for close-packed cases.
proof idea
This is a direct definition that assigns the constant list of atomic numbers without invoking any lemmas or tactics.
why it matters in Recognition Science
This definition supplies concrete examples for the HCP branch of the crystal structure predictions. It supports the module's RS mechanism section on phi-stability and eight-tick coordination by identifying specific metals where HCP is selected over BCC or FCC. No downstream uses are recorded yet.
scope and limits
- Does not derive the list from the forcing chain or RCL.
- Does not compute packing efficiencies or coordination numbers.
- Does not address temperature-driven phase changes.
- Does not claim completeness over all HCP metals.
formal statement (Lean)
180def prefersHCP : List ℕ := [12, 30, 22, 40]
proof body
Definition body.
181
182/-- Alkali metals prefer BCC (strongest 8-tick coherence). -/