IndisputableMonolith.Agronomy.YieldGapFromJCost

   1import Mathlib
   2import IndisputableMonolith.Constants
   3import IndisputableMonolith.Cost
   4
   5/-!
   6# Agricultural Yield Gap from J-Cost (Plan v7 fifty-second pass)
   7
   8## Status: STRUCTURAL THEOREM (0 sorry, 0 axiom).
   9
  10The yield gap is the difference between potential yield (Yp)
  11and actual farmer yield (Ya). RS prediction: the normalized yield gap
  12ratio Ya/Yp has a J-cost reading.
  13
  14The "agronomic tipping point" where intensification stops producing
  15gains is at Ya/Yp = φ⁻¹ ≈ 0.618, where the derivative of J-cost
  16equals the derivative of input cost.
  17
  18## Falsifier
  19
  20Any large-N multi-country yield gap analysis (GYGA database)
  21showing the typical yield-gap ratio outside (0.4, 0.9).
  22-/
  23
  24namespace IndisputableMonolith
  25namespace Agronomy
  26namespace YieldGapFromJCost
  27
  28open Constants
  29open Cost
  30
  31noncomputable section
  32
  33/-- J-cost on the actual-to-potential yield ratio. -/
  34def yieldGapCost (actual_yield potential_yield : ℝ) : ℝ :=
  35  Jcost (actual_yield / potential_yield)
  36
  37theorem yieldGapCost_at_potential (y : ℝ) (h : y ≠ 0) :
  38    yieldGapCost y y = 0 := by
  39  unfold yieldGapCost; rw [div_self h]; exact Jcost_unit0
  40
  41theorem yieldGapCost_nonneg (a p : ℝ) (ha : 0 < a) (hp : 0 < p) :
  42    0 ≤ yieldGapCost a p := by
  43  unfold yieldGapCost; exact Jcost_nonneg (div_pos ha hp)
  44
  45/-- Agronomic tipping point: Ya/Yp = 1/φ. -/
  46def agronomicTipPoint : ℝ := phi⁻¹
  47
  48theorem agronomicTipPoint_pos : 0 < agronomicTipPoint :=
  49  inv_pos.mpr phi_pos
  50
  51theorem agronomicTipPoint_lt_one : agronomicTipPoint < 1 :=
  52  inv_lt_one_of_one_lt₀ one_lt_phi
  53
  54structure YieldGapCert where
  55  cost_at_potential : ∀ y : ℝ, y ≠ 0 → yieldGapCost y y = 0
  56  cost_nonneg : ∀ a p : ℝ, 0 < a → 0 < p → 0 ≤ yieldGapCost a p
  57  tip_pos : 0 < agronomicTipPoint
  58  tip_lt_one : agronomicTipPoint < 1
  59
  60noncomputable def cert : YieldGapCert where
  61  cost_at_potential := yieldGapCost_at_potential
  62  cost_nonneg := yieldGapCost_nonneg
  63  tip_pos := agronomicTipPoint_pos
  64  tip_lt_one := agronomicTipPoint_lt_one
  65
  66theorem cert_inhabited : Nonempty YieldGapCert := ⟨cert⟩
  67
  68end
  69end YieldGapFromJCost
  70end Agronomy
  71end IndisputableMonolith
  72