eightTickCoherence
plain-language theorem explainer
The eight-tick coherence function maps each crystal structure to a real score reflecting alignment with the RS ledger period of eight ticks. BCC receives 1 while FCC and HCP receive 2/3. Materials modelers cite it when weighting periodicity against packing in stability predictions. The definition proceeds by exhaustive case analysis on the three constructors of the Structure type.
Claim. Define the eight-tick coherence function $c$ on crystal structures by $c$(BCC) $= 1$, $c$(FCC) $= 2/3$, and $c$(HCP) $= 2/3$.
background
The Crystal Structure Stability module derives BCC, FCC, and HCP from RS principles. The Structure inductive type classifies crystals into BCC, FCC, and HCP. Upstream the tick constant satisfies one octave equals 8 ticks as the fundamental evolution period. The module states that BCC coordination number 8 directly reflects ledger periodicity, favoring it when 8-tick coherence dominates.
proof idea
The definition implements direct case analysis on the Structure inductive type, returning 1.0 for BCC and 2/3 for both FCC and HCP.
why it matters
This definition supplies the coherence term in stabilityScore and enables bcc_max_8tick_coherence. It realizes the 8-tick coordination mechanism from the module, linking to the eight-tick octave (T7) in the forcing chain. Downstream theorems use it to quantify when high coherence weight favors BCC over close-packed structures.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.