9.3 Threat model and residual risk

The relevant risks are narrower than “arbitrary numerical error,” but wider than the Lean kernel.

Executable/logical disagreement.

A compiler optimization, runtime primitive, implemented_by replacement, or platform-dependent representation can compute a different Boolean from the logical definition. Upstream has fixed concrete bugs that made native_decide usable in derivations of False, including issue #1825 (machine integers), issue #4306 (constant folding), and issue #11773 (divergent array folds). Upstream also tracks open design or provenance hazards around pointer equality and compiler simplification. These reports motivate the threat model; they are not evidence that a current Ternary Goldbach predicate is false, and the three concrete contradiction reports cited above are closed upstream.

Wrong target or semantic bridge.

Exact evaluation can faithfully prove the wrong range, scale, rounding convention, or paper transcription. A Boolean checker alone cannot show that its finite statement is sufficient for the later analytic theorem.

Enumeration and provenance.

A convenient generated name does not prove how an axiom was created. Historically, Lean issue #8840 also showed why merely listing transitively referenced names is not enough; the current upstream traversal was repaired by PR #8842.

Scale and opacity.

The 1,371 atoms are too numerous for a useful flat proof graph. Most are deliberately small shards—1,025 belong to one Rosser–Schoenfeld ladder family—rather than 1,371 independent analytic assumptions. Nevertheless, each shard is a distinct trusted native equality and must remain exactly enumerable.

Corroboration gap.

A Python/GMP, C++, Arb/FLINT, or source-table rerun is useful independent evidence only when it transcribes the same predicate, range, and rounding. It remains an external execution, and a sample cannot certify an unsampled range.

Build and supply-chain execution.

Building Lean code executes project and dependency code. Lean itself recommends isolation for untrusted projects; native evaluation additionally depends on the executable toolchain named above.