观察收敛的条件形式化：基于 Isabelle/HOL 的模型与边界分析

摘要 关于观察的哲学论述，常在已记录的事件、获接受的结果、稳定的判断，以及对这些现象如何产生的解释之间转换。形式化处理必须明确这些转换。本文报告一项在 Isabelle/HOL 中展开的 RC 条件接口开发；RC 即《过程实在论：观察收敛与确定性生成（RC）》，是一个以观察收敛为中心的过程实在论研究纲领 [9]。该开发区分了语境内容、已实现主体、行动、历史记录、当前有效性、分类与延续。它提供了从有限时间精确共识到持续登记标签的条件适配器；内容残余与任务信息损失分解的有限概率证明，包括带守卫的等号成立条件；针对特定事件的报告来源追溯；异议登记协议；以及运行特征见证接口。具体解释包括双主体平均化轨迹、具有零损失和正损失的联合记录／概率模型、三事件异议轨迹，以及预登记的机制特征案例。失败对照揭示了记录缺失、分解结构缺失、来源选择、独立审计、调度与运行值缺失各自的作用。一般的有界信任收敛定理仍是适配器的一项显式输入，而其小规模具体实例则通过计算完成证明。信息论结果属于标准数学；若干事件结论只是定义或假设的展开。归档的、与源文件绑定的复现涵盖 Isabelle2026 下的四个会话与十八个理论。候选贡献在于：对 RC 条件接口、所选场景中共同实例化的义务及其失败边界，给出可检查的说明。新颖性仍需进一步审查；七项完整语义缺口依然存在，也不能由此推出 RC 的整体一致性或经验真实性。