back to table · edit · history · where entries came from · files · download
1700 bytes, as of the version from 2026-10-27 11:53 (current). Recorded here, not run.
## Convert MPFI endpoints to exact rationals before measuring their width
What happened: the first width summary for T547 reported zero for 83 irrational
enclosures. Both endpoint values had been converted with `QQ(endpoint)`. In
SageMath 10.9 this coercion can choose the same nearby rational for distinct
binary floating-point endpoints. The actual MPFI enclosures were valid; the
measurement and containment check had lost their exact endpoints. Replacing
both coercions with `endpoint.exact_rational()` produced a strictly positive
maximum width of 1.89091402092e-124. A new control checks that the exact
endpoints of RealIntervalField(100)(1/3) strictly surround 1/3.
What the skill says now: a measurement needs a control that returns a known
answer; a ball or interval's own error can support proven rigour. It does not
specify exact conversion of binary endpoint values to rational numbers.
What it should say: when a proof compares or measures interval endpoints as
rationals, use `interval.lower().exact_rational()` and
`interval.upper().exact_rational()`, not `QQ(endpoint)`. Test that a known
nonrepresentable rational such as 1/3 remains strictly inside the converted
endpoints and has positive width. A rational approximation of an endpoint
cannot substitute for its exact value in an enclosure proof.
Evidence: T547, `numerical-dry.log` (discarded zero-width measurement),
`numerical-dry-corrected.log`, `numerical-dry.json`, `checks.py` and
`program-check.log` in this run's build-work artifacts. The generator and all
written intervals also passed independent exact Sturm certificates and 150-digit
mpmath checks before and after the measurement fix. No numerical value changed.