Local Agent Implementation Spec

FW_H2 子系列(35-39 篇)收尾,同時是整個 Phase 2 的最後一篇。把前四篇的抽象判準正式規格化成一支要求實作的函式 certify_fw_h2(E, p, profile="FW17_EXACT"),明確要求「輸出必須可 replay,不可只回 boolean」——回傳的 JSON 包含 global_abs_irreducible、potentially_multiplicative、local_reducibility_Fp、phi/dual_phi 的 kernel 多項式與是否有 Q_p-linear factor、最終 fw17_h2 判定,外加 evidence 陣列。四條 backend 規則:Rule 1 優先用 Sage/Magma 既有 certified local isogeny/factorization 機械,不可用浮點 approximation 判斷 Q_p root;Rule 2 若 backend 只能判斷「local $p$-isogeny 存在」但產不出 kernel character 證據,不能把這個當 H2 verdict;Rule 3 kernel 多項式的線性因子必須是 exact $p$-adic factorization 或 Hensel 證書;Rule 4 若 local irreducible 證書本身只是 heuristic,只能回 UNKNOWN,不可升級 PASS。附六組 regression fixture(A 至 F,涵蓋 $p=3$ reducible、potentially multiplicative additive、兩種 kernel 有理根的 FAIL 情形、兩者皆無有理根的 PASS 情形、local irreducible 的 PASS 情形)。文件最後用一個「Do not infer」段落明確列出四個禁止的推論捷徑:Kodaira type alone → PASS、no Q_p rational p-torsion → PASS、potentially supersingular → PASS、global irreducible → local irreducible——全部不得單獨拿來判 PASS。