In binary16 under roundNearestTiesToEven, x+x and 2*x are the same value

Identifier: F:fp16-doubling-add-equals-mul-two
Proof route: smt-clausal
External status: proved
Axiom footprint: ieee754-2019-binary16-arithmetic-semantics-as-encoded-by-axeyum-fp-fpa2bv-lowering, axeyum-fp.add-and-axeyum-fp.mul-are-differentially-VALIDATED-not-proven-bit-blasters, rounding-mode-roundNearestTiesToEven-only, smtlib2-floatingpoint-sort-equality-one-nan-value-signed-zeros-distinct, tseitin-cnf-encoding-preserves-satisfiability, drat-refutation-semantics-as-implemented-by-axeyum-cnf-check-drat, format-binary16-only-this-fact-is-not-format-generic

Recorded description

Let F be the IEEE-754 binary16 interchange format, SMT-LIB `(_ FloatingPoint 5 11)`, and let RNE denote roundNearestTiesToEven. For every value x of F, the correctly-rounded sum fp.add(RNE, x, x) and the correctly-rounded product fp.mul(RNE, 2, x) are the SAME value of F -- equality here is SMT-LIB `=` on the FloatingPoint sort, under which there is exactly one NaN and +0 and -0 are distinct, NOT `fp.eq`. Equivalently: the `x + x` -> `2 * x` strength reduction a compiler or a kernel author may apply is bit-exact at binary16, for every input including the infinities, the NaN and both zeros.

Formal statement

(assert (= (fp.add RNE x x) (fp.mul RNE (fp #b0 #b10000 #b0000000000) x)))

Dependencies

The graph shows direct ledger edges. Follow a node to open its artifact page.

0 direct dependencies 0 direct dependents

Evidence

fp16-doubling-unsat-drat

Kind: unsat-certificate
Status: checked

Supports: The negation of formal.statement is unsatisfiable over binary16, so the identity holds for every binary16 value.

Checker command

test "$(cargo run --release -q -p axeyum-bench --example smtcomp_cli -- --evidence artifacts/facts/smt2/neg-fp16-doubling-add-equals-mul-two.smt2 | tail -1)" = unsat

Evidence notes

Ran 2026-08-14: `; evidence kind=unsat-drat certified=1 recheck=ok arena=ok ms=6317`, verdict `unsat`, 10.4s wall in a release build. `recheck=ok` is axeyum's own `check_drat` (RUP+RAT, ADR-0011) re-checking the emitted DRAT refutation; `arena=ok` is `Evidence::check` replaying against a FRESH PARSE of the file rather than anything the producing solve held in memory. Cross-checked independently: `z3 -smt2` reports `unsat` (0.1s) and `bitwuzla 0.9.1` reports `unsat` (0.1s) on the same file. The checker_command asserts the VERDICT, not merely that the binary ran -- smtcomp_cli exits 0 on any decided verdict, so a bare invocation would pass even if the answer flipped.

fp16-doubling-exhaustive-apfloat

Kind: exhaustive-enumeration
Status: checked

Supports: All 65536 binary16 encodings evaluated by LLVM's APFloat: zero disagreements between x+x and 2*x, under every one of the five SMT-LIB rounding modes.

Checker command

cargo run --release -q -p axeyum-fp --example kernel_equivalence -- doubling --all-modes

Evidence notes

Ran 2026-08-14. This route shares NO code with axeyum's bit-blaster, CNF encoder or SAT core: it decodes each of the 2^16 encodings with `rustc_apfloat` 0.2.3 (LLVM's APFloat, admitted as the reference oracle by ADR-0028) and compares SMT-LIB value classes -- all NaN encodings collapsed to one value, the two zeros kept distinct. examined=65536 failures=0 at RNE, and likewise at RNA, RTP, RTN and RTZ, so the identity is in fact mode-independent even though this fact only asserts RNE. The same run also settles fp8 E5M2 (2^8) and bfloat16 (2^16) with zero failures; those are neighbouring propositions, not this one. The binary exits non-zero on any disagreement.

Provenance

{
  "date": "2026-08-14",
  "established_by": "fp-kernels lane; axeyum SMT front door (QF_FP -> fpa2bv -> CNF -> DRAT) plus an independent exhaustive LLVM-APFloat enumeration",
  "source": "authored here. The question is the one an ML-kernel or compiler author actually asks -- is this rewrite bit-exact, on ALL inputs -- rather than one extracted from a corpus.",
  "prior_art": [
    {
      "who": "David Goldberg",
      "what": "Scaling a binary floating-point value by a power of two is exact whenever the result is representable, so the two roundings coincide; the standard reference statement of the property this fact instantiates.",
      "where": "What Every Computer Scientist Should Know About Floating-Point Arithmetic, ACM Computing Surveys 23(1)",
      "year": 1991,
      "attribution": "standard textbook attribution; this lane did not consult the primary source, and records the citation as the received one. Nothing in the evidence above depends on it -- the fact is established here from scratch."
    }
  ]
}