Local Agent Implementation Spec

The FW_H2 sub-series (documents 35-39) concludes, which is also the final document of the entire Phase 2. It formally specifies the abstract criteria from the previous four documents into a function requiring implementation, certify_fw_h2(E, p, profile="FW17_EXACT"), explicitly demanding that "the output must be replayable, not just returning a boolean"—the returned JSON includes global_abs_irreducible, potentially_multiplicative, local_reducibility_Fp, the kernel polynomials of phi/dual_phi and whether they have a Q_p-linear factor, the final fw17_h2 verdict, plus an evidence array. Four backend rules: Rule 1 prioritizes existing certified local isogeny/factorization machinery in Sage/Magma, and floating-point approximation must not be used to determine Q_p roots; Rule 2 states that if the backend can only determine "local $p$-isogeny exists" but cannot produce kernel character evidence, this cannot be used as an H2 verdict; Rule 3 requires that linear factors of the kernel polynomial must be an exact $p$-adic factorization or a Hensel certificate; Rule 4 states that if the local irreducible certificate itself is merely a heuristic, it can only return UNKNOWN and must not be upgraded to PASS. Six sets of regression fixtures are attached (A through F, covering $p=3$ reducible, potentially multiplicative additive, two FAIL cases with rational roots for the kernel, a PASS case with no rational roots for either, and a PASS case for local irreducible). The document concludes with a "Do not infer" paragraph explicitly listing four prohibited inference shortcuts: Kodaira type alone → PASS, no Q_p rational p-torsion → PASS, potentially supersingular → PASS, and global irreducible → local irreducible—none of these may be used alone to judge a PASS.