labor_equilibrium
plain-language theorem explainer
The theorem establishes that the recognition cost vanishes at unit scale, Jcost(1) = 0, which corresponds to labor market equilibrium where wage equals marginal recognition cost. Labor economists working within the Recognition Science framework would cite this as the base case for frictionless markets. The proof is a direct one-line application of the unit property of the J-cost function.
Claim. The labor market equilibrium condition holds as $J(1) = 0$, where the recognition cost is given by $J(x) = (x-1)^2 / (2x)$.
background
The Labor Economics from RS module interprets five canonical labor market theories as configurations in a five-dimensional space. Equilibrium is identified with vanishing recognition cost J = 0, while frictions correspond to positive J values indicating mismatch. This rests on the J-cost definition from the Cost module, where the upstream result states: J(x) expressed as a squared ratio: J(x) = (x-1)²/(2x).
proof idea
This is a one-line wrapper that directly invokes the Jcost_unit0 lemma from the Cost module, which itself simplifies the definition of Jcost at argument 1.
why it matters
It supplies the equilibrium component for the laborEconomicsCert certificate, which bundles it with the count of five theories and the friction condition. This anchors the labor economics application to the core Recognition Science result that J vanishes at equilibrium, consistent with the J-uniqueness property. The downstream definition sets equilibrium := labor_equilibrium to certify the mapping.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.