RFD 0067 — The temporal literal surface, carrier reach, and the four-valued comparison frontier

Naming. The substrate concept is domain-neutral. This RFD settles how temporal values are written (literals), how far the carriers reach (range × precision), and how temporal comparison behaves under four-valued open-world semantics. The legal effective-dating and agent/robot examples below name motivating domains, not constructs — the design serves both on one substrate.

• State: discussion
• Revises: RFD 0047 (temporal value library — adds the Instant/ZonedDateTime literal forms and the inner-shape kind rule; drops the mandatory-Z datetime literal), RFD 0056 (bitemporal rules — valid-time is nanosecond, not day-granular; out-of-range valid-time must refuse, not saturate), RFD 0063 — both files sharing that number (a pre-existing numbering collision, README “no reuse” notwithstanding): 0063-bitemporal-read-point (nanosecond valid-time / snapshot precision) and 0063-datalogmtl-temporal-engine (the metric timeline runs at a declared resolution decoupled from snapshot precision)
• Relates to: RFD 0024 (Allen as a library — unchanged), RFD 0016 (numeric tower — the out-of-range-literal loud-refusal precedent, OE1373), RFD 0007 (missing-value semantics — NA vs unknown)
• Tracks: issue #1285 (the parked #…Z# carrier decision this resolves); the two firsthand-found defects it surfaced — #1318 (mutation-body insert constants escape the static loud-gate) and #1319 (epoch_day_to_nanos silently saturates out-of-range valid-time)
• Prior art: ISO 8601-1/-2 (EDTF) and RFC 3339 (date/time/datetime/offset grammar); RFC 9557 / IXDTF (the [Zone] bracket annotation and Z=“UTC known, local offset unknown”); TC39 Temporal and Rust jiff (per-type parse — “you pick the type, the suffix only validates”; the Instant/Plain*/Zoned split); XSD 1.1 Part 2 (xsd:dateTime timezone-optional partial order with the ±14h incomparable window; xsd:dateTimeStamp timezone-required total order); Belnap–Dunn FDE / Fitting bilattices (the four-valued codomain); Wałęga, Cuenca Grau, Kaminski et al., “DatalogMTL over the integers” (KR 2020 / TPLP 2023 — the ℤ-restores-decidability vs ℚ-undecidability result); Snodgrass bitemporal / SQL:2011; pandas datetime64[ns] (the i64-nanosecond epoch window this design currently inherits); Elixir sigils and SQL typed literals (the surveyed authored-literal families); the Argon temporal-representation research campaign (78 agents, .local/research/datetime-literal/{recon-map,deep-map,SYNTHESIS}.md + 37 vault concept notes) — the decidability ledger, incomparability lattice, and refutation ledger; Gabbay–Kurucz–Wolter–Zakharyaschev, Many-Dimensional Modal Logics (the Σ¹₁ two-metric-timeline result); Rivieccio–Jung–Jansana (twist structures / four-valued modal logic); Kolaitis–Vardi (Datalog strong monotonicity — the four-valued-= obstruction); Denecker–Marek–Truszczyński (AFT) and Małuszyński–Szałas 4QL (four-valued Datalog is PTIME on a finite lattice); Pollaci 2026 (three-valued WFS-DatalogMTL over ℤ — the adjacent occupied cell)

Question

Issue #1285 asked a narrow question: does a #YYYY-MM-DDTHH:MM:SSZ# literal denote a zoned Instant or a wall-clock PlainDateTime? The token def and book advertise the trailing Z; the value-layer validator refuses it. The literal is broken in every position.

Widened to the real design: what is the coherent temporal literal surface for Argon’s seven value carriers; how far do those carriers reach (does one substrate serve legal effective-dating at day precision and agent/robot state at nanosecond precision — and what about astronomical timescales); and how does temporal comparison behave under Argon’s four-valued, open-world (Truth4) semantics without breaking the integer-timeline decidability the reasoner depends on?

