SolidarityType
plain-language theorem explainer
The inductive definition SolidarityType enumerates five canonical forms of social cohesion that appear when the configuration dimension equals five in the Recognition Science sociology module. Modelers of social structures in this framework cite it to classify cohesion mechanisms drawn from Durkheim and Tönnies. The declaration proceeds by direct enumeration of the five cases and automatically derives the required typeclass instances for decidable equality and finiteness.
Claim. The type of social solidarity is the inductive type whose five constructors are mechanical solidarity, organic solidarity, gesellschaft, gemeinschaft, and network solidarity.
background
The module fixes the configuration dimension at five to produce the canonical social-cohesion types. These are mechanical solidarity (Durkheim, homogeneous societies), organic solidarity (Durkheim, division of labor), gesellschaft (Tönnies, contractual relations), gemeinschaft (Tönnies, communal bonds), and network solidarity (modern interconnected forms). The setting supplies the carrier for downstream counting and certification results with zero axioms or sorry statements.
proof idea
The declaration is a direct inductive definition that introduces five constructors and derives DecidableEq, Repr, BEq, and Fintype via the deriving clause. No lemmas are applied and no tactics are required.
why it matters
This definition supplies the carrier type for the theorem solidarityType_count that proves the cardinality equals five and for the structure SolidarityTypesCert. It realizes the sociology depth of the framework by setting configDim to five, extending the core construction in which spatial dimensions are fixed at three. No open questions attach to the enumeration itself.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.