abundanceCost_at_predicted
plain-language theorem explainer
The theorem states that the J-cost of an abundance ratio is zero exactly when the observed value matches the phi-ladder prediction. Cosmochemists working with stellar spectra would cite it to fix the zero-defect anchor at the iron peak. The proof is a one-line wrapper that unfolds the cost definition, cancels the ratio via the nonzero hypothesis, and invokes the Jcost unit lemma.
Claim. For any nonzero real number $a$, the J-cost of the ratio $a/a$ equals zero, where the abundance cost is defined by applying the J-cost function to the ratio of actual to expected abundance.
background
The StellarAbundanceFromPhiLadder module models cosmic elemental abundances via the phi-ladder, reproducing the Oddo-Harkins rule that even-Z nuclei exceed odd-Z neighbors. The abundanceCost definition applies the J-cost to the ratio of observed to predicted abundance, with J expressed as $(x-1)^2/(2x)$. This rests on the upstream lemma that Jcost of unity vanishes, which follows directly from the squared-ratio form of J.
proof idea
The proof is a one-line wrapper. It unfolds abundanceCost to expose Jcost of the ratio, rewrites the ratio to 1 using the nonzero hypothesis on $a$, and applies the lemma Jcost_unit0.
why it matters
This supplies the cost_at_predicted field inside the StellarAbundanceCert definition, which packages the even/odd ratio bounds and the zero-cost condition. It anchors the minimal-defect point on the phi-ladder at the iron-peak rung, consistent with the Recognition Science prediction that binding energies and abundances follow the same self-similar structure. The result closes one structural requirement for the full certification of Lodders-type abundance patterns.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.