Proof — Verse 1.24-26

अपोद्धारपदार्था ये ये चार्थाः स्थितलक्षणाः ।
अन्वाख्येयाश्च ये शब्दा ये चापि प्रतिपादकाः ॥ २४ ॥
कार्यकारणभावेन योग्यभावेन च स्थिताः ।
धर्मे ये प्रत्यये चाङ्गं संबन्धाः साध्वसाधुषु ॥ २५ ॥
ते लिङ्गैश्च स्वशब्दैश्च शास्त्रेऽस्मिन्नुपवर्णिताः ।
स्मृत्यर्थमनुगम्यन्ते केचिदेव यथागमम् ॥ २६ ॥

Those word-meanings reached by abstraction, and those meanings whose defining marks are fixed; those words that are to be explained, and those that do the explaining; those relations obtaining by way of cause and effect and by way of fitness, which are ancillary to dharma and to cognition, holding among correct and incorrect words — these are set out in this science, by indicatory marks and in their own terms; and only some are followed, for the sake of what is to be remembered, according to tradition.

Endorsed axioms (each cite is verbatim commentary)

• {"kind": "predication", "name": "apoddhāra", "of": "sabda"}“the word is not a natural unit given prior to the sentence but is *extracted* from it by analysis”
• {"kind": "predication", "name": "sthita-lakṣaṇa", "of": "padartha"}“meanings with fixed marks”
• {"kind": "relation", "name": "vyakhyāyate", "from": "pratipadaka", "to": "anvakhyeya"}“the anvakhyeya/pratipadaka distinction between what gets explained and what does the explaining”
• {"kind": "predication", "name": "kāryakāraṇa-bhāva", "of": "sambandha"}“relations of two kinds, causal and of yogyata or fitness”
• {"kind": "predication", "name": "yogya-bhāva", "of": "sambandha"}“relations of two kinds, causal and of yogyata or fitness”

Denials

• {"kind": "predication", "name": "sarva-upavarnita", "of": "padartha"}“not everything true of these matters is transmitted, only kecid eva, some only”

Rejected readings (refuted by compiled theorems)

• “Words are primitive linguistic units from which sentences are built.” — Contradicts the presupposed apoddhara doctrine: the verse grounds itself in the principle that words are extracted from the sentence by analysis, not given as natural prior units. The sentence is the real linguistic whole.
• “This science transmits every true matter concerning meanings and relations.” — The final clause of the verse explicitly denies this: only some matters are transmitted according to tradition, not all. The discipline is selective.

Lean module

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

namespace VakyaVallari.Verses.V1_24_26

open VakyaVallari

def sabda : Entity := ⟨"śabda", Sorta.linguisticItem⟩
def padartha : Entity := ⟨"padartha", Sorta.linguisticItem⟩
def anvakhyeya : Entity := ⟨"anvākhyeya", Sorta.linguisticItem⟩
def pratipadaka : Entity := ⟨"pratipadaka", Sorta.linguisticItem⟩
def sambandha : Entity := ⟨"saṃbandha", Sorta.property⟩
def dharma : Entity := ⟨"dharma", Sorta.absolute⟩
def pratyaya : Entity := ⟨"pratyaya", Sorta.cognition⟩

def contract : Contract :=
  { axioms := [ Claim.predication "apoddhāra" sabda
    , Claim.predication "sthita-lakṣaṇa" padartha
    , Claim.relation "vyakhyāyate" (Node.ent pratipadaka) (Node.ent anvakhyeya)
    , Claim.predication "kāryakāraṇa-bhāva" sambandha
    , Claim.predication "yogya-bhāva" sambandha ]
  , denials := [ Claim.predication "sarva-upavarnita" padartha ]
  , reported := [] }

def accepted : Reading :=
  { claims := [ Claim.predication "apoddhāra" sabda
    , Claim.predication "sthita-lakṣaṇa" padartha
    , Claim.relation "vyakhyāyate" (Node.ent pratipadaka) (Node.ent anvakhyeya)
    , Claim.predication "kāryakāraṇa-bhāva" sambandha
    , Claim.predication "yogya-bhāva" sambandha ] }

theorem accepted_adequate : contract.Adequate accepted := by decide

namespace Counterexamples

/- 'Words are primitive linguistic units from which sentences are built.'
   Why rejected: Contradicts the presupposed apoddhara doctrine: the verse grounds itself in the principle that words are extracted from the sentence by analysis, not given as natural prior units. The sentence is the real linguistic whole. -/
def word_as_primitive : Reading :=
  { claims := [ Claim.predication "prakṛta" sabda ] }
theorem word_as_primitive_inadequate : ¬ contract.Adequate word_as_primitive := by decide
#guard contract.licenses word_as_primitive = false

/- 'This science transmits every true matter concerning meanings and relations.'
   Why rejected: The final clause of the verse explicitly denies this: only some matters are transmitted according to tradition, not all. The discipline is selective. -/
def comprehensive_transmission : Reading :=
  { claims := [ Claim.predication "sarva-upavarnita" padartha ] }
theorem comprehensive_transmission_inadequate : ¬ contract.Adequate comprehensive_transmission := by decide
#guard contract.contradicts comprehensive_transmission = true

end Counterexamples

end VakyaVallari.Verses.V1_24_26