ionicThreshold
plain-language theorem explainer
The ionicThreshold definition supplies the real constant 0.02 as the cutoff for classifying a bond as ionic when the electronegativity proxy difference exceeds it. Chemists applying RS bonding rules would cite this value to confirm ionic character for alkali-halogen pairs. The declaration is introduced as a direct constant assignment based on external numerical checks of enProxy values.
Claim. Define the ionic threshold as the real constant $0.02$. A bond between atomic numbers $Z_1$ and $Z_2$ is ionic when the electronegativity difference exceeds $0.02$.
background
The Ionic Bond Formation Derivation models electron transfer from low-ionization-energy metals to high-affinity non-metals, forming electrostatically bound ions. The RS mechanism emphasizes 8-tick shell closure: alkali metals donate to reach noble-gas configuration while halogens accept to complete their valence shell. Lattice energy and Madelung constants then stabilize the structure, with optimal radii ratios tied to phi-derived values. The threshold is calibrated to the small fractional range of the enProxy function (approximately 0.01-0.17) so that differences such as |0.042 - 0.071| exceed 0.02 while preserving relative ordering.
proof idea
Direct constant definition that assigns the literal value 0.02 to ionicThreshold.
why it matters
The constant is referenced inside the isIonicBond predicate and thereby supports the alkali_halogen_ionic theorem, which asserts that all alkali-halogen pairs satisfy the ionic condition. It operationalizes the 8-tick closure drive described in the module for chemistry. No open scaffolding is closed here; the value remains an empirical anchor within the RS-native units.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.