pith. machine review for the scientific record. sign in
def definition def or abbrev

stabilityScore

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal 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. -/

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (3)

Lean names referenced from this declaration's body.