CounterCyclicalCert
plain-language theorem explainer
CounterCyclicalCert packages a CanonicalCert to certify policies that minimise J-cost on the observed-to-target output-gap ratio while respecting the canonical band. Recognition Science economists cite it when deriving stabilisation rules from the J-functional in the E6 setting. The definition is a one-field structure that directly embeds the six-clause CanonicalCert with no added proof obligations.
Claim. A counter-cyclical certificate consists of a base canonical certificate satisfying $J(1)=0$, the reciprocity $J(x)=J(1/x)$ for $x≠0$, $J(ϕ)>0$, the band $0.11<J(ϕ)<0.13$, and $J(1/ϕ^2)>0$.
background
Recognition Science defines the J-functional from the forcing chain as $J(x)=(x+x^{-1})/2-1$, with the canonical band condition $0.11<J(ϕ)<0.13$ fixing the scale for economic ratios. The upstream CanonicalCert supplies the six required properties that any domain certificate must obey, including zero at unity, reciprocity, positivity at ϕ, the band, and recovery positivity at $1/ϕ^2$. The module specialises this to counter-cyclical policy by applying per-period J-cost to the ratio $r$ of observed output gap over target gap, subject to σ-conservation, with the band gating intervention magnitude.
proof idea
The declaration is a structure definition consisting of a single field base that directly reuses CanonicalCert; no tactics or lemmas are applied beyond the structure constructor.
why it matters
It supplies the certificate type instantiated by the downstream counterCyclicalCert to realise the E6 claim on J-cost minimisation for output-gap stabilisation. This step links the J-functional directly to business-cycle policy, consistent with the framework's phi-ladder and eight-tick octave that generate the 13-year Juglar and 45-year Kondratieff periods. No open scaffolding remains in the module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.