adopterCategoryCount
plain-language theorem explainer
The theorem establishes that the finite type of adopter categories has cardinality five, matching Rogers' classification of innovators, early adopters, early majority, late majority, and laggards. Economists modeling innovation diffusion under Recognition Science cite this to confirm the five-tier structure aligns with the phi-ladder. The proof is a one-line decision procedure that enumerates the inductive constructors via the derived Fintype instance.
Claim. The cardinality of the finite type of adopter categories is five: $|A| = 5$ where $A = $ {innovators, early adopters, early majority, late majority, laggards}.
background
The module Innovation Diffusion from Phi-Ladder connects Rogers' 1962 classification of five adopter categories to the Recognition Science phi-ladder of social recognition costs. The inductive definition AdopterCategory enumerates innovators, earlyAdopters, earlyMajority, lateMajority, and laggards, and derives Fintype to make its cardinality computable. This establishes configDim D = 5 in the RS framework, where adoption thresholds align with phi-powered costs.
proof idea
The proof is a one-line wrapper that invokes the decide tactic. This tactic succeeds because the inductive type derives DecidableEq and Fintype, allowing exhaustive enumeration of the five constructors to confirm the cardinality.
why it matters
This result supplies the five_categories field in the InnovationDiffusionCert definition, which also incorporates the phi_ratio from adoptionTimeRatio. It directly implements the module's claim that five adopter categories equal configDim D = 5, linking to the phi-ladder and the eight-tick octave structure in the broader Recognition Science chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.