module module moderate

`IndisputableMonolith.MusicTheory.Valence`

This module defines valence primitives in music theory, including majorThird, minorThird, and ledgerSkew functions with their basic properties. It extends the HarmonicModes import to formalize interval deviations within the Recognition Science setting. The sibling declarations establish zero at unity, sign behavior, antisymmetry, and the major-minor skew comparison. These objects supply the quantitative language for harmonic valence without embedded proofs.

claimThe module introduces functions $majorThird, minorThird, ledgerSkew : ℝ → ℝ$ together with the statements $ledgerSkew(1) = 0$, $ledgerSkew(x) > 0$ for $x > 1$, $ledgerSkew(x) < 0$ for $x < 1$, antisymmetry of ledgerSkew, and $majorSkew(x) > minorSkew(x)$.

background

The module sits inside the MusicTheory domain of Recognition Science and imports only HarmonicModes plus Mathlib. It introduces ledgerSkew as the signed deviation measure for musical intervals and specializes it to major and minor thirds. The surrounding framework supplies the phi-ladder and J-cost conventions from upstream harmonic-mode results, so that interval calculations remain consistent with self-similar forcing.

proof idea

this is a definition module, no proofs

why it matters in Recognition Science

The valence definitions supply the interval primitives required by any downstream Recognition Science treatment of musical stability or consonance. Although the current used_by list is empty, the module completes the basic ledger-skew toolkit that higher-level harmonic theorems would invoke.

scope and limits

Does not contain theorems or proofs.
Does not import material beyond HarmonicModes and Mathlib.
Does not assign numerical constants or evaluate specific pitches.
Does not connect valence to physical observables or the phi-ladder explicitly.

depends on (1)

Lean names referenced from this declaration's body.

IndisputableMonolith.MusicTheory.HarmonicModes module_import

declarations in this module (19)

def majorThird L28
def minorThird L29
def ledgerSkew L31
theorem ledgerSkew_zero_at_unity L33
theorem ledgerSkew_pos_above_one L36
theorem ledgerSkew_neg_below_one L43
theorem ledgerSkew_antisymmetric L49
theorem major_third_skew L57
theorem minor_third_skew L61
theorem major_third_skew_pos L65
theorem minor_third_skew_pos L70
theorem major_skew_gt_minor_skew L75
inductive Valence L81
def classifyValence L87
theorem major_is_positive L92
theorem minor_is_positive_but_less L98
theorem valence_difference L110
theorem valence_difference_one_twelfth L114
theorem skew_increases_with_interval_size L119