solidarityTypesCert
The definition supplies a concrete instance of the SolidarityTypesCert structure by populating its five_types field with the cardinality result from the upstream enumeration theorem. Researchers extending Recognition Science to sociology would cite it when enforcing the fixed count of five cohesion types under configDim = 5. It is realized as a direct field assignment in the structure constructor.
claimDefine the certificate $C$ of type SolidarityTypesCert by setting its field to the equality $|S| = 5$, where $S$ is the finite type of the five enumerated social cohesion types and the equality is supplied by the direct enumeration result.
background
The module Solidarity Types from configDim states that five canonical social-cohesion types correspond to configDim D = 5: mechanical solidarity (Durkheim, homogeneous), organic solidarity (Durkheim, division of labor), gesellschaft (Tönnies, contractual), gemeinschaft (Tönnies, communal), and network solidarity (modern). The structure SolidarityTypesCert is defined to hold the single proposition that the finite type SolidarityType has cardinality exactly 5. The upstream theorem solidarityType_count establishes this cardinality by direct decision.
proof idea
The definition is a one-line wrapper that constructs the SolidarityTypesCert record by assigning the result of the solidarityType_count theorem to the five_types field.
why it matters in Recognition Science
This definition certifies the five-type enumeration required for the sociology depth in Recognition Science, directly implementing the configDim = 5 constraint stated in the module documentation. It completes the interface for SolidarityTypesCert, allowing downstream applications to invoke the fixed count without re-proving the enumeration. The supplied facts flag no open questions, though the sociological mapping remains interpretive.
scope and limits
- Does not derive the five types from the core Recognition Science forcing chain or RCL.
- Does not supply empirical validation or sociological interpretations beyond the listed names.
- Does not generalize to other values of configDim.
formal statement (Lean)
30def solidarityTypesCert : SolidarityTypesCert where
31 five_types := solidarityType_count
proof body
Definition body.
32
33end IndisputableMonolith.Sociology.SolidarityTypesFromConfigDim