cert_inhabited
plain-language theorem explainer
The theorem establishes that the YieldGapCert structure is inhabited by exhibiting the explicit term cert. Agronomists modeling normalized yield gaps under Recognition Science would cite this to confirm a consistent J-cost certificate exists satisfying the required properties. The proof is a one-line term that directly constructs the Nonempty instance from the prior definition of cert.
Claim. The structure $YieldGapCert$ is inhabited, where $YieldGapCert$ asserts that the yield-gap cost vanishes when actual yield equals potential yield, remains non-negative for positive yields, and the agronomic tipping point satisfies $0 < agronomicTipPoint < 1$.
background
The module models the agricultural yield gap as the difference between potential yield $Y_p$ and actual farmer yield $Y_a$, with the normalized ratio $Y_a/Y_p$ governed by the J-cost function from Recognition Science. The agronomic tipping point occurs where intensification ceases to produce gains, located at $Y_a/Y_p = φ^{-1} ≈ 0.618$ where the derivative of J-cost equals that of input cost. YieldGapCert is the structure requiring four properties: cost vanishes at equality, stays non-negative, and the tipping point is positive and less than one. This result depends only on the definition of YieldGapCert and the explicit inhabitant cert.
proof idea
The proof is a one-line term that applies the Nonempty constructor directly to the term cert, which is the explicit inhabitant of the YieldGapCert structure defined earlier in the module.
why it matters
This theorem confirms existence of a certificate for the yield-gap model, allowing the framework to proceed with J-cost predictions for the normalized yield ratio. It supports the agronomic tipping point at $φ^{-1}$ as required by the Recognition Science forcing chain (T5 J-uniqueness and T6 phi fixed point). No downstream uses are recorded, but it closes the structural theorem for the yield gap in the agronomy module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.