IndisputableMonolith.Economics.CounterCyclicalPolicyFromJCost

   1import Mathlib
   2import IndisputableMonolith.Common.CanonicalJBand
   3
   4/-!
   5# E6: Counter-Cyclical Policy from J-Cost on Output-Gap Ratio
   6
   7Compounds with `Economics/BusinessCyclePeriodFromGap45` (Juglar 13 yr,
   8Kondratieff 45 yr). Per-period J-cost on
   9`r := observed_output_gap / target_gap`. Counter-cyclical policy minimises
  10J-cost subject to per-tick σ-conservation constraints; the canonical
  11band gates the "stabilising vs destabilising" boundary on policy
  12intervention magnitude.
  13
  14Lean status: 0 sorry, 0 axiom.
  15-/
  16
  17namespace IndisputableMonolith
  18namespace Economics
  19namespace CounterCyclicalPolicyFromJCost
  20
  21open Common.CanonicalJBand
  22
  23structure CounterCyclicalCert where
  24  base : CanonicalCert
  25
  26def counterCyclicalCert : CounterCyclicalCert where
  27  base := cert
  28
  29end CounterCyclicalPolicyFromJCost
  30end Economics
  31end IndisputableMonolith
  32