We present a formalization of the technical language of Navya-Nyaya - the "New Logic" school of late-classical Indian philosophy - in CCHM De Morgan cubical type theory (CTT). Previous formalization attempts in first-order logic (Matilal), higher-order logic (Ganeri), and Martin-Lof type theory (Bhattacharyya) each lose load-bearing structure: dependent delimitation (avacchedaka), typed absence (abhava), non-extensional identity (tadatmya), or unbounded relational depth (parampara-sambandha). We argue that CTT closes this gap natively. We give CTT encodings for seven core constructs (sambandha, avacchedaka, abhava, vyapti, tadatmya, higher relations, paryapti) plus the qualifier-qualificand structure; develop a stratified-universe foundation for the padartha system; and prove four signature theorems internal to the encoding (involution of abhava, kevalanvayi irreducibility, coextension without identity, no h-set collapse) and six metatheoretic results (soundness, conservativity, faithfulness, distinction preservation, decidability, commentarial conservativity). We close with worked encodings of fifteen Tattvacintamani passages, comparison with prior formalizations, an implementation sketch in Cubical Agda, and five distinguishing predictions - including a novel argument from Navya-Nyaya's involutive-negation doctrine for the necessity of De Morgan over Cartesian cubical foundations.

翻译：我们提出了一种用CCHM De Morgan立方类型论（CTT）形式化新正理学（Navya-Nyāya）——晚期古典印度哲学的“新逻辑”学派——技术语言的方法。以往在一阶逻辑（Matilal）、高阶逻辑（Ganeri）和马丁-洛夫类型论（Bhattacharyya）中的形式化尝试各自丢失了负载结构：依赖限定（avacchedaka）、类型化缺失（abhava）、非外延同一性（tadatmya）或无界关系深度（parampara-sambandha）。我们论证CTT天然弥补了这一缺口。我们为七个核心构造（sambandha、avacchedaka、abhava、vyapti、tadatmya、高阶关系、paryapti）以及限定-被限定结构给出了CTT编码；为padartha体系发展了分层宇宙基础；并证明了编码内部的四个特征定理（abhava对合、kevalanvayi不可约性、无同一性的共扩展性、无h-集坍缩）和六个元理论结果（可靠性、保守性、忠实性、区分保持性、可判定性、评注保守性）。最后我们提供了十五段《真理宝鉴》（Tattvacintāmaṇi）篇章的编码实例、与先前形式化的比较、在Cubical Agda中的实现草图，以及五个区分性预测——其中包括一个基于新正理学对合否定学说论证De Morgan立方基础优于笛卡尔立方基础的新颖论点。