audit(canonical-proof-suite): promote E2+E4 status not-started → passing

Idris2 --check confirms both files type-check at exit 0.
E2-adder-equivalence.idr: adderEquivalence defined at line 157.
E4-mergesort.idr: mergeSortCorrect defined at line 606.
Both use %default total; no believe_me/sorry/assert_total.

P2-A5 audit finding: all Parameters in v1.0 entries are inside
Section carriers (not free), and no v1.0 entry uses Parameter as
headline shortcut. 16 believe_me occurrences are comment-only.

Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>

Author: hyperpolymath

audits/canonical-proof-suite/MANIFEST.a2ml

@@ -196,7 +196,7 @@
     (prover "idris2")
     (proof-file "proofs/canonical-proof-suite/E2-adder-equivalence.idr")
     (expected-symbol "adderEquivalence")
-    (status "not-started")
+    (status "passing")
     (porting-source "HOL Light hardware archive; Coq Bedrock; mathlib4 (parts)"))
 
   (entry
@@ -216,7 +216,7 @@
     (prover "idris2")
     (proof-file "proofs/canonical-proof-suite/E4-mergesort.idr")
     (expected-symbol "mergeSortCorrect")
-    (status "not-started")
+    (status "passing")
     (porting-source "Idris2 stdlib Data.List.Sort; mathlib4 Data.List.Sort; Coq Sorting.Mergesort"))
 
   (entry