chore(ci): clear the two in-repo governance false-positives

Two governance checks have been red on every PR for reasons unrelated to
any diff; both are repo-level. Fixed against the exact standards@d135b05
check regexes (fetched + verified, not guessed):

- Licence consistency: root LICENSE (verbatim MPL-2.0 text) had no SPDX
  header. check-licence-consistency.sh greps `^SPDX-License-Identifier:`
  and normalises it against the manifest. Prepend
  `SPDX-License-Identifier: MPL-2.0` (matches Cargo.toml `license = "MPL-2.0"`).

- Trusted-base reduction policy: check-trusted-base.sh flags
  `^[[:space:]]*(Axiom|Admitted|admit\.)`; formal/RegionEnvL1.v:17 is a
  PROSE comment ("Axiom budget: this file is axiom-free") that starts with
  "Axiom" — a false positive. Reworded to "On the axiom budget: …" so the
  line no longer matches. Chosen over a .trusted-base-ignore entry on
  purpose: the file stays fully scanned, so a genuine future axiom there is
  still caught (and a TRUSTED:/AXIOM: annotation would be false — the file
  really is axiom-free).

Hypatia's own Elixir CompileError lives in the standards repo and is out of
ephapax's reach. RegionEnvL1.v still compiles (comment-only change).

Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01AGFqWzByua4dKbA7W7oVsL

Author: claude

LICENSE

@@ -1,3 +1,5 @@
+SPDX-License-Identifier: MPL-2.0
+
 Mozilla Public License Version 2.0
 ==================================
 

formal/RegionEnvL1.v

@@ -14,7 +14,7 @@
     [region_name -> nat] (re-entry depth per region; 0 = dead), reasoned
     up to a **pointwise-equality setoid** [renv_eq].
 
-    Axiom budget: this file is axiom-free. We use a setoid relation
+    On the axiom budget: this file is axiom-free. We use a setoid relation
     ([renv_eq]) rather than [functional_extensionality], so [Print
     Assumptions] stays clean — order-insensitivity is *definitional*
     (the carrier is a function; permutation collapses to [renv_eq]),