The two times

A company issues shares on March 15, 2026. The issuance passes evaluation against the securities rules then in force, and the transaction proceeds. Both the issuance and the rules in force on March 15, 2026 become historical facts.

On June 1, 2026, the legislature amends the securities law’s reporting threshold for share issuances. The March issuance required no special reporting under the old law. Under the new law, it would have.

With only a mutable timestamp on each record, the software cannot retain these distinctions. Updating the evaluation under the new law makes a lawful transaction appear unlawful in the historical record. Ignoring the new law leaves a rule that validly reaches the present unapplied. Keeping both results without specifying which question each answers leaves their meaning unclear.

Frozen time records when something happened: the issuance was committed, the amendment enacted, or the evaluation rendered. No later event changes it. A rule’s effective date is also frozen time. That the amendment takes effect on June 1 is a historical fact fixed by enactment.

Derived time results from applying a rule to frozen facts. Examples include a reporting deadline for the March issuance, a tolled limitation period, or a compliance status under a given version of the law. Each computation produces a new, dated consequence while preserving the original record.

The system must retain both the time of the fact and the time that a rule derives from it.

Why two times, not one

Database timestamp columns and object-relational updated_at fields encourage a single mutable timeline in which only the current state survives.

A compliance record must preserve what was true at a specific moment. Silently updating it when rules change destroys that evidence. It then shows only what the current software computes, which may change again, rather than whether the transaction was lawful when it occurred.

An immutable record also permits commitment. Later rules may reinterpret past facts or change their consequences, while the record preserves what happened and when. If past evaluations can be silently revised, none can be treated as final. Closed audits, settled trades, and issued licenses depend on completed evaluations.

The non-retroactivity invariant

Frozen facts can enter a computation that produces derived consequences. No computation can convert a derived consequence into a frozen fact.

A tolling provision illustrates the direction. A claim accrues on a recorded, frozen date, and the limitation rule derives a deadline of June 30. A suspension begins on another frozen date. The tolling rule uses the derived deadline and frozen suspension date to extend the deadline to December 30. That extended deadline remains in the derived stratum.

A second suspension tolls the extended deadline in the same way, without re-deriving it from the accrual. Each deadline references its inputs: either the frozen accrual, or the deadline it extends and the frozen suspension that tolls it. All those inputs remain in the record. June 30 remains June 30, and the accrual and suspensions retain their historical dates. The facts occupy one stratum and the deadlines the other.

A savings clause preserves liability incurred under a repealed statute, as the general federal savings statute, 1 U.S.C. § 109, does. The repeal is a dated enactment with prospective effect, while the earlier liability stands. A limitation rewrite may extend or shorten deadlines for pending claims. The system represents that reach-back as new derived deadlines over unchanged filing facts. In each case, a rule produces a new consequence from a preserved fact.

The invariant forbids a derived value where a frozen value is required. A tolled deadline therefore cannot enter the record as the date of an event. The rule language provides no operation that converts derived time to frozen time. The proof and its scope are stated below.

This is temporal stratification

Temporal stratification borrows its name from stratified logic programming. There, a predicate cannot be defined by negating a predicate in its own or a higher stratum. Excluding recursion through negation gives the program a single intended model (Chandra and Harel, 1985; Apt, Blair and Walker, 1988). A logic program may require arbitrarily many strata. The construction here uses the same discipline of one-way reference between layers, with two strata:

• Stratum 0: frozen historical time. What happened and when, as attested – transactions committed, rules enacted and taking effect, authorities appointed, judgments rendered, observations recorded.
• Stratum 1: derived legal time. What follows from frozen facts under a body of rules. May reference stratum 0; cannot modify it.

Derived time is indexed by the rules that produced it. The rules in force at a moment form a versioned set, the rule pack. Each derived consequence records that pack and its frozen source facts. The verdict “Compliant” requires its context: “compliant under the June 1 pack, derived from the March 15 facts.”

The stratification is flat. Deriving from a derived consequence does not create a third kind of time. Re-evaluating a consequence under a newer pack rebuilds it from the same frozen source under that pack. A time is either a historical fact or a value derived from historical facts under a named pack.

