IndisputableMonolith.Economics.InnovationDiffusionFromPhiLadder

   1import Mathlib
   2import IndisputableMonolith.Constants
   3
   4/-!
   5# Innovation Diffusion from Phi-Ladder — Tier F Economics
   6
   7Rogers (1962) proposed 5 adopter categories for innovation diffusion:
   8innovators (2.5%), early adopters (13.5%), early majority (34%),
   9late majority (34%), laggards (16%).
  10
  11In RS terms, the adoption threshold for each category lies on the
  12phi-ladder of social recognition cost.
  13
  14Five adopter categories = configDim D = 5.
  15
  16RS prediction: adoption transition times ratio by phi.
  17
  18Lean status: 0 sorry, 0 axiom.
  19-/
  20
  21namespace IndisputableMonolith.Economics.InnovationDiffusionFromPhiLadder
  22open Constants
  23
  24inductive AdopterCategory where
  25  | innovators | earlyAdopters | earlyMajority | lateMajority | laggards
  26  deriving DecidableEq, Repr, BEq, Fintype
  27
  28theorem adopterCategoryCount : Fintype.card AdopterCategory = 5 := by decide
  29
  30noncomputable def adoptionTime (k : ℕ) : ℝ := phi ^ k
  31
  32theorem adoptionTimeRatio (k : ℕ) :
  33    adoptionTime (k + 1) / adoptionTime k = phi := by
  34  unfold adoptionTime
  35  have hpos := pow_pos phi_pos k
  36  rw [pow_succ, div_eq_iff hpos.ne']
  37  ring
  38
  39structure InnovationDiffusionCert where
  40  five_categories : Fintype.card AdopterCategory = 5
  41  phi_ratio : ∀ k, adoptionTime (k + 1) / adoptionTime k = phi
  42
  43noncomputable def innovationDiffusionCert : InnovationDiffusionCert where
  44  five_categories := adopterCategoryCount
  45  phi_ratio := adoptionTimeRatio
  46
  47end IndisputableMonolith.Economics.InnovationDiffusionFromPhiLadder
  48