Pith Number

pith:UR32IWKM

pith:2026:UR32IWKMJPJYOATIGHENBSCKRO

not attested not anchored not stored refs pending

FLoPS: Semantics, Operations, and Properties of P3109 Floating-Point Representations in Lean

Jay P Lim, Santosh Nagarakatte, Sehyeok Park, Tung-Che Chang

A Lean formal model of the P3109 low-precision floating-point standard verifies that FastTwoSum computes exact overflow errors under saturation for any rounding mode while ExtractScalar properties fail at one-bit precision.

arxiv:2602.15965 v3 · 2026-02-17 · cs.MS

Open paper page JSON Open Graph Bundle Merged state Verified badge What is a Pith Number?

Add to your LaTeX paper

\usepackage{pith}
\pithnumber{UR32IWKMJPJYOATIGHENBSCKRO}

Prints a linked badge after your title and injects PDF metadata. Compiles on arXiv. Learn more · Embed verified badge

Record completeness

1 Bitcoin timestamp

2 Internet Archive

3 Author claim open · sign in to claim

4 Citations open

5 Replications open

✓ Portable graph bundle live · download bundle · merged state

The bundle contains the canonical record plus signed events. A mirror can host it anywhere and recompute the same current state with the deterministic merge algorithm.

Claims

C1strongest claim

We reveal that FastTwoSum exhibits a novel property of computing exact 'overflow error' under saturation using any rounding mode, whereas previously established properties of the ExtractScalar algorithm fail for formats with one bit of precision.

C2weakest assumption

The Lean encoding faithfully captures the informal semantics and edge cases of the P3109 draft standard, including all interactions between saturation, stochastic rounding, and subnormal handling.

C3one line summary

A Lean formalization of P3109 that verifies FastTwoSum computes exact overflow error under saturation for any rounding mode and shows ExtractScalar properties fail at one-bit precision.

Formal links

2 machine-checked theorem links

Receipt and verification

First computed	2026-05-20T00:04:25.891757Z
Builder	pith-number-builder-2026-05-17-v1
Signature	Pith Ed25519 (`pith-v1-2026-05`) · public key
Schema	pith-number/v1.0

Canonical hash

a477a4594c4bd387026831c8d0c84a8b8f15c296db8831dccf4434a1fada7efc

Aliases

arxiv: 2602.15965 · arxiv_version: 2602.15965v3 · doi: 10.48550/arxiv.2602.15965 · pith_short_12: UR32IWKMJPJY · pith_short_16: UR32IWKMJPJYOATI · pith_short_8: UR32IWKM

Agent API

Resolver JSON Graph JSON Events JSON Schema Signing key

Verify this Pith Number yourself

curl -sH 'Accept: application/ld+json' https://pith.science/pith/UR32IWKMJPJYOATIGHENBSCKRO \
  | jq -c '.canonical_record' \
  | python3 -c "import sys,json,hashlib; b=json.dumps(json.loads(sys.stdin.read()), sort_keys=True, separators=(',',':'), ensure_ascii=False).encode(); print(hashlib.sha256(b).hexdigest())"
# expect: a477a4594c4bd387026831c8d0c84a8b8f15c296db8831dccf4434a1fada7efc

Canonical record JSON

{
  "metadata": {
    "abstract_canon_sha256": "690a95f228bf7257191d524c356be46549775896ecf341811ddb90e708b8f31d",
    "cross_cats_sorted": [],
    "license": "http://creativecommons.org/licenses/by/4.0/",
    "primary_cat": "cs.MS",
    "submitted_at": "2026-02-17T19:30:24Z",
    "title_canon_sha256": "72070ce310f6b388a64949bc47237fa9f38bb2b5ac5c0669d4eca3293317776a"
  },
  "schema_version": "1.0",
  "source": {
    "id": "2602.15965",
    "kind": "arxiv",
    "version": 3
  }
}