oneStepMobilityCost_eq_Jph
plain-language theorem explainer
This theorem equates the one-step upward mobility cost in the social stratification model to the J-cost evaluated at the golden ratio phi. Researchers modeling social mobility within the Recognition Science framework would cite it to anchor stratum transition costs in the phi-ladder. The proof is a direct one-line wrapper that invokes the symmetry of the Jcost_phi_val lemma.
Claim. The one-step mobility cost equals the recognition cost function $J$ evaluated at the golden ratio: oneStepMobilityCost = $J$($phi$), where $J(x) = (x + x^{-1})/2 - 1$.
background
The module derives five canonical social strata from configDim D = 5, matching patterns in Köppen zones and Big Five factors. One-step mobility cost is defined as the base transition cost between adjacent rungs on the phi-ladder, set explicitly to phi - 3/2. The upstream lemma Jcost_phi_val establishes J(phi) = phi - 3/2 exactly via the identity phi^2 = phi + 1 and algebraic reduction in the Cost module.
proof idea
The proof is a one-line wrapper that applies the symmetry of the Jcost_phi_val lemma to the definition of oneStepMobilityCost.
why it matters
This equality embeds the sociological mobility cost directly into the core J-cost of Recognition Science, supporting downstream certification of the five-stratum structure. It fills the T5 J-uniqueness step and the phi-ladder construction in the forcing chain, with the module doc-comment noting the falsifier as any survey on ten or more societies showing a modal stratum count other than five.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.