pith. machine review for the scientific record. sign in
def definition def or abbrev high

voiceQualityFromJbar

show as:
view Lean formalization →

Voice quality is computed from the J-bar value via the formula max(0, 1 minus jbar over the threshold of 0.5). Researchers tracing the T10 forcing chain from cost minimization to forced voice would reference this metric to track signal degradation. The definition is a direct one-line arithmetic expression requiring no additional lemmas.

claim$q(j) = max(0, 1 - j / θ)$ where $θ = 0.5$ is the standing-wave threshold and $j$ is the J-bar cost.

background

The VoiceForcing module establishes T10, showing that voice emerges necessarily from intelligence on a trained lattice once J-bar falls below threshold. voiceThreshold is set to 0.5 as the standing-wave prerequisite where signal exceeds noise. Upstream dependencies include the collision-free is predicate from OptionAEmpiricalProgram and algebraic tautologies from EdgeLengthFromPsi that ground the ledger structure.

proof idea

This is a direct definition that applies the max operator to zero and the expression 1 minus jbar divided by voiceThreshold.

why it matters in Recognition Science

It provides the quality function invoked by voice_forced, voice_emerges_below_threshold, and voice_berry_positive to establish positive Berry content in forced voice. The module positions this as part of the chain from RCL through consciousness to voice, paralleling the derivation of phi and D=3. No open questions are flagged in the supplied results.

scope and limits

formal statement (Lean)

  44def voiceQualityFromJbar (jbar : ℝ) : ℝ :=

proof body

Definition body.

  45  max 0 (1 - jbar / voiceThreshold)
  46
  47/-- Voice quality is zero above threshold. -/

used by (5)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (5)

Lean names referenced from this declaration's body.