cert
plain-language theorem explainer
Packages three elementary facts about the firm-domain cost into a single certificate: cost vanishes on the diagonal, is nonnegative for positive mass and effort, and the canonical threshold is positive. Economists or RS auditors citing the structural Gibrat package would reach for this bundle. The body is a pure structure inhabitant that wires three already-proved lemmas.
Claim. There is a certificate recording that $\mathrm{domainCost}(r,r)=0$ for all $r\neq 0$, that $\mathrm{domainCost}(m,e)\ge 0$ whenever $m>0$ and $e>0$, and that the canonical threshold is strictly positive.
background
The module develops RS Economics as a structural theorem (zero sorry, zero axiom). The motivating claim is Gibrat's law: firm growth rate independent of size. In RS units the recognition-optimal trajectory has growth rate $J(\varphi)$ times revenue growth, numerically about 11.8% per year.
domainCost is the cost functional on the firm domain (mass/effort pair), built from the same $J$-cost that appears in the forcing chain ($J(x)=(x+x^{-1})/2-1$). The structure FirmGrowth4Cert is the minimal interface that later growth lemmas need: diagonal vanishing, nonnegativity, and a positive threshold. Upstream, cost_nonneg in ObserverForcing already records that every recognition event has nonnegative cost via Jcost_nonneg.
proof idea
One-line structure inhabitant. The three fields are filled by the sibling lemmas domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos respectively; no further tactic work.
why it matters
Gives a named, reusable certificate for the four-ingredient firm-growth interface in Foundation.Economics. Downstream consumers (none listed yet in the graph) can assume the three cost/threshold facts by projecting from this single term rather than re-proving them. It sits under the module's structural Gibrat package and inherits the RS cost calculus ($J$-uniqueness from T5, $\varphi$ from T6) without adding new physics content. Closes the definitional side of the economics session so later growth-rate identities can cite a single inhabited certificate.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.