Location
Paper: Paper 5 (Pythagorean Companion)
Version: v1.1
Sections: § 2.2 (prose after the convergents list), § 4.2 (Baker-and-temperaments paragraph), § 7.1 (temperament-relevant approximations)
Source of correction: reported by suhr (Lean Zulip display name; attribution placeholder pending reviewer confirmation) in the #new members topic Music-kernel + Pythagorean comma formalization target, 2026-04-19. Topic: https://leanprover.zulipchat.com/#narrow/channel/113489-new-members/topic/Music-kernel.20.2B.20Pythagorean.20comma.20formalization.20target/near/588730901
The errors
Three distinct issues in the v1.1 text, all correctly flagged by the reviewer:
1. Prose at § 2.2 skips the 24/41 convergent
The convergents sequence (displayed as math) correctly lists ..., 7/12, 24/41, 31/53, .... The prose that follows, however, says:
The next convergent, 31/53, achieves an approximation accurate to roughly 0.0000680 --- whence the theorist's persistent interest in 53-TET...
The convergent immediately after 7/12 is 24/41, not 31/53. 31/53 is the convergent after 24/41. The prose should narrate both — especially because 41-TET is musically significant in its own right (7-limit harmony; see point 2 below).
2. "Practically usable temperaments" is too narrow (§§ 2.2, 4.2, 7.1)
§ 2.2 concludes:
It is a mathematical fact about how log₂(3/2) sits in the reals, and it determines the set of temperaments that are practically useful for closing the fifth-octave cycle.
§ 4.2 asserts:
Baker's theorem constrains the space of practically usable temperaments. ... this explains why 12-TET, 53-TET, and a small number of other equal divisions of the octave are the only temperaments that produce very small commas with small exponents...
§ 7.1 asserts:
... picks out 7/12 and 31/53 as the temperament-relevant approximations.
All three statements implicitly equate "practically usable temperament" with "temperament that minimizes the Pythagorean comma." That is an optimization over the rank-2 prime basis {2, 3} only. Real microtonal practice optimizes over richer prime bases:
- 31-TET (Huygens, Fokker) has worse fifths than 12-TET (≈ 5 cents off instead of ≈ 2) but is an effective 11-limit temperament — excellent approximations to 5/4, 7/4, 11/8, etc.
- 41-TET is a standard 7-limit choice with very good fifths.
- 53-TET is favored in 5-limit contexts (syntonic comma vanishes).
The paper's argument about Baker's theorem applies to the broader family via extended prime bases (§ 4.4 already notes this for the syntonic comma and schisma); the three sentences above should be re-scoped to "temperaments that minimize the Pythagorean comma specifically" rather than "practically usable temperaments".
3. "53-TET is impractical for keyboard construction" (§ 2.2) is outdated
§ 2.2 says:
... even though 53-TET is impractical for keyboard construction.
Modern isomorphic keyboard layouts make 53-TET perfectly playable: Bosanquet's 1875 generalized keyboard (contemporaneous with Bosanquet's advocacy of 53-TET cited a few words earlier in the paper), the contemporary Lumatone keyboard, and the Kite guitar are instances. The claim reads as if the state of microtonal instrument design froze around 1900.
Severity
Proposed correction
Resolved in v1.2 (same commit as this issue — see commit range). Summary of changes:
- § 2.2 prose. Replace "The next convergent, 31/53, achieves..." with a two-convergent narration: 24/41 → 41-TET, then 31/53 → 53-TET, with the Mercator/Bosanquet citation retained for 53-TET. Remove the phrase "even though 53-TET is impractical for keyboard construction" and replace with a short note that isomorphic layouts (Bosanquet 1875; Lumatone; Kite guitar) make it accessible.
- § 2.2 closing sentence of subsection. Re-scope "determines the set of temperaments that are practically useful" → "determines the set of equal temperaments that are optimal for minimizing the Pythagorean comma specifically", with one sentence acknowledging that microtonal practice optimizes for other harmonic targets (5-/7-/11-limit) that correspond to Baker-type problems over extended prime bases.
- § 4.2 last paragraph. Replace "practically usable temperaments" with "equal temperaments that minimize the Pythagorean comma specifically". Add 41-TET to the small-comma list alongside 12-TET and 53-TET. Append one sentence noting that general musical practicality depends on additional harmonic goals.
- § 7.1 opening. Expand "7/12 and 31/53" to "7/12, 24/41, and 31/53 (corresponding to 12-TET, 41-TET, and 53-TET)" and re-scope "temperament-relevant" → "optimal for the Pythagorean comma specifically".
- Version bump to v1.2 with revision note naming the reviewer (placeholder:
suhr via Lean Zulip, pending consent for different attribution).
- Acknowledgements. Paper-level acknowledgements section updated; new repo-root
ACKNOWLEDGEMENTS.md created per CONTRIBUTING.md convention (first merged external contribution).
Submitter
Reported by suhr via Lean Zulip (display-name attribution; pending reviewer's confirmation of preferred credit form). Expertise evident from the response: microtonal music theory, continued-fraction approximants, modern isomorphic-keyboard landscape.
Location
Paper: Paper 5 (Pythagorean Companion)
Version: v1.1
Sections: § 2.2 (prose after the convergents list), § 4.2 (Baker-and-temperaments paragraph), § 7.1 (temperament-relevant approximations)
Source of correction: reported by suhr (Lean Zulip display name; attribution placeholder pending reviewer confirmation) in the
#new memberstopic Music-kernel + Pythagorean comma formalization target, 2026-04-19. Topic: https://leanprover.zulipchat.com/#narrow/channel/113489-new-members/topic/Music-kernel.20.2B.20Pythagorean.20comma.20formalization.20target/near/588730901The errors
Three distinct issues in the v1.1 text, all correctly flagged by the reviewer:
1. Prose at § 2.2 skips the 24/41 convergent
The convergents sequence (displayed as math) correctly lists
..., 7/12, 24/41, 31/53, .... The prose that follows, however, says:The convergent immediately after 7/12 is 24/41, not 31/53. 31/53 is the convergent after 24/41. The prose should narrate both — especially because 41-TET is musically significant in its own right (7-limit harmony; see point 2 below).
2. "Practically usable temperaments" is too narrow (§§ 2.2, 4.2, 7.1)
§ 2.2 concludes:
§ 4.2 asserts:
§ 7.1 asserts:
All three statements implicitly equate "practically usable temperament" with "temperament that minimizes the Pythagorean comma." That is an optimization over the rank-2 prime basis {2, 3} only. Real microtonal practice optimizes over richer prime bases:
The paper's argument about Baker's theorem applies to the broader family via extended prime bases (§ 4.4 already notes this for the syntonic comma and schisma); the three sentences above should be re-scoped to "temperaments that minimize the Pythagorean comma specifically" rather than "practically usable temperaments".
3. "53-TET is impractical for keyboard construction" (§ 2.2) is outdated
§ 2.2 says:
Modern isomorphic keyboard layouts make 53-TET perfectly playable: Bosanquet's 1875 generalized keyboard (contemporaneous with Bosanquet's advocacy of 53-TET cited a few words earlier in the paper), the contemporary Lumatone keyboard, and the Kite guitar are instances. The claim reads as if the state of microtonal instrument design froze around 1900.
Severity
Proposed correction
Resolved in v1.2 (same commit as this issue — see commit range). Summary of changes:
suhr via Lean Zulip, pending consent for different attribution).ACKNOWLEDGEMENTS.mdcreated perCONTRIBUTING.mdconvention (first merged external contribution).Submitter
Reported by suhr via Lean Zulip (display-name attribution; pending reviewer's confirmation of preferred credit form). Expertise evident from the response: microtonal music theory, continued-fraction approximants, modern isomorphic-keyboard landscape.