bcc_is_8_tick
plain-language theorem explainer
The theorem states that the body-centered cubic structure has coordination number exactly 8. Materials physicists modeling alkali metals or high-temperature iron cite it when connecting lattice geometry to the eight-tick coherence period. The proof is a direct reflexivity step on the explicit definition of the coordination function.
Claim. The coordination number of the body-centered cubic crystal structure equals 8.
background
The Crystal Structure Stability module defines a coordination function from Structure to natural numbers that assigns 8 to BCC, 12 to FCC, and 12 to HCP. This assignment encodes the eight-tick ledger period as the direct geometric signature of the forcing chain. The module situates BCC, FCC, and HCP within RS principles where packing efficiency and phi-stability govern energetic ordering, with the explicit prediction BCC coordination = 8 (8-tick).
proof idea
The proof is a one-line reflexivity wrapper that applies the defining equation of the coordination function, which maps the BCC constructor directly to 8.
why it matters
This result supplies the first explicit prediction listed in the module: BCC coordination equals 8, reflecting the eight-tick octave from the UnifiedForcingChain. It anchors the RS mechanism for crystal stability and supports the stated energy ordering FCC ≈ HCP > BCC. No downstream theorems are recorded yet, leaving open the question of how this coordination number enters quantitative energy or phase calculations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.