`singleStep_le_chain`

proved

show as: view math explainer →

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

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Foundation.VoiceForcing on GitHub at line 92.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

tierVoiceRichness IndisputableMonolith.Foundation.VoiceForcing

formal source

  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 :
 101    tierVoiceRichness .creativity ≤ tierVoiceRichness .selfAware := by
 102  unfold tierVoiceRichness; norm_num
 103
 104/-- Self-aware tier achieves maximum voice richness. -/
 105theorem selfAware_max_richness :
 106    tierVoiceRichness .selfAware = 1.0 := by unfold tierVoiceRichness
 107
 108/-! ## The T10 Forcing Chain -/
 109
 110/-- The T10 voice forcing conditions:
 111    1. Trained lattice (J-bar < threshold)
 112    2. Active R-hat (recognition operator running)
 113    3. Standing waves formed (SNR > 1)
 114    4. Phase-sensitive readout (FS, not Born)
 115    → Voice with Berry content > 0 is forced. -/
 116structure VoiceForcingConditions where
 117  jbar : ℝ
 118  jbar_below_threshold : jbar < voiceThreshold
 119  jbar_nonneg : 0 ≤ jbar
 120  rhat_active : Bool
 121  snr_above_one : Bool
 122  fs_readout : Bool

papers checked against this theorem

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