proof(SafeEmail): annotate 19 bodyless decls as OWED (Refs standards#158) (#58)

## Summary

Converts the 19 bodyless `export` / `public export` declarations in
`src/Proven/SafeEmail/Proofs.idr` to the estate's
OWED-with-justification
convention established 2026-05-20 across SafeChecksum, SafeBuffer,
SafeCryptoAccel, SafeHKDF, SafeBloom, SafeFPGA, SafeAPIKey, SafeCORS,
SafeCSV, SafeSemVer, SafeHtml, SafeTOML, SafeMath, SafeNetwork,
SafeOTP, SafeEnv, SafeCSRF, SafeString, SafeYAML:

- Triple-pipe `|||` doc-comment stating the claim
- Leading `0 ` (erased multiplicity, runtime-stripped)
- Bare type signature, no `postulate` keyword
- Explicit Idris2 0.8.0 blocker + discharge condition

Refs hyperpolymath/standards#158.

## The 19 OWED items

### Parsing (2)

1. **`parseEmptyFails`** — `parseEmail "" = Nothing`.
Blocker: Idris2 0.8.0 String-literal pattern reduction gap at type level
(Refl rejected on empty-literal vs empty-literal pattern clause).
Discharge: reflective `Data.String` tactic for String-literal pattern
matching.

2. **`parseNoAtFails`** — `parseEmail "noatsign" = Nothing`.
Blocker: `splitOnLast` threads through opaque `unpack` / `pack` String
FFI primitives.
Discharge: reformulate `splitOnLast` on `List Char`, or reflective
`Data.String` tactic.

### Validation core (4)

3. **`validResultIsValid`** — `validResult.isValid = True`.
Blocker: Idris2 0.8.0 does not reduce record-field projection on named
top-level constructor application without case-split.
Discharge: inline at call sites or reflective record-projection tactic.

4. **`errorMakesInvalid`** — adding an Error issue forces `.isValid =
False`.
Blocker: user-defined `Eq ValidationSeverity` instance + `(/=) = not .
(==)` chain not reducible by Refl.
Discharge: `Bool`-vs-`Prop` reflective lemma for enum-shaped Eq
instances.

5. **`warningKeepsValid`** — adding a Warning issue preserves `.isValid
= True`.
   Same blocker family as (4), plus the (3) projection gap.

6. **`combineValidValid`** — combining two valid results stays valid.
Blocker: record-field projection on universally-quantified `r1, r2 :
ValidationResult` doesn't fire without case-splitting to the
`MkValidationResult` constructor.

### Email structure (1)

7. **`parsedContainsAt`** — successful parse implies `'@'` was in input.
   Blocker: String FFI opacity on `splitOnLast` / `unpack` / `elem`.
Discharge: reflective String FFI model, or factor `splitOnLast` through
`List Char` with a structural lemma.

### Normalization (1)

8. **`normalizeIdempotent`** — `toLower (toLower d) = toLower d`.
   Blocker: `toLower` wraps the opaque `prim__strToLower` FFI primitive.
Discharge: reflective `Data.String` tactic, or character-level lemma
lifted through `pack . map toLower . unpack`.

### Security / sanitization (2)

9. **`sanitizeRemovesNewlinesLemma`** — `filter` post-condition on the
union predicate.
Blocker: Idris2 0.8.0's `Data.List` does not expose `filterAll` as Refl;
direct proof needs induction + `&&`-projection.
Discharge: hand-written `filterAll` lemma, or reflective `Bool` tactic.

10. **`sanitizeRemovesNewlines`** — `sanitizeForHeader s : NoNewlines`.
Blocker: combines the `unpack . pack` String round-trip (opaque) with
the upstream OWED (9).
    Discharge: discharge both upstreams.

### List operations (2)

11. **`filterValidCorrect`** — `all p (filter p xs) = True`.
Blocker: `Data.List` does not expose `filterAllSelf : (xs : List a) ->
all p (filter p xs) = True` as Refl-discharable.
    Discharge: add the missing lemma to `Data.List`.

12. **`uniqueNoDuplicates`** — `length (nubBy p xs) <= length xs`.
Blocker: `Data.List` does not expose the `nubByLengthLTE` lemma; direct
proof needs induction + `LTE n (S n)` transport on the skip-arm.
Discharge: add the missing lemma to `Data.List` / `Data.List.Lemmas`.

### Domain checks (2)

13. **`freeEmailExhaustive`** — Bool-LEM on `isFreeEmail`.
Blocker: Idris2 0.8.0 does not auto-derive Bool-LEM as Refl; case-split
needed.
    Discharge: one-line case-split on `isFreeEmail domain`.

14. **`typoCheckFindsKnown`** — `checkCommonTypos "gmial.com"` returns
the canonical W010 warning.
Blocker: String FFI opacity on `toLower` and String-`(==)` reduction.
    Discharge: reflective String FFI model, or refactor on `List Char`.

### RFC compliance (3)

15. **`validLocalNoStartDot`** — valid local part has no leading dot.
Blocker: `isPrefixOf` threads through `prim__strHead` /
`prim__strSubstr`, plus the (4) Bool-reduction gap on `addIssue`.

16. **`validLocalNoEndDot`** — valid local part has no trailing dot.
    Identical shape to (15) on `isSuffixOf`; same discharge.

17. **`validDomainHasLabel`** — `split (== '.') domain` yields at least
one label.
Blocker: `Data.List1` does not expose the length-lower-bound lemma `LTE
1 (length (forget xs))` as Refl.
    Discharge: one-line case-split on the `List1` constructor.

### Comprehensive validation (2)

18. **`comprehensiveCatchesRFC`** — full-fail implies
comprehensive-fail.
Blocker: combines the (6) `combineResults` projection gap with the
`foldl combineResults` invariant.
    Discharge: alongside (6).

19. **`validPassesComprehensive`** — full-pass implies no errors in
comprehensive.
Blocker: extra checks (typo / role / plus / numeric) only emit non-Error
issues by code inspection (Warning W010, Info I001/I002/I003), but
proving this requires reducing through `foldl combineResults` + the
`hasErrors` `any . (.severity = Error)` Bool-reduction gap.
    Discharge: alongside (4) + (6), plus one step-lemma per extra check.

## Safety posture

- Zero `believe_me`
- Zero `postulate`
- Zero `idris_crash`
- All `0 `-erased — postulates cannot leak into runtime
- Discoverable as named declarations (vs commented-out)
- Refl-discharged decls (`parseDeterministic`, `normalizedEquality`)
preserved as bodied — they are sanity anchors

## Local verification

```
IDRIS2_PREFIX=/.../idris2/0.8.0 \
  idris2 --source-dir src --check src/Proven/SafeEmail/Proofs.idr
-> exit 0
```

Four pre-existing `validResult`-shadowing warnings are unchanged from
baseline (they predate this PR; the originals' positional declarations
already triggered them).

## Scope

- Touches only `src/Proven/SafeEmail/Proofs.idr`
- 19 declarations annotated
- The 2 already Refl-discharged proofs (`parseDeterministic`,
`normalizedEquality`) and the 4 data-type declarations (`ContainsAt`,
`ValidLocalLength`, `ValidDomainLength`, `NoNewlines`) and 2 helper
definitions (`isHeaderSafe`, `sanitizeForHeader`, `uniqueEmails`) are
untouched

## Why draft

Filed DRAFT per the convention so the owner can ratify the OWED claims
against the SafeChecksum / SafeHtml / SafeTOML / sibling precedents and
land once estate CI settles.

## Test plan

- [x] `idris2 --check` exit 0 on the touched module (local Idris2 0.8.0)
- [x] No new warnings introduced (pre-existing shadowings unchanged)
- [ ] CI green on this PR
- [ ] Owner review of OWED reasons against SafeChecksum / SafeHtml /
SafeTOML precedent

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

Author: hyperpolymath