Chemistry Metallic Bond

The electron sea

A metallic bond is the force that holds metal atoms together when their outer electrons detach from individual atoms and move freely through the whole solid. This electron sea (a delocalized cloud of valence electrons) surrounds a lattice of positively charged metal ions, and the electrostatic attraction between the negative sea and the positive ions is what gives metals their strength, conductivity, and malleability. The classical picture, taught since the early 20th century, treats the sea as a shared resource: each atom contributes its few valence electrons, and no electron belongs to any single atom.

Recognition Science (RS) models this same phenomenon through its central concept of recognition cost, a forced expense the framework says reality pays whenever it registers an event. The framework's core theorem proves that any cost function meeting five plain conditions must equal J(x) = (x + 1/x)/2 - 1. In the metallic case, RS argues that delocalizing electrons across the lattice minimizes this cost: spreading the electrons out lowers the total recognition expense compared to holding them pinned on individual atoms. The framework models the metallic state as a coherent many-body system whose electrons share a collective 8-tick rhythm, a cycle derived from the cost function that also produces the number 8 as a structural constant.

The module in the machine-checked library of formal theorems, MetallicBond.lean, establishes concrete facts about this model. It defines which elements count as metals (alkali, alkaline earth, and transition metals), assigns each a free electron count (1 for alkali, 2 for alkaline earth, 2 as a simplified average for transition metals), and defines a conductivity proxy as simply that free electron count. The library proves that alkali metals have exactly one valence electron, that transition metals have higher cohesive energy than alkali metals (using the golden ratio φ as a scaling factor: φ for transition, 1/φ² for alkali), and that close-packed lattices (FCC, HCP) are denser than body-centered cubic (BCC), with coordination numbers 12 versus 8.

The framework also connects its 8-tick cycle to the BCC lattice's coordination number of 8, a numerical match the module records as a theorem. For thermal and electrical conductivity, the library defines the Lorenz number from the Wiedemann-Franz law, L = κ/(σT) ≈ 2.44 × 10⁻⁸ WΩK⁻², and proves it is positive. These are definitional models and small formal theorems, not empirical measurements: the module chooses how to represent metallic properties, and the proofs check that the definitions behave consistently.

What this establishes in plain language is a working vocabulary: RS can describe metallic bonding in its own terms, with specific numbers for electron counts, coordination, and cohesive energy, all checked by machine. The framework does not yet derive a full theory of metallic conductivity from first principles; it models the known chemistry and flags where its constants (like φ in cohesive energy) appear as scaling choices. The payoff is a consistent formal scaffold that connects a textbook chemistry topic to the framework's broader claim that recognition cost shapes physical structure.

/-- The Lorenz number is positive. -/
theorem lorenz_positive : lorenzNumber > 0 := by
  simp only [lorenzNumber]
  apply mul_pos
  · apply div_pos
    · exact sq_pos_of_pos Real.pi_pos
    · norm_num
  · apply sq_pos_of_pos
    apply div_pos <;> norm_num

/-- Metals have low ionization energy (alkali metals are easiest to ionize). -/
theorem alkali_low_ionization (Z : ℕ) (h : Z ∈ alkaliMetalZ) :
    valenceElectrons Z = 1 := by
  simp only [alkaliMetalZ] at h
  -- alkaliMetalZ = [3, 11, 19, 37, 55, 87]
  -- Each alkali metal: Z - prevClosure Z = 1
  fin_cases h <;> native_decide

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

/-- FCC/HCP have higher packing efficiency than BCC. -/
theorem fcc_hcp_denser_than_bcc :
    packingEfficiency .BCC < packingEfficiency .FCC ∧
    packingEfficiency .BCC < packingEfficiency .HCP := by
  constructor <;> { simp only [packingEfficiency]; norm_num }

/-- The Lorenz number is positive. -/
theorem lorenz_positive : lorenzNumber > 0 := by
  simp only [lorenzNumber]
  apply mul_pos
  · apply div_pos
    · exact sq_pos_of_pos Real.pi_pos
    · norm_num
  · apply sq_pos_of_pos
    apply div_pos <;> norm_num

What this page does not claim

No claim that the framework derives metallic conductivity from first principles. No claim that the φ-scaling of cohesive energy is empirically measured. No claim that the 8-tick BCC coordination match is a physical derivation.

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: