Stopping Rules and Claim Ladder

The concluding document of the v0.1 series, gathering the entire Phase 2 odd-$p$ problem into its own seven-level certificate ladder, whose roles correspond to the C0-C10 ladder defined in Phase 0 for the entire BSD research line, but precisely scaled down to this single Phase 2 subproblem: C0 (literature map, only knowing which theorems might be relevant) → C1 (hypothesis compiler, every FW hypothesis has an exact executable meaning) → C2 (fixed $(E,p)$ rigorously proving $\mathrm{FW}(E,p)$) → C3 (twist-uniform fixed $p$, proving $\forall d\in\mathcal D(E),\ \mathrm{FW}(E_d,p)$) → C4 (finite exceptional prime reduction, proving $p\notin P_E\Rightarrow\mathrm{FW}(E,p)$ and $P_E$ is finite and computable) → C5 (closing $p\in P_E$ item by item to obtain $\forall p>2$) → C6 (splicing with Banwait's 2-part/nonvanishing to obtain full $\forall d,\ \operatorname{BSD}(E_d)$). The document directly lists the five most easily committed conceptual bait-and-switches as a "forbidden upgrade" list: testing $p<1000$ does not equal C4/C5; 99.9% of primes does not equal C5; residual image "looking generic" does not equal a theorem; non-semistable sample success does not equal all non-semistable curves; the existence of the Fouquet–Wan theorem does not mean it has been algorithmized. The final "three-round stopping rule" is the most practical research workflow design of the whole piece: if for three consecutive rounds it only increases the checked primes or the number of curves, while the exact meaning of H2/H3 makes no progress and the finite exceptional set is not theoremized, then database scale expansion must be frozen, retreating back to local Galois lemma work—the document explicitly names this to avoid repeating the failure mode of "running more and more data, but the global quantifier hasn't shrunk at all".