YieldGapCert
plain-language theorem explainer
YieldGapCert packages the zero-cost property at matched yields, non-negativity of the J-cost on yield ratios, and the bounds on the agronomic tipping point at phi inverse. Researchers applying the Recognition Science cost model to crop yield gaps would reference this structure to certify consistency of the normalized gap ratio. The declaration is a plain structure definition that assembles four sibling lemmas without additional proof steps.
Claim. Let $J$ denote the J-cost function. A structure $C$ satisfies $C$.cost_at_potential if $J(y/y)=0$ for all nonzero real $y$; $C$.cost_nonneg if $J(a/p)geq0$ whenever $a>0$ and $p>0$; $C$.tip_pos if $0<phi^{-1}$; and $C$.tip_lt_one if $phi^{-1}<1$, where $phi$ is the golden ratio.
background
The module models agricultural yield gaps through the J-cost applied to the ratio of actual yield to potential yield. Specifically, yieldGapCost(actual, potential) equals Jcost(actual/potential), and agronomicTipPoint is defined as the reciprocal of phi. This local setting draws on the non-negativity of recognition costs established in the ObserverForcing module, which states that the cost of any recognition event is non-negative.
proof idea
The declaration is a structure definition. It directly incorporates the lemma yieldGapCost_at_potential to witness the zero cost at potential, yieldGapCost_nonneg which applies the upstream cost_nonneg theorem, and the two lemmas agronomicTipPoint_pos and agronomicTipPoint_lt_one for the tipping point bounds.
why it matters
YieldGapCert supplies the type for the cert instance that populates the fields from the sibling lemmas, confirming the model is inhabited. It bridges the foundational J-cost properties to agronomy by encoding the tipping point at phi inverse, aligning with the self-similar fixed point in the forcing chain. The module's falsifier is any empirical yield gap ratio falling outside the interval (0.4, 0.9).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.