voice_quality_mono
plain-language theorem explainer
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.
Claim. Let $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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.