Context

The value model (settled — RFD 0047)

Seven runtime carriers (oxc-value/src/value.rs), integer- or canonical-string-backed, jiff-validated:

The civil carriers are jiff-backed and span ±9999 years (proleptic Gregorian). Instant uses i128 precisely because a nanosecond count over that span overflows i64.

The current literal surface (broken)

Only two literal tokens exist: #YYYY-MM-DD# → Date, and #…T…# → civil DateTime (decided purely by the presence of a T byte, oxc-lexer). The advertised #…Z# form is loud-refused at value conversion (oxc-value/src/wall.rs:146-168 rejects any trailing Z/offset/[Zone], because DateTime is zone-free). Instant, ZonedDateTime, TimeZone, Time are constructible only through string-parsing builtin functions; Duration only through <int>.days/.weeks sugar. So of seven carriers, five have no literal, and the one datetime literal advertises a form the substrate forbids — the #1285 incoherence.

The reasoning substrate (settled, firsthand-validated)

• One integer (ℤ) metric timeline, and it is the fact valid-time axis. The Lean models time as Nat (spec/lean/Argon/Reasoning/Temporal.lean — “Book §6.10 specifies ℤ”); the reasoner’s interval points are i64 in the timeline’s granularity unit (“days, matching Value::Date”, oxc-value/src/interval.rs:10-13). Rational/real (dense) time is the undecidability cliff (Wałęga TPLP 2023); discreteness — not day-granularity — is what buys decidability.
• Transaction-time is a non-metric frozen selector. All six DatalogMTL operators quantify over valid-time only; tx and rule_vt are single i64 snapshot coordinates (oxc-runtime/src/read_model.rs:131-143). The two-metric-timeline product (LTL×LTL) is Σ¹₁-undecidable over ℤ; Argon avoids it by construction.
• Truth4 is Belnap–Dunn FDE. Its negation is De Morgan and involutive — kernel-checked, axiom-free (spec/lean/Argon/Foundation/Truth4.lean:256-309: neg_neg, neg_truthMeet, neg_truthJoin).
• The bitemporal axes are stored at nanosecond resolution (read_model.rs: vt/tx are epoch-nanos), but the surface caps valid-time at #date# (oxc-instantiate/src/lower/fact_parse.rs:614 — at requires a #YYYY-MM-DD# literal), and the metric materializer floor-projects vt onto the day timeline before reasoning (oxc-runtime/src/federate_translate.rs:271-303).

Two defects found while validating this design (firsthand)

1. The static loud-gate covers rules, not mutation-body constants. #…Z#, a calendar duration (1.months), and even a type-mismatched constant (plain_date_time(…) into a Date field) pass ox check and ox build in insert/struct-field positions and refuse only at mutation execution. The gate (validate_runtime_evaluable_rules) validates rule bodies; insert constants escape it. General — the type-mismatch case is non-temporal.
2. Out-of-range valid-time silently saturates. epoch_day_to_nanos is epoch_days.saturating_mul(NANOS_PER_DAY) (oxc-value/src/civil.rs:241-243). Any valid-time beyond the i64-nanosecond window (1677-09-21 … 2262-04-11) clamps to the boundary. Round-trip-proven: at #5000-01-01# and at #9999-01-01# collapse to the same instant (as_of #5000# and as_of #9999# return identical rows) — a silent coercion, the exact class the loud-gate forbids and that OE1373 already refuses for integer literals.

Decision

1. One delimiter; the inner ISO shape totally determines the carrier

Keep #…# as the sole temporal-literal delimiter. It is collision-free against #[attribute] (single-byte lexer dispatch: #+digit → temporal, #[ → attribute) and is already a leading, static kind marker — the only property the loud gate forces (the kind must never ride on a trailing payload byte that could silently flip it). The inner ISO-8601/RFC-9557 shape determines the carrier, as a total, static, refusing function κ : SurfaceForm → Carrier + Diagnostic:

