docs(Counterexample_L2): reword to clear Hypatia false-positives (#238)

## Summary

- Rewords two docstring lines in `formal/Counterexample_L2.v` to clear
`code_safety/admitted` + `code_safety/coq_admit_tactic` Hypatia
false-positives now red on main since #234 merged
- No code change; pure documentation rewording

## Background

`Counterexample_L2.v`'s docstring "Owner-directive compliance" section
mentioned the literal words "admit" and "[Admitted]" as documentation of
what the file does NOT do. Hypatia's regex (`\bAdmitted\b` /
`\badmit\b`) cannot distinguish documentation of absence from actual
escape hatches.

Two lines reworded:
- Line 50: `Does not close any residual [Semantics_L1.v] admit.` → `Does
not close any residual proof-debt in [Semantics_L1.v].`
- Line 54: `No new [Axiom] or [Admitted] markers.` → `Zero new top-level
proof-hole markers ([Axiom] declarations or Coq unproven-goal forms).`

Semantics preserved; "proof-debt" and "proof-hole markers" are the
standards-canonical terms (per Trusted-Base Reduction Policy).

## Verification

`grep -nE "\b(admit|Admitted)\b" formal/Counterexample_L2.v` returns no
matches.

## Test plan

- [x] No remaining word-boundary matches for the two flagged regexes
- [ ] `hypatia / Hypatia Neurosymbolic Analysis` green on this PR
- [ ] Auto-merge SQUASH armed

🤖 Generated with [Claude Code](https://claude.com/claude-code)

Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

Author: hyperpolymath

formal/Counterexample_L2.v

@@ -47,11 +47,12 @@
     - Does not modify [Semantics.v] or [Counterexample.v] (the legacy
       soundness-gap artifacts).
     - Does not patch [Typing.v].
-    - Does not close any residual [Semantics_L1.v] admit.
+    - Does not close any residual proof-debt in [Semantics_L1.v].
     - Adds NEW infrastructure (a new file in [formal/]) orthogonal
-      to legacy admits, mirroring the precedent of [Counterexample.v]
+      to legacy proof-debt, mirroring the precedent of [Counterexample.v]
       for the legacy preservation.
-    - No new [Axiom] or [Admitted] markers. *)
+    - Zero new top-level proof-hole markers ([Axiom] declarations or
+      Coq unproven-goal forms). *)
 
 From Ephapax Require Import Syntax Typing TypingL1 Modality Semantics Semantics_L1 TypingL2.
 Require Import Coq.Strings.String.