Business-wrong demos
Every structural green in Economoist has a corresponding business-wrong twin: a deliberately corrupted model that violates the property and is refuted at the SMT tier with a decoded counterexample. These twins demonstrate soundness dependence. If the structural assumption is broken, the solver finds a concrete witness.
Purpose
Section titled “Purpose”Business-wrong demos answer the question: "Does the proof actually depend on the stated assumption, or would anything pass?" Each twin removes or corrupts exactly one structural requirement and confirms that the solver returns unsat on the correctness claim (i.e., finds a counterexample to the corrupted property). This is the definitional test of soundness dependence.
Importable twins
Section titled “Importable twins”Each business-wrong model is importable by a stable ID, so you can reference it in CI gates, regression suites, or pedagogical notebooks without path-dependent fragility.
Markov chain twins
Section titled “Markov chain twins”- Rows not summing to one. A transition matrix whose rows sum to 0.9 or 1.1. The solver produces a distribution that leaves the simplex after one step, decoded as a concrete probability vector with a negative entry or entries exceeding one.
Bellman operator twins
Section titled “Bellman operator twins”- Discount outside (0,1). A Bellman operator parameterized with discount factor 1.2 or 0.0. The single-application contraction inequality fails, and the solver returns two value functions whose sup-norm distance does not shrink.
Gordon model twins
Section titled “Gordon model twins”- Growth at or above discount. The Gordon formula is instantiated with growth rate equal to (or exceeding) the discount rate. Positivity fails: the solver produces a counterexample where the denominator is zero or negative, making the present value undefined or negative.
Reading a counterexample
Section titled “Reading a counterexample”When a business-wrong twin is refuted, the prover emits a model (in the SMT-LIB sense): concrete real-valued assignments to every free variable. Economoist decodes this into domain terms. For a Markov twin, you see the input distribution and the output vector that violates the simplex. For a Gordon twin, you see the dividend, growth, and discount values that break positivity. The counterexample is human-readable and machine-parseable.