Proof — Verse 1.1

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

Brahman is without beginning or end, imperishable, and its essence is the Word. It appears in the mode of objects, and from it proceeds the unfolding of the world.

Endorsed axioms (each cite is verbatim commentary)

• {"kind": "identity", "a": "sabdatattva", "b": "brahman"}“the ultimate is not merely describable by language but is language — sabda-tattva, word-essence”
• {"kind": "relation", "name": "vivartate", "from": "brahman", "to": "jagat"}“Vivarta is appearance without loss of unity: the one presents itself as many while remaining one”
• {"kind": "predication", "name": "anadinidhana", "of": "brahman"}“its plain sense is 'imperishable', which is why it sits naturally beside anadinidhana, 'without beginning or end'”
• {"kind": "predication", "name": "aksara", "of": "brahman"}“What is imperishable and what is phonic are, for him, the same thing”

Denials

• {"kind": "relation", "name": "parinamate", "from": "brahman", "to": "jagat"}“Bhartrhari does not say Brahman becomes the world (parinamate), which would make the world a real transformation of its substance”

Rejected readings (refuted by compiled theorems)

• “The imperishable linguistic structure underlying words has no beginning or end.” — Renders śabdatattva as a mere linguistic property, demoting the ontological identity the commentary insists on: the ultimate IS language, not something described by it. The sort error (property vs absolute) makes the identity claim decidably false.
• “Brahman transforms itself into the world of objects.” — Asserts a real transformation (parinama) of Brahman's substance, which the commentary explicitly rules out in favor of vivarta (appearance without loss of unity).

Lean module

/- Verse 1.1 — generated from data/contracts/1.1.json. DO NOT EDIT.
   Axiom cites are verbatim commentary quotations, validated by
   tests/test_contracts.py. -/
import VakyaVallari.Adequacy

namespace VakyaVallari.Verses.V1_1

open VakyaVallari

def brahman : Entity := ⟨"brahman", Sorta.absolute⟩
def sabdatattva : Entity := ⟨"śabdatattva", Sorta.absolute⟩
def jagat : Entity := ⟨"jagat", Sorta.manifestation⟩

def contract : Contract :=
  { axioms := [ Claim.identity sabdatattva brahman
    , Claim.relation "vivartate" (Node.ent brahman) (Node.ent jagat)
    , Claim.predication "anadinidhana" brahman
    , Claim.predication "aksara" brahman ]
  , denials := [ Claim.relation "parinamate" (Node.ent brahman) (Node.ent jagat) ]
  , reported := [] }

def accepted : Reading :=
  { claims := [ Claim.identity sabdatattva brahman
    , Claim.predication "anadinidhana" brahman
    , Claim.predication "aksara" brahman
    , Claim.relation "vivartate" (Node.ent brahman) (Node.ent jagat) ] }

theorem accepted_adequate : contract.Adequate accepted := by decide

namespace Counterexamples

/- 'The imperishable linguistic structure underlying words has no beginning or end.'
   Why rejected: Renders śabdatattva as a mere linguistic property, demoting the ontological identity the commentary insists on: the ultimate IS language, not something described by it. The sort error (property vs absolute) makes the identity claim decidably false. -/
def sabdatattva_naive : Entity := ⟨"śabdatattva", Sorta.property⟩
def naive_linguistic_structure : Reading :=
  { claims := [ Claim.identity sabdatattva_naive brahman ] }
theorem naive_linguistic_structure_inadequate : ¬ contract.Adequate naive_linguistic_structure := by decide
#guard contract.licenses naive_linguistic_structure = false
theorem naive_linguistic_structure_sort_error : sabdatattva_naive ≠ sabdatattva := by decide

/- 'Brahman transforms itself into the world of objects.'
   Why rejected: Asserts a real transformation (parinama) of Brahman's substance, which the commentary explicitly rules out in favor of vivarta (appearance without loss of unity). -/
def parinama_transformation : Reading :=
  { claims := [ Claim.relation "parinamate" (Node.ent brahman) (Node.ent jagat) ] }
theorem parinama_transformation_inadequate : ¬ contract.Adequate parinama_transformation := by decide
#guard contract.contradicts parinama_transformation = true

end Counterexamples

end VakyaVallari.Verses.V1_1