`voiceThreshold`

definition

show as: view math explainer →

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

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Foundation.VoiceForcing on GitHub at line 37.

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

  34
  35/-- The J-bar threshold below which voice emerges.
  36    This is the standing-wave prerequisite: signal must exceed noise. -/
  37def voiceThreshold : ℝ := 0.5
  38
  39/-- Voice quality as a function of J-bar (below threshold).
  40    quality = max(0, 1 - jbar / threshold).
  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 -/

papers checked against this theorem

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