Chemistry Metallic Bond Cohesive Energy Proxy

Cohesive energy proxy

In chemistry, cohesive energy is the energy needed to break a solid metal apart into individual atoms. It is a real, measurable quantity, typically reported in electronvolts per atom, and it varies widely across the periodic table. Transition metals such as iron and tungsten bind strongly, while alkali metals such as sodium and potassium bind weakly. The Recognition Science library contains a declaration called cohesiveEnergyProxy that does not attempt to compute this energy in physical units. Instead, it defines a relative ranking: a dimensionless number that orders metals by bonding strength.

The ranking rule is simple. If the atomic number Z belongs to the transition metals (rows 4 through 6, groups 3 through 12), the proxy equals the golden ratio φ, approximately 1.618. For alkaline earth metals (group 2), it equals 1/φ, about 0.618. For alkali metals (group 1), it equals 1/φ², about 0.382. All other elements receive zero. The library proves a theorem that this proxy for any transition metal is strictly greater than the proxy for any alkali metal. That theorem, transition_cohesive_gt_alkali, is the formal content of the declaration: it establishes an ordering, not a numerical prediction.

The choice of the golden ratio is not arbitrary within the framework. Recognition Science treats the golden ratio as the unique self-similar scaling forced by its cost function, and the library uses φ here as a convenient ladder for relative bond strength. The declaration is a definition, a modeling choice, not a derived physical law. It assigns values to categories of metals; it does not measure or derive actual cohesive energies. The proxy carries no units, so it cannot be compared directly to experimental data in joules or electronvolts.

What the declaration genuinely establishes is a clean, machine-checked statement about ordering: transition metals rank above alkaline earth metals, which rank above alkali metals, in this proxy. This matches the qualitative trend in real cohesive energies, where tungsten and iron sit far above sodium and potassium. The library also records the classical lattice facts that body-centered cubic metals have coordination number 8 and close-packed structures have coordination 12, with a theorem confirming that close-packed structures are denser. Those are separate, conventional results, not consequences of the proxy.

The proxy is a starting point for organizing metallic behavior within the framework, not an endpoint. It gives a reader a compact way to see how the framework orders metals by bonding strength, and it sets up the library's further claims about conductivity and the Wiedemann-Franz law. What it does not do is replace experimental measurement or predict a specific cohesive energy value for any element.

/-- The metallic bond strength proxy is related to cohesive energy.
    Transition metals have higher cohesive energy than alkali metals. -/
def cohesiveEnergyProxy (Z : ℕ) : ℝ :=
  if Z ∈ transitionMetalZ then Constants.phi  -- Higher for transition metals
  else if Z ∈ alkalineEarthZ then 1 / Constants.phi  -- Medium
  else if Z ∈ alkaliMetalZ then 1 / Constants.phi ^ 2  -- Lower for alkali
  else 0

/-- Transition metals have higher cohesive energy than alkali metals. -/
theorem transition_cohesive_gt_alkali (Z_trans Z_alkali : ℕ)
    (h_trans : Z_trans ∈ transitionMetalZ) (h_alkali : Z_alkali ∈ alkaliMetalZ) :
    cohesiveEnergyProxy Z_trans > cohesiveEnergyProxy Z_alkali := by
  simp only [cohesiveEnergyProxy]
  -- Need to show: cohesiveEnergyProxy Z_trans > cohesiveEnergyProxy Z_alkali
  -- Transition metals: Z_trans ∈ transitionMetalZ → φ
  -- Alkali metals: Z_alkali ∈ alkaliMetalZ → 1/φ²
  -- First show that sets are disjoint
  have h_trans_not_alkali : Z_trans ∉ alkaliMetalZ := by
    simp only [transitionMetalZ, alkaliMetalZ] at h_trans h_alkali ⊢
    fin_cases h_trans <;> simp
  have h_trans_not_alk_earth : Z_trans ∉ alkalineEarthZ := by
    simp only [transitionMetalZ, alkalineEarthZ] at h_trans ⊢
    fin_cases h_trans <;> simp
  have h_alkali_not_trans : Z_alkali ∉ transitionMetalZ := by
    simp only [transitionMetalZ, alkaliMetalZ] at h_trans h_alkali ⊢
    fin_cases h_alkali <;> simp
  have h_alkali_not_alk_earth : Z_alkali ∉ alkalineEarthZ := by
    simp only [alkaliMetalZ, alkalineEarthZ] at h_alkali ⊢
    fin_cases h_alkali <;> simp
  simp only [h_trans, h_trans_not_alkali, h_trans_not_alk_earth,
             h_alkali_not_trans, h_alkali, h_alkali_not_alk_earth, ite_true, ite_false]
  -- Now need: φ > 1/φ² (which is φ³ > 1)
  have h_phi_pos := Constants.phi_pos
  have h_phi_gt_1 : Constants.phi > 1 := by
    have := Constants.phi_gt_onePointFive
    linarith
  have h_phi_cubed_gt_1 : Constants.phi^3 > 1 := by
    have : Constants.phi^3 > 1^3 := by
      apply pow_lt_pow_left₀ h_phi_gt_1 (by norm_num) (by norm_num)
    simpa using this
  calc Constants.phi = Constants.phi^3 / Constants.phi^2 := by field_simp
    _ > 1 / Constants.phi^2 := by
      apply div_lt_div_of_pos_right h_phi_cubed_gt_1
      apply pow_pos h_phi_pos

/-- The metallic bond strength proxy is related to cohesive energy.
    Transition metals have higher cohesive energy than alkali metals. -/
def cohesiveEnergyProxy (Z : ℕ) : ℝ :=
  if Z ∈ transitionMetalZ then Constants.phi  -- Higher for transition metals
  else if Z ∈ alkalineEarthZ then 1 / Constants.phi  -- Medium
  else if Z ∈ alkaliMetalZ then 1 / Constants.phi ^ 2  -- Lower for alkali
  else 0

What this page does not claim

The proxy does not predict a specific cohesive energy value in physical units for any element. The golden ratio values are a modeling choice, not a derived consequence from the framework's cost function in this declaration. The ordering theorem does not rank individual metals within a category, only between categories.

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/MetallicBond.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: