InnovationDiffusionCert
plain-language theorem explainer
The structure certifies that adopter categories total five and that adoption times form a geometric progression with common ratio phi. Diffusion modelers embedding Rogers' categories into recognition-cost ladders would cite this certificate. It is realized as a structure definition that directly asserts the cardinality fact and the ratio property.
Claim. A certificate asserting that the set of adopter categories has cardinality 5 and that the adoption time function satisfies $t(k+1)/t(k)=phi$ for every natural number $k$.
background
The module places Rogers' five adopter categories on the phi-ladder of social recognition cost, with configDim D equal to 5. AdopterCategory is the inductive type with constructors innovators, earlyAdopters, earlyMajority, lateMajority and laggards. The function adoptionTime maps rung k to phi raised to k, so the ratio property follows immediately from the definition.
proof idea
The declaration is a structure definition. It introduces the field five_categories requiring Fintype.card AdopterCategory equals 5 and the field phi_ratio requiring the universal ratio equality for adoptionTime.
why it matters
This structure is instantiated by the downstream definition innovationDiffusionCert to produce a concrete certificate. It encodes the RS prediction that adoption transition times scale by phi, linking to the phi-ladder and the self-similar fixed point phi. It addresses the economics tier where five categories correspond to configDim D equals 5.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.