ionian_aeolian_dominant
plain-language theorem explainer
Ionian and Aeolian modes achieve the two lowest J-cost ranks among the seven Greek modes, both at most 1. Musicologists and cognitive scientists studying cross-cultural preferences would cite it to connect Recognition Science's J-function to observed modal dominance in Huron 2006 data. The proof is a one-line term wrapper that applies the decide tactic to the computable costRank values.
Claim. $r(I) ≤ 1 ∧ r(A) ≤ 1$, where $r$ denotes the numerical rank induced by J-cost of each mode's interval ratios relative to the Ionian reference scale.
background
The module derives modal preference from J-cost on φ-rational intervals. The seven Greek modes receive ranks via costRank, a function that orders modes by their J-cost relative to the canonical major (Ionian) reference; lower rank means higher predicted preference. This follows the Recognition Composition Law applied to interval ratios expressed in φ-units, with the Ionian mode as the zero-cost baseline.
proof idea
The proof is a term-mode one-liner: refine ⟨?, ?⟩ <;> decide. This constructs the conjunction by delegating both inequalities to the decide tactic, which succeeds because costRank evaluates to concrete natural numbers on the mode constructors.
why it matters
The theorem supplies the dominance claim required by the ModalPreferenceCert structure, which records Ionian as lowest (rank 0), Aeolian as second (rank 1), and Locrian as highest (rank 6). It fills the Track I10 derivation that cross-cultural preferences track φ-rational J-costs, consistent with T5 J-uniqueness and the eight-tick octave. The module falsifier is a large cross-cultural survey showing best-modal preference outside the predicted Ionian-Aeolian cluster.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.