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.

profile : Str

Identifier of the finite POSIX interval interpretation model.

paired : List(PosixSpan) -> Try(IntervalEvidence, [InconsistentEvidence, TooManyAlternatives, ..])

Construct evidence from 1 to 4096 correlated interval choices. Sort and deduplicate choices while preserving each interval as one alternative.

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

Admit every strictly ordered start/end pair from the supplied lists without materializing their product. Reject empty lists, lists over 4096 entries, or inputs with no start strictly before any end.

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.

definite_coverage : IntervalEvidence -> Coverage

Return the intersection of all admissible intervals: the points that must be inside the unknown interval. The intersection can be empty.

declaration : IntervalEvidence -> Declaration

Return the normalized choices and their paired or independent interpretation.

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.

to_hash : IntervalEvidence, Hasher -> Hasher

Hash the canonical declaration consistently with declaration equality.

to_inspect : IntervalEvidence -> Str

Summarize the declaration kind and choice counts without enumerating pairs.

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

Canonical supplied choices. Paired retains start/end correlation; Independent retains each endpoint list, including endpoints with no admissible partner.

Truth : [Definite, Possible, Impossible]

Point membership across admissible intervals: all (Definite), some but not all (Possible), or none (Impossible).