laborMarketTheoryCount
plain-language theorem explainer
The theorem proves that the inductive enumeration of canonical labor market theories contains exactly five elements. Labor economists applying Recognition Science would cite this result to fix the finite taxonomy in their models. The proof is a direct decision computation on the Fintype instance derived from the five-constructor inductive definition.
Claim. The collection consisting of human capital theory, search friction theory, efficiency wage theory, insider-outsider theory, and implicit contract theory has cardinality five: $|S| = 5$.
background
Recognition Science treats labor markets via the J-cost function that quantifies recognition mismatch. Equilibrium is defined by J = 0, as stated in the upstream equilibrium theorem from nonlinear dynamics. The module enumerates five standard labor market theories as an inductive type whose constructors are human capital, search friction, efficiency wages, insider-outsider, and implicit contracts. This count is identified with configuration dimension D = 5.
proof idea
The proof is a one-line wrapper that invokes the decide tactic on Fintype.card. The tactic succeeds because the inductive type derives DecidableEq, Repr, BEq, and Fintype instances from its five constructors.
why it matters
This theorem supplies the five_theories field inside the laborEconomicsCert definition that certifies the full RS-to-labor-economics mapping. It realizes the module claim that five theories equal configDim D = 5 and connects to the J = 0 equilibrium condition. No open scaffolding questions are indicated in the downstream results.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.