IndisputableMonolith.Agronomy.YieldGapFromJCost
This module specializes the J-cost from Recognition Science to the ratio of actual to potential crop yield. It supplies the core definition yieldGapCost together with non-negativity, tip-point bounds, and a certificate type. Agronomists linking RS cost functions to yield-gap modeling would cite these objects. The module is purely definitional with supporting lemmas.
claimDefine the J-cost on the actual-to-potential yield ratio by $J(y_a/y_p)$ where $J(x)=(x+x^{-1})/2-1$, together with the functions yieldGapCost, agronomicTipPoint, and the certificate YieldGapCert.
background
Recognition Science obtains all constants from the J-function obeying the Recognition Composition Law J(xy)+J(x/y)=2J(x)J(y)+2J(x)+2J(y). The upstream Constants module fixes the RS time quantum τ₀=1 tick. The Cost module supplies the general J-cost. This agronomy module applies that cost to the dimensionless ratio of realized yield to potential yield.
proof idea
This is a definition module, no proofs.
why it matters in Recognition Science
The module supplies the first explicit agronomic object in the Recognition Science mirror, placing J-cost on yield ratios. It prepares the ground for later theorems that would connect the phi-ladder and eight-tick octave to agricultural observables, although no downstream theorems are yet recorded.
scope and limits
- Does not compute numerical crop yields from field data.
- Does not derive the J-function itself.
- Does not incorporate environmental variables beyond the yield ratio.
- Does not prove optimality of the chosen cost function.