Dharma.lean

/-
三个观点，用类型编码（不是定理证明）：

  1. 觉悟 = 无明之灭。定义为否定。
     其「反面」¬觉悟 = ¬¬无明。构造逻辑中 ¬¬无明 ↛ 无明
     ——双重否定不能消去。「不觉」比「无明」更弱，无法做实。

  2. 烦恼依赖无明 → 觉悟拿掉地基，烦恼即灭。
     用归纳类型编码：构造 fannao 必须首先提供 wuming。

  3. 慈心不依赖无明 → 觉悟碰不到它。
     慈经只是信标，不是航道。信标不湿脚。航道在水里。
-/

opaque zhongsheng : Type

-- 无明：心不照了。是谓词，不是实物。
opaque wuming : zhongsheng → Prop

-- 觉悟：无明之灭。纯否定——不是「别的东西」。
def juewu (s : zhongsheng) : Prop := ¬ wuming s

-- ── 烦恼：依无明而有。构造必须提供无明为参数 ──

inductive fannao (s : zhongsheng) : Prop where
  | mk (hw : wuming s) : fannao s

theorem fannao_xiaosan (s : zhongsheng) (h_jue : juewu s) : ¬ fannao s := by
  intro h_fan
  rcases h_fan with ⟨hw⟩
  exact h_jue hw

-- ── 慈心：不依无明。信标在岸上，它在水里自己流。 ──

opaque cixin : zhongsheng → Prop
-- 无公理连接慈心与无明——它不从这里取地基

theorem cixin_buhuai (s : zhongsheng) (h_ci : cixin s) (_h_jue : juewu s) : cixin s :=
  h_ci

/-
结构即论证：

  fannao_xiaosan：fannao 的构造器吞一个 wuming。
     pattern-match 取出那个 wuming，juewu (=¬wuming) 直接咬死。

  cixin_buhuai：证明是恒等函数。juewu 根本没入参——它什么都碰不到。

  juewu := ¬ wuming：定义本身编码了「无正面之反面」。
           构造类型论中，否定是函数类型 (P → ⊥)，不是正面构造。
           ¬P 的「反面」只能是 ¬¬P，即 (P → ⊥) → ⊥。
           而 ¬¬P 推不出 P——所谓「反面」只是一种余影，
           不是一个可以独立成立的实法。

这就是为什么「更迷」不对——它假定了两个正极之间的连续谱。
但只有一极。另一极不存在。

信标不湿脚。航道在水里。
慈经告诉你方向，不需要下水。真正的慈心已经在流了——它不在经里，
不在念里，不在第六识的「造作」里。它在 wuming 灭时不会少一分。
-/

慈心.md

慈心的地基：三性、无明与不依

三性 —— 一张桌子，三种看法

唯识把一切法分成三层，叫「三性」。不是三个东西，是同一个东西的三种认知层次。

遍计所执性：你看到一张桌子，心里说「这是桌子」，然后你把这个标签当真，以为「桌子」是桌子里面的东西。遍计 = 到处贴标签。所执 = 贴上去之后抓着不放。

依他起性：桌子本身。木头、钉子、人工、时间——种种因缘凑在一起，暂时呈现为这个样子。没有「桌子」这个自性在里面，只是缘起假相。依他起 = 依赖其他东西而起。

圆成实性：如实见。不贴标签，也不否定桌子存在，只是看到桌子就是桌子——缘起假相而已，没有多余的东西贴在上面。圆成实 = 圆满成就的真实。

比喻：看电影。遍计所执 = 以为屏幕上真的有人死了，哭了。依他起 = 光打在幕布上形成的影像。圆成实 = 知道这是电影，但不妨碍你看。

无明 —— 遍计所执的根

无明不是「不知道什么」，更不是愚蠢。无明是：把依他起当成遍计所执。把光影当真，把标签当本质。

所以无明不是一个小错误——它是错误的源头。所有的烦恼（贪、嗔、慢、疑）都从这个源错误里长出来。因为如果没有「把标签当真」这一步，你不可能对一个标签起贪、对一个标签起嗔。

这就是为什么 fannao 的构造器必须吞一个 wuming：烦恼 → 无明。烦恼的地基是无明——无明灭了，烦恼没有地方站着。

慈心 —— 不依无明

慈心不是烦恼。但它是不是跟贪一样「属于」遍计所执？要看情况。

凡夫的慈心可以夹杂遍计所执——「我对你慈心，因为你是我孩子」——这个慈心上面贴了「我的」「我」「孩子」的标签。但标签是标签，慈心是慈心。把标签剥掉之后，慈心还在。不像贪——把「我的」标签剥掉之后，贪本身就没有内容了。贪的内容就是「我 + 喜欢的 = 我的」。

不依无明的慈心是什么？是无嗔（adosa）——心所法里一个根本善心所。无嗔不是「修出来的善意」，是嗔的缺位。就像光明不是「制造出来的东西」，是黑暗的不在。

关键区分：

• 贪：内容依赖标签（遍计所执），无明是地基
• 慈：本质是无嗔，无嗔不依赖标签——它不依赖把什么东西当真

所以：觉悟（= 无明灭）→ 遍计所执灭 → 贪灭。但慈心不灭——因为它不依赖遍计所执，也不依赖无明。它的地基不是无明，是真如——是圆成实性那边的东西。

为什么慈心「自己站着」

回到三性框架：

圆成实性 ←─ 慈心在这里。不是修出来的，是无明遮住时也没丢的。
    ↑
依他起性 ←─ 剥掉标签之后的世界。有情受苦，这是事实。
    ↑
遍计所执性 ←─ 贪嗔慢疑在这里。是「把标签当真」的产物。

慈心不需要遍计所执来支撑。它不靠「这人是我的朋友」「这人在我团体里」「这人值得帮助」来成立——它成立的方式是：嗔不在。

所以你不用「生成」慈心——它不是遍计所执那边「造」出来的。它只是还没被认出来。