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

packingEfficiencyApprox

show as:
view Lean formalization →

packingEfficiencyApprox supplies the standard approximate packing fractions for BCC, FCC, and HCP structures in the Recognition Science model. Chemists comparing cohesive energies or stability tradeoffs would cite these values when weighting packing density against 8-tick coherence. The definition proceeds by exhaustive case analysis on the Structure inductive type.

claimThe approximate packing efficiency is defined by cases: 0.68 for body-centered cubic structures, 0.74 for face-centered cubic structures, and 0.74 for hexagonal close-packed structures.

background

The module CrystalStructure introduces the inductive type Structure with constructors BCC, FCC, and HCP. The sibling definition coordination assigns 8 to BCC and 12 to FCC/HCP, directly reflecting the 8-tick period. The module doc states that BCC coordination equals 8-tick while FCC and HCP achieve maximum packing efficiency of approximately 74 percent with coordination 12. Upstream, Constants.tick supplies the fundamental RS time quantum with one octave equal to 8 ticks.

proof idea

The definition is implemented by direct pattern matching on the Structure constructors, returning the fixed numerical values 0.68 for BCC and 0.74 for FCC and HCP.

why it matters in Recognition Science

This definition supplies the packing numbers used in bcc_packing_lt_fcc to prove BCC packing is strictly lower than FCC and in fcc_hcp_same_packing to prove FCC equals HCP. It feeds stabilityScore and stability_tradeoff to quantify the tradeoff between packing efficiency and 8-tick coherence. In the framework it supports the module prediction that FCC/HCP packing exceeds BCC, consistent with the eight-tick octave and close-packing limits.

scope and limits

Lean usage

theorem bcc_lt_fcc : packingEfficiencyApprox .BCC < packingEfficiencyApprox .FCC := by simp [packingEfficiencyApprox]; norm_num

formal statement (Lean)

  60def packingEfficiencyApprox : Structure → ℝ
  61| .BCC => 0.68
  62| .FCC => 0.74
  63| .HCP => 0.74
  64
  65/-- BCC coordination equals 8-tick. -/

used by (4)

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

depends on (4)

Lean names referenced from this declaration's body.