v0.1.0 — 观察面相对的可逆性：定理 + Lean 形式化 + 三态判决

首版。把「卸载之后环境回没回来」从一个没人核的义务，变成一个有定理背书的判决。

定理（一般形式）

设状态空间 S、观察 q : S → O、装载 L、卸载 U。若存在观察层变换 Lₒ, Uₒ 使两个方块交换

q ∘ L = Lₒ ∘ q        q ∘ U = Uₒ ∘ q

则

(∀ s, q (U (L s)) = q s)   ⟺   (∀ o ∈ range q, Uₒ (Lₒ o) = o)

即逐状态的往返与可达观察值上的左逆是同一件事；由此逐次运行的核对等于观察商上的恒等。
推论（含机器可读的反例）：单射/满射只在可达值域内成立、Lₒ ∘ Uₒ 幂等且不动点恰为装载像、
多组件必须反序卸载、幂等本身不构成闭包。

三态判决

不要求「全世界可逆」，要求不许静默：verified-reversible / declared-irreversible / unknown，
其中第一档必须由三项独立核对挣来（装载记录对账、撤销报告对账、往返快照），判决 fail-closed。

这一版里有什么

• Reversibility/：七个模块（一般定理与推论、三态判决与可靠性、正反试件、精确有限例、语句守卫），
  只依赖 Mathlib，lake build 通过（CI 每次推送都跑）。
• CORRESPONDENCE.md：记号与论文节号、定义号的逐条对应，机器核的那一栏与要人读的那一栏分开写。
• skill/plugin-teardown-obligation/SKILL.md：给插件作者的那条义务的落点 ——
  能进 mediation 的一律进并交回 cleanup，进不去的必须具名，声明永远覆盖不了一次失败的 cleanup。
• PROVENANCE.md / BUILD.md：来历与构建记录。

范围

证明的是编码进去的语句与前提。不涉及：任何真实系统的可逆性；工程观察与论文 contextual equivalence
之间的桥（那需要一个显式前提）；declared-irreversible 与 unknown 的「不可逆」含义；
物理状态的全等（L ∘ U = id）。判决相对于一个声明的观察面成立，观察面是政策选择。