Proof — Verse 1.108-109 doxographic

लब्धक्रियः प्रयत्नेन वक्तुरिच्छानुवर्तिना ।
स्थानेष्वभिहतो वायुः शब्दत्वं प्रतिपद्यते ॥ १०८ ॥
तस्य कारणसामर्थ्याद्वेगप्रचयधर्मणः ।
सन्निपाताद्विभज्यन्ते सारवत्योऽपि मूर्तयः ॥ १०९ ॥

(108) Air, set in motion by the effort that follows the speaker's wish, striking upon the places of articulation, attains the condition of the word. (109) Through the potency of its cause, possessing the properties of velocity and accumulation, it divides by its impact even bodies that possess solidity.

This verse is doxographic: the commentary reports a rival view (pūrvapakṣa) it does not itself endorse. Reported axioms are held separately in the Lean contract (Contract.reported); they license a faithful translation of the report without being asserted as Bhartṛhari's doctrine.

Endorsed axioms (each cite is verbatim commentary)

Reported (pūrvapakṣa) axioms — commentary reports, does not endorse

Denials

Rejected readings (refuted by compiled theorems)

Lean module

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

namespace VakyaVallari.Verses.V1_108_109

open VakyaVallari

def vayu : Entity := ⟨"vāyu", Sorta.manifestation⟩
def sabdatva : Entity := ⟨"śabdatva", Sorta.property⟩
def iccha : Entity := ⟨"icchā", Sorta.cognition⟩
def prayatna : Entity := ⟨"prayatna", Sorta.property⟩
def sthanani : Entity := ⟨"sthānāni", Sorta.property⟩
def vega : Entity := ⟨"vega", Sorta.property⟩
def pracaya : Entity := ⟨"pracaya", Sorta.property⟩
def samarthya : Entity := ⟨"sāmarthya", Sorta.power⟩
def sannipata : Entity := ⟨"sannipāta", Sorta.property⟩
def murta : Entity := ⟨"mūrta", Sorta.manifestation⟩

def contract : Contract :=
  { axioms := []
  , denials := [ Claim.predication "paryapta" vayu ]
  , reported := [ Claim.relation "anuvartati" (Node.ent iccha) (Node.ent prayatna)
    , Claim.relation "pratipadyate" (Node.ent vayu) (Node.ent sabdatva)
    , Claim.relation "abhihati" (Node.ent vayu) (Node.ent sthanani)
    , Claim.predication "yuktavega" vayu
    , Claim.predication "yukti-pracaya" vayu
    , Claim.relation "vibhajyante" (Node.ent sannipata) (Node.ent murta) ] }

-- pūrvapakṣa: this contract carries reported (non-endorsed) claims
#guard contract.doxographic = true

def accepted : Reading :=
  { claims := [ Claim.relation "anuvartati" (Node.ent iccha) (Node.ent prayatna)
    , Claim.relation "pratipadyate" (Node.ent vayu) (Node.ent sabdatva)
    , Claim.relation "abhihati" (Node.ent vayu) (Node.ent sthanani)
    , Claim.predication "yuktavega" vayu
    , Claim.predication "yukti-pracaya" vayu
    , Claim.relation "vibhajyante" (Node.ent sannipata) (Node.ent murta) ] }

theorem accepted_adequate : contract.Adequate accepted := by decide

namespace Counterexamples

/- "Air alone, shaped by the speaker's will and striking the places of articulation, is fully the word itself, capable of being understood by any hearer."
   Why rejected: The verse presents the vayu doctrine as mechanist explanation of word-formation, but the commentary explicitly notes this is incomplete: shaped air must be grasped as one word by the hearer, which requires the epistemic unity that air-collision alone cannot provide. This reading treats the material mechanism as sufficient when Bhartrhari shows it is necessary but not sufficient. -/
def vayu_is_sufficient : Reading :=
  { claims := [ Claim.predication "paryapta" vayu ] }
theorem vayu_is_sufficient_inadequate : ¬ contract.Adequate vayu_is_sufficient := by decide
#guard contract.contradicts vayu_is_sufficient = true

/- "The air itself is the primary cause of wordhood, generated by the speaker's wish without any intervening mechanism."
   Why rejected: The axioms establish a chain: iccha → prayatna → vayu's motion → collision with sthanani → sabdatva. This reading elides the causal stages and treats vayu as originating from wish directly, losing the mechanistic precision Bhartrhari is documenting. The chain is what the doctrine claims. -/
def vayu_naive : Entity := ⟨"vāyu", Sorta.absolute⟩
def vayu_primary_cause : Reading :=
  { claims := [ Claim.relation "anuvartati" (Node.ent iccha) (Node.ent vayu_naive) ] }
theorem vayu_primary_cause_inadequate : ¬ contract.Adequate vayu_primary_cause := by decide
#guard contract.licenses vayu_primary_cause = false
theorem vayu_primary_cause_sort_error : vayu_naive ≠ vayu := by decide

/- 'Air naturally carries the property of wordhood without requiring the effort of the speaker to direct its motion.'
   Why rejected: The verse is explicit: effort (prayatna) following the wish (iccha) is what sets the air in motion. Wordhood is achieved through this intentional, effortful shaping, not passively. This reading treats sabdatva as an inherent property rather than an attainment (pratipadyate), contradicting the causal structure. -/
def sabdatva_achieved_passively : Reading :=
  { claims := [ Claim.predication "sabdatva" vayu ] }
theorem sabdatva_achieved_passively_inadequate : ¬ contract.Adequate sabdatva_achieved_passively := by decide
#guard contract.licenses sabdatva_achieved_passively = false

end Counterexamples

end VakyaVallari.Verses.V1_108_109