Abstract
This paper reports a machine-checked consistency test of a classification that its source states twice, once feature by feature and once class by class. The source is chapters 1–3 of the Abhidhammattha-saṅgaha, a standard manual of the Theravāda Buddhist Abhidhamma, which classifies consciousness into 89 types (121 when the supramundane types are reckoned by meditative absorption) and states which of 52 mental factors combine with each type. In the Lean 4 theorem prover, a nine-clause generator builds the types as a product of chapter 1's classification axes, and eighteen rules over those axes, none naming an individual type, assign each type its factors. Checked by kernel evaluation against a separate answer key cited to the Chaṭṭha Saṅgāyana (CST) edition, the rules reproduce every per-type and per-factor count of chapter 2. Nine deliberate faults each make the check fail. The result is mutual consistency of the chapter's two methods under one 27-clause rule set, not a derivation independent of the text, and the rule set is not claimed to be unique; the enumeration of the 89 and 121 from the axes has a public precedent and is not claimed. Three further checks each run on one list: the Dhammasaṅgaṇī's canonical list for the first wholesome type names 29 distinct factors, the count its fifth-century commentary also gives; the manual's 38 for that type is exactly those 29 plus nine factors the commentary supplies; and the Cambodian Buddhist Institute edition and the CST name the same 56 terms in the same order.
Creative Commons License
This work is licensed under a Creative Commons Attribution 4.0 License.
Recommended Citation
Ly, Thon, "Machine-Checked Consistency of a Buddhist Classification: Lean Theorems for the Abhidhamma's 89 and 121 Types of Consciousness — Formal Verification of a Class–Feature Incidence Structure Against Both Stated Projections, with Mutation Testing", Technical Disclosure Commons, ()
https://www.tdcommons.org/dpubs_series/12054