Proof — Verse 1.62

उच्चरन् परतन्त्रत्वाद्गुणः कार्यैर्न युज्यते ।
तस्मात्तदर्थैः कार्याणां संबन्धः परिकल्प्यते ॥ ६२ ॥

In being uttered it is dependent, and so the subordinate element is not joined to the operations; therefore the relation of the operations is construed with what those elements mean.

Endorsed axioms (each cite is verbatim commentary)

• {"kind": "predication", "name": "paratantra", "of": "guna"}“Uttered, it is paratantra, not standing on its own”
• {"kind": "relation", "name": "na_yujyate", "from": "karya", "to": "guna"}“grammatical operations do not attach to it directly in that dependent condition”
• {"kind": "relation", "name": "parikalpyate", "from": "karya", "to": "artha"}“the relation of karya to item is parikalpyate, construed, through the artha, the function or value of the element within the whole”

Rejected readings (refuted by compiled theorems)

• “Qualities, being dependent on substances, do not undergo grammatical operations directly.” — Shifts guna from a grammatical category (constituent, stem in compound) to a metaphysical one (quality-substance relation). The sort error—guna as property rather than linguistic item—breaks the verse's argument about how grammar works with subordinate linguistic elements.
• “Grammatical operations directly apply to dependent elements without semantic mediation.” — Contradicts the verse's core claim by asserting that operations do join dependent elements directly. This ignores the parikalpyate (construing) that the verse establishes—the connection is preserved, not eliminated, but redirected through artha (meaning).

Lean module

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

namespace VakyaVallari.Verses.V1_62

open VakyaVallari

def guna : Entity := ⟨"guṇa", Sorta.linguisticItem⟩
def karya : Entity := ⟨"kārya", Sorta.power⟩
def artha : Entity := ⟨"artha", Sorta.property⟩

def contract : Contract :=
  { axioms := [ Claim.predication "paratantra" guna
    , Claim.relation "na_yujyate" (Node.ent karya) (Node.ent guna)
    , Claim.relation "parikalpyate" (Node.ent karya) (Node.ent artha) ]
  , denials := []
  , reported := [] }

def accepted : Reading :=
  { claims := [ Claim.predication "paratantra" guna
    , Claim.relation "na_yujyate" (Node.ent karya) (Node.ent guna)
    , Claim.relation "parikalpyate" (Node.ent karya) (Node.ent artha) ] }

theorem accepted_adequate : contract.Adequate accepted := by decide

namespace Counterexamples

/- 'Qualities, being dependent on substances, do not undergo grammatical operations directly.'
   Why rejected: Shifts guna from a grammatical category (constituent, stem in compound) to a metaphysical one (quality-substance relation). The sort error—guna as property rather than linguistic item—breaks the verse's argument about how grammar works with subordinate linguistic elements. -/
def guna_quality : Entity := ⟨"guṇa", Sorta.property⟩
def quality_not_element : Reading :=
  { claims := [ Claim.predication "paratantra" guna_quality ] }
theorem quality_not_element_inadequate : ¬ contract.Adequate quality_not_element := by decide
#guard contract.licenses quality_not_element = false
theorem quality_not_element_sort_error : guna_quality ≠ guna := by decide

/- 'Grammatical operations directly apply to dependent elements without semantic mediation.'
   Why rejected: Contradicts the verse's core claim by asserting that operations do join dependent elements directly. This ignores the parikalpyate (construing) that the verse establishes—the connection is preserved, not eliminated, but redirected through artha (meaning). -/
def direct_attachment : Reading :=
  { claims := [ Claim.relation "yujyate" (Node.ent karya) (Node.ent guna) ] }
theorem direct_attachment_inadequate : ¬ contract.Adequate direct_attachment := by decide
#guard contract.licenses direct_attachment = false

end Counterexamples

end VakyaVallari.Verses.V1_62