solidarityType_count
plain-language theorem explainer
The theorem establishes that the finite type of social solidarity forms has cardinality exactly five, anchoring the configDim parameter in the Recognition framework. Sociologists modeling cohesion mechanisms under Recognition Science would cite this count when classifying the five canonical types. The proof is a one-line decision procedure that computes the cardinality directly from the inductive enumeration of five constructors.
Claim. The set of solidarity types has cardinality five: $|S| = 5$ where $S = $ {mechanical, organic, gesellschaft, gemeinschaft, network}.
background
The module introduces SolidarityType as an inductive type whose five constructors enumerate the canonical social-cohesion forms: mechanical (Durkheim, homogeneous), organic (Durkheim, division of labor), gesellschaft (Tönnies, contractual), gemeinschaft (Tönnies, communal), and network (modern). This enumeration is identified with configDim D = 5. The upstream result is the inductive definition itself, which automatically derives Fintype, DecidableEq, and related instances.
proof idea
The proof is a one-line wrapper that applies the decide tactic to evaluate Fintype.card on the inductive type SolidarityType, whose five constructors are enumerated by the derived Fintype instance.
why it matters
This cardinality supplies the five_types field in the downstream definition solidarityTypesCert, certifying the enumeration for further sociological derivations. It fills the sociology depth of the Recognition Science framework by linking social cohesion to the configDim parameter, consistent with the module's statement of zero sorry and zero axiom.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.