IntervalEvidence

IntervalEvidence :: # (opaque)

Finite evidence for one unknown nonempty POSIX interval, profile finite-posix-interval-alternatives-v1. Endpoints use signed I64 microseconds. Paired choices preserve correlation. Independent choices admit every start/end combination with start < end; invalid combinations are not interpretations. Empty admissible evidence errors. Unknown/unbounded and civil descriptions require separate explicit interpretation; no zone or tolerance is inferred.

Construction accepts at most 4096 spans or 4096 endpoints on each side, normalizes inputs in O(n log n) and retains O(n) input/summary storage. Independent construction never materializes the Cartesian product. Point queries cost O(log n) for paired choices and O(1) for independent choices.

paired : List(PosixSpan) -> Try(IntervalEvidence, [InconsistentEvidence, TooManyAlternatives, ..])
independent : { starts : List(PosixBoundary), ends : List(PosixBoundary) } -> Try(IntervalEvidence, [InconsistentEvidence, TooManyAlternatives, ..])
contains : IntervalEvidence, PosixBoundary -> Truth

Definite means every admissible interval contains the point; Possible means some but not all; Impossible means none. Queries do not allocate or enumerate pairs and can include either I64 boundary without overflow.

possible_coverage : IntervalEvidence -> Coverage

Existential union and universal intersection, respectively. These are explicit projections of evidence, not the unknown actual interval.

is_eq : IntervalEvidence, IntervalEvidence -> Bool

Declaration equality preserves paired versus independent intent and all normalized supplied choices, including nonparticipating endpoint values. This does not claim equivalence for all interval-reasoning propositions.

Declaration : [Paired(List(PosixSpan)), Independent({ starts : List(PosixBoundary), ends : List(PosixBoundary) })]
Truth : [Definite, Possible, Impossible]