Route 01 / starts at 8
Target horizon / independently checked
Where does the winner change?
Move any one reading through [0, 10], holding the rest fixed. This report classifies every real target under that stipulated model.
[17/3, 95/12] exact midpoint span
The boundaries belong to the tie region. The finite route intervals overlap at the original sample’s midpoint, so they cover the whole region without gaps.
01 / Decision boundary
The complete target line
t < 17/3Mean
Strictly closer for every permitted one-reading move
17/3 ≤ t ≤ 95/12
Tie attainableAt least one permitted move ties at each real target, including both endpoints
t > 95/12Median
Strictly closer for every permitted one-reading move
The midpoint range shown above is independent of the input target interval. A strict result means one estimator has a smaller absolute error for every allowed one-reading move; it is conditional on these inputs.
02 / Exact model
Readings and a concrete probe
r1 = 8r2 = 6r3 = 8r4 = 7r5 = 0r6 = 8
Permitted moved reading: [0, 10]. Supplied target interval: [6, 6]. At its midpoint t = 6: Tie. Move reading 1 to 4; its two absolute errors are exactly equal.
Original sample midpoint of the two estimators: 41/6. Every route passes through this anchor at its unchanged reading.
03 / All movements
6 exhaustive routes
Each segment maps the exact target midpoints reached while moving that reading from the movement lower bound to its upper bound. The gold tick is the common original-sample midpoint. Diagram position is approximate; fractions and the JSON are exact.
Route 02 / starts at 6
Move reading 2
Route 03 / starts at 8
Move reading 3
Route 04 / starts at 7
Move reading 4
Route 05 / starts at 0
Move reading 5
Route 06 / starts at 8
Move reading 6
Boundary labels identify routes attaining the global endpoints. A route’s midpoint segment is not itself a strict-winner guarantee.
04 / Evidence and scope
Verify independently
Lean checked worked model
The six_reading_full_horizon theorem proves this full classification for the six displayed readings and movement [0,10], including all six movable indices and every real target. Lean checks its explicit model; it does not parse this JSON or certify the source of the readings.
Checked JSON bytes
The independent Python verifier recomputes all route partitions, endpoint midpoints, side winners, and exact tie witnesses before this page is rendered. SHA-256 identifies matching bytes; it does not authenticate their author.
1ebfd5c70b9005311b25ca21506f0584b555bc9d2571501a4a64d38037cda1c8Replay with python3 tools/verify_odd_target_box.py target-horizon-v6.json
using the independent checker.
The report remains readable offline. Neither this certificate nor its diagram establishes that the supplied readings came from real measurements, or which estimator is generally appropriate.