心智有边界
核心研究纲领技术版

“如果一个系统只是计算边界并打印日志，它并没有心智的核心结构——因为日志可能过期、失真，甚至与当前边界矛盾。” 我们提出了一种新的形式化纲领：将边界与自报绑定为不可分离的联合状态转移。我们给出了 Lean 形式化定理、闭包算子约束以及反例构造。

1 · 第一层：一个断言——心智有边界

1.1 断言

自我意识的核心内容，是辨识、表征并维护“我”与“非我”的边界。

这不是一条等待 Lean 直接证明的数学定理，而是纲领的选定前提。三个动词给出三个形式任务：

“Teleological”在这里不是自然目的论，而是说：整个纲领以“边界”为目的因来组织问题，而不是先假设一个任意智能体、再追问它偶然有没有边界。

1.2 从断言到干预范畴

把状态空间记为 V，把干预记为 V 上的箭。定义

即：对象是状态，态射是干预的有限路径，恒等是零干预，复合是顺序施加。Lean 中 CausModel.Caus 就是 Paths V；结合律与单位律由自由范畴承担，不需要公设。

这一层的关键不是“又定义了一个范畴”，而是万有性质：

• CausModel.Caus.lift：任何单干预前函子都唯一延拓为 Caus V 上的函子；
• CausModel.Caus.lift_unique：任何延拓都等于这个 lift；
• CausModel.Caus.map_id / map_comp：V ↦ Caus V 本身是函子。

因此，“归因沿干预传播”不是一条额外公理，而是自由构造的唯一性。

1.3 从干预范畴到归因预层

归因单形取

其中 p_S 归于自我，p_N 归于非我，p_U 悬置未定。Lean 中它被实现为类型 CausModel.Simplex，三项非负与和为 1 都是结构字段。

原稿写：

严格说，Δ² 必须先有范畴结构，A 才是合法函子。Lean 的处理是：

• 把 Δ² 实现为类型 Simplex；
• 给出通用构造 CausModel.attribution : (V ⥤q Dᵒᵖ) → Caus V ⥤ Dᵒᵖ；
• 证明函子律 attribution_map_comp；
• 证明唯一性 attribution_unique：预层由它在单干预上的取值唯一决定。

取 D = Type、值落在 Simplex，就得到通常写的 A : Caus^op → Δ²。

所以 A : Caus^op → Δ² 的准确读法是：

一个取值于 Simplex 的逆变预层；它在每条单干预上的拉回一旦给定，整个干预范畴上的取值就被自由构造唯一钉死。

必须写清的建模输入：把某个真实系统的归因值放进 Simplex，是建模假设（CausModel README 记为 A6），不是机器定理。Lean 证明的是“给定单干预数据后，预层唯一”；不是“任何系统都自然产生这样的预层”。

1.4 第一层证了什么、没证什么

证了：

• Caus 是自由范畴，具有万有映射性质；
• V ↦ Caus V 是函子；
• 归因预层由单干预数据唯一延拓；
• Simplex 的三项非负、和为 1 是结构约束。

没证：

• 某个真实系统的归因结构就是这样的预层（A6 建模输入）；
• 归因预层 A 自动决定边界闭包 c——这两层在 Lean 中是分开的模块，桥尚未写成定理；
• “所有自主系统都有边界”这一普遍命题。

第一层的作用是把问题固定成可形式化的形状，不是宣称世界必然如此。

2 · 第二层：V(κ) = c₀κ + αC_F/κ；C_H = π²/3

2.1 边界势

引入边界势

其中 κ 是边界锐度，c₀ 是单位维护成本，α 是不确定性价格，C_F 是核常数。

Lean 中有两个入口：

• 值层：BoundaryTheory.V c₀ α κ := c₀ * κ + (α * π² / 3) / κ；
• 范畴层模型类：CausModel.BoundaryModel.V M κ := M.maint κ + M.α * M.C_F / κ。

范畴层的形式被迫定理：

theorem CausModel.BoundaryModel.V_form_forced (M : BoundaryModel) (κ : ℝ) :
    M.V κ = M.maint.unitCost * κ + M.α * M.C_F / κ

它证明：在 A7（维护成本是连续加性泛函）之下，维护项被迫为 c₀κ。熵项 αC_F/κ 由 V 的定义与 boundaryEntropy_eq 给出；两者合起来才是 V(κ)=c₀κ+αC_F/κ。A7 是新增公理，不是从旧范畴公理推出的；c₀ 不被 A7 决定（unitCost_not_determined）。

