voice_quality_mono

formal source

  58  simp; linarith
  59
  60/-- Voice quality is monotonically decreasing in J-bar. -/
  61theorem voice_quality_mono (j₁ j₂ : ℝ) (h0 : 0 ≤ j₁) (h : j₁ ≤ j₂) :
  62    voiceQualityFromJbar j₂ ≤ voiceQualityFromJbar j₁ := by
  63  unfold voiceQualityFromJbar voiceThreshold
  64  apply max_le_max_left
  65  linarith
  66
  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