SolidarityType
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.
claimThe 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 in Recognition Science
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.
scope and limits
- Does not claim these five types exhaust all possible social structures.
- Does not derive the types from the Recognition Composition Law or the forcing chain.
- Does not specify transition rules or stability conditions between the types.
formal statement (Lean)
17inductive SolidarityType where
18 | mechanical
19 | organic
20 | gesellschaft
21 | gemeinschaft
22 | network
23 deriving DecidableEq, Repr, BEq, Fintype
24