stabilityScore
Stability score for a crystal structure is the weighted sum of its packing efficiency and eight-tick coherence. Materials modelers comparing BCC metals to close-packed lattices cite this when tuning the relative importance of density versus coordination periodicity. The definition is a direct linear combination of the two component functions.
claimThe stability score of crystal structure $s$ is $w_p p(s) + w_c c(s)$, where $p(s)$ is the approximate packing efficiency of $s$ and $c(s)$ is the eight-tick coherence factor of $s$.
background
The module classifies crystal structures into three inductive cases: BCC, FCC, and HCP. Eight-tick coherence returns 1 for BCC and 2/3 for FCC or HCP, because coordination number 8 matches the ledger period exactly while coordination 12 matches only partially. Packing efficiency approximates 0.68 for BCC and 0.74 for FCC or HCP, matching the known geometric densities.
proof idea
One-line definition that multiplies the supplied packing weight by packingEfficiencyApprox s and adds the coherence weight times eightTickCoherence s.
why it matters in Recognition Science
This definition supplies the scoring function used by the stability_tradeoff theorem, which proves that high coherence weight selects BCC while high packing weight selects FCC. It encodes the module's RS mechanism: BCC coordination equals the eight-tick octave while close packing maximizes density at the cost of diluted coherence. The construction sits inside the chemistry module that derives lattice types from the eight-tick ledger period.
scope and limits
- Does not incorporate temperature or pressure dependence.
- Does not use the phi-ladder mass formula or J-cost functional.
- Does not compute exact packing fractions from geometry.
- Does not address stacking faults or HCP c/a deviations.
Lean usage
stabilityScore .BCC 0.3 0.7formal statement (Lean)
153def stabilityScore (s : Structure) (packing_weight coherence_weight : ℝ) : ℝ :=
proof body
Definition body.
154 packing_weight * packingEfficiencyApprox s + coherence_weight * eightTickCoherence s
155
156/-- With high coherence weight, BCC wins; with very high packing weight, FCC wins.
157 For FCC to beat BCC: 0.74p + 0.667c > 0.68p + 1.0c → 0.06p > 0.333c → p/c > 5.5
158 So we need packing weight over 5× the coherence weight. -/