cert
The definition assembles a certificate object that bundles the equality of social stratum count to 5 with zero self-transition cost, non-negative mobility costs for positive arguments, and strictly positive one-step mobility cost. Recognition Science researchers or mathematical sociologists would cite it to anchor the five-layer stratification prediction derived from configDim D=5. The construction is a direct record literal that references the stratum count equality and the three cost lemmas.
claimThe certificate cert is the structure whose stratum count field equals 5, whose cost-at-stratum field asserts mobilityTransitionCost(s,s)=0 for all s≠0, whose cost-nonneg field asserts mobilityTransitionCost(a,e)≥0 whenever a>0 and e>0, and whose mobility-cost-pos field asserts oneStepMobilityCost>0.
background
The module derives five canonical social strata (upper, upper-middle, middle, working, lower) from configDim D=5, the same template that forces five Köppen zones and five sleep stages. Transition costs between strata are governed by the J-cost function, with upward mobility from working to middle class carrying J-cost J(φ²). The SocialStratificationCert structure packages the stratum count together with the three cost properties. Upstream, cost_nonneg from ObserverForcing states that the cost of any recognition event is non-negative, while the sibling lemmas establish zero self-cost, non-negativity under positive arguments, and positivity of the one-step mobility cost.
proof idea
This is a definition that constructs the SocialStratificationCert record by direct field assignment: stratum_count is taken from socialStratumCount_eq, cost_at_stratum from mobilityTransitionCost_at_stratum, cost_nonneg from mobilityTransitionCost_nonneg, and mobility_cost_pos from oneStepMobilityCost_pos.
why it matters in Recognition Science
The definition supplies the complete certificate for the five-stratum sociological prediction forced by configDim D=5. It closes the structural theorem in the Recognition Science sociology module and aligns with the phi-ladder and eight-tick octave landmarks of the forcing chain. No downstream theorems yet reference it, but the module doc-comment identifies the falsifier as any comparative survey on ten or more societies that finds a modal stratum count reliably different from 5.
scope and limits
- Does not prove the empirical existence of social strata in any real society.
- Does not compute explicit J-cost values for multi-step transitions.
- Does not address cultural or historical variation in stratum boundaries.
- Does not derive the configDim=5 premise itself.
formal statement (Lean)
75noncomputable def cert : SocialStratificationCert where
76 stratum_count := socialStratumCount_eq
proof body
Definition body.
77 cost_at_stratum := mobilityTransitionCost_at_stratum
78 cost_nonneg := mobilityTransitionCost_nonneg
79 mobility_cost_pos := oneStepMobilityCost_pos
80