Proof — Verse 1.102 doxographic

यः संयोगविभागाभ्यां करणैरुपजन्यते ।
स स्फोटः शब्दजाः शब्दा ध्वनयोऽन्यैरुदाहृताः ॥ १०२ ॥

What is generated by the organs through conjunction and disjunction — that is the sphota; the sounds born from that word are what others call the dhvanis.

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

• {"kind": "relation", "name": "utpadyate", "from": "karana", "to": "sphota"}“the one generated by the articulators' contacts and releases (samyoga-vibhaga”
• {"kind": "relation", "name": "sabda_ja", "from": "sphota", "to": "sabda_ja"}“the sounds born *from* that sound”
• {"kind": "identity", "a": "sabda_ja", "b": "dhvani"}“'dhvani' names the sabda-ja sabdah, the sounds born *from* that sound”
• {"kind": "predication", "name": "acoustic", "of": "sphota"}“the sphota is itself acoustic and produced”

Denials

• {"kind": "identity", "a": "sphota", "b": "partless_sphota"}“the partless meaning-bearer — is not in this picture at all”

Rejected readings (refuted by compiled theorems)

• “The sphota is the partless, metaphysical word-essence that generates secondary acoustic phenomena.” — Verse 1.102 explicitly reports an alternative view that denies this: the sphota here is acoustic and produced, not partless and metaphysical. This reading confuses Bhartrhari's own doctrine (developed later) with the competing account presented in this verse.
• “The dhvani are the primary sounds generated by the organs; the sphota is a secondary echo or propagation.” — Reverses the relation: the verse explicitly states dhvani are sounds *born from* the sphota, making sphota the primary producer. The backward relation is not entailed by the axioms.

Lean module

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

namespace VakyaVallari.Verses.V1_102

open VakyaVallari

def sphota : Entity := ⟨"sphoṭa", Sorta.manifestation⟩
def karana : Entity := ⟨"karaṇa", Sorta.power⟩
def dhvani : Entity := ⟨"dhvani", Sorta.manifestation⟩
def sabda_ja : Entity := ⟨"śabdajāḥ", Sorta.manifestation⟩
def partless_sphota : Entity := ⟨"partless sphoṭa", Sorta.absolute⟩

def contract : Contract :=
  { axioms := []
  , denials := [ Claim.identity sphota partless_sphota ]
  , reported := [ Claim.relation "utpadyate" (Node.ent karana) (Node.ent sphota)
    , Claim.relation "sabda_ja" (Node.ent sphota) (Node.ent sabda_ja)
    , Claim.identity sabda_ja dhvani
    , Claim.predication "acoustic" sphota ] }

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

def accepted : Reading :=
  { claims := [ Claim.relation "utpadyate" (Node.ent karana) (Node.ent sphota)
    , Claim.relation "sabda_ja" (Node.ent sphota) (Node.ent sabda_ja)
    , Claim.identity sabda_ja dhvani ] }

theorem accepted_adequate : contract.Adequate accepted := by decide

namespace Counterexamples

/- 'The sphota is the partless, metaphysical word-essence that generates secondary acoustic phenomena.'
   Why rejected: Verse 1.102 explicitly reports an alternative view that denies this: the sphota here is acoustic and produced, not partless and metaphysical. This reading confuses Bhartrhari's own doctrine (developed later) with the competing account presented in this verse. -/
def sphota_partless : Reading :=
  { claims := [ Claim.predication "partless" sphota ] }
theorem sphota_partless_inadequate : ¬ contract.Adequate sphota_partless := by decide
#guard contract.licenses sphota_partless = false

/- 'The dhvani are the primary sounds generated by the organs; the sphota is a secondary echo or propagation.'
   Why rejected: Reverses the relation: the verse explicitly states dhvani are sounds *born from* the sphota, making sphota the primary producer. The backward relation is not entailed by the axioms. -/
def dhvani_primary : Reading :=
  { claims := [ Claim.relation "sabda_ja" (Node.ent dhvani) (Node.ent sphota) ] }
theorem dhvani_primary_inadequate : ¬ contract.Adequate dhvani_primary := by decide
#guard contract.licenses dhvani_primary = false

end Counterexamples

end VakyaVallari.Verses.V1_102