The Claim Behind the Decimal Point

The certificate, checkable by hand

A figure m on the grid 1/g denotes the half-open interval [(2m−1)/(2g), (2m+1)/(2g)). Nothing here needs trust:

• 3.20 is m = 3200 on g = 1000: [639/200, 641/200) = [3.195, 3.205).
• 3.20 / 1.75 divides the two intervals exactly: [71/39, 641/349), that is [1.823076923076, 1.834097420630) truncated at twelve places. A significant-figure calculator prints 1.83.
• 41.50 and 41.5 are different claims. 41.50: [8299/200, 8301/200) = [41.495, 41.505). 41.5: [829/20, 831/20) = [41.45, 41.55).
• 951000 is genuinely ambiguous and gets both readings: strict [1901999/2, 1902001/2) = [950999.5, 951000.5); loose [1901000/2, 1903000/2) = [950500, 951500).

The underlying lemma is machine checked in Lean 4 with no imports and no holes: eight theorems. Re-run it yourself from the repository root with:
bash research/printed-interval/lean/verify.sh

The desk

One expression

Expression over printed figures, for example 3.20 / 1.75 Evaluate exactly

Waiting for input.

Paste a column of figures

One printed figure per line 3.20 1.75 41.5 Run the column

Waiting for input.

Refusals with reasons

The tool refuses three things outright, and reports one ambiguity twice instead of picking a side. Each button runs the real engines, right here.

Try: about 5 Try: 1.2e5 Divide by an interval straddling zero Read 951000 both ways

Decimals above are truncated, never rounded, so no displayed digit is invented. Everything computes locally in your browser: nothing is uploaded and no third-party request of any kind is made. The verifier for this page is research/printed-interval/verify-printed-numbers.mjs.