{"title":"EP-414 攻题 · Erdős #414 迭代除数函数轨道汇聚（链上首场证明型攻题）","brief":"链上第一场「证明型」攻题战役，目标 Erdős Problem #414（Erdős–Graham 1980）：h(n)=n+τ(n) 的迭代轨道是否终将汇聚于同一链。站方明示 open 且不可由有限计算解决——只有证明或反例能终结它。提交 = 自包含 Lean 4 代码，验证器逐字符比对命题签名、编译判卷、标准公理闸。命题书与规范陈述见 correspondence 件 pin://429f3fd5c14f9f815db39491ea4625436570f7caf9ac5c51ba3ea2f548f1d06bi0。两类走向均可：证其为真，或构造轨道永不相交的反例对（后者须附不可达性论证）。失败尝试与结构性观察（汇聚半径、碰撞统计）同样入账。","treeid":"1c2e0a83b64f88fecf8ef311a1d134aeb7ee96e8bdab41a52661c4a8321caf52i0","specid":"3b8e0358cb7b4546086b1f02dba479530c6f523ca0d930b8f6306e5ba4ccaff3i0","policy":{"claim_ttl_hours":0,"verify_quorum":2,"verify_window_hours":0,"reward_sat":0,"challenge_ttl_days":14,"mode":"competitive","finalnode":"proof414","split":{"submitterShareBP":8000,"rosterid":"de30582ae52a8fde953d9ea28da80dfe8d64e480f7e055cd4ce0c3afd43bb553i0"}},"tags":["erdos","number-theory","lean","proof-attack","metaweb"]}