laborEconomicsCert
plain-language theorem explainer
This definition assembles a concrete LaborEconomicsCert instance that equates five canonical labor market theories to a configuration dimension of five in Recognition Science, with equilibrium at J-cost zero and positive friction for mismatched rates. Economists embedding labor models in the J-cost formalism would cite it to anchor the five-theory count to the RS dimension structure. The construction is a direct record build that pulls in the prior theorems for theory cardinality, equilibrium, and friction.
Claim. The labor economics certificate is the structure asserting that the set of labor market theories has cardinality five, that the J-cost function satisfies $J(1)=0$, and that $J(r)>0$ for every positive real $r$ distinct from one.
background
In Recognition Science the J-cost function quantifies recognition mismatch, with equilibrium defined by vanishing cost at unit rate and friction by strictly positive cost elsewhere. The LaborEconomicsCert structure packages three properties: the cardinality of LaborMarketTheory equals five, the equilibrium condition Jcost 1 = 0, and the friction condition that Jcost r > 0 whenever r > 0 and r ≠ 1. The module documentation states that these five theories correspond to configDim D = 5 and that labor equilibrium is J = 0 while frictions arise from J > 0.
proof idea
The definition is a direct record construction that sets the five_theories field to laborMarketTheoryCount, the equilibrium field to labor_equilibrium, and the friction field to market_friction. Each field is supplied by an upstream theorem already proved in the same module or its imports.
why it matters
This definition supplies the concrete instance of LaborEconomicsCert that certifies the labor economics sector of Recognition Science, realizing the module claim that five theories equal configDim D = 5. It closes the zero-sorry scaffolding for applying the J-cost formalism to labor markets and connects to the equilibrium theorem from NonlinearDynamicsFromRS. No downstream uses are recorded yet.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.