cert_inhabited
plain-language theorem explainer
cert_inhabited establishes nonemptiness of MarketEquilibriumCert by direct construction. Economists modeling price deviations via the Recognition Science J-function cite it to confirm existence of equilibrium points obeying nonnegativity and threshold conditions. The proof is a term-mode instantiation that supplies the explicit cert witness.
Claim. The type of market equilibrium certificates is nonempty. A certificate requires that the price deviation function satisfies $δ(p,p)=0$ for all nonzero $p$, $δ(p,e)≥0$ for positive $p,e$, and that the significance threshold $τ>1$.
background
The Market Equilibrium from J-Cost module treats equilibrium as the price at which supply equals demand. Any departure from this point incurs a J-cost: overshooting costs J(p/p*) while undershooting costs the symmetric J(p*/p) by the Recognition Composition Law. The module predicts that the smallest noticeable deviation corresponds to J(φ)≈0.118, or a roughly 62% shift from equilibrium price.
proof idea
The proof is a one-line term proof that directly constructs an element of MarketEquilibriumCert by supplying the cert definition.
why it matters
This theorem closes the MarketEquilibriumFromJCost module by confirming existence of the required certificate, supporting the module's claim of structural theorem status with zero axioms. It aligns with the Recognition Science φ-ladder prediction for significant price departures and touches the module falsifier on commodity-market reversion times matching the 1-rung φ-ladder scale. No downstream uses are recorded.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.