shell_radius_increases_with_period
plain-language theorem explainer
The theorem proves that the golden ratio raised to natural number exponents is strictly monotonic. Recognition Science models of atomic radii invoke this to establish that shell radii grow with period number. The proof is a brief tactic sequence: it obtains phi greater than one from an upstream bound and then applies the standard real power monotonicity result to the cast natural number inequality.
Claim. Let $phi$ denote the golden ratio. Then $phi^n < phi^m$ holds for all natural numbers $n, m$ with $n < m$.
background
The module derives atomic radii from φ-ladder scaling in Recognition Science. Radii scale as φ to the shell number, with effective radius reduced by valence electrons via screening. The local setting predicts radii increase down a group as new shells form farther out, while decreasing across a period due to increasing Z. This theorem supplies the monotonicity in shell number. It relies on the upstream lemma establishing φ > 1.5, which follows from the quadratic definition of the golden ratio.
proof idea
The tactic proof first invokes the lemma phi_gt_onePointFive to obtain phi > 1.5, then uses linarith to strengthen it to phi > 1. It applies Real.rpow_lt_rpow_of_exponent_lt to this base inequality together with the cast of n < m.
why it matters
The result supports the group trend prediction in the CH-007 atomic radii framework. It rests on the self-similar fixed point property of phi from the forcing chain. No immediate downstream theorems are listed, leaving open its integration into full radius calculations that include screening.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.