proof(formal): general linear-coverage theorem — splitLinearCoverage (#85)

## Proof-debt P0 — ephapax (epic standards#124, arm standards#134)

### What

`src/formal/Ephapax/Formal/Qualifier.idr` documented (on `Split`) that
**every linear binding, at any position in the context, appears in
exactly one sub-context**, but only `nonDiminishment` was proved — and
that covers solely a linear binding at the **head** of the context.

This adds **`splitLinearCoverage`**, the general theorem:

```idris
splitLinearCoverage : (s : Split full left right)
                    -> (b : Binding) -> b.bindQual = Linear
                    -> Elem b full -> Either (Elem b left) (Elem b right)
```

Pure structural induction over the `Split` derivation. Affine-head /
`SplitAffDrop` cases are discharged via a `private`
`Uninhabited (Affine = Linear)` (the head cannot be the linear `b`);
`SplitNil` via `absurd` on the empty-list `Elem`.

### Oracle

`idris2 0.8.0` build of `src/formal/ephapax-formal.ipkg` — **3/3
modules green** before and after. No `believe_me` / `assert_*` /
holes; `%default total` in force, so the new clauses are
total + covering.

### Scope (deliberately bounded — not over-claimed)

Proves **coverage** (linear bindings are never dropped — the
non-diminishment direction generalised to all positions). It does
**not** assert exclusivity ("exactly one" under value-equal duplicate
bindings) — a distinct, stronger property left as future work and
explicitly NOT claimed in the docstring.

### Out of scope (still OWED on standards#134)

- 14 `idris2/src/*.idr` lacking SPDX headers — owner-gated, not
  auto-edited.
- Stale docs (ROADMAP "92%" vs actual; Coq `preservation` is `Qed`
  not Admitted) — tracked separately.
- No SPARK seam exists in this repo.

Refs hyperpolymath/standards#134
Refs hyperpolymath/standards#124
(Refs, not Closes — human-gated.)

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

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

Author: hyperpolymath

src/formal/Ephapax/Formal/Qualifier.idr

@@ -15,6 +15,7 @@
 module Ephapax.Formal.Qualifier
 
 import Data.List
+import Data.List.Elem
 
 %default total
 
@@ -184,3 +185,63 @@ public export
 nonDiminishment : (s : Split (MkBinding n Linear t :: rest) left right) -> LinearPreserved s
 nonDiminishment (SplitLinL _) = PreservedLeft
 nonDiminishment (SplitLinR _) = PreservedRight
+
+--------------------------------------------------------------------------------
+-- Linear Coverage (general form of Theorem 5.1)
+--------------------------------------------------------------------------------
+
+||| `nonDiminishment` only covers a linear binding at the HEAD of the context.
+||| The docstring on `Split` (above) makes the stronger claim that *every*
+||| linear binding — at any position in `full` — appears in (at least) one of
+||| the two sub-contexts. That general statement was previously unproven.
+|||
+||| `splitLinearCoverage` discharges it: for any split and any linear binding
+||| that is a member of the full context, that binding is a member of the left
+||| or of the right sub-context (i.e. it is never dropped). The proof is pure
+||| structural induction over the `Split` derivation.
+|||
+||| Scope: this proves COVERAGE (linear bindings are not dropped — the "at
+||| least one" / non-diminishment direction). It does not assert exclusivity
+||| ("exactly one"): with value-equal duplicate bindings that is a distinct,
+||| stronger property and is left as future work; it is intentionally NOT
+||| claimed here.
+private
+Uninhabited (Affine = Linear) where
+  uninhabited Refl impossible
+
+public export
+splitLinearCoverage : (s : Split full left right)
+                    -> (b : Binding)
+                    -> b.bindQual = Linear
+                    -> Elem b full
+                    -> Either (Elem b left) (Elem b right)
+splitLinearCoverage SplitNil _ _ el = absurd el
+-- Linear head goes left
+splitLinearCoverage (SplitLinL _) _ _ Here = Left Here
+splitLinearCoverage (SplitLinL s) b prf (There e) =
+  case splitLinearCoverage s b prf e of
+    Left el  => Left (There el)
+    Right er => Right er
+-- Linear head goes right
+splitLinearCoverage (SplitLinR _) _ _ Here = Right Here
+splitLinearCoverage (SplitLinR s) b prf (There e) =
+  case splitLinearCoverage s b prf e of
+    Left el  => Left el
+    Right er => Right (There er)
+-- Affine head, kept left: the head cannot be our linear `b`
+splitLinearCoverage (SplitAffL _) _ prf Here = absurd prf
+splitLinearCoverage (SplitAffL s) b prf (There e) =
+  case splitLinearCoverage s b prf e of
+    Left el  => Left (There el)
+    Right er => Right er
+-- Affine head, kept right
+splitLinearCoverage (SplitAffR _) _ prf Here = absurd prf
+splitLinearCoverage (SplitAffR s) b prf (There e) =
+  case splitLinearCoverage s b prf e of
+    Left el  => Left el
+    Right er => Right (There er)
+-- Affine head, dropped (weakening): the head cannot be our linear `b`,
+-- and the sub-contexts are unchanged by the drop.
+splitLinearCoverage (SplitAffDrop _) _ prf Here = absurd prf
+splitLinearCoverage (SplitAffDrop s) b prf (There e) =
+  splitLinearCoverage s b prf e