cohesiveEnergyProxy
plain-language theorem explainer
cohesiveEnergyProxy assigns a real-valued proxy for metallic cohesive energy by atomic number Z: phi for transition metals, one over phi for alkaline earth metals, one over phi squared for alkali metals, and zero otherwise. Chemists modeling bond strengths within the Recognition Science framework cite it when comparing lattice energies across metal families or deriving conductivity proxies. The definition proceeds by direct case analysis on membership in the three predefined atomic-number lists.
Claim. cohesiveEnergyProxy(Z) := φ if Z ∈ transitionMetalZ, 1/φ if Z ∈ alkalineEarthZ, 1/φ² if Z ∈ alkaliMetalZ, and 0 otherwise, where φ is the golden-ratio constant supplied by the Recognition Science constants.
background
Metallic bonding is modeled here as electron delocalization across a lattice that minimizes recognition cost (J-cost) while participating in an 8-tick collective rhythm, with properties exhibiting φ-scaling. The sets alkaliMetalZ = {3,11,19,37,55,87}, alkalineEarthZ = {4,12,20,38,56,88}, and transitionMetalZ (d-block rows 4–6) classify metals by group and are imported from sibling definitions in the same module and from IonicBond. Constants.phi is drawn from the CPM bundle of universal constants and supplies the scaling factor consistent with the self-similar fixed point of the forcing chain.
proof idea
The definition is realized by nested if-then-else checks that test membership of Z in transitionMetalZ, then alkalineEarthZ, then alkaliMetalZ, returning the corresponding multiple of phi or zero. No lemmas are invoked; the body is a direct case distinction on the three sibling list definitions.
why it matters
This definition supplies the concrete values required by the downstream theorem transition_cohesive_gt_alkali, which establishes that transition metals exceed alkali metals in the proxy. It implements the φ-scaling prediction stated in the module's CH-011 derivation and connects metallic properties to the eight-tick octave and phi-ladder of the broader framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.