Proof — Verse 1.103 doxographic

अल्पे महति वा शब्दे स्फोटकालो न भिद्यते ।
परस्तु शब्दसन्तानः प्रचयापचयात्मकः ॥ १०३ ॥

Whether the word is small or great, the time of the sphota does not differ; but the subsequent train of sounds has the nature of increase and decrease.

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)

• {"kind": "identity", "a": "sphota_kala", "b": "prakrta"}“even theorists who deny the transcendent word are driven to split the invariant from the variable within speech”
• {"kind": "identity", "a": "sabda_santana", "b": "vaikrta"}“the structure of prakrta versus vaikrta (1.76-77) reappears inside pure acoustics”

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

• {"kind": "predication", "name": "na_bhidyate", "of": "sphota_kala"}“that first event's time 'does not differ' with loudness — alpa or mahat, whispered or bellowed”
• {"kind": "predication", "name": "pracaya_apacaya_atmaka", "of": "sabda_santana"}“the after-train, waxes and wanes (pracaya-apacaya) with the force of utterance”

Denials

• {"kind": "predication", "name": "pracaya_apacaya_atmaka", "of": "sphota_kala"}“that first event's time 'does not differ' with loudness — alpa or mahat, whispered or bellowed”
• {"kind": "predication", "name": "na_bhidyate", "of": "sabda_santana"}“the after-train, waxes and wanes (pracaya-apacaya) with the force of utterance”

Rejected readings (refuted by compiled theorems)

• “The time of the sphota increases and decreases with the loudness of the utterance, while the after-train remains constant.” — Reverses the verse's explicit assertion: the sphota-kala does not differ (is invariant), while the sabda-santana varies. This misreads which acoustic phenomenon carries the invariance structure.
• “The sphota and the subsequent train of sounds are the same acoustic phenomenon, subject to the same variation.” — Ignores the critical distinction between the invariant first-produced sphota (prakrta) and the variable propagated train (vaikrta). The verse carefully separates what does and does not differ with loudness.
• “Both the sphota-kala and the subsequent train are invariant because both derive from the same articulation.” — Incorrectly generalizes the sphota-kala's invariance to the sabda-santana. The commentary is explicit: loudness is a property of propagation, not articulation. The after-train must vary with utterance force.

Lean module

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

namespace VakyaVallari.Verses.V1_103

open VakyaVallari

def sphota_kala : Entity := ⟨"sphoṭakāla", Sorta.linguisticItem⟩
def sabda_santana : Entity := ⟨"śabdasantāna", Sorta.manifestation⟩
def prakrta : Entity := ⟨"prakṛta", Sorta.power⟩
def vaikrta : Entity := ⟨"vaikṛta", Sorta.manifestation⟩

def contract : Contract :=
  { axioms := [ Claim.identity sphota_kala prakrta
    , Claim.identity sabda_santana vaikrta ]
  , denials := [ Claim.predication "pracaya_apacaya_atmaka" sphota_kala
    , Claim.predication "na_bhidyate" sabda_santana ]
  , reported := [ Claim.predication "na_bhidyate" sphota_kala
    , Claim.predication "pracaya_apacaya_atmaka" sabda_santana ] }

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

def accepted : Reading :=
  { claims := [ Claim.predication "na_bhidyate" sphota_kala
    , Claim.predication "pracaya_apacaya_atmaka" sabda_santana ] }

theorem accepted_adequate : contract.Adequate accepted := by decide

namespace Counterexamples

/- 'The time of the sphota increases and decreases with the loudness of the utterance, while the after-train remains constant.'
   Why rejected: Reverses the verse's explicit assertion: the sphota-kala does not differ (is invariant), while the sabda-santana varies. This misreads which acoustic phenomenon carries the invariance structure. -/
def reversed_invariance : Reading :=
  { claims := [ Claim.predication "pracaya_apacaya_atmaka" sphota_kala ] }
theorem reversed_invariance_inadequate : ¬ contract.Adequate reversed_invariance := by decide
#guard contract.contradicts reversed_invariance = true

/- 'The sphota and the subsequent train of sounds are the same acoustic phenomenon, subject to the same variation.'
   Why rejected: Ignores the critical distinction between the invariant first-produced sphota (prakrta) and the variable propagated train (vaikrta). The verse carefully separates what does and does not differ with loudness. -/
def collapse_distinction : Reading :=
  { claims := [ Claim.identity sphota_kala sabda_santana ] }
theorem collapse_distinction_inadequate : ¬ contract.Adequate collapse_distinction := by decide
#guard contract.licenses collapse_distinction = false

/- 'Both the sphota-kala and the subsequent train are invariant because both derive from the same articulation.'
   Why rejected: Incorrectly generalizes the sphota-kala's invariance to the sabda-santana. The commentary is explicit: loudness is a property of propagation, not articulation. The after-train must vary with utterance force. -/
def propagation_invariant : Reading :=
  { claims := [ Claim.predication "na_bhidyate" sabda_santana ] }
theorem propagation_invariant_inadequate : ¬ contract.Adequate propagation_invariant := by decide
#guard contract.contradicts propagation_invariant = true

end Counterexamples

end VakyaVallari.Verses.V1_103