What is proved, and where

The companion paper Lex: A Logic for Jurisdictional Rules (section 3.2) makes both sorts first-class in the rule language’s type system. Time₀ represents frozen historical time, and Time₁ represents derived legal time. Effective dates, repeals, tolling, and pack evolution are typed terms. A derived time is a closure containing the frozen source fact, the pack, and a derivation witness that cites the rules used.

Soundness here means that no path leads from derived time back to frozen time. The mechanized theorem establishes this property for the language’s temporal constructor graph. Its rules cover lifting, derivation, tolling, effective dates, timestamping, and pack re-evaluation. No rule with a Time₀ conclusion has a Time₁ premise. The transitive closure of the temporal coercions therefore contains no path from Time₁ to Time₀.

A companion result establishes that re-evaluation under a new pack rebuilds the closure over the same frozen source. The source projection is definitionally unchanged. Both results are machine-checked in the Lex development’s temporal-stratification and pack re-evaluation modules.

Two obligations remain open. First, the theorem covers the temporal fragment’s rule graph. Connecting the full typing relation to that graph remains an integration obligation.

Second, pack-evolution soundness remains open: a well-typed judgment transported across a pack rewrite must remain well-typed and preserve its verdict. The companion paper states this at two levels (section 3.3). In the stable fragment, every rule cited by the derivation survives by digest. The named proof target there is induction on the typing derivation. For the modal and temporal subsystem, re-evaluation must also commute with the temporal and tribunal modalities, and soundness remains a conjecture.

Within the proved fragment, “the type system forbids it” is a theorem. Outside that scope, the same rule shapes enforce the design intent, but the proof does not yet cover it.

Prior art

Temporal databases have distinguished valid time, when a fact held, from transaction time, when it was recorded, since Snodgrass and Ahn (1985). Jensen et al. (1994) consolidated the vocabulary. SQL:2011 standardized both through application-time periods and system-versioned tables (Kulkarni and Michels, 2012). A system-versioned table preserves past states.

The norm-change literature formalizes abrogation, annulment, and temporal rule versions (Governatori and Rotolo, 2010). Legislative-markup standards also track point-in-time statute versions (Palmirani, 2011). The single-mutable-timeline failure comes from omitting these techniques, rather than from versioning itself.

Record versioning alone leaves the programs that compute over records unconstrained. A rule engine can read a bitemporal store and write a tolled deadline where a frozen accrual date belongs. The store will then version that error. Typing the rule language over time rejects this ill-formed program before execution.

This typing restriction determines how retroactive law is represented. Without a coercion from derived to frozen time, an old evaluation cannot be updated to express retroactive application. A retroactive tax amendment or extended limitation period instead produces a fresh derivation under the new pack from the frozen facts. It coexists with the original evaluation. Reach-back occurs in the derived stratum and remains attributed to its rule.

Why this matters for compliance

Without stratification, the March 15 issuance passes evaluation under the rules then in force, and the transaction proceeds. On June 1, the system re-evaluates it under changed rules and reports failure. A historically approved transaction now appears non-compliant, although the earlier approval was correct under its rules. The software cannot report “compliant then, non-compliant now,” because it retains only one time. It has lost the original evaluation, which was evidence of lawful conduct.

Regulators, auditors, and counterparties need both answers. The frozen-context question asks for the transaction’s status under the rules in force at commitment. The derived question asks what its status would be under current rules. Answering the latter must preserve the evidence needed to answer the former.

With stratification, the March evaluation under the March pack is frozen at stratum 0. The June re-evaluation is derived at stratum 1 and indexed by the June pack. Both remain queryable, and the rule language supplies no operation that collapses one into the other. An auditor can see that the transaction was compliant when it occurred and would be non-compliant under current rules.

Authority is a stratum-0 fact

The attested institutional authority record is also frozen: which regulator supervised the firm, which court held the case, and which officer held a delegation, over which periods. Each rendered judgment is likewise a timestamped event, just as the share issuance is. Applying a pack to those events derives consequences such as remedy deadlines, tolled periods, and the status following a ruling.

