ball_float Design

ball_float is the certified real-enclosure domain of floating 0.7.1. It builds bare and decorated intervals on BinFloat endpoints and aligns its declared operation boundary with IEEE 1788-2015. Correctness is defined first by set inclusion: a wider interval may be less useful, but an interval that omits a possible exact result is invalid.

Design Contract

The package turns a point operation into an enclosure pipeline:

input interval(s)
  -> classify Empty / Entire / finite / unbounded domains
  -> choose monotone endpoint, critical-point, or full endpoint-product rule
  -> evaluate lower bounds toward -infinity
  -> evaluate upper bounds toward +infinity
  -> apply BallContext bounds and flags
  -> optionally propagate IEEE 1788 decoration

This pipeline separates the mathematical set rule from endpoint arithmetic. bin_float owns dyadic rounding and certified scalar kernels; ball_float owns which endpoint combinations and domain fallbacks are required to enclose the image of a set.

Representation And Invariants

A non-empty bare interval stores a lower endpoint lo_, upper endpoint hi_, and precision, with lo_ <= hi_ and no NaN endpoint. Empty and Entire are explicit states. BallFloat::new(center, radius) is a constructor view; the stored object is still an endpoint interval.

Constructors and precision changes round lo_ toward negative infinity and hi_ toward positive infinity. Therefore conversion or retuning may widen an interval but cannot shrink the represented set. BallFloat::exact(x) embeds the exact dyadic value represented by x; it does not assert that a prior decimal-to-binary approximation equals the original decimal real value.

BallFloatDecorated combines a bare interval with IEEE 1788 decorations and a distinct NaI state. Empty is a valid bare set; NaI records an invalid decorated operation and must not be collapsed into Empty.

IEEE 1788 Alignment

The standard-facing model keeps set values, decorations, and status separate:

• bare interval operations compute set enclosures;
• decorated operations lower the result decoration to the minimum permitted by the operands and operation continuity/domain;
• NaI remains distinct from all bare intervals;
• relations such as subset, interior, overlap, and precedes are set relations, not scalar comparison;
• reverse operations remain outside the 0.7.1 support boundary.

The strict pinned ITF1788 run passes 4,656/4,656 selected cases, including general power, trigonometric, hyperbolic, inverse-trigonometric, and 375 atan2 cases. rootn and extension operations have package-level evidence but are reported separately when the pinned corpus does not cover them. Passing a finite corpus does not imply every IEEE 1788 operation or guaranteed tightness.

Basic Arithmetic Selection

Basic operations select formulas from monotonicity and sign structure:

Operation	Enclosure rule	Important boundary
addition	[a.lo + b.lo, a.hi + b.hi] with directed rounding	Empty propagates
subtraction	[a.lo - b.hi, a.hi - b.lo]	endpoint order reverses for the subtrahend
multiplication	minimum/maximum of four endpoint products	sign shortcuts may reduce work but not candidates
reciprocal/division	reciprocal endpoints when zero is excluded	interior zero crossing yields Entire; one-sided zero may yield a half-infinite interval
square/root	monotone pieces plus zero/domain checks	negative-only square-root domain yields Empty
intersection/hull	endpoint max/min	disjoint intersection yields Empty

BallContext then rounds both endpoints to its precision/exponent range and returns BallFlags for inexact, overflow, and underflow. Entire is a successful enclosure rather than a generic error.

Certified Elementary Functions

Elementary functions use directed dyadic certificates over BinCoeff. Each series or reduction step rounds outward, and an explicit analytic remainder bound encloses the truncated tail. The implementation uses:

• range reduction plus a bounded exponential series for exp;
• power-of-two reduction plus a certified unit-interval series for ln;
• certified logarithms and exact shortcuts for log2/log10;
• Machin-formula bounds for pi, certified quadrant reduction, alternating series, and exact critical-point tests for sin/cos;
• the same reduction plus pole detection for tan;
• monotonic endpoint evaluation and domain splitting for inverse/hyperbolic functions; and
• exp(exponent × ln(base)) with guarded outward arithmetic for general positive-base power.

The shared certification budget permits 12 refinements and increases work precision by max(32, work / 2). try_* operations expose range-reduction, resource-limit, or target-rounding failures as structured certification errors. Total interval operations use conservative set fallbacks when their contract permits it:

• uncertified or very large sin/cos returns [-1, 1];
• a tan pole or uncertified reduction returns Entire;
• analogous composed operations choose their documented whole-domain bound.

This boundary is intentional. The try_* family is appropriate when proof failure must be observable; the total family is appropriate when a valid but possibly wide enclosure is more useful than stopping a calculation.

Critical Points, Poles, And Switching Boundaries

Endpoint evaluation alone is sufficient only for monotone functions. Periodic functions additionally compute a certified range of quadrant/critical indices. If that range contains an extremum, the corresponding -1 or 1 endpoint is included. If it contains a tangent pole, the result is Entire. The decision is made in exact/certified index space, not by comparing an approximate remainder to a heuristic epsilon.

For bounded ordinary arguments, refinement attempts a tight certificate. For unbounded arguments or arguments whose adjusted binary exponent exceeds the resource cutoff max(65,536, 4 × precision), the total path switches directly to the safe range fallback; the try_* path returns a resource-limit detail. This is a proof-resource boundary, not a claim that the mathematical function is undefined.

Decorations And Relations

Decorations propagate by the weakest operand/operation grade. Domain clipping or discontinuity can lower the grade even when the bare enclosure is valid. Set observers retain their interval meaning:

• contains asks whether a point belongs to the set;
• subset, interior, and set_equal compare sets;
• overlap_state classifies relative geometry;
• definitely_lt/definitely_gt prove an order only when all points satisfy it;
• maybe_eq reports compatibility rather than equality.

No total scalar order is defined for intervals. Likewise, Sign::Zero may mean that the set crosses zero rather than that it is the singleton {0}.

Optimization And Trade-offs

Basic interval operations perform a constant number of endpoint operations, so their cost is O(M(p)) at endpoint precision p, with storage for two BinFloat values. Elementary functions add range reduction, bounded series, and up to 12 refinement steps. Their cost is data-dependent because difficult rounding cells and large arguments require more proof precision.

The implementation optimizes repeated constants, exact special cases, monotonicity, and shared trigonometric reduction before increasing precision. It does not optimize by dropping an endpoint candidate or replacing outward rounding with nearest rounding. When tightness and resource bounds conflict, the total API widens and the checked API reports why.

0.7.1 Semantic Preservation Proof

For each finite endpoint candidate y, downward rounding is a lower certificate and upward rounding is an upper certificate. The interval code first selects the mathematical extremum from monotonicity and sign structure, then applies the matching direction; quantize_interval preserves the same outward relation at the stored precision.

The integer-power proof obligations are explicit: positive odd powers increase, positive even powers decrease on the negative half-axis, negative odd powers decrease away from zero, and negative even powers increase on the negative half-axis. Zero-containing negative powers use the pole/whole-real branches. The negative-half-axis regression, directed endpoint tests, and strict ITF1788 aggregate verify ordered set inclusion for the declared forward interval surface. A wider fallback is valid; a reversed or inward-rounded endpoint is not.

Evidence Map

• API reference inventories bare, decorated, context, and try_* operations.
• Tutorial demonstrates safe construction, relations, elementary functions, and proof-failure policy.
• Conformance defines the exact pinned ITF1788 claim and exclusions.
• bin_float design owns endpoint kernels and coefficient dispatch; bin_float performance owns their crossover evidence.