超立方体 Ramsey（openai/math 家族 171）攻坚日志｜D25–D30：商赋值纤维界、Row‑Link 树见证编码与小像赋值两步合并因子分解（Lean4 形式化审计）
专栏：ER‑03 超立方体 Ramsey（r(Qn,Ks)r(Q_n,K_s)r(Qn,Ks)，Burr–Erdős 猜想）形式化证明审计
工具栈：Lean 4.32｜固定隔离复验器｜Hash‑bound 证据账本｜Matrix 证据合约治理
状态标记：H11 = PARTIAL；主定理链路未闭合，仅底层计数、商结构、赋值因子化骨架完成，不代表原论文证明成立
作者：Valhalla Matrix治理实验室
前言
本阶段从商映射下纤维恒定赋值的加权和等式切入，依次完成：商赋值双射与纤维子和上界、固定树端口选择计数、最短根路径规范父指针构造、跨树父编码与树见证单射上界、端口方向等价与匹配条件核验，最终闭合小像赋值的两步合并因子分解。
整条链路的核心目标：把论文里的「违规赋值事件」约束，翻译成Lean内部可控的商纤维受限求和模型；全程坚持一个审计铁则：单向包含、基数上界、编码单射 ≠ 论文事件等价，绝不提前放行概率、Hall引理、Ramsey主链。所有失败迭代、simp化简告警、影子收据偏差全部留档，区分「编译通过」「固定复验通过」「论文语义对齐」三层验收标准。
D25｜两步商赋值：Pullback等价 & 纤维恒定赋值加权子和（h11merged136）
设满射商映射f:X→Yf: X \to Yf:X→Y，我们首先建立pullbackAssignmentEquiv：Y→αY \to \alphaY→α的商赋值，和满足纤维不变条件（f(x)=f(y) ⟹ assign(x)=assign(y)f(x) = f(y) \implies \mathrm{assign}(x) = \mathrm{assign}(y)f(x)=f(y)⟹assign(x)=assign(y)）的原图赋值构成双射。
重点结论quotient_supported_sum_eq_fiber_restricted：商图带 row 端点支持约束的加权和，精确等价于原图上纤维恒定赋值子集的加权和。
⚠️ 关键区分：这个等式不是原图全部合法赋值的求和相等。只有纤维恒定的这一部分被纳入商求和；其余不满足纤维不变的赋值依然可以有正权重。在 row kernel 非负前提下，可以得到：纤维恒定子和 ≤ 原图全体支持赋值之和。
针对两次合并商twoMergeClass a b c d，导出two_merge_fiber_restricted_supported_row_partition_bound，将纤维子和接入已有的消费者界：q⋅Bp−2⋅A2q\cdot B^{p-2}\cdot A^2q⋅Bp−2⋅A2。
✅ 工程验收：Lean 4.32 隔离重放零诊断；公理仅propext、Classical.choice、Quot.sound；hash verifier PASS。
🔴 开放缺口：尚未确认论文定义的「许可赋值」是否恰好等于这套纤维恒定赋值；多重性、代表选取规则未对齐，暂时不能把该界直接作为论文事件上界。
D26｜固定Row-Link树：端口选择代码计数（h11merged139）
针对有限标号简单树Fin p\mathrm{Fin}\ pFinp，基础引理：ppp顶点树有p−1p-1p−1条无向边。
构造treeEdgeIndexEquiv，将边集合与Fin(p−1)\mathrm{Fin}(p-1)Fin(p−1)等势每条 link 两侧有两组端口选择择Fin 2×Fin 2\mathrm{Fin}\,2\times\mathrm{Fin}\,2Fin2×Fin2，证明固定一棵树时，全部端口选择总数为4p−14^{p-1}4p−1。
进一步固定根节点，构造tree_endpoint_choice_diagram_code_injective：单棵树的端口选择代码，可以单射嵌完整 diagram 代码空间间。
✅ 价值：论文计数表达式里的端口因子，在单树场景下完成形式化闭合。
🔴 开放缺当前 parent 字段是固定常值常值，这套编码不能从代码反向恢复不同的树；pp−1p^{p-1}pp−1的父指针因子还无法用于跨树的见证总数上界。
D27｜最短根路径：规范Parent映射构造（h11merged144给定有限树与根 root，定义rootedTreeParent：对每个非根顶点，映射到根到该点最短路径的倒数第二个顶点。点证明两条基础性质：parent 与子顶点相邻；顶点到根的距离严格减 1。1。
使用rootedTreeParentCode，定义域限定在非根顶点集合，规避索引越界，同时证明每个父指针代码对应一条真实树边。
✅ 价值：拿到一套不依赖样例、对所有有限树通用的父指针生成构造，是跨树恢复树结构的前置底座🔴 开放缺口：未证明 parent 映射是单射/满射，无法推出不同树对应不同 parent 代码；边位置对齐、端口索引运输待 D28 解决。解决。
D28｜跨树Parent恢复，Row-Link见证计数上界（h11merged147）
本阶段是计数链路的核心卡点闭合。rootedTreeParentEdge将每个非根子节点映射到对应的无向父子边；利用根距离严格下降，排除双向互为父节点的循环矛盾，直接得到该映射单射。
有限集合基数相等、单射即满射，得到rootedTreeParentEdgeEquiv，父指针集合与树边一一对应；进而证明rootedTreeParentCode_recovers_tree：父代码相同 ⇒ 两棵树完全相等。
定义见证类型RowLinkTreeWitness p：标号树 + 全部边上端口选择的依赖和类型。
构造统一索引nonrootRowIndexEquiv，不同树共用同一套子节点位置；编码同时存储【父指针信息 + 对应边端口pair】，证明整体编码单射。
由此得到核心上界：
card(RowLinkTreeWitness p)≤pp−1⋅4p−1 \mathrm{card}(\mathrm{RowLinkTreeWitness}\ p) \le p^{p-1}\cdot 4^{p-1}card(RowLinkTreeWitnessp)≤pp−1⋅4p−1
工程复盘插曲：h11merged146数学正确，但残留不必要
simpa告警，固定复验器直接拒绝PASS；清理冗余化简为普通simp后，h11merged147零诊断通过。
治理结论：Matrix影子收据、AI辅助检索召回结果，仅作为流程快照，不能替代Lean原生编译诊断，证据验收必须绑定原生可复现哈希。
🔴 开放缺口：根节点固定，没有计入换根因子；端口pair存储顺序沿edge.out方向，还需要方向等价桥接；论文代表码、许可赋值语义、事件覆盖关系仍未接通。
D29｜父子方向等价、匹配条件、商关系不变性（h11merged1回到论文原文区段做规格对齐：论文的结构见证是标号行上的生成树 + link 端点识别，不把 root 作为独立见证字段，root 可以统一固定，不需要额外乘ppp的根选择因子。择因构造edgePortOrientationEquiv：根据边输出端点是否为 parent，选择恒等或者坐标交换，建立端口方向的等价转换。价核心等价结论：编码的父子端点配对，双向覆盖原始selectedEndpointPair；编码生成的等价关系Relation.EqvGen，和原始端点路径等价关系完全一致——编码不会改动端点商结构，不只是标签相等或者单向保边。向保定义匹配见证子类型MatchingRowLinkTreeWitness，收纳逐 link 标签匹配的树见证；连通 row-link 图可以构造出该类型实例，并且匹配条件和编码判定条件互为 iff，复现匹配见证同套计数上界。数上界。
✅ 价值：补齐端口方向转换层，消除「编码顺序和论文端口定义不一致」的语义🔴 开放缺口：两次合并后的赋值覆盖定理缺失；不能用 D25 纤维子和不等式反向冒充违规事件上界。事件上界。
D30｜小像赋值：两步合并因子分解（h11merged设赋值定义域∣X∣=p+1|X|=p+1∣X∣=p+1，赋值像大小range(assign)≤p−1\mathrm{range}(\mathrm{assign}) \le p-1range(assign)≤p−1。p-1$。
由鸽巢原理：像集容量不足，一定存在一对不同原元素映射到同一第一步：识别这对点，商映射到第一次合并类，赋值像保持不变，商集合大小为ppp；为ppp；
再次使用鸽巢原理，在一级商内部找到同标签等价类，执行第二次合并，得到两阶段商。
定理exists_two_mergers_factoring_small_image：所有这类小像赋值，都可以被分解为上述两步合并商；进一步exists_two_mergers_fiber_constant_small_image：原赋值在该两步商的每一条纤维上恒定。
✅ 价值：完成违规赋值的标准化分解构造，是「违规赋值被有限多组两步商纤维赋值覆盖」的前🔴 开放缺口：尚未证明违规赋值集合可以被这些纤维恒定赋值的并集覆盖；并集加权和的控制、代表选取的(p+1)4(p+1)^4(p+1)4界待验证。$界待验证。概率核、Hall引理、Ramsey主线保持冻结，不提前启动。
本阶段全局总结 & 下一阶段切口
D25–D30 完整打通一条底层骨架：
商映射纤维求和 → 单树端口计数 → 规范父指针构造 → 跨树树恢复与见证上界 → 端口方向等价匹配 → 小像赋值两步合并分解。
所有定理均在Lean4内隔离可复现，公理集合严格收敛，无新增强公理依赖；同时守住审计底线：骨架引理 ≠ 论文主论证成立。
下一轮攻坚唯一切口：
- 证明违规赋值被两步商纤维恒定赋值族覆盖；
- 完成代表选取编码，建立并集加权上界；
止损规则：若该包含方向无法证明，按预案暂停171项目，不再继续向上推进概率、Hall与Ramsey链路。
免责声明：本文为形式化审计攻坚日志，不构成对原Burr–Erdős猜想相关证明的正确性背书；所有结果为Lean内部模型引理，H11状态持续PARTIAL。
