LaborEconomicsCert
plain-language theorem explainer
LaborEconomicsCert packages the Recognition Science account of labor economics by requiring exactly five canonical market theories, equilibrium at J-cost zero, and strictly positive J-cost for all other positive relative wages. Economists using recognition-based models cite it to ground labor analysis in the J-functional. The structure is a definition whose fields are populated downstream by a one-line construction that assembles the inductive count, the equilibrium lemma, and the friction predicate.
Claim. The structure asserts that the set of labor market theories has cardinality five, that the J-cost function satisfies $Jcost(1)=0$, and that $Jcost(r)>0$ for every positive real $r$ with $r≠1$.
background
The module enumerates five canonical labor market theories as the inductive type with constructors humanCapital, searchFriction, efficiencyWages, insiderOutsider, and implicitContracts. This enumeration is required to have cardinality five, matching the configuration dimension D=5 stated in the module header. Labor equilibrium is identified with J=0 (wage equals marginal recognition cost) while frictions are identified with J>0 (recognition mismatch).
proof idea
The declaration is a structure definition containing no proof body. Its three fields are instantiated by the downstream definition laborEconomicsCert, which supplies laborMarketTheoryCount for the cardinality, labor_equilibrium for the J-cost identity, and market_friction for the positivity predicate. These rely on the Fintype instance derived for the inductive type and the upstream equilibrium theorem.
why it matters
LaborEconomicsCert supplies the certified interface that realizes the module claim of five theories equaling configDim D=5 and links J-cost properties directly to labor equilibrium and friction. It feeds the parent definition laborEconomicsCert and anchors the economic application of the J-functional imported from the Cost module. No open questions are flagged in the supplied material.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.