fr_valence_one
plain-language theorem explainer
The declaration establishes that francium (atomic number 87) has exactly one valence electron under the Recognition Science definition of valence as the excess over the prior noble gas closure. Modelers of atomic radii via φ-ladder scaling would cite this result when locating francium at the start of its period in radius proxy calculations. The proof reduces to a single native_decide tactic that evaluates the subtraction in the valenceElectrons definition.
Claim. For atomic number $Z=87$, the number of electrons beyond the previous noble gas core equals 1.
background
The module derives atomic radii from φ-ladder scaling, with radii decreasing across periods from rising nuclear charge and increasing down groups from new shells. Valence electrons are defined as $Z$ minus the atomic number of the previous noble gas closure, with noble gases occurring precisely when this difference equals the period length. The upstream definition of valenceElectrons supplies the subtraction used here, while the period function from astrophysics supplies the underlying φ^k scaling for shell structure.
proof idea
The proof is a one-line wrapper that applies the native_decide tactic to evaluate valenceElectrons 87 directly from its definition as subtraction from the prior closure.
why it matters
This supplies the valence count for francium in the alkali metal series that feeds radius proxy calculations in the atomic radii module. It instantiates the group trend from the module documentation that alkali metals exhibit maxima after noble gas closures. Within the Recognition Science framework it contributes to chemistry predictions derived from the eight-tick octave and φ-ladder scaling.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.