Duration stays a unit-suffixed quantity (30.days), not a #…# literal — it is a length, not a point.

This resolves #1285: #…Z# is the Instant literal (which is what a trailing Z = UTC always meant), not a refused pseudo-DateTime. Every reasoning-relevant carrier becomes a first-class literal reachable in compile-time positions. This is kind-determination, not suffix-inference: each shape maps to exactly one carrier, decided statically at parse; a malformed or ambiguous inner form is loud-refused. It is the loud-gate reframed as a proof obligation — κ total + deterministic is the formal content of “never silently coerce.”

2. Nanosecond reach; valid-time is not day-granular

The bitemporal axes are nanosecond. at <…> and as_of <…> accept an Instant literal (sub-day), not only #date#. Snapshot selection (“the fact valid at instant t”) is a granularity-free integer comparison — so one substrate serves agents/robots at nanosecond precision and legal effective-dating at day precision, differing only in which literal precision the modeler writes. The #date# form is a convenience (midnight-UTC), not the resolution.

3. Out-of-range valid-time refuses; the loud gate covers insert constants

• Replace the epoch_day_to_nanos saturation with a loud refusal when a valid-time’s epoch-nanos exceeds the axis (following the OE1373 out-of-range-literal precedent). Never silently clamp.
• Extend the static loud gate to validate statically-knowable mutation-body constants — #…Z#, calendar durations, type-mismatches must refuse at ox check/ox build, not at execution.

4. Carrier reach and astronomical time

• Civil carriers reach ±9999 years (Gregorian, jiff) — covering all recorded human history and any agent/robot in the present ± centuries. The nanosecond bitemporal axis currently spans the i64-nanosecond window 1677-09-21 … 2262-04-11 (the pandas datetime64[ns] range).
• Astronomical/geological time is a modeled domain on the substrate, not a stretch of the civil carriers. The reasoning core (a discrete integer timeline + interval/Allen/metric algebra) is scale-agnostic and decidable at any discrete tick, so geological spans are reasoned over at a coarse tick as an ordinary ordered domain. The civil Date/Instant carriers are not extended to cover them: the Gregorian calendar is physically inapplicable at Myr/Gyr scale, and precision × range is bit-bounded. This is the ontology-neutral posture — model the domain, don’t weld it into the built-in carrier.

5. Reasoning-core dispositions (validated; recorded as decided)

• as_of axis dispatch stays lexical: as_of <int> = transaction-time, as_of <#date#|instant> = valid-time. Transaction-time remains a non-metric selector (the only decidable bitemporal regime).
• Calendar month/year shifts are anchored Date → Date functions (add_months/add_years), never metric operators or durations. A non-uniform (anchor-dependent) metric step has no decidability result; calendar-relative durations are loud-refused (OE1337). The metric timeline’s step is fixed/uniform by construction (interval.rs).
• NA (non-applicable) is a schema/type concern, not a fifth truth value. It is expressed by field: T? (StructurallyOptional → a positive ⟨.is, none⟩, Lean-proven in TypeSystem/Soundness/FieldAccess.lean), [0..0] cardinality, or conditional impls. Can stays reserved for existing-but-unknown. Truth4 stays four values (drift-gate-locked).
• Cross-time identity: = stays rigid, two-valued, congruent over system-allocated IndividualId (a four-valued or counterpart = provably breaks the Datalog join engine). Identity-mutation (legal merger = fusion, spinoff = fission) — which the current surface cannot express and which Argon’s legal/tax-restructuring domain requires — is closed by an explicit, first-class, std-neutral successorOf/mergedInto succession relation carrying valid-time, joined explicitly by the modeler, never the engine =.
• Replay across oxup update: stored values read identically by construction — Instant is an integer; ZonedDateTime is an offset-baked, self-describing string (reading and ordering need no tzdb). The bundled tzdb/leap version pins at the build-artifact closure (make it observable — stamp jiff_tzdb::VERSION into artifact provenance). A zone-aware re-derivation (arithmetic producing a new zoned value across a revised DST rule) pins its version to the recorded read-point; discharged when zoned reasoning is surfaced.

