The two times

Consider a corporate transaction: a company issues shares on March 15, 2026. On that date the issuance is evaluated against the securities rules then in force, the evaluation passes, and the transaction proceeds. March 15, 2026 is frozen. The issuance happened, and which rules were in force that day is a matter of record.

Now the legislature amends the securities law on June 1, 2026, changing the reporting threshold for share issuances. Under the old law the March issuance required no special reporting; under the new law it would have.

If the software has only one notion of time – a mutable timestamp on each record – every available move is wrong. Update the evaluation to reflect the new law, and the record of a lawful transaction now reads as unlawful. Ignore the new law, and a rule that validly reaches the present goes unapplied. Keep both results with no stated rule for which answers which question, and the system is neither correct nor comprehensible.

The resolution is two kinds of time. The first is the time at which something happened: the issuance was committed, the amendment was enacted, the evaluation was rendered. Call this frozen time. It is immutable; no later event changes it. A rule’s effective date is frozen time too – that the amendment takes effect on June 1 is itself a historical fact, fixed by the enactment. The second is time produced by applying a rule to frozen facts: the reporting deadline the new threshold implies for the March issuance, a limitation period tolled by a suspension, a compliance status computed under a given version of the law. Call this derived time. Deriving is not replacing. The computation yields a new, dated consequence and leaves the original record untouched.

The distinction between the time of the fact and the time derived by a rule from the fact is the load-bearing one, and the rest of this note is about keeping it.

Why two times, not one

The temptation is to collapse them. Every database has a timestamp column, every object-relational layer an updated_at field; the habits of software push toward a single mutable timeline in which the current state is the only state.

Institutional records cannot live on that timeline. The point of a compliance record is that it captures what was true at a specific moment. If the record is silently updated when the rules change, its evidentiary value is destroyed: it no longer shows that the transaction was lawful when it occurred, only that someone’s software currently computes it lawful – a much weaker statement, and one that may change again tomorrow.

An immutable record is also a precondition for commitment. The past can be reinterpreted, new consequences can be derived from old facts, and rules can reach back to change consequences; what no rule changes is the record of what happened and when. A system in which past evaluations can be silently revised can never treat any evaluation as final – and institutions run on finality. The closed audit, the settled trade, the issued license all depend on some evaluation being over.

The non-retroactivity invariant

The relationship between the two times is asymmetric. Frozen time flows into derived time: a historical fact enters a computation and a derived consequence comes out. Derived time never flows back into frozen time. This is a one-way gate.

Concretely: a tolling provision suspends a limitation period. The claim accrued on a recorded date – frozen. The limitation rule applied to that fact yields a deadline of June 30 – derived. The suspension began on a recorded date – frozen – and the tolling rule, consuming the derived deadline and the frozen suspension date, extends it to December 30 – derived, in the same stratum as the deadline it extends. A second suspension tolls the tolled deadline the same way: tolling stacks in the derived stratum and never re-derives from the accrual. Each derived deadline references what it was derived from – the frozen accrual, or the deadline it extends and the frozen suspension that tolls it – and replaces none of it. June 30 remains June 30, the accrual and the suspensions remain on the record as they happened, and the dates coexist, the facts in one stratum and the deadlines in the other.

The same shape recurs across law. A savings clause preserves liability incurred under a repealed statute – the general federal savings statute, 1 U.S.C. § 109, does exactly this – so the repeal is a dated enactment whose effect runs forward, and what was incurred before it stands. A limitation rewrite extends or shortens deadlines for pending claims: reach-back, expressed as new derived deadlines over unchanged filing facts. In every case a frozen fact combines with a rule to produce a derived consequence; the consequence is new, and the fact is untouched.

The invariant is that nothing derived is accepted where something frozen is required. The tolled deadline cannot be written back into the record as if it were something that happened. In the rule language this note rests on, that is not a convention but an absence: no operation converts derived time to frozen time. What the absence is worth – what is proved about it, and where the proof stops – has its own section below.

This is temporal stratification

The name is borrowed from stratified logic programming, where predicates are assigned to strata so that no predicate is defined by negating one in its own or a higher stratum; forbidding recursion through negation is what gives such a program a single intended model (Chandra and Harel, 1985; Apt, Blair and Walker, 1988). What is borrowed is the discipline of one-way reference between layers, not the count: a logic program may need arbitrarily many strata. Here two suffice.

