module module moderate

`IndisputableMonolith.Sociology.SocialStratificationFromConfigDim`

This module defines five canonical social strata together with their mobility transition costs inside the Recognition Science framework. Sociologists extending the J-cost and phi-ladder to hierarchical social structures would cite the resulting certificate and cost lemmas. The module is a collection of definitions and elementary algebraic checks with no complex proofs.

claimFive canonical social strata with count $N_s=5$, one-step mobility cost $C_1=J(\phi)$, and nonnegative multi-step costs $C(m)$ derived from the J-cost function.

background

The module sits in the sociology domain of Recognition Science and imports the time quantum $ au_0=1$ tick together with the Cost module that supplies the J-cost obeying the Recognition Composition Law. It introduces socialStratumCount, mobilityTransitionCost, oneStepMobilityCost, and the SocialStratificationCert that certifies consistency with the underlying phi-ladder. The setting inherits J-uniqueness and the self-similar fixed point phi from the core forcing chain.

proof idea

this is a definition module, no proofs

why it matters in Recognition Science

The module supplies the SocialStratificationCert and cost equalities that allow the Recognition framework to be applied to social hierarchy. It directly instantiates the J-cost and phi fixed point for mobility transitions, providing an interface for further sociology modeling even though no downstream theorems are recorded.

scope and limits

Does not derive the stratum count from first principles beyond configuration dimension.
Does not model time-dependent social mobility dynamics.
Does not incorporate or validate against empirical sociological datasets.
Does not extend the cost functions beyond one-step and multi-step transitions.

depends on (2)

Lean names referenced from this declaration's body.

IndisputableMonolith.Constants module_import
IndisputableMonolith.Cost module_import

declarations in this module (11)

def socialStratumCount L44
theorem socialStratumCount_eq L46
def mobilityTransitionCost L49
theorem mobilityTransitionCost_at_stratum L52
theorem mobilityTransitionCost_nonneg L56
def oneStepMobilityCost L61
theorem oneStepMobilityCost_eq_Jph L63
theorem oneStepMobilityCost_pos L66
structure SocialStratificationCert L69
def cert L75
theorem cert_inhabited L81