feat(proofs): Coq binop parity — or/sub/mul/div/mod + comparisons in WokeLang.v (#86)

## Why

`WokeLang.v` (Coq) was **behind the Lean file on binops** — only
`add`/`eq`/`and` — the Lean↔Coq asymmetry flagged in
[`AUDIT.md`](../blob/main/docs/proofs/verification/AUDIT.md) and carried
as a `should` in `debt.a2ml`. This closes it.

## What

Each new operator gets a `has_type` rule, a `step` rule, and **full
`progress` + `preservation` coverage** (mirroring the proven
`T_Add_Int`/`T_And` templates), axiom-free:

| Group | Ops | Result |
|---|---|---|
| logical | `or` | `bool` |
| integer arithmetic | `sub`, `mul` | `Z` |
| integer division | `div`, `mod` | `Z`, **panic to `VOops`** on a zero
divisor (reuses the proven unwrap-of-oops fragment) |
| comparisons | `lt`, `gt`, `le`, `ge` | `Z → bool` |

This matches the Lean file exactly. (`BNeq` stays a deliberate symmetric
gap — neither prover has it; float arithmetic variants remain unmodelled
on both.)

## The interesting bit — `preservation` performance

`preservation` is the AUDIT-flagged brute-force `try solve [...]`
cascade. Naively adding the ops made the file take **>12 minutes** to
typecheck (the new congruence cases `S_BinOp_Left/Right` had no
reconstruction branch, so they fell through to the "nuclear" `repeat
inversion` blocks). Fixed by:
- extending the `first [...]` reconstruction block with the new ops
(both step orderings), and
- adding an early, guarded literal-result closer (`|- has_type _ (ELit
_) _ => inversion; subst; constructor`).

Now every new case dispatches deterministically — **compiles in ~7s**.

## Verified

- `coqc WokeLang.v` → **exit 0** (Coq 8.18.0).
- **No new axioms**: `Print Assumptions` on
`progress`/`preservation`/`type_safety` shows only the pre-existing
`Coq.Reals` pair (`ClassicalDedekindReals.sig_forall_dec` +
`functional_extensionality`).
- Zero `Admitted`/`admit`/`Axiom` in active code.
- `AUDIT.md` updated (binop section → parity).

Draft for review.

https://claude.ai/code/session_013wg3Mtq2QFhYi4XVw1Z6z7

---
_Generated by [Claude
Code](https://claude.ai/code/session_013wg3Mtq2QFhYi4XVw1Z6z7)_

Co-authored-by: Claude <noreply@anthropic.com>

Author: hyperpolymath

docs/proofs/verification/AUDIT.md

@@ -185,8 +185,13 @@ treatment as the Lean file.
   - Coq models floats as `ℝ` ⇒ `value_eq_dec` is fully decidable (`Req_EM_T`),
     at the cost of the classical-reals axioms above. (Lean models `Float` as
     opaque IEEE and decides equality classically via `by_cases`.)
-  - Coq is **behind on binops**: only `add`/`eq`/`and` have rules — none of
-    `sub/mul/div/mod` or the comparisons/`or` the Lean file now has.
+  - Coq is now **at parity on integer binops** (landed 2026-06-15): on top of
+    `add`/`eq`/`and` it gains `or`, `sub`, `mul`, `div`/`mod` (which panic to
+    `VOops` on a zero divisor, mirroring the proven unwrap-of-oops fragment) and
+    the comparisons `lt`/`gt`/`le`/`ge` (`Z` → `bool`) — each with a `has_type`
+    rule, a `step` rule, and full `progress`/`preservation` coverage, axiom-free.
+    Float arithmetic variants remain unmodelled on both sides, and `BNeq` is a
+    symmetric gap (neither Lean nor Coq has it).
 
 - **`cap_subsumes` bug fixed.** Its catch-all was `TODO: false`, so the relation
   was **not even reflexive** (`cap_subsumes CapProcess CapProcess = false`).
@@ -199,7 +204,10 @@ treatment as the Lean file.
   large brute-force `try solve [...]` pile ending in a literal *"Nuclear
   option"* — it compiles and is axiom-honest, but is fragile and unreviewable.
   A clean per-case rewrite (in the style of the Lean `preservation`) is worth
-  doing. Also: bring the Coq binops up to parity with the extended Lean set.
+  doing — the binop-parity work (2026-06-15) extended its `first [...]`
+  reconstruction block and added an early literal-result closer rather than
+  rewriting it. (That cascade also scales badly: the new ops had to be closed
+  early and deterministically to avoid a multi-minute typecheck.)
 
 ## Status