oneStepMobilityCost_pos
plain-language theorem explainer
oneStepMobilityCost_pos establishes that the one-step upward mobility cost is strictly positive. Sociologists modeling class transitions via the Recognition Science template would cite it to guarantee positive J-cost for adjacent-stratum moves. The proof is a one-line wrapper that unfolds the definition and applies linear arithmetic with the bound phi greater than 1.61.
Claim. $0 < J(φ)$ where $J(φ) = φ - 3/2$ is the one-step upward mobility cost between adjacent social strata in the five-layer model.
background
The module treats social stratification as five layers forced by configDim D = 5, the same template that produces five Köppen zones, sleep stages, and Big Five factors. The one-step mobility cost is the J-cost for moving from stratum k to k+1, defined explicitly as phi minus 3/2 (approximately 0.118). This sits inside a structural theorem with zero axioms or sorrys.
proof idea
The proof is a one-line wrapper: unfold oneStepMobilityCost to its definition phi - 3/2, then apply the linarith tactic citing the upstream lemma phi_gt_onePointSixOne.
why it matters
The result supplies the mobility_cost_pos field inside the cert construction of SocialStratificationCert. It confirms the positivity requirement for J-cost transitions, consistent with J-uniqueness (T5) and the phi fixed point (T6) in the forcing chain. No open scaffolding remains at this step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.