Machine-Checked Consistency of a Buddhist Classification: Lean Theorems for the Abhidhamma's 89 and 121 Types of Consciousness — The Counts Check

A pre-registered formalization of the Abhidhammattha-saṅgaha's combination rules, collated against the Chaṭṭha Saṅgāyana, with the Dhammasaṅgaṇī list collated against its commentary and against the Cambodian edition The Theravāda Abhidhamma classifies consciousness into 89 types (121 when the supramundane types are reckoned by jhāna). It also states, factor by factor and type by type, which of 52 mental factors (cetasika) combine with each type. This paper reports a formal verification in the Lean 4 theorem prover of those statements, as given in chapters 1–3 of the Abhidhammattha-saṅgaha. The formalization has two parts. A nine-clause generator builds the types from the classification axes of chapter 1. Eighteen rules, each stated over classes of consciousness and none naming an individual type, give each type its factors. Checked by kernel evaluation against a key cited paragraph by paragraph to the Chaṭṭha Saṅgāyana (CST) text, the formalization reproduces: - the 89 and the 121 (from the generator); - every per-type combination count in chapter 2 (from the rules); - every per-factor count in chapter 2, in the text's own mixed reckonings (from the rules); - chapter 3's counts by feeling and by root (from the generator's axes, without the rules). Nine deliberate breaks each make the check fail. What this establishes is mutual consistency: the chapter's two methods, factor by factor (sampayoga-naya) and type by type (saṅgaha-naya), agree with each other under a single rule set of 27 clauses for 121 types, and the generator's axes agree with chapter 3. It is not a derivation independent of the text, and the rule set is not claimed to be the only one that would pass. The enumeration of the 89 and 121 from chapter 1's axes has a public precedent nine days older than this paper's generator (§4.2); it is reported here, not claimed. Three further results concern textual layers and editions, each run on one list: - The canon's own list for the first wholesome sense-sphere type (Dhammasaṅgaṇī §1) names 29 distinct factors under a synonym map fixed before the text was read (Appendix A). The count is consistent with the one the fifth-century commentary gives (the Aṭṭhasālinī's samatiṃsa dhammā, thirty with consciousness). It is not independent of it, since the 52-factor scheme the map targets inherits the commentary's identifications. - The Saṅgaha's 38 for that type is exactly those 29 plus nine further factors. The nine are first named for this list by the commentary, which presents them as the Buddha's, drawn from sutta passages. The Saṅgaha inherits them as members and arranges them in its own classes. - The Cambodian Buddhist Institute edition names the same 56 terms, in the same order, as the CST for that list. Every spelling difference was checked against the printed page. The predictions were pushed to a public repository before the formalization was written (first file) and before either edition of the Dhammasaṅgaṇī was read (second file). The Saṅgaha's tables were known to the author. The chapter 3 results, the dissent's figure and the 29 + 9 = 38 inheritance were not predicted. The predictions are entered in the public prediction register. Keywords: formal verification, Lean theorem prover, Abhidhamma, Abhidhammattha-saṅgaha, Buddhist philosophy of mind, classification consistency, incidence matrix, combinatorial enumeration, mutation testing, textual criticism, collation, Pāli canon, Dhammasaṅgaṇī, Aṭṭhasālinī, Khmer Tipiṭaka, pre-registration, defensive publication. --- Provenance. This paper is part of the THonly research corpus, dedicated to the public domain under CC0 1.0. The canonical version is at https://thonly.org/research/the-counts-check. Its SHA-256 is edc3fa58718e8792c3a798a67591509fddb383d0a5cc116a242d2f3476635795, independently timestamped to the Bitcoin blockchain via OpenTimestamps and signed under RFC 3161 by three trust authorities, one of them eIDAS-qualified. AI co-authorship is disclosed. Miss Aquarius is the consistent name used for the AI collaboration across all venues.