置真对接架构：理论基础、条件命题与产品研究框架
状态：研究提案与数学审计，2026-10-19 修订。本文不是已实现能力说明，也不替代现行对象、权限、审批、执行或客户端契约。
2026-10-21 注：第 2 节所说的现行设计（对象标准的五要素、执行流、审批规范、五个固定 Hook）已随旧服务器退役，“B/C/D/E、现有执行链和已批准规则继续按其当前规范运行”一句不再成立。现行设计的权威是通用模型（contracts/model.json，摘要见通用模型）；本文作为研究提案的地位不变。
本文修订 ea926d4 中的原稿。原稿中的“四大定理”“最高裁决准则”“100% 真值”“有限轮完美收敛”等整体保证没有完成相应证明，本版撤回这些保证及其对既有设计的自动取代效力。历史原稿由 Git 保留。
本文保留受限生成、精确引用、确定性转换、结构化检查与受控执行这些研究方向，并分别说明文献基础、条件命题、未证假设和候选实现。文中的小型证明是条件性的手工推导，未经过证明助手机械检查；它们不构成整个 Circle 平台的可靠性证明。
1. 研究问题与论证纪律
研究对象是在只能部分观察、会持续变化的工程系统上完成任务的 agent。任务可能同时包含：
- 状态目标：修改程序、恢复服务、改变配置或形成符合契约的制品。
- 认知目标：确认版本影响、排除假设、定位原因或检验性质。
- 过程约束：权限、资源范围、安全不变量、时间与计算预算。
- 完成条件：哪些结果必须发生，哪些判断需要何种范围的证据。
“恢复了服务”和“确定了根因”是不同的完成条件。把它们分别表示，是受认知与现实状态目标联合规划研究启发的建模选择，不是证明所有工程任务都能归约到一个可解问题。
本研究区分三层工作：
| 层 | 要回答的问题 | 不能由什么替代 |
|---|---|---|
| 理论内部有效性 | 定义是否一致，结论是否由明确前提推出 | 测试通过、论文数量、架构图 |
| 模型适用性 | 真实系统是否满足模型的覆盖、观察和干扰假设 | 模型内证明、来源 SHA |
| 实现符合性 | 代码、编译器和执行协议是否实现了规定语义 | 类型正确、接口返回成功 |
每项保证应有定义、量词、前提、证明或反例、适用范围与实现义务。“定义”“文献已有结果”“本文条件命题”“工程策略”“架构候选”“未证假设”不得混写。
2. 与现行设计的关系
本研究不以误读现行设计为前提：
- 对象标准与运行对象参考划分权威状态和职责；专业算法与领域验证已有方法层归属。职责划分与计算闭环可以同时存在。
- 执行流已有持久状态、观察、动作与步骤身份。纯状态转换函数不直接调用模型，不能据此推出整个系统不能调用模型或形成循环。
- 知识 V1 参考把精确解析与语义判断分开。semantic=not-asserted 限制结论范围，不否定已完成的结构检查。
- 审批规范已有绑定具体执行输入、只能由对应操作消费的 execution-submission。按操作影响细化策略是研究方向，不是从“旧设计完全无执行审批”推出的结论。
- 五个固定 Hook 及其领域 subject 确实是现行契约。是否以及如何通用化，需要独立的契约设计、兼容方案与验收，本文不直接废除它们。
B/C/D/E、现有执行链和已批准规则继续按其当前规范运行。任何替代设计须单独确认范围，再修改代码和契约。现行行为与实现进度仍见对应设计文档及阶段记录。
3. 值得引入的理论及其边界
| 理论 | 可借鉴的内容 | 不能直接继承的保证 |
|---|---|---|
| 认知规划与部分可观测决策 [R1][R2] | 区分状态目标与认知目标；依据行动与观察更新认识；条件式计划 | R1 使用有限状态、确定性动作和规定的感知语义；R2 的状态估计与最优性结论依赖指定的转移、观察及决策模型 |
| 抽象解释与语义保持 [R3][R11] | 明确表示所保留的性质；证明模型或转换与具体行为的关系 | AST、命令树、配置和日志不会因连成图而自动等价；确定性转换本身不证明正确性 |
| 程序逻辑与语法引导合成 [R4][R5] | 前后置条件、组合义务、候选语法和语义规格 | Schema 正确不证明语义正确；部分正确性不证明终止；有限语法描述不意味着候选程序集合有限 |
| 反例引导抽象精化 [R6] | 区分实际反例和抽象引入的伪反例，按证据细化模型 | 任意现场失败不自动证明模型错误，也不授权削弱验收条件 |
| 证明携带代码 [R7] | 将候选生产与独立检查分开，缩小需信任的检查核心 | 内容哈希、签名或测试报告不是形式化证明，也不自动授权执行 |
| 溯源与增量计算 [R8][R9] | 记录输入、活动、责任、推导和依赖；判断哪些结果需要重新计算 | 溯源不证明结论为真；实时观察不能仅按文件缓存规则永久复用 |
| 时序规格与因果推理 [R10][R12] | 分别研究执行轨迹性质，以及观察、干预与原因判断 | 最终状态恢复不证明过程中没有损失；相关观察不自动识别因果关系 |
各理论有不同的状态、概率、时间和观察假设。将它们组合需要定义接口处的语义关系，并重新建立所需性质，不能把文献的保证直接相乘或相加。
4. 一个最小的集合式知识更新模型
本节固定同一模型修订、命题解释和任务范围。它是条件命题的形式对象，不声称真实工程系统已经满足这些假设。
定义：
- S：该范围内的具体系统状态集合；状态必须包含所讨论性质依赖的信息。
- A：动作集合。
- s_t：第 t 个观察边界对应的真实状态。
- B_t ⊆ S：尚未排除的可能状态集合，不是概率分布。
- T(s,a) ⊆ S：从 s 执行动作 a 到下一观察边界之间，真实系统可能到达的状态；包含该区间内允许的环境干扰。
- T_hat(s,a) ⊆ S：实现所使用的转移近似。
- C_a(o) ⊆ S：与动作 a 后观察 o 相容的状态集合。目标、版本、时间、读取范围和解析方式属于观察语义的一部分。
定义更新：
Post_hat(B,a) = ⋃ { T_hat(s,a) : s ∈ B }
B_(t+1) = Post_hat(B_t,a_t) ∩ C_(a_t)(o_(t+1))
P1：真实状态覆盖保持（条件命题）
前提：
- A1 初始覆盖：s_0 ∈ B_0。
- A2 转移覆盖：对范围内所有 s,a，T(s,a) ⊆ T_hat(s,a)。
- A3 观察保守：每个实际观察 o_(t+1) 都满足 s_(t+1) ∈ C_(a_t)(o_(t+1))。
- A4 轨迹与时点一致：实际步骤满足 s_(t+1) ∈ T(s_t,a_t)；用于相交的观察描述同一个边界的状态。分时采样、外部修改及延迟必须纳入 T、状态或观察模型。
结论：
对所有已定义的步骤 t，s_t ∈ B_t
证明：t=0 由 A1 成立。假设 s_t ∈ B_t，由 A4 有 s_(t+1) ∈ T(s_t,a_t)，再由 A2 得 s_(t+1) ∈ T_hat(s_t,a_t)，因此属于 Post_hat(B_t,a_t)。由 A3，它也属于 C_(a_t)(o_(t+1))，故属于二者交集 B_(t+1)。由归纳得证。
这是标准保守状态估计思路下的一段手工推导，不主张新的数学发现。P1 不证明 A1–A4 在某设备、解析器、数据集或执行协议中成立，也不证明计划安全、最优或最终成功。
C1：带范围的性质判定（P1 的条件推论）
令 P 是 S 上解释固定的性质。若 B_t 非空且对 B_t 中所有状态 P 都成立，则 P(s_t) 成立。证明：由 P1，s_t 是 B_t 的成员，直接应用全称条件。
判定接口必须区分：
- B_t 非空且全部状态满足 P：在本节前提下支持 P。
- B_t 非空且全部状态满足非 P：在本节前提下反驳 P。
- B_t 同时包含满足与不满足 P 的状态：未决。
- B_t 为空：假设与观察不相容；不得利用空集上的全称命题判定业务性质为真或为假。
这些是研究模型的判定含义，不是对现有 API 状态枚举的修改。历史观察只支持其对应边界的状态；跨到派发时刻需要额外转移或原子条件。
缺少前提时的反例
| 缺口 | 反例 | 失去的保证 |
|---|---|---|
| 初始覆盖失败 | 真实目标运行另一构建，但初始状态只包含预期构建 | 后续推导可能始终自洽，却描述错对象 |
| 转移覆盖失败 | 建模时遗漏重启、并发管理员修改或远端已接受但本地未收到回执 | 真实后继状态可能被排除 |
| 观察不保守 | 将超时解释为“未执行”；实际已执行但回执丢失 | 可能错误重派并产生重复副作用 |
| 观察时点不一致 | 拼接不同时间的两个字段，假装成一份原子快照 | 两项分别真实的观察也可能产生错误交集 |
| 空集被当作成功 | 冲突数据把 B_t 清空后，使用“全部候选都满足 P”放行 | 同时可以推出 P 与非 P |
对于丢失回执，观察相容集合通常需要保留“已执行”与“未执行”的可能性，除非有额外协议事实排除其中一种。仅增加置信度字段不能修复错误的观察语义。
本流程只有在所需协议前提已按目标版本认证、请求记录覆盖本次投递且可按原请求身份核对时，才把丢回执的未知限定为持续到核对完成：先只读核对请求记录、作业记录或回读结果，再按所得凭据判定；“查无记录”的未执行证明还受记账与清理边界约束。缺这些前提或核对证据时，上述两种可能性仍须保留，按 D04、B07 继续核对、恢复证据或重新证明基线，不把超时解释成未执行。
5. 有限搜索与终止：另一项独立命题
P2：有限候选穷举的轮数上界（条件命题）
| 固定任务规格及其解释，令候选集合 H 有限， | H | =N。假定： |
- 每轮检查一个尚未检查的候选；选择和检查都在有限时间内结束。
- 检查器对该固定规格给出正确且完备的通过或不通过结论。
- 搜索持续到发现通过候选或 H 耗尽；不在中途更改规格、候选集合或检查器语义。
则至多 N 次候选检查后，找到一个满足规格的候选，或者确认 H 中没有满足规格的候选。
证明：每次不通过都移除一个此前未检查的候选，剩余数量严格减一。若有通过候选，正确检查器接纳它；若 N 次均不通过，由穷尽性，H 中没有解。
这一上界是候选检查次数，不是统一的墙钟时间或实际运行效果保证。它也不证明 H 覆盖用户允许的全部方案。若检查器可返回 unknown，或者只是有限测试，不能据此确认 H 无解。
反例与边界：
- 即使 H 只有“正确”和“错误”两个候选，生成器始终重复错误候选也不收敛。
- 有限的语法符号可生成无限多个程序；类型或 JSON Schema 约束不自动满足有限 H。
- 修改规格、模型或方法版本后，原轮数证明不自动适用。
- 用固定预算 K 停止，只保证运行受到限制；用完预算不证明存在解或已找到正确解。
- LLM 建议顺序可以帮助搜索效率，但不会自动建立不重复、完备性或终止条件。
6. 仍待定义和证明的核心性质
下列事项是证明义务，不是本文已经获得的定理：
| 事项 | 必须补齐的定义和前提 | 实现需要承担什么 |
|---|---|---|
| 转换保持规定语义 | 源语言、目标语言、观察口径、允许行为及转换关系 | 转换器证明，或明确范围的逐产物验证；固定版本与输入 |
| 方法组合正确 | 前后置条件、资源范围、干扰假设、顺序与并发语义 | 检查相邻契约，处理共享状态；分别论证终止 |
| 原件引用保持 | 引用解析、权限、字节身份、编码与装配语义 | 不透明引用与字节核对；仍须检查是否引用了正确对象 |
| 判断有充分依据 | 命题含义、来源与模型范围、检查器性质 | 保存依赖、未决条件、反例及适用时点 |
| 原因可识别 | 候选模型、允许观察和干预、区分条件 | 表示竞争解释并选择实验；不可区分时不强行给唯一原因 |
| 执行不越权或重复 | 授权消费、目标端协议、并发、故障及恢复模型 | 派发、接受、结果与对账分开；目标端条件与身份核对 |
| 进展与恢复 | 安全不变量、终止条件、公平性及环境可用性假设 | 预算、等待、取消、恢复和 unresolved 路径 |
“零转录”只移除模型重新生成原字节这一类故障通道；来源选错、引用错绑、编译器错误和过期状态仍需要各自的分析。SHA 或签名证明身份/完整性的能力，不等同于证明业务性质。
可逆性是操作策略的一个输入。恢复配置不说明期间的连接、外部通知或业务损失已恢复。状态差分、环境重要性、授权范围、可观察性及恢复条件应分别建模。
执行安全研究对象是完整轨迹，而不只是最终状态。检查与写入之间存在干扰时，单独的派发前哈希检查不建立原子条件；需要目标端协议或另行证明的互斥边界。
7. 从理论到产品的候选框架
以下划分是设计选择，没有唯一性或整体可靠性证明。
两条编译链
- 领域编译链：版本化资料与接口 → 结构提取与模型构建 → 领域类型、谓词、转换、动作和观察能力。语义推断应保留为带依据的假设；不能把所有提取结果自动提升为真实行为。
- 任务编译链：用户目标 → 明确任务规格 → 验证义务 → 有条件分支的行动计划。每项义务说明命题、范围、可接受证据与未决处理。
运行证据反馈到知识和任务两条链。修改候选方案与修改领域模型是不同活动；模型、规格或验证器变更均形成新修订，并有独立的审查与回归依据。
逻辑模块与责任
| 模块候选 | 要实现的职责 | 关键对象 |
|---|---|---|
| 领域模型与方法 | 规定类型、行为、转换、观察与检查语义 | 模型修订、方法契约、转换器、验证器 |
| 知识与证据 | 保存原件、观察、推导依赖与适用范围 | 来源修订、证据、结论、依赖图 |
| 任务编译 | 将目标分解成待满足条件及方法候选 | 任务规格、验证义务、候选计划 |
| 规划与实验选择 | 在预算和权限内选择调查、构造、检查或行动 | 假设集合、实验、分支与预算 |
| 核验与授权 | 分别检查条件满足与动作授权 | 验证记录、策略决定、单次许可 |
| 持久执行 | 实现派发、并发、断连与结果核对协议 | 操作意图、租约、回执、对账 |
领域语言须有语法、类型和执行/解释规则。TypeScript 类型及运行时 schema 只承担其明确的结构检查，不代替上述语义或协议保证。模型可以提议候选和调查步骤；声明“已验证”或持有一个哈希不能绕过权威检查与授权。
不同产品线可以有不同的领域语言，共享检查、证据和执行契约；本研究不要求一个全能 IR，也不要求先拆成六个部署服务。具体迁移须检查现有代码与消费者边界后单独设计。
产品视图
任务页面可围绕目标、已知事实、竞争假设、待验证条件、候选变更、授权与实际结果组织。应能区分“任务已交付”“某项性质在某范围内已检查”和“外部状态已改变”。这些界面是研究候选，不是本次文档修改已经交付的功能。
8. 数学审计优先的研究顺序
- 冻结最小定义与假设，明确每项性质的量词、语义与范围。
- 完成条件命题的手工证明，并用反例检查每个前提是否必要、是否充分。
- 对适合机械化的部分使用证明助手；对有限协议模型使用模型检查。分别报告证明助手信任基、模型边界和未覆盖情况。
- 建立真实来源、解析器、转移近似、观察器与形式模型之间的对应义务。
- 使用已有工程原件、执行记录和获授权的追踪数据寻找反例、检验适用性与实现符合性，不以更多样本替代证明。
- 仅在这些边界明确后，决定核心接口、领域包契约和迁移范围。
现有工程与追踪资料可作为后续研究材料，当前优先级是推导和假设审计，不是新增样本收集。公开文档只记录可公开的定义、脱敏合成反例与结论范围；访问位置、凭据、原始业务内容与私有追踪不进入公共仓库。
本文仅提供 P1、C1、P2 的手工条件证明和若干逻辑反例；没有机械证明、真实数据结论、目标端保证或平台整体正确性证明。参考归档 SHA/Git 树检查与其测试仅验证归档完整性，不验证本文数学或架构。
9. 原始研究与标准
- R1 Baier、Mombourquette、McIlraith，2014，Diagnostic Problem Solving via Planning with Ontic and Epistemic Goals。
- R2 Kaelbling、Littman、Cassandra，1998，Planning and Acting in Partially Observable Stochastic Domains。
- R3 Cousot 与 Cousot，1977，Abstract Interpretation。
- R4 Hoare，1969，An Axiomatic Basis for Computer Programming。
- R5 Alur 等，2013，Syntax-Guided Synthesis。
- R6 Clarke 等，2000，Counterexample-Guided Abstraction Refinement。
- R7 Necula，Proof-Carrying Code 研究说明与原论文入口。
- R8 W3C，2013，PROV-DM。
- R9 Mokhov、Mitchell、Peyton Jones，2018，Build Systems à la Carte。
- R10 Lamport，Specifying Systems。
- R11 CompCert，语义保持、验证范围与编译器结构。
- R12 Pearl，The Three Layer Causal Hierarchy。
这些引用说明可采用的理论及其原始范围，不为本提案的组合或实现背书。本提案不主张上述研究、公理或一般方法为 Circle 的独创。
许可
Copyright (c) 2026 qingshanfeihu。本文的文字与图表按 CC BY 4.0 授权，引用与改编按许可证署名 Circle Hub 与 qingshanfeihu、注明原始出处及修改。被引用研究保留其各自作者与许可。见设计索引与 NOTICE。