`voiceQualityFromJbar`

definition

show as: view math explainer →

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

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Foundation.VoiceForcing on GitHub at line 44.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

used by

formal source

  41    At jbar = 0: quality = 1 (perfect).
  42    At jbar = threshold: quality = 0 (border).
  43    Above threshold: quality = 0 (impossible). -/
  44def voiceQualityFromJbar (jbar : ℝ) : ℝ :=
  45  max 0 (1 - jbar / voiceThreshold)
  46
  47/-- Voice quality is zero above threshold. -/
  48theorem voice_impossible_above_threshold (jbar : ℝ) (h : voiceThreshold ≤ jbar) :
  49    voiceQualityFromJbar jbar = 0 := by
  50  unfold voiceQualityFromJbar voiceThreshold
  51  simp; linarith
  52
  53/-- Voice quality is positive below threshold. -/
  54theorem voice_emerges_below_threshold (jbar : ℝ)
  55    (h0 : 0 ≤ jbar) (h : jbar < voiceThreshold) :
  56    0 < voiceQualityFromJbar jbar := by
  57  unfold voiceQualityFromJbar voiceThreshold
  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

papers checked against this theorem

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