cert_inhabited
plain-language theorem explainer
The theorem establishes that a certificate asserting exactly five social strata with the required mobility cost properties is inhabited by exhibiting an explicit witness. Sociologists working within Recognition Science would cite it to ground the structural prediction of five layers forced by configDim D = 5. The proof is a one-line term that supplies the pre-constructed cert as the inhabitant of the Nonempty type.
Claim. There exists a structure certifying that the number of social strata equals five, that mobility transition costs vanish on the diagonal for nonzero strata, that all transition costs are nonnegative when both arguments are positive, and that the one-step mobility cost is strictly positive.
background
The module derives social stratification from the Recognition Science configDim parameter, which equals five and forces the same five-fold division seen in Köppen zones, soil horizons, and Big Five personality factors. The SocialStratificationCert structure packages four properties: stratum_count fixes the total at five; cost_at_stratum requires mobilityTransitionCost(s,s) = 0 for s ≠ 0; cost_nonneg asserts nonnegativity of costs for positive arguments; and mobility_cost_pos requires oneStepMobilityCost > 0. These rest on the J-cost function imported from the Cost module, where upward mobility from working to middle class incurs J(φ²) and downward steps incur J(φ).
proof idea
The proof is a one-line term that directly supplies the witness cert to the Nonempty constructor, confirming the structure is inhabited once the four field properties have been established by prior sibling definitions.
why it matters
This result closes the existence question for the stratification certificate, confirming that the five-stratum model is mathematically consistent inside the Recognition Science framework. It supports the broader claim that configDim D = 5 produces the same layer count across sociology, climate, and biology, aligning with the eight-tick octave and the J-uniqueness fixed point. The module falsifier states that any survey of ten or more societies finding a reliably different modal stratum count would refute the prediction.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.