An open-source research programme on structural incompleteness in domains organized around a minimal generative operation, and on the shared mathematical and epistemological floor underneath.
This repository holds the papers themselves, the open validation items they contain, and the infrastructure for anyone who wants to read, comment, verify, correct, or formalize their claims.
New here, or not a specialist? Skip the jargon below and read
START-HERE.md— the whole idea in plain English in five minutes, starting from why there are twelve notes in the Western musical tradition. No background needed.
Project status. Working drafts. Arguments marked
[REQUIRES FORMAL VALIDATION]need external expert engagement before the claims can be advanced as settled. Nothing in this repository is peer-reviewed in the traditional sense; validation happens here, in the open.
| Layer | Status | Where |
|---|---|---|
| Four-cell partition | [K] kernel-checked (Lean) | lean/FalseWorkPapers/Positions/Partition.lean, preprints/four-position-partition/paper.md |
Music anchor (Div12, tritone kernel) |
[K] witness | lean/FalseWorkPapers/Examples/DivisorLattice12.lean, Wolfram wolfram/music-anchor/ |
| Epistemic dependency / correction architecture | Paper 2 → arXiv v1 (June 2026); Stage 4 (T&N convergence) open | papers/paper2-epistemic-dependency/ |
| Practice domains (cinema, literature, …) | [A] classifier + expert correspondence | falsework.dev/kernels |
| Cross-domain derivation theorem | [O] schema + open validation | validation/claims/five-position-derivation-formalization.md |
The critical path: close music + Paper 2 before expanding domain or metaphysics claims.
All papers are authored by Chris Brink (independent researcher), distributed under CC-BY-4.0, and cite each other as a coherent series. Papers 1–5 form the core research programme; paper 6 is an exploratory / practitioner-outcome companion. The Markdown source is authoritative; each released DOCX is preserved in the per-paper archive/ subdirectory.
| # | Paper | Current version | Latest DOCX archive |
|---|---|---|---|
| 1 | Kernels and Commas: A Structural Derivation of Universal Positions in Domains with Self-Limiting Generative Operations | v11.8 | v11.7 † |
| 2 | Epistemic Dependency as Structural Condition | v8.18 (arXiv v2 prep) | v8.2 † |
| 3 | The Distinction Operation and the Generative Floor | v9.4 | v9.3 † |
| 4 | Mathematics as Comma: The Distinction Operation and the Unreasonable Effectiveness of Formal Systems | v5.3 | v5.3 |
| 5 | The Pythagorean Comma, the Irrationality of √2, and a Shared Diophantine Floor | v1.3 | v1.3 |
| 6 | Canonical Confrontation: Kernel/Comma Topology and the Structural Production of Canonical Status (exploratory companion) | v2.1 | v2.1 |
† Paper 1 v11.8 and Paper 3 v9.4 are top-matter revision-note bumps recording an architectural refinement of the position dictionary (five positions → four-position partition + Commitment gate; see papers/comma-formal-structure-note.md). Body-level rewriting is deferred to Paper 1 v11.9 / Paper 3 v10.0; DOCX archives for v11.8 / v9.4 are deferred to those body-level revisions. The Markdown is authoritative; the latest DOCX archive (v11.7 / v9.3) carries the substrate against which v11.8 / v9.4 record their architectural note. Paper 2 v8.18 (arXiv v2 prep): Markdown authoritative; DOCX archive still v8.2 (deferred post-arXiv).
A paper-by-paper overview with abstracts, current open validation items, and cross-reference graph lives at papers/INDEX.md. The canonical statement of the refined four-cells-plus-gate architecture lives at papers/comma-formal-structure-note.md, with the version-tracked validation status at validation/claims/five-position-derivation-formalization.md (currently v0.6). The previously-blocking absence of HeytingAlgebra (Subobject _) on elementary topoi in Mathlib4 has been closed locally by an in-repo construction following Mac Lane–Moerdijk IV.6 Proposition 2; the four-position partition theorem and the asymptotic-residue theorem are both lake build-checked with no sorry anywhere in the formalization tree, and the construction has been submitted upstream as Mathlib PR #39618 (opened 2026-05-20, CI green, closed without merge 2026-05-28 under the project's new-contributor AI-use policy). Full history at lean/HEYTING-GAP.md.
Focused, peer-review-targeted mathematical papers extracted from the framework live under preprints/. These are narrower in scope and mathematics-only in voice, distinct from the broader framework essays above. The current preprint:
- A Four-Position Partition of Morphisms in Elementary Topoi with Distinction Structure — Chris Brink, May 2026, preprint not yet submitted. Formalizes the framework's central structural claim as a theorem about elementary topoi with non-trivial distinction structure. Kernel-checked in Lean 4 against Mathlib4; supporting
HeytingAlgebra (Subobject _)instance upstreamed as Mathlib PR #39618. Self-contained and verifiable in an evening by a categorically literate reader. Seepreprints/README.mdfor the register and conventions.
Depending on what brought you here — sorted by the question you're asking, not your job title:
- "Just tell me what this is, plainly" →
START-HERE.md(five minutes, no jargon, starts from music) and then Discussions if you want to react or ask anything. - "I want the whole programme in one approachable walk" →
papers/field-guide.md(The Distinction That Does Not Cancel) — ontology → four-fold → why-twelve → domains → method → corpus map. Thenpapers/bach-at-the-kernel.mdfor the deep music specimen. - "Why are there twelve notes in Western music? What does this have to do with Bach, Coltrane, Schoenberg?" →
START-HERE.mdcovers it, thenvalidation/claims/why-twelve-tet.mdfor the proof. - Curious, want the narrative gist → falsework.dev/thesis (the narrative argument, ≈10-minute read) or falsework.dev/theory (the full technical exposition; includes a 3-minute summary at the top).
- Mathematician / category theorist / logician → Paper 1 § 2 and § 2.1 (the Lawvere fixed-point unification of the Cantor and Gödel groundings, and the G ∧ R ∧ C ↔ Lawvere's-hypothesis correspondence reframing the extension-to-practice problem; tracked at
validation/claims/lawvere-unification-of-formal-groundings.md), Paper 3 § 4 (the six-point music-kernel categorical claim needing verification), and Paper 5 (Baker's theorem applied to the Pythagorean comma and the irrationality of √2). Concrete open items: Issue #1, Issue #2, Issue #4. - Philosopher / humanist / reception studies → Paper 2 (epistemic dependency as structural condition in AI-assisted scholarship) and Paper 6 (canonical status as the structural trace of kernel-level confrontation — exploratory companion). Open item with a testable empirical prediction: Issue #8.
- Philosopher of science (emergence, multi-level ontology, philosophy of physics) → Paper 1 § 5.4 and Paper 3 § 7.3 cite Ellis (2016) and Cartwright (1999) as adjacent scholarly precedent for the paper's domain-dependent-formalism posture. Whether the citations are correctly scoped is an open validation claim: Issue #10.
- Practitioner (composer, architect, filmmaker, software engineer) → falsework.dev/kernels (the registered kernels as a working navigational instrument) and falsework.dev/structural-profile (the analysis pipeline that generates structural profiles of specific works).
- Lean 4 / formalization contributor →
lean/README.md— formalization targets, including (i) the music-kernel endofunctor formalization (Paper 3 § 4, Tier 1–3 entries), and (ii) the four-position-partition + Commitment-gate formalization underlean/FalseWorkPapers/Positions/(partition theorem and asymptotic-residue theorem both kernel-checked; full tree sorry-free; Commitment gate at schema level) with thepapers/comma-formal-structure-note.mdexpository companion. A single-page proof-dependency-and-status diagram lives atlean/ARCHITECTURE.md. A first Mathlib contribution drawn from this work is open as PR #39618.
The papers make claims that cross mathematics, physics, philosophy, formal logic, musicology, and the practice-based creative domains. Most interdisciplinary work of this kind is either published privately and never validated, or locked inside closed peer-review processes whose outputs are binary (accept/reject) rather than structured. This project operates on a different premise: validation is a distributed, open, modular process, and the honest state of a research programme is legible to anyone who wants to inspect it.
Concretely:
- Every
[REQUIRES FORMAL VALIDATION]flag in the papers is mirrored as a structured entry invalidation/OPEN.md, with an authoritative claim statement invalidation/claims/and a matching GitHub Issue for discussion. - Any mathematician, philosopher, logician, or domain expert who wants to verify, correct, or dispute a claim can do so by opening an issue or PR. Acceptance criteria are documented in
CONTRIBUTING.md. - Resolved validations move to
validation/RESOLVED.mdwith the validator's name (with permission) and a pointer to the revision that absorbed their feedback. - The
lean/directory hosts Lean 4 formalization targets — the music-kernel endofunctor (six points, Tier 1–3) and the four-position-partition + Commitment-gate formalization underlean/FalseWorkPapers/Positions/(partition theorem kernel-checked; Mathlib PR #39618 submitted for the underlyingHeytingAlgebra (Subobject _)construction). Open to collaborators. Seelean/README.md. - Outreach drafts for specific validator engagements (mathematicians, Lean community, philosophers) live in
docs/outreach/— also version-controlled, also open to improvement.
The papers describe a framework; the framework runs live as an instrument:
- falsework.dev/kernels — the registered-kernels instrument. Each kernel from the papers (the Fifth, the Cut, the Mark, Gravity, the Conditional Branch, the Wave Function, Syntax) appears here with its four-criteria evidence, field topology, and the works empirically classified against its territories. This is where the abstract categorical sketch becomes a working navigational object.
- falsework.dev/thesis — the narrative argument with historical and scholarly precedents cited inline (Spencer-Brown, Bruner, Meyer & Land, Feynman, Hurwitz/Frobenius, Baker, Lakatos, and the domain-specific precursors each kernel inherits).
- falsework.dev/theory — the full technical exposition. Dual-register: a 3-minute summary and a complete reading. Links back to each paper in this repository at the relevant citation.
- falsework.dev/structural-profile — the seven-stage analysis pipeline that generates structural profiles of specific works. This is where the framework becomes a testable instrument: profiles are hypotheses the papers predict, and their empirical behavior is part of the framework's validation record.
The site is a separate codebase (proprietary). The papers in this repository are the formal record; the site is the applied instrument. Links are one-way: papers point at live URLs, the site points at paper markdown files in this repository.
Currently open: validation/OPEN.md · all validation-claim issues ↗ · all open-research-direction issues ↗
Already resolved: validation/RESOLVED.md tracks four categories of completed engagement — corrections (a specialist identified an error; a paper was revised), validations (a specialist reviewed a specific open claim and confirmed/corrected it), corroboration (independent scholarly work converges on a claim without reviewing FalseWork), and formalizations (machine-checkable proof of a paper claim). Scope limits are stated explicitly in every entry to guard against overstating what an external engagement produced.
Per-engagement index (across venues): docs/observations/validation-architecture-outcomes.md is the rolling record of what the validation architecture has produced in practice — one row per contact event, across scholarly correspondence, community threads, and outreach. Cross-references RESOLVED.md; neither duplicates the other. The per-engagement file also records venue-norm observations (e.g. scholarly-community norms about AI-drafted posts) that inform how future outreach is conducted.
- Start with Paper 1 § 1 for the framework. Paper 2 § 1 extends it to AI-assisted knowledge production. Paper 3 § 1 lays the Spencer-Brown / categorical foundation. Paper 4 § 1 is the strongest ontological claim. The Pythagorean companion is the technical unification of the Pythagorean comma and the irrationality of √2. The Canonical Confrontation companion is an exploratory practitioner-outcome paper applying the kernel/comma topology to the question of canonical persistence.
- Each paper's top matter includes a revision history and explicit
[REQUIRES FORMAL VALIDATION]markers. Nothing is hidden.
- Browse
validation/OPEN.mdfor the current open items. - Each claim has an authoritative statement at
validation/claims/[slug].mdand a GitHub Issue for discussion. - Follow the instructions in
CONTRIBUTING.mdfor what counts as a valid verification, correction, or disproof.
- Two formalization targets are documented:
- The six-point music-kernel formalization (Lean 4 against current Mathlib). See
lean/README.mdfor the full specification — Tier 1 entries are accessible first-PR work. - The four-position-partition + Commitment-gate formalization under
lean/FalseWorkPapers/Positions/, with thepapers/comma-formal-structure-note.mdexpository companion. The partition theorem (four_position_partition) and the asymptotic-residue theorem (refusal_residueunder theHasIrregularKernelhypothesis) are bothlake build-checked against an in-repoHeytingAlgebra (Subobject _)construction atlean/FalseWorkPapers/Heyting/SubobjectInstance.leansubmitted upstream as Mathlib PR #39618. The entire formalization tree is sorry-free; one framework-level open conjecture (the refusal bridge) is carried atvalidation/claims/refusal-bridge.md.
- The six-point music-kernel formalization (Lean 4 against current Mathlib). See
- Any categorical, number-theoretic, or set-theoretic formalization contribution is welcome. Acceptance criterion: passing
lake buildwith the claimed theorem proved.
The principal theorems of the ordinary-elements preprint can be verified without trusting any code in this repository, using comparator:
- Read
lean/Challenge.lean— a short, self-contained file that imports Mathlib only and states the claimed theorems (withsorry). Check that the statements say what you think the paper claims. Its counterpartlean/Solution.leanimports the project code that proves them. - Run comparator (Linux; from
lean/, withlandrun,lean4export, andcomparatorbuilt at the pinned toolchain on yourPATH):
cd lean/
lake exe cache get
lake build && lake build Challenge Solution
lake env comparator config.jsonOn success, comparator guarantees Solution proves the exact statements in Challenge.lean, uses only propext / Classical.choice / Quot.sound, and is accepted by the Lean kernel — all inside a landrun sandbox, so you never execute untrusted project code. CI runs this on every push touching lean/ (workflow). Machine-readable project metadata is in formalization.yaml. Full setup instructions are in lean/README.md.
Scope note. The no-sorry / no-native_decide claims attach to the files cited by the preprint's §10 audit table (listed in formalization.yaml). Two files elsewhere in lean/FalseWorkPapers/Examples/ — MusicKernelZMod12Accum.lean and PythagoreanCommaConvergents.lean, which belong to the music-kernel track of a different paper — do use native_decide and are outside the preprint's claims and the comparator scope.
- Open an issue using the Open Research Direction template. It will be added to
validation/OPEN.mdafter a brief review.
The series was developed with substantial AI assistance. Claude (Anthropic) was the primary development collaborator — used for drafting, structural editing, and sustained dialogue through the framework's formation. Other systems used in supporting roles include GPT (OpenAI, for independent formalization attempts and cross-checking), Grok (xAI, for adversarial review), and Gemini (Google, in the specific documented incident Paper 2 § 6.5 treats as a case of inherited validity without correction architecture).
Paper 2 is the canonical disclosure: it documents the AI-assisted development of this framework as a live case study and treats epistemic dependency in AI-assisted scholarship as a structural condition rather than a peripheral limitation. What differs between knowledge-producing systems is not the presence of epistemic dependency but the maturity of the correction mechanism available to detect and address it. Correction architecture — dependency prediction, expert correspondence, contemporaneous documentation — is built into the framework's design and into how this repository operates: the validation queue, the PR workflow, and the public commit history are the correction mechanism Paper 2 argues for.
- Papers (all prose, figures, citations in
papers/,validation/,docs/): Creative Commons Attribution 4.0 International (CC-BY-4.0). - Code (
lean/, any future tooling): Apache License 2.0.
You may read, copy, translate, redistribute, and build on any of the content, commercial or not, provided you give appropriate credit and indicate changes.
Every tagged release of this repository is archived to Zenodo and assigned a permanent Digital Object Identifier (DOI). Two DOI variants are available:
- Concept DOI —
10.5281/zenodo.19673672— always resolves to the most recent release. Use this when citing the project as a whole. - Version DOI — e.g.
10.5281/zenodo.22016585for Release 2026.08 (10.5281/zenodo.19673673for Release 2026.04) — resolves to one specific release. Use this when citing a specific claim at a specific version, because subsequent revisions may alter it.
Project-level citation (concept DOI — follows the latest release):
Brink, C. (2026). The FalseWork Papers. Zenodo. https://doi.org/10.5281/zenodo.19673672
Release-level citation (version DOI — pinned to Release 2026.08, which timestamps the aperture programme: the preprint, the kernel-checked closed form, and the Mathlib study):
Brink, C. (2026). The FalseWork Papers (Release 2026.08). Zenodo. https://doi.org/10.5281/zenodo.22016585
Paper-at-version citation (most precise — pinned to a specific paper inside a specific release):
Brink, C. (2026). Kernels and Commas: A Structural Derivation of Universal Positions in Domains with Self-Limiting Generative Operations (v11.8). In The FalseWork Papers (Release 2026.08). Zenodo. https://doi.org/10.5281/zenodo.22016585
BibTeX, RIS, and EndNote entries for any version can be exported directly from the Zenodo record page. Both concept and version DOIs resolve programmatically — see the Zenodo REST API for structured access. Each subsequent release (per-paper or collection-wide) will receive its own version DOI under the same concept DOI.
- Author: Chris Brink — Independent researcher
- Email:
chris@falsework.dev - Site: falsework.dev
- Preferred channel for validation and correction: GitHub Issues
- Email is fine for pre-submission discussion or any interaction you would prefer to start privately. Anything that becomes part of the project's validation record will be moved to a public issue with your consent.
See ACKNOWLEDGEMENTS.md for the running record of external contributions. Every validator, corrector, and formalizer who contributes substantively to the project is credited there by name (with their permission, or by the handle under which their contribution was made). The author gratefully accepts reference-letter requests from graduate-student contributors.