SolidarityTypesCert
plain-language theorem explainer
SolidarityTypesCert is a structure that certifies the inductive SolidarityType has cardinality exactly five, matching the five social cohesion forms tied to configDim D=5. Sociologists extending Recognition Science to Durkheim and Tönnies distinctions would cite it to fix the enumeration in the framework. The definition is a direct structure declaration whose field is discharged by the Fintype instance derived from the five-constructor inductive.
Claim. Let $S$ be the finite type whose elements are mechanical solidarity, organic solidarity, gesellschaft, gemeinschaft, and network solidarity. SolidarityTypesCert is the structure asserting that the cardinality of $S$ equals 5.
background
The module maps configDim D=5 to five canonical social-cohesion types: mechanical solidarity (Durkheim, homogeneous), organic solidarity (Durkheim, division of labor), gesellschaft (Tönnies, contractual), gemeinschaft (Tönnies, communal), and network solidarity (modern). SolidarityType is the inductive type with exactly these five constructors, from which Fintype, DecidableEq, and cardinality instances are derived automatically. Recognition Science places this enumeration in the sociology extension of the core forcing chain, where the single functional equation yields both physical and social structure.
proof idea
SolidarityTypesCert is a one-line structure declaration introducing the field five_types of type Fintype.card SolidarityType = 5. The witness is supplied by the downstream definition solidarityTypesCert, which directly applies the Fintype instance generated by the inductive definition of SolidarityType.
why it matters
This structure supplies the type for the certificate constructed by solidarityTypesCert, anchoring the five-type count to configDim D=5 in the sociology module. It extends the T0-T8 forcing chain and Recognition Composition Law into social domains without introducing new axioms. The module reports zero sorry or axiom, closing the enumeration step for downstream use.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.