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

Structure

show as:
view Lean formalization →

Crystal structures are enumerated as the inductive type with constructors BCC, FCC, and HCP. Researchers deriving coordination numbers or packing efficiencies from the eight-tick ledger would cite this base type. The definition is a direct inductive enumeration with no computational content or additional axioms.

claimThe crystal structures form an inductive type consisting of the constructors BCC (body-centered cubic), FCC (face-centered cubic), and HCP (hexagonal close-packed).

background

The Chemistry.CrystalStructure module models BCC, FCC, and HCP as emerging from RS principles. The 8-Tick Coordination assigns BCC coordination number 8 to match ledger periodicity, while FCC and HCP reach coordination 12 with packing efficiency π/(3√2) ≈ 74%. The phi-Stability sets the ideal HCP c/a ratio √(8/3) ≈ 1.633 ≈ φ, and Energy Ordering places FCC ≈ HCP above BCC in cohesive energy. This local setting follows the forcing chain and supplies the types used by downstream coordination and eightTickCoherence definitions. It depends on the meta-realization structure from UniversalForcingSelfReference.for, which records the structural properties required for self-reference axioms.

proof idea

The declaration is an inductive definition that directly introduces the three constructors BCC, FCC, and HCP.

why it matters in Recognition Science

This inductive type underpins the coordination, eightTickCoherence, energyScale, and packingEfficiency definitions in the same module, plus windowSums_shift_equivariant in CostAlgebra and PhiInt in PhiRing. It realizes the CM-001 predictions for crystal structure stability by supplying the types that link BCC to the eight-tick octave (T7) and HCP to the φ fixed point. It touches the open question of how the phi-ladder extends from mass formulas to material packing efficiencies.

scope and limits

formal statement (Lean)

  41inductive Structure
  42| BCC  -- Body-centered cubic
  43| FCC  -- Face-centered cubic
  44| HCP  -- Hexagonal close-packed
  45deriving Repr, DecidableEq
  46
  47/-- Coordination number for each structure. -/

used by (40)

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

… and 10 more

depends on (1)

Lean names referenced from this declaration's body.