The Translation That Proves Itself

Grammar will not save you

The Vākyapadīya opens with a single verse that carries the whole system:

अनादिनिधनं ब्रह्म शब्दतत्त्वं यदक्षरम् ।
विवर्ततेऽर्थभावेन प्रक्रिया जगतो यतः ॥

anādinidhanaṃ brahma śabdatattvaṃ yad akṣaram /
vivartate 'rthabhāvena prakriyā jagato yataḥ //

Every word is a decision. Is śabdatattva (“word-essence”) a property of language, or the Absolute itself? Does vivartate mean the world is a transformation of Brahman, or its appearance without transformation? Does akṣara mean “imperishable”, “phoneme”, or, as the grammarians insist, deliberately both? Each choice yields a grammatical English sentence. The choices differ as much as materialism differs from idealism.

What settles them is not syntax. It is the commentary: the vṛtti tradition that fixes, verse by verse, which reading the text licenses. Those constraints are real. They have simply always lived in the philologist's head.

Three renderings, one verdict each

Click a rendering to see what the machine proved about it.

receipts: lean/VakyaVallari/Verses/V1_1.lean · data/contracts/1.1.json · proof page for 1.1

Translation validation, transplanted

Compiler engineers gave up on proving whole compilers correct long before they gave up on correctness. The workaround, translation validation, checks each individual run: the optimizer is untrusted, a semantic reference says what the output must preserve, and a validator checks the pair after the fact.

Transplant the pattern. The translator is the untrusted optimizer. The commentary, compiled into a per-verse semantic contract, is the reference. Lean 4 is the validator. A contract declares the verse's entities with ontological sorts, its axioms and explicit denials, the claims the accepted translation makes, and, crucially, a set of plausible mistranslations that must provably fail.

receipts: docs/specs/2026-07-16-vakya-vallari-design.md · lean/VakyaVallari/Ontology.lean · Adequacy.lean

Agents propose. Gates dispose.

One agent per verse, each given the verse record, the schema, an exemplar, and the validator as its exit gate; rounds of 9 to 30 agents with an adjudication pass between rounds; an append-only ledger recording every draft, rejection, repair, and acceptance. Acceptance is never a judgment call. A verse is done when its contract passes the validator, its Lean module compiles with zero sorry, and its entity sorts survive the corpus-wide consistency gate.

receipts: research/ledger.jsonl (99 events) · CI: pytest + lake build + zero-sorry sweep

What the gates caught

The interesting evidence is the failures. Every class of agent error that occurred is now a mechanical gate.

receipts: research/ledger.jsonl · paper §7, Table 2

The verified Brahmakāṇḍa

Of the 361 refuted mistranslations, 156 assert something the commentary explicitly denies and 205 assert what no axiom licenses. Together they form a negative image of the doctrine, in theorem form: pariṇāma for vivarta (1.1), grammar demoted from discipline to convention (1.11–1.14), inference granted an autonomy the text denies it (1.30–1.42), sphoṭa temporalized (1.75–1.77), the corrupt form elevated to equal standing with the correct (1.147–1.155).

receipts: Brahmakāṇḍa edition pages · per-verse proof pages · lake build in CI

The pun the gate refused to flatten

The consistency gate demands one sort per term, everywhere, unless the exact partition of uses is registered as polysemy with a textual justification. The registry is where mechanical discipline meets philology.

receipts: data/ontology/homonyms.json · 41 terms, 91 senses, one justification each

What Lean checks, and what it cannot

Lean verifies the internal coherence of the formalization: the accepted reading satisfies the contract, and the rivals provably do not. Whether the contract is faithful to Bhartṛhari is not a theorem and cannot be one. That link is kept auditable by construction: every axiom carries the exact commentary sentence it derives from, so checking a contract against the commentary is a lookup, not a reconstruction. The prover keeps commitments; the philologist judges them.

The audit that did not discriminate

A GPU embedding pass ranks every verse by translation–commentary similarity, as a review queue. At Book-I scale the contested flag does not separate: contested verses average 0.567 against 0.550 for uncontested ones, and the lowest tail is not enriched. The queue's head is still useful (its lowest-ranked verse, 1.74, is a contested verse whose commentary is dominated by a doxographic dispute), but the instrument is a screen, not a measure of fidelity. The paper reports the null alongside the queue.

receipts: research/audit/similarities.json · scripts/semantic_audit.py · paper §10

The translation and commentary themselves carry the interpretive standpoint of one primary source, K. A. Subramania Iyer's edition and translation of Book I with the Vṛtti (Deccan College, 1965), and the contracts inherit it. Contracts keyed to rival commentaries would turn inter-commentarial disagreement into diffable, checkable data. That is the open vine.

What an adversarial team could and could not break

Six independent reviewers, each with a fresh context and a hostile lens (logical triviality, fabrication, kernel soundness, completeness, philology, paper-versus-reality), were told to break the method, not admire it; every serious finding was then reproduced by a separate verifier. Most attacks failed — and a failed attack is evidence for the defense: no sorry, no fabricated citations, relations correctly directional, verse namespaces isolated, and a swap test that licensed zero of one verse's readings by another's contract (0 of 20,592 ordered pairs).

Three critiques landed, and each became a fix. The strongest was philological: a verbatim-citation gate cannot tell “we hold X” from “some say X”, so a handful of doxographic verses (1.102–1.113, 1.68–69, 1.70, 1.81) had encoded reported rival views as if endorsed. Those axioms now carry a reported stance held in a separate Contract.reported field, the verse wears a doxographic badge, and the proof page shows endorsed and reported axioms in separate sections. The other two: a “tautology” objection (accepted readings are subsets of the author's axioms by design — true, and now made falsifiable by the corpus-wide discriminativity gate above), and hygiene (a contract may no longer both license and deny the same claim; every contract now carries at least two refuted misreadings).

receipts: research/ledger.jsonl (review, upgrade events) · tests/test_stance_and_hygiene.py · src/vallari/discriminativity.py · paper §Adversarial evaluation