agronomicTipPoint
plain-language theorem explainer
Agronomists working in the Recognition Science framework cite the agronomic tipping point as the normalized yield ratio Ya/Yp at which marginal J-cost equals marginal input cost and further intensification yields no net gain. The value is fixed at the reciprocal of the golden ratio φ. This constant anchors the certification of yield-gap models. The definition is a direct binding to φ^{-1} from the constants layer.
Claim. The agronomic tipping point is defined as the value $Y_a/Y_p = φ^{-1}$, where $φ$ is the golden ratio satisfying $φ = 1 + φ^{-1}$.
background
The module treats the yield gap as the difference between potential yield Yp and actual farmer yield Ya, with the normalized ratio Ya/Yp interpreted via the J-cost function. J-cost measures the recognition penalty attached to scaling deviations and obeys the composition law J(xy) + J(x/y) = 2J(x)J(y) + 2J(x) + 2J(y). The local theoretical setting is a structural theorem with zero axioms or sorrys that locates the tipping point, where the derivative of J-cost matches the derivative of input cost, at Ya/Yp = φ^{-1}.
proof idea
The definition is a direct assignment of the reciprocal of φ, where φ is the positive root of x² - x - 1 = 0 supplied by the Constants module.
why it matters
This definition supplies the constant required by the YieldGapCert structure, which asserts nonnegativity of yieldGapCost together with the strict bounds 0 < agronomicTipPoint < 1. It instantiates the T6 self-similar fixed-point step of the forcing chain inside the agronomy domain and supports the module falsifier that any large-N GYGA-style analysis placing the typical ratio outside (0.4, 0.9) would refute the prediction.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.