evenOddAbundanceRatio_in_range
plain-language theorem explainer
The even-odd abundance ratio near the iron peak lies between 1.5 and 3.0. Cosmochemists modeling stellar spectra would cite this to anchor the phi-ladder prediction for the Oddo-Harkins rule. The proof unfolds the definition to phi and applies the established bounds on phi through linarith and nlinarith.
Claim. $1.5 < r < 3.0$ where $r$ is the even/odd abundance ratio for adjacent elements near the iron peak, given by the golden ratio on the nuclear ladder.
background
The module derives stellar elemental abundances from the phi-ladder. It records that cosmic abundances exhibit even-Z elements more abundant than odd-Z, matching the Oddo-Harkins rule. Recognition Science predicts the even/odd ratio for Z and Z+1 scales near phi because of J-cost structure on the multiplicative recognizer for binding energies at the iron peak (rung 26).
proof idea
Constructor splits the conjunction. The lower bound unfolds the definition to phi and applies linarith with phi_gt_onePointSixOne. The upper bound unfolds, introduces phi^2 < 2.7 from phi_squared_bounds, then applies nlinarith with one_lt_phi and phi_pos.
why it matters
This supplies the ratio_in_range field inside StellarAbundanceCert, which packages the bounds and cost properties for the abundance prediction. It completes the structural theorem of the cosmochemistry module and supplies the falsifiable interval (1.5, 3.0) for iron-peak elements. The result instantiates the phi-ladder mass formula at nuclear scales and links to the J-cost on recognition events.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.