Auditing translation decisions: what a proof assistant shows, and where it stops, in Buddhist accounts of karmic continuity

When a text is formalized in a proof assistant, the decisive steps are the decisions that turn sentences into formulas, and these decisions can fix the results. We present a way of auditing them, with a case study: Buddhist accounts of how acts bear re- sults that ripen later although there is no enduring self. In Lean 4 without Mathlib we encoded accounts attributed to the Vaibhāṣika, Sautrāntika and Yogācāra schools, the avipraṇāśa position of Mūlamadhyamakakārikā 17, the Pudgalavāda and Mad- hyamaka refusals of the tetralemma corners, and the statement “I have no thesis”. No-self is not encoded as a separate premise; the reading of the person as a series is built in. The study was pre-registered, with a post-hoc addendum after the first code review. Every hypothesis is tied to a primary-source passage, and all quotations were checked verbatim against open editions (86 of 86 in the final version). Review was carried out by simulated reviewer roles of one model family, which are not inde- pendent. The main contribution is a catalogue of 23 encoding decisions that fixed or distorted results, each with its place in the code and the way it was found, together with a single labelling of results (trivial, reconstruction, non-trivial) and of claims (verification stages W, Q, M). The case study gives a modest result: each encoded ac- count is consistent, and Lean reproduces known positions, among them the classical objection that a momentary act does not by itself reach its fruit. We distinguish three kinds of statements. Statements about mechanisms (trace, seed, store) have models in classical logic; the refusal of all four tetralemma positions needs truth-value gaps; “I have no thesis” is contradictory with one standpoint and representable with two. The boundary so drawn is the boundary of what can be asserted within a formal frame, and it is relative to the frame. Madhyamaka also has a conventional account of karma, which we did not encode. Meditative experience is neither formalized nor touched. The work gives no verdict on any school or doctrine.