6. Declared-resolution metric timeline (decided — resolves the former open question)

The metric-operator tick is a package-declared resolution, decoupled from the granularity-free snapshot precision. Decidability rests on discreteness, not on the tick equalling a day; the tick is a positive-integer coarsening of the same ℤ timeline (strictly fewer points, never crossing into density), so ultimate-periodicity and the finite-materialization argument transfer verbatim.

• Surface: a package-global [temporal.metric] resolution manifest setting (resolution = "week", or "<N><unit>" like 2weeks) — not per-rule or per-module. The metric timeline is one axis shared by every rule and fact interval; a per-rule tick would let two rules quantize the same fact set to incompatible grids — the silent scale-mismatch the loud gate forbids. It mirrors default_world (a package-global evaluation cut, stamped into the artifact’s GlobalControl, threaded to the runtime). It lives under a [temporal] umbrella, not a bare top-level [metric]: metric alone is overloaded (it reads as a measurement/units/observability knob, especially beside the Real/Decimal/Money value tower, and only disambiguates for a reader who already knows the modal-vs-metric DatalogMTL split — the one who least needs it); and it is not a bare [temporal], which over-claims — temporal is the umbrella sub-tier and metric is one operator family inside it (beside the modal box/diamond family; the classifier’s additive-composition rule is stated in exactly those terms, OE0712). [temporal.metric] keeps the precise word scoped to the metric timeline, has the correct containment direction (temporal ⊇ metric), and leaves a growable sibling namespace ([temporal.modal], [temporal.snapshot], axis width, …). ([metric.temporal] was rejected — it inverts the hierarchy and returns the overloaded word to the owning position; a flat metric_timeline_resolution = is the acceptable no-nesting fallback.)
• Semantics: one MetricResolution (ns-per-tick) feeds BOTH fact valid-time projection and metric-window bound scaling, so the fact grid and the window unit can never disagree. Snapshot reads stay full-nanosecond (they never consult the tick). A metric bound authored in whole days maps onto the tick by integer division; a non-tick-multiple bound loud-refuses (since[3 days] at a week tick → 3/7 → refuse, never rounds to 0/1). Fact intervals euclidean-floor onto the tick grid (inclusive-lo → containing tick; exclusive-hi → (nanos−1) floored, so a tick-aligned end excludes its whole tick and an empty window stays empty). The default is DAY — an undeclared package is byte-identical to the pre-RFD behaviour.
• Bounds are authored in days (via .days/.weeks/bare int), the tick coarsens that authored unit; this preserves the meaning of existing day-authored programs (the alternative — tick-native bounds where since[3] = 3 ticks — was rejected as it silently reinterprets existing box_minus[1,3]). Sub-day fact ticks are admitted (still ℤ); authored sub-day bounds (.hours) are out of v1 scope (a day-authored bound at a sub-day tick refuses).
• An unrecognized [temporal.metric] resolution value warns (OW1240) and falls back to DAY, per the RFD 0030 §D6 manifest-honesty convention (unrecognized manifest values are non-fatal + treated-as-absent, for forward-compatibility — an older toolchain must not hard-die on a future unit spelling). This is deliberately not a hard refusal: the mis-default yields internally-consistent day-tick results plus a surfaced warning, not corrupt/dropped data, so the loud-gate’s silent-wrong-value concern does not bite; the manifest-forward-compat convention wins.
• The tick coarsens the metric operators only; the stored i64-nanosecond valid-time axis is untouched. Composing a very-coarse tick with an i128 axis widening (for deep-range bitemporality) is deferred to the separate axis-width open question below.

Rationale

