cert
plain-language theorem explainer
The definition cert constructs a concrete instance of the YieldGapCert structure that packages the four properties required for the J-cost model of agricultural yield gaps. An agronomist applying Recognition Science to crop data would cite it to confirm that the normalized yield ratio satisfies nonnegativity and the tipping-point bounds. The construction is a direct record instantiation that simply names four lemmas already established in the same module.
Claim. Let $cert$ be the structure of type $YieldGapCert$ whose fields are supplied by the theorems $yieldGapCost_at_potential$, $yieldGapCost_nonneg$, $agronomicTipPoint_pos$ and $agronomicTipPoint_lt_one$.
background
The module treats the yield gap as the difference between potential yield $Y_p$ and actual yield $Y_a$, with the normalized ratio $Y_a/Y_p$ assigned a J-cost reading. The structure $YieldGapCert$ collects the four properties needed for this cost function to be a valid model: it vanishes when actual yield equals potential yield, remains nonnegative for positive arguments, and the agronomic tipping point (equal to $φ^{-1}$) lies strictly between 0 and 1. These rest on the nonnegativity of J-cost for positive ratios together with the elementary inequalities $0 < φ^{-1} < 1$.
proof idea
The definition is a direct record construction that supplies the four required fields by naming the already-proved theorems yieldGapCost_at_potential, yieldGapCost_nonneg, agronomicTipPoint_pos and agronomicTipPoint_lt_one.
why it matters
This certificate closes the structural theorem for the yield-gap model in the agronomy module. It supplies the concrete object that would be invoked by any downstream application of the J-cost framework to GYGA-style yield data. The construction thereby makes the falsifier stated in the module doc-comment (a yield-gap ratio outside (0.4,0.9)) directly testable against the Recognition Science prediction.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.