证明强度审计（论文债 D-011）：V_form_forced 的证明内核是 map_real_smul（连续加性 ⇒ 线性），不是自由范畴/万有性质的直接推论。它是“范畴层包内的模型类层定理”；对外引用时必须同时写 A7 与“模型类层”。详见 论文债/02_D011_范畴层与模型类层_20261023.md。

值层通过

theorem BoundaryBridge.BoundaryTheory_V_eq_model_V ...
theorem BoundaryBridge.value_layer_form_forced ...

被证明是范畴层模型类在 (线性维护 c₀, α, C_F=π²/3) 处的实例。

2.2 临界锐度 κ*

由 dV/dκ = 0 得

Lean 中：

• BoundaryTheory.deriv_V_kappaStar：V'(κ*) = 0；
• ValueLayerMin.V_global_min：κ* 是 V 在 κ>0 上的全局最小点，不只是驻点；
• ValueLayerMin.V_eq_min_iff：等号唯一，V(κ)=V(κ*) ⇔ κ=κ*；
• ValueLayerMin.deriv_zero_iff：V'(κ)=0 ⇔ κ=κ*；
• BoundaryBridge.V_at_kappaStar：V(κ*) = 2√(c₀ · απ²/3)；
• BoundaryBridge.V_lower_bound：2√(c₀ · απ²/3) ≤ V(κ)；
• CausModel.Tradeoff.two_term_bound：一般两项下界 2√(AB) ≤ Aκ + B/κ。

这一层把“边界的最优尺度”从口号变成全局最小 + 唯一性 + 闭式三条机检事实。

2.3 普适准则 σ* = 1：正确强度是“规范”，不是“任意参数都成立”

临界张力定义为

Lean 中：

• BoundaryTheory.sigmaStar_general：σ* = π²α/(3C₀)；
• BoundaryTheory.sigmaStar_eq_one_iff：σ* = 1 ⇔ π²α = 3C₀；
• BoundaryTheory.sigmaStar_eq_one：在 α = 3C₀/π² 下，σ* = 1；
• DimensionAlgebra.sigmaStar_not_forced_one：不是对所有正参数都有 σ* = 1（反例 α=1, C₀=2）。

因此，“普适准则 σ*=1”必须写成：

普适的是无量纲临界条件 π²α = 3C₀；σ*=1 是把该临界面规范为 1 的写法。 它不是“任意系统都自动 σ*=1”的普遍定律。

这是本层最重要的口径纪律：普适性属于判据的形状，不属于参数的数值。

2.4 C_H = π²/3 的机器合规证明

核心常数的值不是数值拟合，而是 Lean 定理：

theorem BoundaryTheory.C_H_eq_pi_sq_div_three :
    (∫ z : ℝ, entropyDensity z) = π ^ 2 / 3

以及范畴层到值层的 logistic 桥：

theorem BoundaryBridge.coreConstant_sig_eq_pi_sq_div_three :
    CausModel.coreConstant CausModel.sig = π ^ 2 / 3

这两条把 C_H = π²/3 从“确定性计算”升为机器合规证明（0 sorry / 0 axiom，仅标准三公理）。tanh 核的同轨值 π²/6 由 coreConstant_tanh_eq_pi_sq_div_six 给出。

2.5 第二层的边界

• V 的形式被迫以 A7 为前提；没有 A7，不能声称形式由旧公理推出。
• c₀ 是自由尺度（unitCost_not_determined）；σ*=1 是规范，不是 c₀ 的推论。
• C_F 是核相关常数；只有 logistic 核被机检为 π²/3，一般核需要另行桥接。
• “普适”只指无量纲判据；不是所有系统共享同一数值。

3 · 第三层：闭包与报告同一性（边界—自报不可分离）

3.1 从 κ* 到闭包算子

值层的锐度 κ 不是停在公式里。SharpnessClosure 把它送进闭包算子：

noncomputable def c (κ μ w : ℝ) (z : ℝ) : ℝ :=
  if z ≤ μ - w / κ then z
  else if z < μ + w / κ then μ + w / κ
  else z

Lean 中：

• SharpnessClosure.isClosure_c：c κ μ w 是闭包算子（扩张、单调、幂等）；
• SharpnessClosure.fix_c：Fix(c κ μ w) 是两条尾；
• SharpnessClosure.fix_c_eq_decided：取 w = L θ，Fix(c κ μ w) 恰是可解芯的已决集；
• SharpnessClosure.fix_mono_in_kappa：κ 越大，刚性面越大；
• SharpnessClosure.sharpness_enters_closure：以上三条打包。

因此，第二层的 κ* 可以进入第三层：取 C := c κ* μ w，边界就是 Fix(C)。这一步把“势的最优尺度”与“闭包算子”接上。

