innovationDiffusionCert
plain-language theorem explainer
The definition constructs a certificate that innovation diffusion follows the phi-ladder by supplying exactly five adopter categories and successive adoption times in golden ratio. Economists or econophysicists modeling Rogers diffusion inside Recognition Science would cite it to anchor the five-category split in the self-similar scaling forced by the T6 fixed point. The construction is a direct field assignment from the decidable cardinality theorem and the algebraic ratio theorem.
Claim. Let $AdopterCategory$ be the finite type of adopter classes and let $t_k$ denote adoption time at rung $k$. The certificate asserts $|AdopterCategory|=5$ together with the scaling law $t_{k+1}/t_k=phi$ for every natural number $k$, where $phi$ is the golden ratio.
background
The module reinterprets Rogers' 1962 five adopter categories (innovators, early adopters, early majority, late majority, laggards) as thresholds on the phi-ladder of social recognition cost, with the count five identified with configuration dimension D=5. The golden ratio phi enters as the self-similar fixed point forced in the UnifiedForcingChain (T6). The structure InnovationDiffusionCert packages two properties: the cardinality of AdopterCategory equals 5, and the ratio of successive adoption times equals phi for all k. Upstream, adopterCategoryCount establishes the cardinality by decision, while adoptionTimeRatio proves the ratio by unfolding adoptionTime, invoking positivity of phi powers, and closing with ring simplification.
proof idea
The definition is a direct construction that supplies the five_categories field from adopterCategoryCount and the phi_ratio field from adoptionTimeRatio. It is a one-line wrapper that populates the two fields of the InnovationDiffusionCert structure from the upstream theorems.
why it matters
The definition supplies the concrete certificate that realizes the RS prediction of phi-scaled adoption times inside the five-category structure, thereby embedding Rogers' empirical pattern into the phi-ladder framework. It sits downstream of the forcing-chain derivation of phi (T6) and the eight-tick octave (T7) that yields D=3 spatial dimensions, though no downstream theorems yet consume it. The module doc-comment cites Rogers (1962) as the source proposition being formalized.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.