proof(idris2): tighten Ephapax.Affine.Emit to %default total (#100)

## Summary

**Ninth and final file** in the ephapax `%default partial` →
totality-tightening campaign. After this lands together with the rest,
no `%default partial` remains anywhere in `ephapax/idris2/src/Ephapax/`.

The file is a one-line wrapper:

```idris
emitModule : Module -> String
emitModule = encode
```

Its totality is exactly `Ephapax.IR.Decode.encode`'s. On the chain's
exit state (with PR #96 merged), `encode` is `covering` — the `show .
toSExpr` pipeline inherits `covering` from Decode's recursive
`encode`/`decode` functions (justified in #96's body).

Mark `emitModule` `covering` to match. Flip file default `%default
partial → %default total`. The `covering` modifier on the one defined
function is the entirety of the "escape" footprint — explicit, narrow,
justified.

No `assert_total` / `believe_me`.

## Verification

```
$ IDRIS2_PREFIX=…/idris2/0.8.0 idris2 --check Ephapax/Affine/Emit.idr
1/4: Building Ephapax.IR.SExpr
2/4: Building Ephapax.IR.AST
3/4: Building Ephapax.IR.Decode
4/4: Building Ephapax.Affine.Emit
```

## Refs — the full campaign

- `#124` (proof-debt audit epic)
- `#134` (ephapax totality sub-issue)

| # | File | PR | Annotation outcome |
|---|---|---|---|
| 1 | `IR/SExpr.idr` | #89 | `%default total`, fueled mutual parser |
| 2 | `Parse/Stream.idr` | #90 | `%default total`, fueled
`remaining/build` |
| 3 | `Parse/Util.idr` | #91 | `%default total`, fueled `many` +
`sepBy.sepTail` |
| 4 | `Parse/Lexer.idr` | #93 | `%default total`, fueled `lex.go` (57
call sites) |
| 5 | `IR/AST.idr` | #94 | `%default total` + 6 retained `covering`
(showPrec/(/=) loop) |
| 6 | `IR/Decode.idr` | #96 | `%default total` + 7 `covering`
(map/traverse SCT limit) |
| 7 | `Affine/Typecheck.idr` | #97 | `%default total` + pre-existing
baseline-rot layout fix |
| 8 | `Parse/Parser.idr` | #99 | `%default covering` (LL(k)
Stream-recursion, ~30 fns, large refactor deferred) |
| 9 | `Affine/Emit.idr` | **this** | `%default total` + 1 `covering`
(inherits from Decode.encode) |

## Test plan

- [x] `idris2 --check Ephapax/Affine/Emit.idr` builds green under
`%default total`
- [ ] CI green
- [x] No `assert_*` / `believe_me`; only `covering` on `emitModule`
(matches dependency)

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

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

Author: hyperpolymath

idris2/src/Ephapax/Affine/Emit.idr

@@ -3,8 +3,9 @@ module Ephapax.Affine.Emit
 import Ephapax.IR.Decode
 import Ephapax.IR.AST
 
-%default partial
+%default total
 
 public export
+covering
 emitModule : Module -> String
 emitModule = encode