stability_tradeoff
plain-language theorem explainer
The theorem shows BCC structures outrank FCC under coherence-dominant weighting while FCC overtakes when packing weight dominates. Materials chemists modeling alkali-metal and transition-metal preferences would cite it to quantify the 8-tick versus close-packing competition. The proof is a one-line wrapper that unfolds the stabilityScore definition and dispatches both inequalities by norm_num.
Claim. Let $p$ be the packing weight and $c$ the coherence weight. Define the stability score of a structure $s$ by $p$ times its approximate packing efficiency plus $c$ times its eight-tick coherence factor. Then the BCC score at $(p,c)=(0.3,0.7)$ exceeds the FCC score at the same weights, while the FCC score at $(0.9,0.1)$ exceeds the BCC score at those weights.
background
The module treats BCC, FCC and HCP lattices as direct consequences of the Recognition Science ledger. BCC coordination equals eight, matching the fundamental eight-tick period; FCC and HCP achieve higher packing density with coordination twelve. The upstream definitions are packingEfficiencyApprox (0.68 for BCC, 0.74 for FCC) and eightTickCoherence (1.0 for BCC, 2/3 for FCC). StabilityScore is their linear combination with user-supplied weights. The constant tick supplies the RS-native time unit underlying the eight-tick ledger.
proof idea
The term proof first applies simp to unfold stabilityScore, packingEfficiencyApprox and eightTickCoherence into explicit arithmetic expressions. Constructor splits the conjunction; norm_num then verifies both numerical inequalities by direct computation of the resulting rationals.
why it matters
The result makes concrete the T7 eight-tick octave prediction inside crystal chemistry: high coherence weight selects the eight-tick lattice while high packing weight selects the close-packed lattice. It supplies the quantitative threshold (packing weight more than 5.5 times coherence weight) needed to decide metal preferences. No downstream theorems are yet attached, leaving the link to specific element assignments as an open closure point.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.