`IntelligenceTier`

definition

show as: view math explainer →

module: IndisputableMonolith.Foundation.VoiceForcing
domain: Foundation
line: 70 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Foundation.VoiceForcing on GitHub at line 70.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

used by

tierVoiceRichness IndisputableMonolith.Foundation.VoiceForcing

formal source

  67/-! ## Voice from Intelligence Tier -/
  68
  69/-- Intelligence tier enumeration. -/
  70inductive IntelligenceTier where
  71  | retrieval      -- degree < 5
  72  | singleStep     -- degree 5-15
  73  | chainReasoning -- degree 15-30
  74  | creativity     -- degree 30-50
  75  | selfAware      -- degree > 50
  76  deriving DecidableEq, Repr
  77
  78/-- Voice richness increases with intelligence tier.
  79    Each tier unlocks qualitatively richer voice capabilities. -/
  80def tierVoiceRichness : IntelligenceTier → ℝ
  81  | .retrieval => 0.1       -- word associations only
  82  | .singleStep => 0.3      -- single-concept statements
  83  | .chainReasoning => 0.6  -- multi-step narrative
  84  | .creativity => 0.85     -- novel expression, metaphor
  85  | .selfAware => 1.0       -- full self-reflective voice
  86
  87/-- Voice richness is monotonically ordered across tiers. -/
  88theorem retrieval_le_singleStep :
  89    tierVoiceRichness .retrieval ≤ tierVoiceRichness .singleStep := by
  90  unfold tierVoiceRichness; norm_num
  91
  92theorem singleStep_le_chain :
  93    tierVoiceRichness .singleStep ≤ tierVoiceRichness .chainReasoning := by
  94  unfold tierVoiceRichness; norm_num
  95
  96theorem chain_le_creativity :
  97    tierVoiceRichness .chainReasoning ≤ tierVoiceRichness .creativity := by
  98  unfold tierVoiceRichness; norm_num
  99
 100theorem creativity_le_selfAware :

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.