SocialStratificationCert
plain-language theorem explainer
SocialStratificationCert packages four properties: exactly five social strata, zero cost for identical status pairs, nonnegative transition costs for positive inputs, and strictly positive one-step mobility cost. Sociologists working in the Recognition Science framework cite this structure when formalizing class mobility via J-cost on status ratios. It is a pure structure definition that directly assembles the four sibling definitions with no additional proof steps.
Claim. A structure asserting that the number of social strata equals 5, that the mobility transition cost between any equal nonzero statuses is zero, that the mobility transition cost is nonnegative whenever both achieved and expected statuses are positive, and that the one-step mobility cost is strictly positive.
background
The module derives social stratification from configDim D = 5, the same template that produces five Köppen zones, five sleep stages, and the Big Five personality factors. Mobility transition cost is defined as the J-cost of the ratio of achieved to expected status. One-step mobility cost equals phi minus 3/2, the explicit value of J(phi) for a single rung step on the phi-ladder. The nonnegativity clause reuses the general result that every recognition event carries nonnegative cost.
proof idea
Structure definition that directly records the four properties. Stratum count is taken from the constant definition of five strata. The zero self-transition clause follows from the ratio definition of mobility transition cost. Nonnegativity is imported from the upstream recognition cost theorem. Positivity of one-step cost is immediate from the explicit phi expression.
why it matters
The structure supplies the canonical certificate for the five-stratum prediction and is instantiated by the downstream cert definition, which in turn yields the inhabited instance. It closes the structural claim in the module that five layers are forced by configDim D = 5, consistent with the phi-ladder and eight-tick octave in the forcing chain. The module falsifier remains any cross-cultural survey that finds a modal stratum count reliably different from five.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.