yieldGapCost_at_potential
plain-language theorem explainer
The theorem establishes that J-cost vanishes for the normalized yield ratio when actual yield equals potential yield, provided the common value is nonzero. Agronomists and RS modelers would cite it to anchor the zero-gap baseline in yield-gap analyses. The proof is a one-line wrapper that unfolds the definition, simplifies the ratio via division, and applies the unit lemma for J-cost.
Claim. Let $y$ be a nonzero real number. Then the J-cost of the ratio of actual yield to potential yield equals zero: $J(y/y)=0$.
background
The module treats the agricultural yield gap as the difference between potential yield Yp and actual farmer yield Ya, assigning the normalized ratio Ya/Yp a J-cost value under Recognition Science. The definition yieldGapCost(actual, potential) is obtained by feeding the ratio actual/potential into the J-cost operator. Upstream, Jcost_unit0 states that Jcost(1)=0, which supplies the mathematical content of the no-gap case and is invoked directly here. The module doc frames this as a structural theorem whose falsifier is any large-N multi-country analysis placing the typical yield-gap ratio outside (0.4,0.9).
proof idea
The proof is a one-line wrapper. It unfolds yieldGapCost to expose Jcost(y/y), rewrites the division to 1 using div_self under the nonzero hypothesis, and concludes by exact application of the lemma Jcost_unit0.
why it matters
This result supplies the cost_at_potential field inside the YieldGapCert structure that collects all certified properties for the agronomic model. It confirms the zero baseline required by the module's structural theorem and aligns with the Recognition Science prediction that J-cost measures deviation from the self-similar fixed point (unity ratio). The parent cert definition uses this together with nonnegativity and the tipping-point bounds at phi^{-1} to close the agronomy fragment.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.