mobilityTransitionCost_nonneg
plain-language theorem explainer
The theorem establishes non-negativity of the mobility transition cost for positive real parameters a and e. Sociologists applying Recognition Science to stratification models cite it to confirm that stratum transitions incur no negative costs in the five-layer structure. The proof is a one-line term wrapper that unfolds the definition and invokes the J-cost non-negativity lemma on the positive ratio a/e.
Claim. For positive reals $a > 0$ and $e > 0$, the mobility transition cost satisfies $0 ≤ J(a/e)$, where $J$ is the J-cost function.
background
The module derives five social strata from configDim D = 5, matching the template for Köppen zones and other five-phase systems. Mobility transition cost is the J-cost of the ratio a/e, representing the expense of moving between adjacent strata; upward moves from working to middle class carry cost J(φ²) ≈ 0.38. The upstream lemma Jcost_nonneg states that J(x) ≥ 0 for positive x by the AM-GM inequality, with the explicit form J(x) = (x - 1)² / (2x).
proof idea
The proof is a one-line term-mode wrapper. It unfolds mobilityTransitionCost to expose Jcost (a / e), then applies Jcost_nonneg to the positive quantity a/e supplied by div_pos ha he.
why it matters
The result supplies the cost_nonneg field inside SocialStratificationCert, completing the structural theorem for five strata with non-negative J-cost transitions. It aligns with the Recognition forcing chain (T5 J-uniqueness, T6 phi fixed point) and the multiplicative recognizer cost definition. No open scaffolding remains for this non-negativity step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.