This file records external engagements with the paper series that have produced outcomes the papers absorbed — corrections, validations, corroborations, and formalizations. It serves as the project's memory of what the validation architecture has actually produced, and distinguishes between types of engagement for readers inferring the programme's external reception.
Four categories are kept deliberately distinct:
- Corrections. A specialist identified a specific error, and a paper was revised to fix it.
- Validations. A specialist reviewed a specific open claim and confirmed or corrected its formulation.
- Corroboration. Independent scholarly work (pre-existing or contemporaneous) converges on a paper's claim without the scholar having reviewed FalseWork at the programme level. This is not validation in the review sense — it is inter-framework agreement that counts as empirical grounding for a claim without counting as endorsement of the framework producing the claim.
- Formalizations. A formal proof, Lean verification, or equivalent machine-checkable derivation of a paper claim.
Each entry names the contributor's scope carefully, to avoid overstating what they did. Scope limits are stated explicitly because overclaiming is the dominant failure mode for scholarly-infrastructure projects of this kind.
- Contributor: suhr (Lean Zulip display name; attribution placeholder subject to update on request).
- Venue: Lean Zulip chat,
#new members, topic Music-kernel + Pythagorean comma formalization target, 2026-04-19 reply. - Scope: three corrections to Paper 5 v1.1 —
- § 2.2 continued-fraction narration skipped the
24/41convergent oflog₂(3/2)and referred to31/53as "the next" convergent after7/12. Fixed: narration now runs7/12 → 24/41 → 31/53, with41-TETnamed alongside12-TETand53-TET. - §§ 2.2, 4.2, 7.1 claims about "practically usable temperaments" conflated minimization of the Pythagorean comma with practicality in other harmonic contexts (11-limit, 7-limit, 5-limit — Baker-type problems over extended prime bases). Fixed: all three statements re-scoped to "equal temperaments that minimize the Pythagorean comma specifically," with explicit acknowledgement of other harmonic-optimization targets.
- § 2.2 "53-TET is impractical for keyboard construction" was anachronistic given isomorphic-keyboard instruments (Bosanquet 1875; Lumatone; Kite guitar). Fixed: remark removed; replaced with a short note pointing to the isomorphic-keyboard landscape.
- § 2.2 continued-fraction narration skipped the
- Resolution: corrected. Paper 5 v1.1 → v1.2. Tracked at Issue #9. Archived at
papers/pythagorean-shared-floor/archive/v1.2.docx. - Scope limits: the corrections resolved the three specific errors listed. The six-point music-kernel check (
music-kernel-umbrella) and the Pythagorean explanatory debts (pythagorean-explanatory-debts) remain open. - Crediting:
ACKNOWLEDGEMENTS.mdunder Corrections. - Follow-on pointer (2026-04-19, same Zulip thread): suhr additionally recommended the Xenharmonic Wiki (
https://en.xen.wiki/) as a community reference for continued microtonal practice. Integrated into Paper 5 v1.3 as a new Further reading — community resources subsection in the References (not a correction; a resource addition). - Follow-on theoretical pointer (2026-04-19, same Zulip thread): suhr additionally noted that the classical continued-fraction characterization of optimal N-TETs generalizes via the theory of MOS (Moment of Symmetry) scales and the Stern-Brocot tree, with Xen Wiki references at
5L_2sandScale_tree. Integrated intoclaims/optimal-ntet-continued-fraction.mdas a new Broader theoretical context subsection (not a correction of the claim statements; a refinement of framing relevant to how the claim would slot into a broader Lean xenharmonic library should one emerge). No paper change. - Third follow-on theoretical pointer (2026-04-19, same Zulip thread): suhr further noted the Riemann zeta function approach to temperament optimization (peaks of
|ζ(s)|along specific lines in the critical strip correspond to equal temperaments that approximate all prime harmonics simultaneously), referencing Xen Wiki'sThe_Riemann_zeta_function_and_tuning. Integrated as a one-paragraph extension to the Broader theoretical context subsection of the same claim file, completing a three-framework trajectory (continued fractions → MOS / scale tree → Riemann zeta). Outside Paper 5's current scope; noted for theoretical completeness. No paper change.
2026-06-11 — Alex Citkin: prior-art adjudication of the ordinary-element uniqueness (first validation engagement)
- Contributor: Alex Citkin, author of "An Algebraic Proof of the Nishimura Theorem" (Logics 2(4), 2024) — the load-bearing [C] citation for the math anchor's
Z_ntruncations. - Venue: email reply (2026-06-11) to the prior-art inquiry drafted in
docs/outreach/citkin-email.md(sent 2026-06-10; full outcome recorded there). - Scope: adjudication of novelty standing, not of proof correctness (the proofs are machine-checked; he was not asked to review Lean).
- Question (a) — uniqueness of the ordinary element in one-generated Heyting algebras (
nishimura_ordinary_unique): adjudicated folklore. He is "not aware of any known proofs," and supplied the reason it is specialist-obvious: the Rieger–Nishimura ladder has a single ordinary element, the finite one-generated algebras are its quotients, and regularity/density are preserved under quotients. Standing after adjudication, corrected the same day: reading his current preprint (arXiv:2512.05633, Dec 2025) revealed the statement is in print — asserted there without proof (p. 13: "the algebra Zn contains a single ordinary element that generates the entire algebra"). Final standing: statement published by Citkin as an unproved observation; the repository's machine-checked proof is apparently the first written proof — consistent with his email, which said no known proofs. Not a new theorem. - Question (b) —
Div12 = Z_6and thep²qcharacterization: closed as unassessable through this correspondence (second reply, 2026-06-11). Frame gap: "divisor lattice of 12" parsed as a twelve-element algebra; inquiry never received. Identification remains [K+C]; novelty unestablished in his eyes. Do not pursue with Citkin. - Incidental facts supplied ([C], pers. comm.): (i) unique generator in one-generated HA of cardinality > 5; (ii) second reply: converse failure independently confirmed via
Z_6 + Z_3construction (matches enumeration witnessH8); (iii) dense-filter lemma confirmed with direct proof. - Converse failure: [K] + independently confirmed [C]; novelty low — specialist reconstructs readily once posed; same standing shape as (a).
- Question (a) — uniqueness of the ordinary element in one-generated Heyting algebras (
- Resolution: uniqueness novelty downgraded as before. Question (b) closed unassessable (not open). Converse and dense-filter move from kernel-checked alone to kernel-checked + independently confirmed; not promoted to novel results.
- Scope limits: adjudication of three math-anchor lattice substrate facts only — not the four-position partition, music weld, or any [A]-level framework claim. Not "Citkin validated FalseWork."
- Crediting: permission granted (second reply, 2026-06-11): "And if you wish, you can include a reference to me." Cited as A. Citkin, personal communication, 2026-06-11 in validation records and
ACKNOWLEDGEMENTS.md. Correspondence closed after three contacts.
Dmitri Tymoczko — Paper 1 § 4.1: three-way Coltrane discrimination and exploitation-target refinement
- Contributor: Dmitri Tymoczko (Professor of Music, Princeton University).
- Primary sources: Tymoczko (2006), "The geometry of musical chords," Science 313(5783), 72–74. Tymoczko (2011), A Geometry of Music: Harmony and Counterpoint in the Extended Common Practice, Oxford University Press.
- Additional engagement: personal correspondence with Chris Brink, 2026.
- Scope:
- Independent corroboration of FalseWork's three-way structural discrimination of Coltrane's output — without being asked to validate the classifications, Tymoczko described Coltrane's A Love Supreme, Giant Steps, and late period mapping onto the same three structural fields (diatonic, symmetric/quasi-symmetric, chromatic) from his own geometric framework, noting that this tripartition organizes the entire history of twentieth-century music from Rimsky and Debussy onward. The convergence of two independent analytical systems on the same three-way mapping is the strongest empirical grounding the music kernel has; Paper 1 names it as such.
- Refinement of the exploitation target for Giant Steps — from the circle of fifths (as originally framed by FalseWork) to the major-third cycle's specific topological properties within the symmetric territory. The refinement was absorbed into Paper 1 prior to v11.0.
- Scope limits: Tymoczko has not reviewed the five-position derivation, the G ∧ R ∧ C condition, the kernel/comma topology at the programme level, or the other papers in the series. His engagement is specific to the music-kernel empirical demonstrations. In the same correspondence, Tymoczko expressed skepticism that the Pythagorean comma remains operative as a structural condition for practitioners working in fixed temperament — an open theoretical caveat documented at Paper 1 § 4.1 and § 4.4 that is treated as a hypothesis pending the proxy feature program, not as a resolved claim. The corroboration counts as inter-framework convergence, not as endorsement of FalseWork's broader framework.
- Absorbed in: Paper 1 v11.4 § 4.1 (abstract, body text, references). Exploitation-target refinement absorbed before v11.0.
- Crediting:
ACKNOWLEDGEMENTS.mdunder Corroboration.
- Contributor: James E. Cutting (Susan Linn Sage Professor of Psychology Emeritus, Cornell University).
- Primary sources: Cutting, DeLong & Nothelfer (2010), "Attention and the evolution of Hollywood film," Psychological Science 21(3), 432–439. Cutting (forthcoming), Four cinematic forms and their psychological bases, University of Texas Press.
- Additional engagement: personal correspondence with Chris Brink, 2026.
- Scope:
- Empirical grounding for three of the four kernel criteria of the cinema kernel (prior, monogenic, inescapable) via Cutting's empirical taxonomy of cinematic forms.
- The 78-cuts-in-45-seconds threshold analysis for Hitchcock's Psycho shower scene — the anchor for Paper 1 § 4.2's exploitation-target discrimination between Hitchcock and Eisenstein's Odessa Steps sequence, both of which share the coordinate Exploitation · montage · SELF_CONSTRAINS × EXPOSED × EXPLOITS but differ in what they exploit (density vs. juxtaposition).
- Scope limits: Cutting's work does not confirm the comma formulation for the cinema kernel. Paper 1 § 4's introduction explicitly notes this: "Cutting's correspondence provides strong empirical grounding for three of the four kernel criteria (prior, monogenic, inescapable) but does not confirm the comma formulation, which is treated as a hypothesis throughout this section." The correspondence is content-specific, not a programme-level endorsement.
- Absorbed in: Paper 1 v11.4 § 4 (abstract, body text, references). Cutting's published work absorbed before v11.0; the 2026 personal correspondence cited at v11.0+.
- Crediting:
ACKNOWLEDGEMENTS.mdunder Corroboration.
None yet. The Lean 4 formalization target is specified at lean/README.md; no mathlib-level formal proof of any paper claim has been produced. Engagement is tracked at docs/outreach/lean-zulip-post.md, and the first Zulip engagement (suhr, 2026-04-19) produced a correction rather than a formalization — recorded under Corrections above.
When a new item moves from OPEN.md to this file, use:
### YYYY-MM-DD — <contributor-short-name>: <one-line description>
- **Contributor:** <name> (<affiliation if public>)
- **Venue:** <specific URL / conference / correspondence>
- **Scope:** <what specifically was done>
- **Scope limits:** <what was NOT done — guards against overstating>
- **Resolution:** corrected / verified / partially verified / disputed / withdrawn
- **Paper revision absorbing outcome:** Paper N v<X.Y> § <section> (<date>)
- **Crediting:** [`ACKNOWLEDGEMENTS.md`](../ACKNOWLEDGEMENTS.md) under <category>
The scope-and-scope-limits discipline is load-bearing. It is easy to overstate what an external engagement produced; the architecture guards against this by requiring explicit limits in every entry.