FirmGrowth4Cert
plain-language theorem explainer
Certificate structure packaging three analytic conditions for the RS firm-growth model: domain cost vanishes on the diagonal, is nonnegative for positive arguments, and the canonical threshold is strictly positive. Cited by anyone invoking the Gibrat-law RS trajectory (~11.8%/yr). As a structure it has no proof body; inhabitants are assembled by sibling definitions.
Claim. A firm-growth certificate is a triple of properties: (i) for every nonzero real $r$, the domain cost of the pair $(r,r)$ equals zero; (ii) for all positive reals $m,e$, the domain cost of $(m,e)$ is nonnegative; (iii) the canonical threshold is strictly positive.
background
The module develops Recognition Science economics. Its headline is a specialization of Gibrat's law (firm growth rate independent of size) to an RS-optimal trajectory whose growth rate is $J(\varphi)$ times revenue growth, numerically about 11.8% per year.
Domain cost is the two-argument cost used to score mismatches between paired real quantities (market vs equity, or measure vs expectation). It sits on top of the J-cost geometry of recognition events. Upstream, ObserverForcing records that "the cost of any recognition event is non-negative," discharged by Cost.Jcost_nonneg on a positive state.
The canonical threshold is the positive cutoff marking the recognition-optimal growth band against which firm trajectories are scored.
proof idea
Pure structure definition: three Prop-valued fields and no proof body. Any inhabitant must supply diagonal vanishing of domain cost, nonnegativity of domain cost on the positive quadrant, and positivity of the canonical threshold. Concrete discharge is deferred to the sibling cert, which fills the fields with domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos.
why it matters
This certificate is the interface type for the RS economics session. Downstream, cert assembles a concrete inhabitant from the three sibling lemmas, and cert_inhabited records Nonempty FirmGrowth4Cert, closing the module's structural claim (0 sorry, 0 axiom).
It anchors the Gibrat specialization in the J-cost geometry forced by T5 (J-uniqueness) and the golden-ratio fixed point T6, so the ~11.8% recognition-optimal growth rate has a certified analytic substrate rather than an ad-hoc constant. Without the bundle, later economics lemmas would restate the same three obligations inline.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.