the assumption in the proof we could not discharge

A proof had a step in it that looked like bookkeeping and was actually the whole problem. The claim was that two parties deriving the same value from slightly different inputs will round to the same bucket with overwhelming probability, because the difference between their values is small next to the spacing between buckets.

Making that rigorous means bounding the size of the difference. The difference is a sum of products of small random terms, and the sum has as many terms as the ambient structure has coefficients. So the argument ran: bound one coefficient with a concentration inequality, then multiply by the number of coefficients. That multiplication is where it came apart. The coefficients of the sum are not independent draws; they are rearrangements of the same underlying random variables, so a per-coefficient bound cannot simply be paid for once per coefficient. A second gap sat underneath: the clean tail bound is proven for continuous variables, and what the system samples is discrete.

We could have kept the word theorem. Instead we demoted the claim to a conjecture, published the two obstacles side by side, and said plainly that the evidence for it is measurement rather than proof — a large number of trials at the real parameters, and margins the measurements never came close to exhausting.

The correctness statement now says what is proven, what is assumed, and which assumption would have to be discharged to upgrade the claim. It proves the team will pay the reputational cost of a weaker claim in order to keep the stronger one honest.