Selecting the authority for a dispute requires a rule over that frozen assignment record. Legal systems use different selectors by domain. Criminal liability generally selects by event time, while United States diversity jurisdiction selects by filing time (Grupo Dataflux v. Atlas Global Group, 541 U.S. 567 (2004)). Tribunals established after events can also hear them. The International Criminal Tribunal for the former Yugoslavia was established in 1993 with jurisdiction reaching back to 1991. It applies a new selector to the frozen event record without rewriting who held authority in 1991.

The frozen assignment record makes event-time, filing-time, and decision-time selection well-posed queries with definite answers. If current assignments overwrite earlier ones, the system retains only the data needed for the decision-time question.

Evidence is a stratum-0 fact

A frozen decision context has two coordinates: the rules in force and the evidence available at the time of the act. The same discipline protects both. Each observation carries its recording time as a frozen fact, so two strata still suffice.

Suppose a transaction is approved in March and disputed in August. The intervening record contains new filings, attestations, counterparty disclosures, and examination findings. Retrieving the whole corpus answers the March question with knowledge unavailable to the March actor. A compliance officer given the current file makes the same error as a machine with unbounded retrieval.

Two retrospective questions fix different coordinates. Asking whether the act was lawful under the rules then in force, on the facts now known, fixes the rules while admitting later evidence. Fraud discovered in August can reveal that the March act was unlawful then. The evidence reveals the past without revising it.

Asking whether the determination was sound on the record then before the decision-maker fixes both coordinates. This question of due diligence and reasonable reliance excludes hindsight. It can be answered only from evidence available at the time. An as-of bound separates these questions, which a single timeline silently blends.

The query interface enforces that bound. A retrospective query names a reference point, and retrieval admits only records whose recording time is at or before it. This is a precondition on access, independent of the querier’s diligence. It applies the database distinction between valid time and transaction time to the non-retroactivity invariant’s second coordinate. Judging a determination on later-recorded evidence makes the same error as judging it under later-enacted rules when the question excludes hindsight.

The general pattern

1. A fact is committed at a specific moment. That moment is frozen.
2. A rule is applied to the fact, possibly much later. The application produces a derived, dated consequence, attributed to the rule and pack that produced it.
3. The consequence coexists with the fact. It does not replace it.
4. The flow is one-directional: facts into derivations, never derivations back into facts.

Accounting similarly separates historical cost from fair-value adjustment, and science separates observations from reinterpretation under a new theory. Version control preserves commits while branch pointers move. In institutional computing, confusing the strata misstates what was lawful when it occurred and erases the evidence needed to detect that error.

The rule language therefore needs two sorts of time, a one-way coercion, and derived consequences indexed by their governing rules. Together, these preserve historical evidence while allowing the system to compute new legal consequences.

References

Apt, K. R., Blair, H. A. and Walker, A. (1988). “Towards a Theory of Declarative Knowledge.” In Minker, J. (ed.), Foundations of Deductive Databases and Logic Programming, Morgan Kaufmann, 89–148.

Chandra, A. K. and Harel, D. (1985). “Horn Clause Queries and Generalizations.” Journal of Logic Programming, 2(1), 1–15.

Governatori, G. and Rotolo, A. (2010). “Changing Legal Systems: Legal Abrogation and Annulment in Defeasible Logic.” Logic Journal of the IGPL, 18(1), 157–194.

Jensen, C. S. et al. (1994). “A Consensus Glossary of Temporal Database Concepts.” SIGMOD Record, 23(1), 52–64.

Kulkarni, K. and Michels, J.-E. (2012). “Temporal Features in SQL:2011.” SIGMOD Record, 41(3), 34–43.

Palmirani, M. (2011). “Legislative Change Management with Akoma-Ntoso.” In Sartor, G., Palmirani, M., Francesconi, E. and Biasiotti, M. A. (eds.), Legislative XML for the Semantic Web, Springer.

Snodgrass, R. and Ahn, I. (1985). “A Taxonomy of Time in Databases.” Proceedings of the 1985 ACM SIGMOD International Conference on Management of Data, 236–246.