Chemistry Crystal Structure Fcc Hcp Same Packing

The shared packing

In crystallography, face-centered cubic (FCC) and hexagonal close-packed (HCP) are two common ways to stack spheres so that they occupy the largest possible fraction of space. Both achieve a packing efficiency of π/(3√2), about 74 percent. The two structures differ only in how their layers repeat: FCC follows an ABCABC sequence, while HCP follows ABAB. For a given sphere radius, both structures fill the same volume fraction, which is the maximum possible for equal spheres.

The framework's machine-checked library of formal theorems records this shared density as a proved equality. Its declaration fcc_hcp_same_packing states that the packing efficiency assigned to FCC equals the packing efficiency assigned to HCP. A companion theorem confirms that both structures have coordination number 12, meaning each sphere touches twelve neighbors. The equality is a theorem, not a definitional choice: it follows from the framework's own definitions of packing efficiency for the two structures, which both evaluate to the same expression.

In Recognition Science, this shared packing is one of several structural facts the framework derives from its principles. The framework models recognition, a discrete record of events, as the basis for physical structure. Within that account, the 74 percent packing and coordination 12 are not fitted parameters but consequences of the framework's forced cost function. The framework also notes that the ideal height-to-width ratio for HCP is √(8/3), about 1.633, which lies within 0.03 of the golden ratio, a constant that emerges elsewhere in the framework's derivations.

What the declaration does not claim is important. It does not say FCC and HCP are the same crystal, nor that they have identical energies or properties. It establishes only that their packing efficiencies match. The framework's own energy scale assigns both structures 0.917 relative to BCC, but that is a separate definition, not part of the packing theorem. The declaration also does not claim that real materials always adopt one structure over the other; it records a geometric equality, not a prediction about which metal forms which crystal.

For a reader, the practical consequence is a clean statement of a known geometric fact: for filling space, FCC and HCP are tied. The framework's contribution is to make that equality a formal, checkable result inside its own system, alongside its other structural derivations. The classical crystallography stands on its own; the framework provides a distinct, machine-checked path to the same number.

/-- Packing efficiency (fraction of space filled by spheres). -/
def packingEfficiency : Structure → ℝ
| .BCC => Real.pi * Real.sqrt 3 / 8  -- ≈ 0.68
| .FCC => Real.pi / (3 * Real.sqrt 2) -- ≈ 0.74
| .HCP => Real.pi / (3 * Real.sqrt 2) -- ≈ 0.74

/-- FCC and HCP have same packing. -/
theorem fcc_hcp_same_packing : packingEfficiencyApprox .FCC = packingEfficiencyApprox .HCP := rfl

/-- FCC and HCP have coordination 12. -/
theorem close_packed_coordination : coordination .FCC = 12 ∧ coordination .HCP = 12 := by
  constructor <;> rfl

/-- The ideal HCP ratio is close to φ ≈ 1.618.
    √(8/3) ≈ 1.633, φ ≈ 1.618, difference ≈ 0.015.
    Using available bounds: 1.63 < √(8/3) < 1.64, 1.61 < φ < 1.62.
    This gives |√(8/3) - φ| < 1.64 - 1.61 = 0.03. -/
theorem hcp_ratio_near_phi : |idealHCPRatio - phi| < 0.03 := by
  simp only [idealHCPRatio]
  -- First establish that √(8/3) > φ, so |√(8/3) - φ| = √(8/3) - φ
  have h_phi_lt : phi < 1.62 := phi_lt_onePointSixTwo
  have h_163_lt_sqrt : (1.63 : ℝ) < Real.sqrt (8/3) := by
    rw [Real.lt_sqrt (by norm_num : (0 : ℝ) ≤ 1.63)]
    norm_num
  have h_sqrt_gt_phi : Real.sqrt (8/3) > phi := by linarith
  rw [abs_of_pos (by linarith : Real.sqrt (8/3) - phi > 0)]
  -- Now show √(8/3) - φ < 0.03
  -- √(8/3) < 1.64 and φ > 1.61, so √(8/3) - φ < 1.64 - 1.61 = 0.03
  have h_sqrt_lt : Real.sqrt (8/3) < 1.64 := by
    rw [Real.sqrt_lt' (by norm_num : (0 : ℝ) < 1.64)]
    norm_num
  have h_phi_gt : phi > 1.61 := phi_gt_onePointSixOne
  linarith

What this page does not claim

FCC and HCP are the same crystal structure. The packing equality implies equal cohesive energy or stability for FCC and HCP. The framework predicts which real metals will adopt FCC versus HCP.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Chemistry/CrystalStructure.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: