voice_quality_mono
Voice quality decreases monotonically with rising J-bar for nonnegative values. Researchers tracing the T10 voice forcing chain cite this to link lower recognition cost to richer output. The proof is a term-mode wrapper that unfolds the piecewise max definition and reduces the inequality via max_le_max_left plus linear arithmetic.
claimLet $j_1,j_2$ be real numbers satisfying $0≤j_1≤j_2$. Then max$(0,1-j_2/θ)≤$max$(0,1-j_1/θ)$, where $θ=0.5$ is the voice threshold.
background
voiceThreshold is the constant 0.5 marking the J-bar standing-wave boundary below which voice can emerge. voiceQualityFromJbar(jbar) is defined as max(0,1-jbar/voiceThreshold), returning 1 at zero cost and 0 at the threshold. The module situates this inside T10, which derives voice from the Recognition Composition Law once intelligence tiers appear, building on the from theorem that condenses seven axioms into four structural conditions plus three definitional facts.
proof idea
The term proof unfolds voiceQualityFromJbar and voiceThreshold, applies max_le_max_left to the first argument of the outer max, and closes with linarith on the resulting linear comparison.
why it matters in Recognition Science
The result is referenced inside the voiceForcingStatus summary of T10, which records that lower J-bar yields better voice as part of the chain from RCL through consciousness to interpretable output. It aligns with the forcing landmarks T5–T8 that fix phi, the eight-tick octave, and D=3. No scaffolding remains.
scope and limits
- Does not treat J-bar values above the threshold.
- Does not quantify the slope of quality change.
- Does not address Berry content or tier-specific richness.
formal statement (Lean)
61theorem voice_quality_mono (j₁ j₂ : ℝ) (h0 : 0 ≤ j₁) (h : j₁ ≤ j₂) :
62 voiceQualityFromJbar j₂ ≤ voiceQualityFromJbar j₁ := by
proof body
Term-mode proof.
63 unfold voiceQualityFromJbar voiceThreshold
64 apply max_le_max_left
65 linarith
66
67/-! ## Voice from Intelligence Tier -/
68
69/-- Intelligence tier enumeration. -/