LaborMarketTheory
plain-language theorem explainer
LaborMarketTheory enumerates five canonical labor market theories as an inductive type equipped with a Fintype instance. Economists embedding labor models inside Recognition Science cite it to fix the configuration dimension at D = 5. The declaration is a direct inductive definition whose deriving clause supplies the finite-type structure needed for immediate cardinality computation.
Claim. Let $T$ be the inductive type whose constructors are human capital, search friction, efficiency wages, insider-outsider models, and implicit contracts. Then $T$ carries instances of decidable equality, representation, Boolean equality, and finite type.
background
Recognition Science treats labor equilibrium as the condition Jcost 1 = 0, where the J-cost function measures recognition mismatch between wage and marginal cost. Frictions appear whenever the rate parameter r satisfies 0 < r and r ≠ 1, forcing Jcost r > 0. The present module imports the Jcost definition from Cost and uses Mathlib finite-type machinery to encode the five standard labor theories as the configuration dimension D = 5.
proof idea
The declaration is an inductive type definition that introduces the five constructors and derives DecidableEq, Repr, BEq, and Fintype in a single deriving clause.
why it matters
LaborMarketTheory supplies the finite set required by the downstream LaborEconomicsCert structure, which asserts Fintype.card T = 5 together with the equilibrium Jcost 1 = 0 and the friction inequality. It realizes the module statement that five theories correspond to configDim D = 5, anchoring labor economics inside the Recognition Science forcing chain at the point where recognition costs govern equilibria.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.