Independent audit / exact rational arithmetic

Find the first tie.
Check every step.

Target Lens finds the smallest reading drift that allows a tie. A separate Python calculation derives the threshold, checks both possible routes, and builds exact readings that attain each one.

Run the worked audit ↓Read the proof ↓

01 / Reproduce

One command. Two exact routes.

The included JSON receipt is checked before the audit starts. Save your own receipt from Target Lens and replace the file path to audit your case. Python 3 needs no third-party packages.

From the repository root

python3 tools/audit_stability_edge.py examples/stability-case-a.json

Use --mask 5 to allow only readings one and three to move; --json emits machine-readable exact fractions. Inspect the independent script and the full derivation.

Route 01 / first

The estimates meet

ε = 16/3

Readings [128/3, 131/3, 166/3, 166/3, 239/3]; target 0.

Mean = median = 166/3. Both absolute errors are 166/3.

Route 02 / later

Target meets the midpoint

ε = 75

Readings [0, 0, 0, 0, 10]; target 1.

Mean = 2, median = 0. Both absolute errors are 1.

The later route remains a valid tie construction even though the universal strict guarantee ended at the first route.

02 / Portable evidence

Download it. Recheck it independently.

In Target Lens, set the five readings and target range, then choose Download verifiable JSON in the exact stability panel. The file contains the original proof receipt, both rational routes, the first six-decimal setting, and an exact tie witness for each reachable route. The browser constructs it locally; the Python program recomputes the threshold from scratch and checks every supplied witness.

Check a browser download from the repository root

python3 tools/verify_stability_certificate.py inward-stability-edge-certificate.json

You can first try the worked certificate JSON. Read the independent checker or inspect the versioned format. The displayed SHA-256 identifies the exact bytes checked; it does not authenticate who chose the readings or target. A finite, exact audit supports the conditional result within this model; it is not a formal proof-assistant certificate.

03 / Why the boundary is exact

A finite scan covers every real drift.

Write S for the sum of the five allowed readings, M for their median, and t for any target in the selected closed interval. The squared-error difference factors as:

(|mean − t|² − |median − t|²) × 25 = (S − 5M)(S + 5M − 10t)

Fix the baseline signs. At zero drift, a strict winner gives each factor a fixed nonzero sign over the entire target interval. A tie first appears when either signed factor can reach zero.
Check all configurations. The target factor reaches its extremes at all-low or all-high readings and a target endpoint. For the estimate factor, five possible median indices and six choices of two lower readings give 30 ordering cells.
Scan every change point. Within an ordering cell the extremal expression is affine until a reading clips at 0 or 100, or two reading intervals meet. Those finitely many landmarks include half-gaps for two moving readings and full gaps for one moving reading.
Exhibit the boundary. The audit solves each affine zero as an exact fraction, chooses the earliest one, and checks that its rational witness stays inside the box and ties the two errors. Smaller boxes preserve the strict signs; larger boxes retain the witness.

This result is conditional on the five stipulated readings, target interval, and independent symmetric drift bounds. It does not establish the true target, input provenance, probabilities, or real-world estimator performance.