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

Identifier: F:fp32-doubling-add-equals-mul-two
Proof route: smt-clausal
External status: proved
Axiom footprint: ieee754-2019-binary32-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-binary32-only-this-fact-is-not-format-generic

Recorded description

Let F be the IEEE-754 binary32 interchange format, SMT-LIB `(_ FloatingPoint 8 24)`, 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`.

Formal statement

(assert (= (fp.add RNE x x) (fp.mul RNE (fp #b0 #b10000000 #b00000000000000000000000) x)))

Dependencies

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

0 direct dependencies 0 direct dependents

Evidence

fp32-doubling-exhaustive-apfloat

Kind: exhaustive-enumeration
Status: checked

Supports: All 4294967296 binary32 encodings evaluated by LLVM's APFloat: zero disagreements between x+x and 2*x under RNE.

Checker command

cargo run --release -q -p axeyum-fp --example kernel_equivalence -- doubling-fp32

Evidence notes

Ran 2026-08-14: examined=4294967296 failures=0, 51.4s wall at 8 threads on a machine at load 16 (6m01s of CPU). This is the most expensive checker in the fact ledger and it is deliberately opt-in -- `doubling-fp32` is not part of the example's `all` set, because every other claim there is seconds. Sharded across `std::thread::available_parallelism()` threads by default. `rustc_apfloat` 0.2.3 (LLVM APFloat) shares no code with axeyum's bit-blaster, CNF encoder or SAT core; comparison is by SMT-LIB value class, all NaN encodings collapsed to one value and the two zeros kept distinct. The binary exits non-zero on any disagreement.

fp32-doubling-unsat-drat

Kind: unsat-certificate
Status: checked

Supports: The negation of formal.statement is unsatisfiable, decided symbolically -- without enumerating the 2^32 inputs.

Evidence notes

Ran 2026-08-14: `; evidence kind=unsat-drat certified=1 recheck=ok arena=ok ms=116653`, verdict `unsat`, 3m22.7s wall in a release build. `recheck=ok` is axeyum's own `check_drat` (RUP+RAT, ADR-0011) re-checking the emitted refutation; `arena=ok` is `Evidence::check` against a fresh parse. Cross-checked independently: `bitwuzla 0.9.1` reports `unsat` in 0.1s and `z3 4.13.3` reports `unsat` in 0.1s on the same file -- a 2000x gap in favour of the specialised FP solvers, recorded because it is a measurement this project should not flatter. THIS ROW CARRIES NO `checker_command` ON PURPOSE. At 3m22s it would exceed the default 120s per-checker budget of scripts/check-fact-evidence-replay.sh and turn a passing gate into a timeout. The fact stays covered by the exhaustive row above, which re-runs in ~51s. To re-derive this row by hand: cargo run --release -q -p axeyum-bench --example smtcomp_cli -- --evidence artifacts/facts/smt2/neg-fp32-doubling-add-equals-mul-two.smt2

Provenance

{
  "date": "2026-08-14",
  "established_by": "fp-kernels lane; an exhaustive LLVM-APFloat enumeration of all 2^32 binary32 values, corroborated by a symbolic CNF/DRAT refutation from axeyum and by two external FP solvers",
  "source": "authored here as the binary32 sibling of F:fp16-doubling-add-equals-mul-two, to make the exhaustive-versus-symbolic distinction concrete rather than rhetorical.",
  "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.",
      "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."
    }
  ]
}