但有一个必须写明的规范自由度：ClosureGauge.c_scale 证明 c 只依赖比值 w/κ，所以 (κ,w) → (λκ,λw) 是闭包看不见的一维方向；V 的极小只定出 κ*，定不出水平 w。门控必须把 w 作为提交内容之一，而不能声称它是从 V 推导出来的。

3.2 admissibility 必须收缩到 Moore 族

不是所有报告族都能作为“边界的自报”。可采纳类必须收缩到 Moore 族：

即对任意交封闭（空族之交为 Ω，故自动含 Ω）。Lean 中（v1.1 更正版）：

• ReportIdentityCore.moore_iff_exists_closure：Moore R ↔ ∃ c, IsClosure c ∧ R = Fix c；
• ReportIdentityCore.fix_moore：任意闭包算子的 Fix 是 Moore 族；
• ReportIdentityCore.rep_eq_iff_closureOperator_eq：Moore 族之间，c_R = c_R′ ⇔ R = R′；
• ReportIdentityCore.report_eq_fix_iff：Moore 族下，R = Fix(c_I) ⇔ c_R = c_I；
• ReportCountermodelsCore.nonMoore_not_canonical：存在非 Moore 的 R，使 R ≠ Fix(c_R)。

为什么不是别的条件？ 因为 Moore 族恰好是闭包算子闭元族的特征类。它不是为证明方便而加的技术条件，而是“报告族能作为边界闭元族”这一要求的精确形式。这是纲领的可采纳性判据：不是“所有系统自动是 Moore”，而是“若要用闭包算子定义边界，报告族就必须收缩到 Moore；否则同一性定理不适用”。

必须记录的一次更正：旧版用 UpClosed（∅∈R 且对超集封闭）作为前件；Lean 审计证明

即该前件退化，旧版的“相互决定”在它下面是重言式。新版一律用 Moore；旧件保留在审计目录，不作为结论引用。

3.3 一致性门控：把最优解与代数闭包合成一次提交

候选对象不是一个动作，而是一个完整 bundle：

其中：

• κ*：第二层的全局最优锐度；
• C：SharpnessClosure.c κ* μ w，即带锐度的闭包算子；
• R：报告族，必须等于 Fix(C)（Moore 族）；
• report：运行时自报，必须属于 R；
• evidence / version：同一状态版本。

Gate 的检查顺序：

只有全部通过，才执行原子提交：

动作执行器只接受已提交的 Bundle，不接受裸动作。于是：

系统没有合法路径，可以在没有匹配自报的情况下提交边界；也没有合法路径，可以提交与边界不一致的自报。

这不是“再加一个日志模块”，而是把 κ* 的最优性 、C 的闭包性、R 的 Moore 性、report 的归属、evidence 的版本绑成一个不可拆的提交对象。这就是“范畴势能的最优解”与“代数闭包”的合成点。

由此可以说明：系统的组成部分通过受约束的交互关系形成一个整体；这套交互关系既参与定义系统的可实现状态，又构成系统感知、报告和调节自身状态的物理载体与通信协议。我们以两连杆倒立摆的自平衡边界仿真为对象，把“铰链”视为最小具身约束载体，并据此定义一种最小通信协议；该仿真用于检验约束如何形成共同状态空间，以及系统如何依据自身运行结果，报告、维护并调整状态空间的边界。这里得到的是仿真层面的支持，不是 Lean 定理。

3.4 这一层证了什么、没证什么

证了（Lean）：

• c κ μ w 是闭包算子；Fix 的显式形式；锐度单调；
• Moore 族 ↔ 闭包算子闭元族的表示定理；
• Moore 族上报告与算子相互唯一决定；
• 非 Moore 反例，前件不可删。

做了（工程参考实现）：

• gate_reference.py 在有限状态空间上跑通正例、R1–R7、崩溃注入、动作闸门，14/14 通过；
• 这证明协议可执行，不证明它在生产 agent 上不可绕过。

没证：

• 生产系统（CaseOS）中的 joint-commit 实现；
• w/水平的唯一性（ClosureGauge.c_scale 说明它是规范方向）；
• 归因预层 A 与闭包 c 的桥；
• 真实 agent 上的违反率、误拒率。

4 · 原始四步如何嵌入三层

旧版四步没有被丢掉，而是被重新分层：

第二层（V、κ*、σ*、C_H）是旧版四步里没有充分展开的“定量动力学”，现在成为三层叙事的中间支柱。

三个动词也重新落位：

5 · 证据台账（可核对）