• 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.

Two refinements make this exact. First, derived time is indexed by the rules that produced it. The rules in force at a moment form a versioned set – call it the rule pack – and a derived consequence records the pack under which it was derived along with the frozen facts it was derived from. “Compliant” is never a bare verdict; it is “compliant under the June 1 pack, derived from the March 15 facts.” Second, 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 the new pack. Either a time is a historical fact or it is derived from historical facts under a named pack. The distinction is binary, which is why two sorts carry it.

What is proved, and where

The companion paper Lex: A Logic for Jurisdictional Rules (section 3.2) makes the two sorts first-class in the type system of a rule language: Time₀ for frozen historical time, Time₁ for derived legal time, with effective dates, repeals, tolling, and pack evolution as typed terms rather than metadata. A derived time there is a closure – the frozen source fact, the pack under which the consequence was derived, and the derivation witness citing the rules used.

Soundness, for this note, means exactly one property: no path from derived time back to frozen time. The mechanized theorem is that property and no more. In the temporal constructor graph of the language – its lifting, derivation, tolling, effective-date, timestamping, and pack re-evaluation rules – no rule with a Time₀ conclusion has a Time₁ premise, and the transitive closure of the temporal coercions contains no path from Time₁ to Time₀. A companion result gives re-evaluation its meaning: re-evaluating a derived consequence under a new pack rebuilds the closure over the same frozen source, and the source projection is definitionally unchanged. Both are machine-checked in the Lex development, in its temporal-stratification and pack re-evaluation modules.

Two obligations remain open, and the claim is scoped by them. The theorem governs the temporal fragment’s rule graph; the coverage result connecting the language’s full typing relation into that graph is an unfinished integration obligation. And pack-evolution soundness – that a well-typed judgment carried across a pack rewrite stays well-typed and keeps its verdict – is open at both levels at which the companion paper states it (section 3.3): on the stable fragment, where every rule the derivation cites survives the rewrite by digest, it is a named obligation with a proof target, induction on the typing derivation; for the modal and temporal subsystem, where re-evaluation must also commute with the temporal and tribunal modalities, it is a conjecture. Within that scope, “the type system forbids it” is a theorem. Outside it, it is the design intent, enforced by the same rule shapes but not yet covered by the proof.

Prior art

The two-time distinction is not new. Databases have separated valid time – when a fact held in the world – from transaction time – when the system recorded it – since Snodgrass and Ahn (1985); the temporal-database community consolidated the vocabulary (Jensen et al., 1994), and SQL:2011 standardized both as application-time periods and system-versioned tables (Kulkarni and Michels, 2012). A system-versioned table is precisely a record layer that never destroys a past state. On the legal side, the norm-change literature gives formal accounts of abrogation, annulment, and the temporal versioning of rules (Governatori and Rotolo, 2010), and legislative-markup standards track point-in-time versions of statutes (Palmirani, 2011). The single-mutable-timeline failure described above is the mark of a system built without this prior art, not a defect of versioning itself.

What the record layer does not do is constrain the programs that compute over the records. A rule engine reading from a perfectly bitemporal store can still take a tolled deadline and write it where a frozen date belongs – as the accrual the next derivation starts from – and the store will faithfully version the corruption. The move made here is to push the distinction into the type system of the rule language: rules, not only records, are typed over time, and the ill-formed program is rejected before it runs.

The cost of the move should be stated as plainly as the benefit. Because no coercion from derived to frozen time exists, retroactive application cannot be expressed as an update to an old evaluation. A rule that reaches back – the retroactive tax amendment, the extended limitation period – is applied as a fresh derivation under the new pack over the frozen facts, alongside the original. That is a deliberate representation of legal reach-back, not its absence: the reach-back lives in the derived stratum, attributed to the rule that performed it.

Why this matters for compliance

Run the March example without stratification. The system evaluates the issuance on March 15 against the rules then in force; the evaluation passes; the transaction proceeds. On June 1 the rules change, the system re-evaluates against current rules, and the evaluation fails. A historically approved transaction now displays as non-compliant. Was the approval wrong? No – the rules changed. But the software cannot say “compliant then, non-compliant now,” because it has only one time. Its record misstates what was lawful when it occurred, and the original evaluation – evidence of lawful conduct – is gone.

