Conventional Knowledge Commits v0.1.0

Summary

Conventional Knowledge Commits (CKC) is a convention for commit messages that record knowledge work: mathematical claims and proofs, and empirical scientific findings. It builds on Conventional Commits 1.0.0.

CKC is a strict superset. Every CKC commit is also a valid Conventional Commit. It adds a research vocabulary (commit types), a way to record how established a claim is (its status), and structured footers (git trailers). Together these let tooling read the commit history and answer questions a plain log cannot: what is conjectured, what is proved, what rests on a cited axiom, what has been refuted, and what a refutation or a closed gap means for everything that depended on it.

<type>[~][(scope)][!]: <description>

[body]

[footers]

Why use CKC

The commit log becomes an honest, current record of what is proved, what is assumed, what is open, and what has been disproved, without anyone keeping a separate status document.
The relation footers form a dependency graph (see the ClaimGraph). When a claim is refuted, you can see which results now depend on something false. When a gap is closed, the results above it are promoted.
Negative results have a place. Counterexamples, null results, and failed replications are normal commit types, so they are recorded instead of quietly dropped.
Provenance travels with the work: the Lean name and #print axioms for a proof, the dataset, seed, and effect size for an experiment. Claims stay auditable and reproducible.
There is nothing new to install. A CKC commit is a Conventional Commit, so existing changelog and lint tooling keeps working, and CKC-aware tooling reads the extra types and footers.
Collaborators and reviewers share one vocabulary for the state of the work.

The two axes

Software change has one scale: backward compatibility, which Conventional Commits maps onto SemVer (fix is a PATCH, feat is a MINOR, BREAKING CHANGE is a MAJOR). Knowledge change has two independent scales, and CKC keeps them apart on purpose.

Dependency impact. Does this commit invalidate things built on it? This is the direct SemVer analog. It lives in the type and the ! marker, and it is a fact about history that does not change later. The values are a repair (PATCH-like), an additive result (MINOR-like), or a breaking change (MAJOR-like) such as refuting, retracting, re-stating, or redefining something that others depend on.
Epistemic status. How strongly is the claim established right now? This has no analog in Conventional Commits, and it is the real extension. It lives in the Status: footer, and it is advanced by later commits, never by editing an earlier one. The ladders are conjectured to proved to machine-checked for mathematics, and hypothesis to measured to replicated for science.

Keeping the two apart is what lets CKC leave history untouched. When a sorry is closed months later, you do not rewrite the old commit's type. You add a new formalize commit that moves the Status: footer from math.open to math.machine-checked. The type says what happened; the footer says what is believed now.

Profiles

A profile is a domain vocabulary layered on the shared core. CKC ships two:

the proof profile, for mathematics and formal proving (the reference tooling is Lean and Mathlib);
the science profile, for empirical work (experiments, data, replication).

Each profile defines its own commit types, status values, and trusted-base markers. The shared core types (conjecture, lit, review, refute, retract, expose, meta) work in either. The type you choose implies the profile: formalize is a proof commit, experiment is a science commit, conjecture is shared. A Profile: footer is used only to disambiguate a commit that genuinely spans both. The per-profile detail is in the proof profile and the science profile.

Specification

The key words "MUST", "MUST NOT", "REQUIRED", "SHALL", "SHALL NOT", "SHOULD", "SHOULD NOT", "RECOMMENDED", "MAY", and "OPTIONAL" are to be interpreted as described in RFC 2119.

