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

conductivityProxy

show as:
view Lean formalization →

The conductivityProxy maps an atomic number to a real number that serves as a linear proxy for electrical conductivity in metals, scaled directly by the count of delocalized valence electrons. Chemists and Recognition Science modelers working on metallic lattices would cite it when estimating conductivity trends from the electron-sea picture. The definition is a one-line cast of the freeElectrons count to reals.

claimFor atomic number $Z$, the conductivity proxy equals the number of free valence electrons per atom, expressed as a real number.

background

The module derives metallic bonding from Recognition Science by treating delocalized electrons as a collective state that minimizes J-cost across an 8-tick coherent lattice. Free electron count is supplied by the sibling definition freeElectrons, which returns 1 for alkali metals, 2 for alkaline earth metals, and an average of 2 for transition metals. The input type Z is the integer anchor map from Masses.Anchor (and its certified alias), used here only to index the periodic table. The module states that conductivity correlates with free electron density and exhibits phi-related scaling in metal families.

proof idea

One-line definition that applies freeElectrons to the input atomic number and coerces the resulting natural number to a real.

why it matters in Recognition Science

The definition supplies the basic conductivity proxy inside the metallic bonding derivation (CH-011). It directly implements the module's claim that electrical conductivity tracks free electron density under the electron-sea and 8-tick coherence picture. No downstream results currently reference it, leaving open its use in quantitative band-structure or phi-scaling predictions.

scope and limits

formal statement (Lean)

  69def conductivityProxy (Z : ℕ) : ℝ :=

proof body

Definition body.

  70  (freeElectrons Z : ℝ)
  71
  72/-- Coordination number in metallic lattices.
  73    BCC: 8, FCC/HCP: 12 -/

depends on (3)

Lean names referenced from this declaration's body.