Proof — Verse 1.57

अतोऽनिर्ज्ञातरूपत्वात् किमाहेत्यभिधीयते ।
नेन्द्रियाणां प्रकाश्येऽर्थे स्वरूपं गृह्यते तथा ॥ ५७ ॥

Hence, when the form has not been discerned, one asks 'what did he say?'; in the case of an object illuminated by the senses, its own form is not grasped in that way.

Endorsed axioms (each cite is verbatim commentary)

• {"kind": "predication", "name": "pratyayaka", "of": "sabda"}“the word is both pratyayaka and pratyayya, conveyor and conveyed”
• {"kind": "predication", "name": "pratyayya", "of": "sabda"}“the word is both pratyayaka and pratyayya, conveyor and conveyed”
• {"kind": "relation", "name": "apeksa", "from": "artha", "to": "sabda"}“meaning waits on the second”
• {"kind": "relation", "name": "prakasayati", "from": "indriya", "to": "visaya"}“The eye illuminates the pot without itself being grasped in the act”

Denials

• {"kind": "relation", "name": "prakasayati", "from": "sabda", "to": "artha"}“the word cannot mediate unless it is itself apprehended”

Rejected readings (refuted by compiled theorems)

• “The word conveys meaning through illumination, like a sense organ - it need not itself be apprehended for its meaning to be determined.” — The verse explicitly establishes a disanalogy: sense organs illuminate their objects without themselves being grasped, while words require their own apprehension to convey meaning. The word is unique precisely in being both conveyor and conveyed.
• “Both words and sense organs must be apprehended by consciousness to convey their meanings - they share the same structure as pratyayaka and pratyayya.” — The verse emphasizes through 'one does not see one's seeing' that sense organs illuminate without themselves being grasped, precisely what makes words different. Words are unique in being both conveyor and conveyed, whereas sense organs are merely pratyayaka.

Lean module

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

namespace VakyaVallari.Verses.V1_57

open VakyaVallari

def sabda : Entity := ⟨"śabda", Sorta.linguisticItem⟩
def sabdarupa : Entity := ⟨"śabdarūpa", Sorta.property⟩
def artha : Entity := ⟨"artha", Sorta.manifestation⟩
def indriya : Entity := ⟨"indriya", Sorta.power⟩
def visaya : Entity := ⟨"viṣaya", Sorta.manifestation⟩
def pratyaya : Entity := ⟨"pratyaya", Sorta.cognition⟩

def contract : Contract :=
  { axioms := [ Claim.predication "pratyayaka" sabda
    , Claim.predication "pratyayya" sabda
    , Claim.relation "apeksa" (Node.ent artha) (Node.ent sabda)
    , Claim.relation "prakasayati" (Node.ent indriya) (Node.ent visaya) ]
  , denials := [ Claim.relation "prakasayati" (Node.ent sabda) (Node.ent artha) ]
  , reported := [] }

def accepted : Reading :=
  { claims := [ Claim.relation "prakasayati" (Node.ent indriya) (Node.ent visaya) ] }

theorem accepted_adequate : contract.Adequate accepted := by decide

namespace Counterexamples

/- 'The word conveys meaning through illumination, like a sense organ - it need not itself be apprehended for its meaning to be determined.'
   Why rejected: The verse explicitly establishes a disanalogy: sense organs illuminate their objects without themselves being grasped, while words require their own apprehension to convey meaning. The word is unique precisely in being both conveyor and conveyed. -/
def word_as_sense_organ : Reading :=
  { claims := [ Claim.relation "prakasayati" (Node.ent sabda) (Node.ent artha) ] }
theorem word_as_sense_organ_inadequate : ¬ contract.Adequate word_as_sense_organ := by decide
#guard contract.contradicts word_as_sense_organ = true

/- 'Both words and sense organs must be apprehended by consciousness to convey their meanings - they share the same structure as pratyayaka and pratyayya.'
   Why rejected: The verse emphasizes through 'one does not see one's seeing' that sense organs illuminate without themselves being grasped, precisely what makes words different. Words are unique in being both conveyor and conveyed, whereas sense organs are merely pratyayaka. -/
def sense_organs_also_pratyayya : Reading :=
  { claims := [ Claim.predication "pratyayya" indriya ] }
theorem sense_organs_also_pratyayya_inadequate : ¬ contract.Adequate sense_organs_also_pratyayya := by decide
#guard contract.licenses sense_organs_also_pratyayya = false

end Counterexamples

end VakyaVallari.Verses.V1_57