Proof — Verse 1.68-69 doxographic

स्वं रूपमिति कैश्चित्तु व्यक्तिः संज्ञोपदिश्यते ।
जातेः कार्याणि संसृष्टा जातिस्तु प्रतिपद्यते ॥ ६८ ॥
संज्ञिनीं व्यक्तिमिच्छन्ति सूत्रे ग्राह्यामथापरे ।
जातिप्रत्यायिता व्यक्तिः प्रदेशेषूपतिष्ठते ॥ ६९ ॥

(68) But by some, it is the individual that is taught as the name in 'its own form'; the class, being connected, receives the operations of the class. (69) Others hold that it is the individual that is the named, to be grasped in the sutra; the individual, conveyed through the class, presents itself in the particular contexts.

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

Rejected readings (refuted by compiled theorems)

Lean module

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

namespace VakyaVallari.Verses.V1_68_69

open VakyaVallari

def vyakti : Entity := ⟨"vyakti", Sorta.manifestation⟩
def jati : Entity := ⟨"jāti", Sorta.power⟩

def contract : Contract :=
  { axioms := [ Claim.predication "apparatus_component" vyakti
    , Claim.predication "apparatus_component" jati ]
  , denials := []
  , reported := [ Claim.relation "samsrsta" (Node.ent jati) (Node.ent vyakti)
    , Claim.relation "jati_pratyayita" (Node.ent jati) (Node.ent vyakti) ] }

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

def accepted : Reading :=
  { claims := [ Claim.predication "apparatus_component" vyakti
    , Claim.predication "apparatus_component" jati
    , Claim.relation "samsrsta" (Node.ent jati) (Node.ent vyakti) ] }

theorem accepted_adequate : contract.Adequate accepted := by decide

namespace Counterexamples

/- 'The form-universal (jāti) is the sole and sufficient basis for grammatical reference, with the individual form (vyakti) playing no essential role.'
   Why rejected: Directly contradicts the commentary's assertion that 'rule-stated language requires an apparatus of types and tokens' — an irreducible coordination. Denying vyakti's role violates the apparatus structure both reported positions affirm. -/
def jati_monopoly : Reading :=
  { claims := [ Claim.predication "sufficient_alone" jati ] }
theorem jati_monopoly_inadequate : ¬ contract.Adequate jati_monopoly := by decide
#guard contract.licenses jati_monopoly = false

/- 'The individual form (vyakti) and the class (jāti) play interchangeable roles in grammatical reference, or are functionally equivalent.'
   Why rejected: The verse's force rests on distinguishing two positions: position 1 assigns vyakti and jāti different roles (vyakti as name, jāti as connected operator), while position 2 assigns them mediated roles (vyakti as named-through-jāti). Conflating them erases the reported distinction, which the commentary emphasizes as the 'akrti/vyakti controversy'. -/
def conflated_positions : Reading :=
  { claims := [ Claim.identity vyakti jati ] }
theorem conflated_positions_inadequate : ¬ contract.Adequate conflated_positions := by decide
#guard contract.licenses conflated_positions = false

end Counterexamples

end VakyaVallari.Verses.V1_68_69