• Inner-shape κ over #…#, not a typed prefix or suffix-inference. The loud gate forbids silent coercion, not static kind-determination; a total κ over the inner shape is loud-gate-compatible, keeps a single delimiter, honors the carriers’ own ISO/RFC-9557 semantics (Z=UTC=Instant; [Zone]=Zoned), and needs no new lexer facility. Suffix-inference — a bare Z contextually flipping a value’s kind — is the footgun the loud gate exists to ban; κ is not that (one shape, one carrier, statically). The requirement that forced Instant into the literal set (sub-day valid-time for agents/robots) is met most economically by the inner shape.
• Nanosecond is decidability-safe. The ℤ-vs-ℚ cliff is a density property; nanoseconds are integers. “Day-granular” was a legal-domain default, not a substrate requirement; Argon’s general mandate (agents, robots, fast-changing state) requires sub-day and pays nothing for it.
• Saturation → refusal, insert-gate coverage: silent clamp and silently-mistyped inserts both violate the loud-gate invariant (“a build that drops or mis-stores a value yields wrong answers”). OE1373 is the precedent.
• Every §5 disposition is forced by ground truth, not chosen: kernel-checked Lean (neg, FieldAccess), structural locks (drift gate, interval.rs fixed step, IndividualId), and runtime proofs (OE1337; the identity diagonal; the offset-baked round-trip).

Alternatives considered

• Typed-prefix literals (date"…", instant"…"). The cross-provider design consensus (three independent model families). Rejected: #…# already satisfies the only forced constraint, inner-shape κ covers all carriers, and a typed prefix is a new lexer facility (Argon has no string-prefix lexing today) that buys nothing forced. Retained as the runner-up: if the inner-shape lexing of zone/offset forms proves problematic, the typed prefix (CamelCase, type-name-aligned) is the fallback.
• Suffix-inference (ISO/Temporal-from-string). Rejected: a keystroke silently changing the carrier kind is the Python-aware/naive and OWL partial-order footgun.
• Day-granular valid-time (keep it). Rejected: domain-biased, fails the agent/robot mandate, and unnecessary (sub-day is decidability-safe).
• Widen Date/Instant to astronomical scale. Rejected: Gregorian is physically inapplicable at Myr/Gyr, and precision × range is bit-bounded; astronomical time is a modeled domain.
• Native four-valued =, a fifth NA value, a standalone Offset carrier. Rejected respectively: breaks the join engine; is a schema-layer applicability concern; an offset-only string is losslessly absorbed by Instant and ZonedDateTime correctly requires a named zone.

Consequences