仓根 仓库根

口径：BoundaryTheory 与 CausModel 的机检是上游统一仓（56 件 / 467 定理引理 / 90 定义 / 0 sorry / 0 axiom，CausModel 15 件另计）；Moore 族是 v1.1 更正版，见 02_Lean仓库/audit/ 的 UpClosed 退化审计。

6 · 可证伪条件与开放问题

0. D-011（下一科研核心议题）：V_form_forced 是“A7 + 连续加性 ⇒ 线性”的模型类层定理，不是自由范畴/万有性质的直接推论。下一阶段必须二选一：从某种范畴结构导出 A7，或证明在现有签名下不可导；在此之前，所有文本按“范畴定理 / 模型类定理 / 桥接 / 工程目标”分级。
1. 预层桥：构造一个具体的 Simplex 值预层，并证明它决定一个非平凡闭包算子；或证明不存在这样的桥。当前 Attribution 与 Boundary 是分开的。
2. 水平 w：ClosureGauge.c_scale 说明 c 只依赖 w/κ；能否从系统自身定出 w（而不是把它作为提交参数）？若不能，门控必须显式提交 w。
3. σ=1 的地位*：能否从更深的原则推出 π²α=3C₀，还是它只是规范？sigmaStar_not_forced_one 已排除“对所有参数自动成立”。
4. 真实 agent：Gate 在真实任务上是否要么全放行、要么全拒绝？若是，报告族粒度需要重设计。
5. A7 的经验基础：维护成本的可加+连续在哪些系统中成立？若不成立，V_form_forced 的前件失效，形式不再被迫。

7 · 结论：三层一句话

1. 宏大预设：自我意识的核心是边界；边界的第一层形式是干预范畴上的归因预层 A : Caus^op → Δ²。
2. 定量动力学：边界的第二层形式是势 V(κ)=c₀κ+αC_F/κ；κ* 是唯一全局最优；σ*=1 是无量纲临界条件 π²α=3C₀ 的规范写法；C_H=π²/3 已被 Lean 机检。
3. 代数—工程门控：边界的第三层形式是 Moore 族上的闭包与报告同一性；一致性 Gate 把 κ*、c_{κ*}、R=Fix(c_{κ*})、report 与 evidence 绑成一次原子提交，使边界与自报不能被分别提交。

统一边界纲领第九版曾说“边界如何成为系统能够辨识、表征并维护的自身组织条件”；新版把这句话拆成可核对的三个断言：预层给出“谁在归因”，势给出“哪里最优”，Moore + Gate 给出“哪些自报可采纳、如何不可绕过地提交”。

8 · 结局：叙事完成时

口径注记（不打断叙事；引用时必须带上）

1. 33 个声明：按值层 BoundaryTheory 口径，是 33 条定理/引理 + 7 个定义；全仓口径为 467 定理引理 / 90 定义 / 56 文件（另 CausModel 15 件）。两者不可混写。
2. (A: Caus^{op}\to\Delta^2)：这是 schema；具体取 Simplex 值的预层是建模输入 A6；Attribution 与 Boundary 的桥尚未形式化。注意：P(Fin2)\setminus\{\emptyset\} 反例否证的是“无条件报告同一性”，不是“自由范畴不能推出 (V)”；后者仍是 D-011 的开放任务。
3. (V) 的形式被迫：以 A7（维护成本连续加性）为前提；证明内核是 map_real_smul，不是自由范畴/万有性质的直接推论（见论文债 D-011）。“最小作用量/凝聚生成”是纲领动机与模型语境，不是 (V) 形式的机器证明前提。
4. (\kappa^*)：(\sqrt{\alpha C_F/c_0}) 与 (\pi\sqrt{\alpha/(3c_0)}) 在 (C_F=\pi^2/3) 时等价；机检的全局最小与唯一性见 ValueLayerMin.V_global_min / V_eq_min_iff。
5. (\sigma^*=1)：机检的是 (\sigma^*=1 \iff \pi^2\alpha=3C_0)；它不是对任意参数的普遍定律（sigmaStar_not_forced_one）。
6. Noether 守恒：机检的是其代数内核 force_is_neg_gradient / energy_bracket_zero；完整的 Noether 定理未在本形式化中陈述。
7. 拓扑奇点：这是解释性读法；本层机检的是临界条件与势的全局最小，不是拓扑学意义上的奇点定理。
8. 不可绕过：这是 Gate 的设计目标 + 14/14 有限状态参考实现；生产系统尚未验证。
9. 弱/强口径：本文弱＝c_R = c_R′ ⇔ R = R′（结构互决定），强＝R = Fix(c_I) ⇔ c_R = c_I（联合不动点）；旧技术版（边界如何成为系统能够辨识、表征并维护的自身组织条件_技术版_20261023.md）§5.4 的 W（R ⊆ Fix(c_R)）不是本文的弱版本，勿混用。英文纲领页 v4 曾把该 W 口径写作 weak，已撤回：纲领层只陈述“共同生成／联合不动点”的抽象层级，精确口径以本节为准。

