Phase 2 First Agent Experiment

Transforms the compiler goals from documents 02 and 04 into a seven-step experimental design, named FW-Hypothesis-Compiler / Weight-2 Elliptic Curves. Step 1 deliberately avoids scanning the full database, selecting only 60 curves (20 semistable known to pass, 20 non-semistable analytic-rank-0, 20 deliberately chosen bad/control groups); the document explicitly states this is solely for compiler correctness, not for statistics. Step 2 builds a local prime table for each curve over a fixed set of small primes plus rational isogeny primes and bad reduction primes. Steps 3 and 4 are the core of the document: assigning independent Agents to perform symbolic derivation for H2 and H3 respectively. H2's task is to specialise Fouquet–Wan's local semisimplification prohibition to weight-2 elliptic curves, deriving computable local criteria classified by the four reduction types (good ordinary/supersingular/multiplicative/additive), and requires outputting a lemma, proof, allowed assumptions, counterexamples, and a Sage predicate, rather than writing code first. H3's task is to compare Fouquet–Wan's auxiliary $\ell$ condition with Banwait's existing $p\nmid v_\ell(\Delta_E)$ criterion, aiming for one of three outcomes—exact equivalence, strict implication, or not equivalent—and the document explicitly forbids assuming they are the same by default. Step 5 formalises the three bridge lemmas, recommending dual output in Lean/theorem-style prose. Step 6 searches for a finite exceptional prime theorem, but if no theorem guarantees completeness, it must not be marked complete. Step 7 finally scans the search pool of about 895,988 non-semistable analytic-rank-0 curves; the first database output must be in the three-state format FW_COMPILER_PASS/FAIL/UNKNOWN, and UNKNOWN must not be swallowed. Finally, the document explicitly relaxes the success Gate for v0.1: finding new curves is not required; as long as the H2/H3 exact specialisation is completed, twist-invariance lemmas are completed, and finite-prime reduction holds on at least one nontrivial curve class, it already constitutes a new mathematical result in standard language.