--- /dev/null
+\section{Commit annotation}
+
+We annotate each Topbloke commit $C$ with:
+\gathbegin
+ \patchof{C}
+\gathnext
+ \baseof{C}, \text{ if } C \in \py
+\gathnext
+ \bigforall_{\pq}
+ \text{ either } C \haspatch \pq \text{ or } C \nothaspatch \pq
+\gathnext
+ \bigforall_{\pqy \not\ni C} \pendsof{C}{\pqy}
+\end{gather}
+
+$\patchof{C}$, for each kind of Topbloke-generated commit, is stated
+in the summary in the section for that kind of commit.
+
+Whether $\baseof{C}$ is required, and if so what the value is, is
+stated in the proof of Unique Base for each kind of commit.
+
+$C \haspatch \pq$ or $\nothaspatch \pq$ is represented as the
+set $\{ \pq | C \haspatch \pq \}$. Whether $C \haspatch \pq$
+is in stated
+(in terms of $I \haspatch \pq$ or $I \nothaspatch \pq$
+for the ingredients $I$)
+in the proof of Coherence for each kind of commit.
+
+$\pendsof{C}{\pq^+}$ is computed, for all Topbloke-generated commits,
+using the lemma Calculation of Ends, above.
+We do not annotate $\pendsof{C}{\py}$ for $C \in \py$. Doing so would
+make it wrong to make plain commits with git because the recorded $\pends$
+would have to be updated. The annotation is not needed in that case
+because $\forall_{\py \ni C} \; \pendsof{C}{\py} = \{C\}$.
+