Fouquet–Wan Hypothesis Compiler

Fouquet–Wan proved the Iwasawa Main Conjecture for modular motives with arbitrary reduction, giving a $p$-part BSD corollary in the weight 2/elliptic curve case, but the paper itself admits "it is not immediately apparent how to algorithmically verify these conditions"—this document formally turns this statement into a compiler problem. Level 0 chooses to first compile a stronger but easier-to-implement sufficient hypothesis package, defining three conditions that must be preserved for every odd prime $p$: FW-H1 (absolutely irreducible $\bar\rho_{E,p}$, state is directly EXACT/THEOREM, using Sage/LMFDB Galois-image/isogeny metadata instead of wildly guessing from a few Frobenius traces), FW-H2 (local residual non-degeneracy at $p$, the document explicitly forbids guessing equivalent conditions like a_p != something in the first round; it must first be derived from the theorem/local representation formalism and then compiled into a predicate—this is exactly why the entire subsequent FW_H2_Local_Isogeny_Compiler sub-series exists), FW-H3 (auxiliary multiplicative prime $\ell\ne p,\ \ell\parallel N$, the document specifically warns that Fouquet–Wan's precise local condition is finer than Banwait's $p\nmid\operatorname{ord}_\ell(\Delta_E)$ criterion and cannot be directly borrowed). Level 1 defines the JSON schema output for each $(E,p)$, where the claim field is tri-state: FW_APPLICABLE / FW_NOT_APPLICABLE / UNKNOWN. Level 2 is the true mathematical goal: instead of scanning $p<1000$ and declaring completion, it aims to establish the form of a "generic large prime theorem + finite exceptional prime list" such as $\exists P_E\text{ finite}: p\notin P_E\Rightarrow\mathrm{FW}(E,p)$. If this cannot be achieved, it must honestly output "FW verified for tested primes" and cannot be upgraded to full BSD. The document condenses the true goal of the entire piece into a single sentence: infinite prime quantifier → finite certificate is the real Phase 2 mathematical advancement, not a count of a million curves.