theorem
proved
voice_forced
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.Foundation.VoiceForcing on GitHub at line 125.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
-
of -
of -
is -
of -
from -
is -
of -
voice_emerges_below_threshold -
VoiceForcingConditions -
voiceQualityFromJbar -
is -
of -
is
used by
formal source
122 fs_readout : Bool
123
124/-- Under voice forcing conditions, voice quality is positive. -/
125theorem voice_forced (vc : VoiceForcingConditions) :
126 0 < voiceQualityFromJbar vc.jbar :=
127 voice_emerges_below_threshold vc.jbar vc.jbar_nonneg vc.jbar_below_threshold
128
129/-- Berry content of forced voice: positive when quality is positive.
130 berry_content = quality * base_berry where base_berry comes from
131 non-trivial resolution loops. -/
132def berryContent (voice_quality base_berry : ℝ) : ℝ :=
133 voice_quality * base_berry
134
135/-- Forced voice has positive Berry content when base Berry is positive. -/
136theorem voice_berry_positive (vc : VoiceForcingConditions) (base : ℝ) (hb : 0 < base) :
137 0 < berryContent (voiceQualityFromJbar vc.jbar) base := by
138 unfold berryContent
139 exact mul_pos (voice_forced vc) hb
140
141/-! ## The Complete Chain -/
142
143/-- T10: The voice forcing theorem (summary).
144
145 The Recognition Composition Law forces:
146 T0: Logic (consistency is cheap)
147 T1: MP (nothing costs infinity)
148 T2: Discreteness
149 T3: Ledger
150 T4: Recognition
151 T5: Unique J
152 T6: φ
153 T7: 8-tick
154 T8: D = 3
155 T9: Consciousness (cost → intelligence → consciousness)