market_friction
plain-language theorem explainer
The market friction theorem asserts that the J-cost is strictly positive for any positive real ratio r different from 1. Labor economists working inside the Recognition Science framework cite the result when quantifying wage mismatches that prevent equilibrium. The proof is a direct one-line application of the J-cost positivity lemma already established in the Cost module.
Claim. For every real number $r > 0$ with $r ≠ 1$, the J-cost satisfies $J(r) > 0$.
background
In the Recognition Science treatment of labor economics the J-cost quantifies recognition mismatch between a wage offer and marginal recognition cost. Labor equilibrium holds exactly when this cost is zero; any deviation produces positive friction. The module states that the five canonical labor-market theories correspond to configDim D = 5 and that frictions are captured by J > 0.
proof idea
The proof is a one-line wrapper that applies the lemma Jcost_pos_of_ne_one (from IndisputableMonolith.Cost and its siblings) to the supplied hypotheses 0 < r and r ≠ 1.
why it matters
The theorem supplies the friction field required by the downstream laborEconomicsCert definition, which packages the five labor-market theories together with equilibrium and friction statements. It directly realizes the module claim that market frictions correspond to positive J-cost and thereby connects to the J-uniqueness property in the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.