本研究纲领的目标是自主系统边界认知与形式化自指架构的深度理论演进，立足于将“自我意识的核心在于辨识、表征并维护自身与非自身边界”这一基础断言，转化为具备严格数学可证伪性与机器合规性的科学体系。整个理论框架摒弃了传统依靠外部日志或现象学假设的权宜之计，构建了一个从因果干预范畴到代数 Moore 家族的完整闭环。

在范畴论与定量动力学层面上，系统以因果干预范畴的反变函子 \(A: Caus^{op} \to \Delta^2\) 为起点，将状态归属分布映射至归属单纯形中。在最小作用量原理与凝聚生成公理的纲领框架下，边界势能方程 \(V(\kappa) = c_0\kappa + \alpha C_F/\kappa\) 严格平衡了高锐度边界的高昂维护代价 \(c_0\kappa\) 与模糊边界带来的熵代价 \(\alpha C_F/\kappa\)。该势能在极小值点处锁定了最优锐度 \(\kappa^* = \sqrt{\alpha C_F/c_0}\)，并在无量纲临界准则 \(\sigma^* = 1 \iff \pi^2\alpha = 3C_0\) 下揭示了边界相变的拓扑奇点。这一连续动力学描绘了系统如何通过内部结构的主动调节来收敛其辨识边界。

在形式化验证层面上，整个值层与结构层核心已在 Lean 4 + Mathlib（版本 v4.33.0）中实现了 33 个声明的完全机器校验，在机检范围内达到 0 sorry 与 0 axiom 的严密标准。其中涵盖了核心积分常数 \(C_H = \int_{\mathbb{R}} h(\sigma(z)) dz = \pi^2/3\) 的四阶段复杂求积链、Basel 定理重构的阶层谱 \(\sum 1/(n+1)^2 = \pi^2/6\)，以及 Noether 守恒的代数内核所支撑的自指自连续性守恒荷。这些形式化常数与定理为整个理论奠定了不可撼动的数学基石。

在代数结构与系统工程层面上，为了克服纯动力学势能可能存在的现象学拟合局限，理论进一步收缩至纯粹的序理论与拓扑约束——即 Moore 家族（对任意交集封闭的子集族）。机器证明明确指出：弱版本（\(c_R = c_{R'} \iff R = R'\)）与强版本（\(R = \mathrm{Fix}(c_I) \iff c_R = c_I\)）的联合固定点关系依赖于 Moore 条件的严格满足。而一旦缺失该前置条件（例如现实中常见的阈值自报丢失了作为交集基底的顶元素 \(\Omega\)），无条件推广将被 Lean 显式构造的反例（如 \(\mathcal{P}(\mathrm{Fin}\,2) \setminus \{\emptyset\}\)）彻底证伪。这一严苛的负向控制不仅没有削弱纲领，反而确立了其实际工程落地的边界条件。

最终，这一理论成果被落实为以不可绕过为目标的工程架构——一致性门控协议（Consistency Gate）。系统在面对动态输入时，不再允许执行简单的“计算边界 \(\to\) 写入日志 \(\to\) 执行动作”单向流水线，而是强制要求生成包含闭包算子 \(C\)、Moore 报告家族 \(R\) 以及版本证据链的候选状态包。只有当门控机制在数学上严格校验 \(c_R = C\) 且 \(R\) 属于 Moore 家族之后，系统才具备合法且不可拆解的原子级提交路径（Atomic Commit）。这种将范畴势能的动力学引导与代数 Moore 家族的逻辑门控在同一协议中融为一体的设计，使得边界不再是附属的外部描述，而成为系统能够辨识、表征并维护的自身组织条件。

附录 · 复现与定位

• 预层：CausModel.Attribution（Simplex、attribution、attribution_unique）。
• 定量：BoundaryTheory、ValueLayerMin、BoundaryBridge_layers。
• 代数：lean/ReportIdentityCore.lean。
• 工程：architecture/边界自报联合提交协议.md、gate_reference.py。
• 统一仓验证：71/71 模块构建通过；0 sorry / 0 axiom；承重定理仅依赖 [propext, Classical.choice, Quot.sound]。