Every CKC commit MUST be a valid Conventional Commits 1.0.0 message: a type, an OPTIONAL scope, an OPTIONAL !, a REQUIRED terminal colon and space, and a description, with an OPTIONAL body and OPTIONAL footers separated by blank lines.
The type MUST be a noun. It SHOULD be one of the CKC types: a shared type (conjecture, lit, review, refute, retract, expose, meta), a proof-profile type (state, proof, formalize, axiomatize, strengthen, generalize, weaken, port), or a science-profile type (experiment, result, replicate, null, data, protocol, method, analysis, repro-fix). A Conventional Commits type (feat, fix, chore, build, ci, docs, refactor, test) MAY be used for surrounding tooling and prose.
A scope MAY be provided. For knowledge commits it SHOULD name the claim or area the commit concerns, for example formalize(fubini):.
Dependency impact (axis 1). A commit that invalidates results which depend on it (refuting, retracting, re-stating a theorem so dependents no longer hold, redefining a term, or correcting data in a way that changes downstream conclusions) MUST signal it, either with a ! immediately before the :, or with a BREAKING CHANGE: footer (synonym BREAKING-CHANGE:), as in Conventional Commits. A BREAKING CHANGE: footer, when present, MUST name the affected claim(s). A commit MAY make the impact explicit with an Impact: patch | minor | major footer.
Epistemic status (axis 2). A commit that asserts or changes the status of a claim SHOULD carry a Status: footer with a namespaced value (math.* or sci.*; see the profiles). Status MUST NOT be changed by amending or rewriting an earlier commit. It is advanced, or demoted, by a new commit referencing the same claim.
Trusted-base markers. A commit whose results rest on a newly introduced assumption MUST declare it with an uppercase footer, in the manner of BREAKING CHANGE. In the proof profile that is AXIOM: (a cited or added axiom) or OPEN: (a sorry, admit, or sorryAx). In the science profile it is ASSUMES: (an untested assumption) or UNREPLICATED: (a single, un-replicated run). A trusted-base marker affects the status (it becomes axiomatised, open, or unreplicated). It is also a dependency-breaking change only when it invalidates an existing dependent.
Stable identity. A claim, theorem, definition, or hypothesis that other commits reference MUST have a stable identifier (see Identifiers). In the proof profile this is the Lean fully-qualified name (Lean: or Formal-Statement: lean:<FQN>) and an optional blueprint label. In the science profile it is a curated slug registered in the claims registry. A commit SHOULD NOT silently rewrite a claim under an unchanged identifier. Use Supersedes: or a breaking change.
Relations. Footers that express a relation between claims MUST use the git-trailer form (Token: value, with - in place of spaces in the token) and MAY be repeated. The relation tokens are Depends-On, Assumes, Proves, Refutes, Disproves, Supersedes, Retracts, Invalidates, and Closes. These edges define the knowledge graph (see the ClaimGraph).
Provenance. Verification and provenance footers SHOULD be recorded where they apply: Lean, Formal-Statement, Axioms, Verified-By, Proof-Hash, Cites, Phase, Gate for proofs; Dataset, Protocol, Method, Sample-Size, Effect-Size, CI, P-Value, Seed, Hardware, Metric, Pre-Registration for science. For a formalized result, the Axioms: footer SHOULD be the literal output of #print axioms.
Negative results are normal commits. Counterexamples, disproofs, null results, and failed replications MUST be expressible as ordinary commits (refute, null, or a replicate with a sci.not-replicated status). They are never hidden, deferred, or relabelled as a fix.
Granularity. A commit SHOULD concern one claim, theorem, or finding, so the knowledge graph has well-defined nodes. Bundle only changes that are genuinely inseparable.
The ~ marker. A ~ MAY be placed immediately after the type (for example axiomatize~(exp-sum):) to flag at a glance that the commit carries a trusted-base caveat (an AXIOM:, OPEN:, ASSUMES:, or UNREPLICATED: footer). A tool MAY also accept it just before the :. The footer is the record that tooling reads. The ~ is a convenience for human readers and MUST NOT be the only indicator.
The units of information in CKC MUST NOT be treated as case-sensitive by implementors, except for the uppercase trusted-base and breaking tokens (BREAKING CHANGE, AXIOM, OPEN, ASSUMES, UNREPLICATED), which MUST be uppercase.

Relation to SemVer and the payoff

The artifact CKC primarily serves is the knowledge dependency graph (see the ClaimGraph). From the relation footers, tooling can propagate a refutation to its dependents and mark them as in question, promote dependents when a gap closes, and produce both a status report (what is proved, axiomatised, open, or replicated) and, if you want one, a SemVer-style release version for a knowledge artifact such as a paper or a formalized library: a breaking knowledge change is a MAJOR release, an additive result or replication is a MINOR, a repair or cleanup is a PATCH.