helium_is_noble
plain-language theorem explainer
Helium with atomic number 2 satisfies the noble gas predicate under the eight-window neutrality definition. Chemists using the Recognition Science periodic table scaffold would cite this as the base case confirming the first shell closure. The verification reduces to a direct decidable membership test in the fixed noble gas list.
Claim. The atomic number $Z=2$ belongs to the noble gas closure set, i.e., $2$ is a point where cumulative valence cost returns to 8-window neutrality.
background
The module implements a fit-free periodic table engine that maps the eight-tick octave to chemical shell structure via phi-tier rails and fixed block offsets. Noble gases are defined exactly as those Z where the running valence imbalance sum achieves 8-window neutrality, isomorphic to the ledger balance condition. The predicate isNobleGas(Z) holds when Z lies in the set nobleGasZ, which the module documentation states is forced to be {2, 10, 18, 36, 54, 86} by the neutrality requirement.
proof idea
The proof is a one-line wrapper that applies native_decide to the membership statement 2 ∈ nobleGasZ.
why it matters
This supplies the base case for the Noble Gas Closure Theorem (P0-A0) stated in the module documentation. It directly instantiates the eight-tick neutrality condition (T7) at the chemical level and confirms the first element of the predicted closure set without parameter fitting. No downstream uses are recorded yet.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.