binary16 addition under roundNearestTiesToEven is monotone in its first argument

Reproduced independently by the fp16-evidence lane, 2026-08-28, in its own worktree with a fresh `cargo build --release -p axeyum-bench --example smtcomp_cli` (this fact's evidence depends on code that landed within the hour, ADR-0613, so a stale prebuilt binary would have measured the OLD superlinear-checking route). Two full end-to-end runs, both `unsat`/`certified=1`/`recheck=ok`/`arena=ok`: run 1 (host load ~2.8/16): search 424,601 conflicts/26.556s -> 827,048 proof steps/193,214,020 bytes; backward_lrat_certify 827,048/827,048 steps, elapsed_ms=95,932, certified=true; printed line `; evidence kind=unsat-drat certified=1 recheck=ok arena=ok ms=136898`; verdict `unsat`. Measured via `/usr/bin/time -v` around the WHOLE process: wall clock 5:39.01 (339.01s), 99% CPU, RSS 3.11 GB. run 2 (host load ~20.7/16, contended): printed line `; evidence ... certified=1 recheck=ok arena=ok ms=168081`; verdict `unsat`. Measured via date-diff around the whole `cargo run` invocation: wall clock 353s. IMPORTANT CORRECTION TO THE ADR-0613 NUMBERS THIS FACT'S NOTES ALREADY QUOTE. The `; evidence ... ms=NNN` field printed by `smtcomp_cli` is captured in `evidence_report_line`'s caller BEFORE `UnsatProof::recheck()` and the `arena` fresh-parse check run (see `crates/axeyum-bench/examples/smtcomp_cli.rs`, the `started.elapsed().as_millis()` argument is evaluated before `evidence_report_line` calls `proof.recheck()` and `evidence.check_outcome(...)`). So `ms=136898`/`ms=168081` measure only parse+solve+certify, NOT the full checked claim this evidence row needs -- `recheck=ok` (an independent second pass: `check_lrat` plus, in rejecting-only position, `check_drat_backward` over the full 827,048-step proof) and `arena=ok` (a second fresh parse of the original SMT-LIB file plus re-evaluation) both run AFTER that timer stops. The ADR calls its `ms=125098` figure "end to end"; measured here, the ACTUAL end-to-end wall clock (what this checker_command, or any external caller of the binary, actually waits for) is 2.5-2.9x that: 339-353s across two runs at different contention levels, not ~125-137s. This does not weaken the ADR's underlying finding -- checking still moved from never-observed-to-finish to under six minutes, roughly two orders of magnitude, not three -- but the smaller number is a sub-stage timer, not the wall-clock cost of running the command. WHY THIS IS THE ONLY EVIDENCE ROW, UNLIKE THE FP8 SIBLING. F:fp8-add-monotone-rne is settled twice, by exhaustive enumeration of all 2^24 triples AND by this same symbolic CNF/DRAT route. Binary16 has 2^48 triples; brute-force enumeration is not available at this width (see that fact's own arity-wall note), so this fact rests on the symbolic route alone. The `checker_command`'s exit status depends on three independently-tested substrings of the real run's stdout (`^unsat$`, `certified=1 `, `recheck=ok`), each verified against BOTH a captured real positive run and two synthetic negative-control transcripts (sat/uncertified: U=C=R=0, chain fails; unsat-but-certified=0: C=0, chain fails) before this row was written -- if the claim were false, this command exits nonzero because at least one of those three greps would count zero matching lines and the chained `test` would fail on the first zero it hits.