Proof — Verse 1.38

अतीन्द्रियानसंवेद्यान् पश्यन्त्यार्षेण चक्षुषा ।
ये भावान् वचनं तेषां नानुमानेन बाध्यते ॥ ३८ ॥

Those who see, with the seer's eye, things that lie beyond the senses and cannot be felt — their word is not overturned by inference.

Endorsed axioms (each cite is verbatim commentary)

• {"kind": "predication", "name": "arsa_caksu", "of": "rsi"}“the rsis' knowledge is perceptual in character”
• {"kind": "relation", "name": "perceives", "from": "arsa_caksu", "to": "atindriya"}“direct seeing is available to some and inference to all”
• {"kind": "identity", "a": "anumana", "b": "pramana"}“Inference is a real pramana”
• {"kind": "predication", "name": "vacana", "of": "rsi"}“vacana — their word, the agama — cannot be arraigned by tarka”
• {"kind": "relation", "name": "not_overturned_by", "from": "vacana", "to": "anumana"}“vacana — their word, the agama — cannot be arraigned by tarka”
• {"kind": "predication", "name": "defeasible", "of": "anumana"}“inference is defeasible in the way 1.34 showed”
• {"kind": "relation", "name": "stronger_than", "from": "direct_seeing", "to": "anumana"}“the weaker instrument does not get to overrule the stronger”

Denials

• {"kind": "relation", "name": "can_overrule", "from": "anumana", "to": "vacana"}“vacana — their word, the agama — cannot be arraigned by tarka”
• {"kind": "relation", "name": "can_overrule", "from": "anumana", "to": "direct_seeing"}“the weaker instrument does not get to overrule the stronger”

Rejected readings (refuted by compiled theorems)

• “The inference of ordinary reasoners can overturn the testimony of the seers.” — Directly contradicts the verse's core claim that the rsis' word cannot be overturned by inference. The commentary explicitly denies that the weaker instrument (inference) can overrule the stronger (direct seeing).
• “The seers have no special perceptual faculty; their knowledge comes only from ordinary inference like everyone else.” — Denies the ārṣa-cakṣus (seer's eye) as a distinct power, which is central to the verse's claim that they see what lies beyond the senses. This demotes the seer's faculty from a unique power to ordinary cognition.
• “Inference and direct perception have equal epistemic status in the domain of dharma.” — Reverses the hierarchy established by the verse and commentary. The commentary is explicit that the weaker instrument (inference) does not override the stronger (direct seeing), and that direct seeing is available to seers but inference to all.

Lean module

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

namespace VakyaVallari.Verses.V1_38

open VakyaVallari

def rsi : Entity := ⟨"ṛṣi", Sorta.absolute⟩
def arsa_caksu : Entity := ⟨"ārṣa-cakṣus", Sorta.power⟩
def bhava : Entity := ⟨"bhāva", Sorta.manifestation⟩
def atindriya : Entity := ⟨"atīndriya", Sorta.property⟩
def vacana : Entity := ⟨"vacana", Sorta.linguisticItem⟩
def anumana : Entity := ⟨"anumāna", Sorta.power⟩
def pramana : Entity := ⟨"pramāṇa", Sorta.power⟩
def direct_seeing : Entity := ⟨"direct seeing", Sorta.cognition⟩

def contract : Contract :=
  { axioms := [ Claim.predication "arsa_caksu" rsi
    , Claim.relation "perceives" (Node.ent arsa_caksu) (Node.ent atindriya)
    , Claim.identity anumana pramana
    , Claim.predication "vacana" rsi
    , Claim.relation "not_overturned_by" (Node.ent vacana) (Node.ent anumana)
    , Claim.predication "defeasible" anumana
    , Claim.relation "stronger_than" (Node.ent direct_seeing) (Node.ent anumana) ]
  , denials := [ Claim.relation "can_overrule" (Node.ent anumana) (Node.ent vacana)
    , Claim.relation "can_overrule" (Node.ent anumana) (Node.ent direct_seeing) ]
  , reported := [] }

def accepted : Reading :=
  { claims := [ Claim.predication "arsa_caksu" rsi
    , Claim.relation "perceives" (Node.ent arsa_caksu) (Node.ent atindriya)
    , Claim.predication "vacana" rsi
    , Claim.relation "not_overturned_by" (Node.ent vacana) (Node.ent anumana) ] }

theorem accepted_adequate : contract.Adequate accepted := by decide

namespace Counterexamples

/- 'The inference of ordinary reasoners can overturn the testimony of the seers.'
   Why rejected: Directly contradicts the verse's core claim that the rsis' word cannot be overturned by inference. The commentary explicitly denies that the weaker instrument (inference) can overrule the stronger (direct seeing). -/
def inference_overrules_testimony : Reading :=
  { claims := [ Claim.relation "can_overrule" (Node.ent anumana) (Node.ent vacana) ] }
theorem inference_overrules_testimony_inadequate : ¬ contract.Adequate inference_overrules_testimony := by decide
#guard contract.contradicts inference_overrules_testimony = true

/- 'The seers have no special perceptual faculty; their knowledge comes only from ordinary inference like everyone else.'
   Why rejected: Denies the ārṣa-cakṣus (seer's eye) as a distinct power, which is central to the verse's claim that they see what lies beyond the senses. This demotes the seer's faculty from a unique power to ordinary cognition. -/
def arsa_caksu_ordinary : Entity := ⟨"ārṣa-cakṣus", Sorta.cognition⟩
def no_seer_eye_distinction : Reading :=
  { claims := [ Claim.predication "arsa_caksu_ordinary" rsi ] }
theorem no_seer_eye_distinction_inadequate : ¬ contract.Adequate no_seer_eye_distinction := by decide
#guard contract.licenses no_seer_eye_distinction = false
theorem no_seer_eye_distinction_sort_error : arsa_caksu_ordinary ≠ arsa_caksu := by decide

/- 'Inference and direct perception have equal epistemic status in the domain of dharma.'
   Why rejected: Reverses the hierarchy established by the verse and commentary. The commentary is explicit that the weaker instrument (inference) does not override the stronger (direct seeing), and that direct seeing is available to seers but inference to all. -/
def inference_equals_direct_seeing : Reading :=
  { claims := [ Claim.relation "equal_status" (Node.ent anumana) (Node.ent direct_seeing) ] }
theorem inference_equals_direct_seeing_inadequate : ¬ contract.Adequate inference_equals_direct_seeing := by decide
#guard contract.licenses inference_equals_direct_seeing = false

end Counterexamples

end VakyaVallari.Verses.V1_38