Immediate, forced fixes (shippable, #1285’s real scope):

• Grammar/lexer/parser: recognize the zone/offset inner shapes; route #…Z#/#…±HH:MM# → Instant, #…[Zone]# → ZonedDateTime; keep #YYYY-MM-DD#/#…T…#.
• oxc-instantiate fact_parse: accept an Instant in at/as_of; refuse out-of-range valid-time (replace saturating_mul).
• Extend the static loud gate to insert-body constants.
• Drift fixes: the tree-sitter grammar (grammar.js still requires Z), the lit.toml DATETIME desc, the book (lexical-structure.md, stdlib.md drop the mandatory Z), and the DST-gap-invalid canonical example in value.rs.
• Directed diagnostics (e.g. a typed code for a malformed instant literal that names the carrier).

Builds (scheduled):

• Surface the Instant/ZonedDateTime/TimeZone type names (std::datetime, per RFD 0047) — with the read-point tzdb-version pin, not as a hollow surface.
• The successorOf succession package (parallelizable — a sibling work stream).
• Observable tzdb-version artifact stamp; the declared-resolution metric timeline (decouple metric-op tick from snapshot precision).

Lean/book: revise the Lean dateTime grammar (drop mandatory-Z; inner-shape κ); reconcile the book.

Migration: small and mostly additive — Date/DateTime literals are unchanged; Instant/Zoned literals are new; the #…Z# uses in the tree are three lexer/parser/instantiate tests (oxc-lexer/src/lib.rs, oxc-parser/tests/fact_arg_literals.rs, oxc-instantiate/tests/fact_arg_literal_set.rs) and a research doc — no std/, examples/, or production use.

The research campaign’s decision surface (SYNTHESIS §7) lists six commitments “only the owner can make”; §5 above records all six as resolved against Argon ground truth — Truth4 negation is De Morgan-involutive (kernel-checked); transaction-time is a non-metric selector; metric operators range over one timeline; identity is surface-rigid = over perdurantist storage slices; the tzdb/leap version lives at the build-artifact closure (with a read-point pin for zone-aware re-derivation); calendar month/year units are anchored functions / EDB, never metric operators. That leaves Tier-1 (four-valued metric decidability, Open Questions below) as the sole research obligation, and it gates claiming — not shipping — the four-valued lift.

Open questions

• The one genuine research obligation — four-valued metric decidability. Cross-kind temporal comparison is structurally four-valued: a zoneless DateTime vs an absolute Instant, an offset-unknown value, or two values across the XSD ±14h window are genuinely incomparable, which is a Can verdict a total order cannot produce. Truth4’s kernel-checked De Morgan involution satisfies the quasi-Boolean→classical reduction precondition — but no published result establishes the decidability of a Belnap/four-valued metric reasoner over ℤ. The 2-valued DatalogMTL decision procedure rests on three pillars — least-fixpoint over {true, ¬derived}, consistency ≡ ⊥-never-derived, and ultimate-periodicity over the 2-valued canonical model — and a designated, non-explosive Both attacks all three; whether the ℚ-undecidability lower bound even survives paraconsistency is open in every direction. The 2-valued-plus-refusal comparison ships sound today; moving to native Can/Both temporal comparison requires a Lean proof campaign (scratch-first) before it can be claimed decidable. This warrants its own RFD and a mechanization campaign; it gates claiming, not shipping, the four-valued lift.

  The concrete first proof step (from the research campaign’s decidability ledger): show the twist-structure “two coupled Boolean copies” reduction (Rivieccio–Jung–Jansana) factors the metric T_Π canonical-model / ultimate-periodicity ruler argument coordinate-wise — established for qualitative modal box/diamond, open for the metric ℤ ruler. Note four-valuedness is not itself the cost (Fitting/AFT: complexity-neutral over a finite interlaced bilattice, and 4QL keeps plain four-valued Datalog PTIME); the specific threat is the designated non-explosive Both against pillar (b) (consistency ≡ ⊥-never-derived) and pillar (c) (2-valued periodicity). Two adjacent sub-obligations ride along: a mechanized totality proof of the multi-carrier kind function κ (no published multi-carrier kind-inferred-from-body grammar has one — a new result), and ω-admissibility of the Allen layer over discrete ℤ (proven only over the dense line). The value-half of κ is itself four-valued at construction: a DST gap is a no-Is-witness, a fold is Both — today collapsed to a strategy parameter, which the loud-gate should instead surface.

• Bitemporal axis width. The i64-nanosecond axis gives the 1677–2262 window; widening to i128-nanos (matching the Instant value carrier’s ±9999yr @ ns) if fine-grained deep-range bitemporality is wanted — a knob, priority-second to the saturation refusal.

• Metric-timeline declared resolution. Decoupling the metric-operator tick (cost scales with tick count) from the granularity-free snapshot precision. Resolved — see Decision §6 ([temporal.metric] resolution package-global setting; one MetricResolution feeds fact projection + bound scaling; DAY default).

• Explicit as_of/as_recorded axis naming. Only if authored fine-grained transaction-time instants become a need (transaction-time is a system watermark, rarely hand-written).

• Incomparability composition. Whether the distinct incomparability causes (offset-unknown, calendar-vs-fixed duration, cross-kind, causal concurrency) collapse into one Truth4 algebra or require a product/bilattice of per-cause comparison relations — an open algebraic question in formal KR.