Both questions are legitimate. What a transaction’s status was under the rules in force at commitment is the frozen-context question. What its status would be under current rules is the derived question. Regulators, auditors, and counterparties ask both. The defect is answering the second while destroying the means of answering the first.

With stratification the system holds both. The March evaluation under the March pack is frozen at stratum 0. The June re-evaluation under the June pack is derived at stratum 1, indexed by its pack, sitting alongside. Both are queryable, and the rule language supplies no operation that collapses one into the other. An auditor sees that the transaction was compliant when it occurred and would be non-compliant under current rules. These are different facts, and the system represents them as different facts.

Authority is a stratum-0 fact

The same discipline applies to institutional structure. Who held which authority over which period – which regulator supervised the firm, which court had the case, which officer held the delegation – is an attested historical record, and it is frozen. So is each judgment actually rendered: that a tribunal ruled on a given day is an event with a timestamp, as immutable as the share issuance. What is derived is the consequence computed from those events under a pack – the remedy deadline, the tolled period, the status that follows from the ruling.

Which authority governs a given dispute is not a frozen fact. It is a rule – a selector over the assignment record – and legal systems select differently by domain. Criminal liability generally selects by the time of the events. United States diversity jurisdiction selects by the time of filing (Grupo Dataflux v. Atlas Global Group, 541 U.S. 567 (2004)). And tribunals created after events routinely take jurisdiction over them: the International Criminal Tribunal for the former Yugoslavia was established in 1993 with jurisdiction reaching back to 1991. The new tribunal does not rewrite who held authority in 1991; it applies a new selector to the frozen record of what happened then.

Stratification is what makes every selector computable. Because the assignment record is frozen, event-time, filing-time, and decision-time selection are each well-posed queries with definite answers. A system with one mutable timeline, where the current assignment overwrites its predecessors, can answer only the decision-time question – and answers it by having destroyed the data the other two need.

Evidence is a stratum-0 fact

The frozen decision context has two coordinates, not one: the rules in force at the time of the act, and the evidence on hand at the time of the act. Everything above protects the first coordinate. The second needs the same discipline, and costs nothing structurally – every observation carries the time at which it was recorded, and that recording time is itself a frozen fact. Two strata still suffice.

The failure the second coordinate prevents is concrete. A transaction is evaluated and approved in March. In August a dispute raises the question: was this compliant when it occurred? Between March and August the record has kept accumulating – filings, attestations, counterparty disclosures, examination findings. An inquiry that retrieves from the whole corpus answers the March question with August knowledge, knowledge the March actor could not have had. Nothing about the failure depends on who or what does the reasoning: a compliance officer handed the current file makes the same error, and so does any machine whose retrieval is unbounded.

Two retrospective questions must be kept apart, because they pin different coordinates. Whether the act was lawful under the rules then in force, on the facts as now known, pins the rules and leaves the evidence open: fraud discovered in August makes the March act unlawful then – later evidence reveals the past; it does not revise it. Whether the determination was sound on the record then before the decision-maker pins both coordinates: this is the hindsight-excluded question of due diligence and reasonable reliance, answerable only against the evidence available at the time. A system with one timeline blends the two silently. The as-of bound is what makes them separately askable.

The restriction is structural, not procedural. A retrospective query names its reference point, and retrieval answers only from records whose own recording time is at or before that point – a property of the query interface, a precondition on data access, not a demand on the querier’s diligence. This is the valid-time and transaction-time separation of the database literature, met again one level up: recording time is the second coordinate of the non-retroactivity invariant itself. For the hindsight-excluded question – was the determination sound on the record then before the decision-maker – judging it on evidence recorded after the act is the same error as judging it under rules enacted after the act.

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.

The pattern is not unique to law. Accounting keeps historical cost distinct from fair-value adjustment; science keeps the observation distinct from its reinterpretation under a new theory; version control keeps the commit immutable while branch pointers move. What distinguishes institutional computing is the cost of failure. Elsewhere, confusing the strata produces a bug. Here it produces records that misstate what was lawful when it occurred, and it erases the evidence by which anyone could tell – the two injuries a system of record exists to prevent.

Two sorts of time, a one-way coercion between them, and derived consequences indexed by the rules that produced them: that is what the invariant asks of a rule language. A system that computes over institutional rules without it will confuse the past with the present, and fail the commitments it was built to keep.

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.