Algorithm 1 Soundness Gates

Formally converges the disciplines scattered across previous documents into six directly citable soundness gates. S1: analytic $\Sha$ must not masquerade as actual $\Sha$—the sha field can only serve as an analytic prediction/gate input, and the certificate must preserve the descent source. S2: $\dim\Sha[2]$ must not masquerade as $\operatorname{ord}_2\#\Sha$—the current safety policy only accepts $\operatorname{BSD}(E,2)$ when $v_2(\Sha_{\mathrm{an}})=0$ and descent strictly pins down $\Sha[2]=0$; positive valuations must be marked "OPEN / higher 2-power descent needed". S3: timeout is UNKNOWN—an mwrank timeout is not a theorem failure and must not be misread as a mathematical rejection. S4: testing flag contamination—once skip_filter_S or skip_BSD_at_2_check is enabled, the entire run certificate is automatically downgraded; you cannot downgrade just a single curve. S5: deterministic theorem gate—the production gate for $\mathcal S\ne\varnothing$ uses a deterministic criterion; bounded search can only serve as cross-validation/witness and cannot be the primary certificate. S6: provenance—every PASS must preserve a complete record of seven items: predicate, value, evidence_type, backend, semantic_version, file/commit SHA, and timestamp. Together, these six rules constitute the concrete implementation of the entire Phase 1 pipeline's goal to "prevent engineering output from being secretly swapped for mathematical theorems".