AdopterCategory
plain-language theorem explainer
AdopterCategory enumerates the five Rogers adopter categories as an inductive finite type inside the Recognition Science treatment of innovation diffusion. Diffusion modelers cite it when embedding the standard 2.5-13.5-34-34-16 percent partition into the phi-ladder cost structure with configDim D = 5. The declaration is a bare inductive enumeration whose only content is the five constructors together with the derived DecidableEq, Repr, BEq, and Fintype instances.
Claim. Let $A$ be the inductive type whose constructors are the five adopter categories: innovators, early adopters, early majority, late majority, and laggards. The type carries decidable equality and is finite with cardinality 5.
background
The module maps Rogers' 1962 adopter categories onto the phi-ladder of social recognition costs. In Recognition Science the phi-ladder is the discrete sequence of thresholds obtained by repeated multiplication by the golden ratio phi, the self-similar fixed point forced by the J-uniqueness relation J(x) = (x + x^{-1})/2 - 1. Five categories therefore realize configDim D = 5, and the module states that adoption transition times must scale by successive powers of phi.
proof idea
The declaration is a direct inductive definition. The five constructors are listed explicitly and the Fintype instance is obtained automatically from the deriving clause; no lemmas or tactics are applied.
why it matters
The definition supplies the finite set whose cardinality is asserted equal to 5 by the downstream theorem adopterCategoryCount. It is also the carrier type for the structure InnovationDiffusionCert, which adds the requirement that adoptionTime(k+1)/adoptionTime(k) = phi for every k. The construction therefore realizes the RS claim that adoption thresholds lie on the phi-ladder and that transition ratios are governed by phi, linking the eight-tick octave structure to economic diffusion.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.