yieldGapCost
plain-language theorem explainer
The definition maps any pair of actual and potential yields to the J-cost of their ratio. Agronomists working with Recognition Science predictions for yield gaps cite it when establishing nonnegativity and the location of the agronomic tipping point. It is realized as a direct one-line wrapper around the J-cost function applied to the normalized ratio.
Claim. Let $Y_a$ and $Y_p$ be actual and potential yields. The yield gap cost is defined by $J(Y_a / Y_p)$, where $J$ is the J-cost function satisfying $J(1)=0$ and $J(x)≥0$ for $x>0$.
background
The module treats the yield gap as the difference between potential yield $Y_p$ and actual farmer yield $Y_a$, with Recognition Science predicting that the normalized ratio $Y_a/Y_p$ carries a J-cost reading. The J-cost function is imported from the Cost module and obeys the Recognition Composition Law together with the fixed-point properties that force the self-similar ratio $φ^{-1}$. The agronomic tipping point is stated to occur where the derivative of J-cost equals the derivative of input cost, at ratio $φ^{-1}≈0.618$.
proof idea
This is a one-line definition that applies the Jcost function directly to the ratio of the two input yields.
why it matters
The definition supplies the cost function required by the YieldGapCert structure, which asserts that the cost vanishes when yields are equal, remains nonnegative, and that the tipping point lies strictly between zero and one. It realizes the RS prediction that normalized yield gaps are measured by J-cost, connecting to the phi-ladder and the eight-tick octave. The module falsifier is any large-N multi-country analysis (GYGA database) showing typical ratios outside (0.4, 0.9).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.