# Causal Horizons and Why-Not

> **Status:** architectural plan. Cursor parentage, leased dataspaces, checkpoints, effects, and receipts exist in experimental form. Horizon-indexed logic and why-not explanations do not yet.

A Cursors world does not have one authoritative wall-clock “now.” It has evidence accumulated along partially ordered execution histories, live leases observed by particular bodies, and local projections chosen by a Self or curve.

A **causal horizon** is a named frontier of that evidence.

It is not:

- a synchronized clock;
- global consensus;
- the newest fact in the universe;
- proof that every predecessor is still materially available;
- a promise that every observer has the same view.

It is the smallest explicit answer to:

> “From this curve, using these accepted roots and this frontier of cursor heads, which facts and derivations are in scope?”

## Horizon shape

A scalar sequence number is insufficient because two cursor branches may be concurrent. A horizon is therefore a finite set or antichain of cursor heads plus a curve and evidence policy:

```text
causal_horizon H
  curve: family-room
  heads:
    cursor:cedar/91
    cursor:mirror/44
  accepted roots:
    self:local
    invitation:family-room/v3
  evidence policy:
    verified cursor ancestry
    live leased assertions observed by this body
    receipts accepted under named effect domains
```

The durable snapshot contains the accepted ancestor closure of the heads. Live assertions, material availability, routes, leases, and policy observations should be projected alongside that durable closure rather than silently folded into it.

## Suggested SQLite projection

```sql
CREATE TABLE causal_horizons (
  horizon_id TEXT PRIMARY KEY,
  curve_id TEXT NOT NULL,
  generation INTEGER NOT NULL,
  observed_at INTEGER,
  evidence_policy_root BLOB NOT NULL,
  status TEXT NOT NULL
);

CREATE TABLE causal_horizon_heads (
  horizon_id TEXT NOT NULL,
  cursor_id TEXT NOT NULL,
  PRIMARY KEY (horizon_id, cursor_id)
);

CREATE TABLE cursor_parent_edges (
  child_cursor TEXT NOT NULL,
  parent_cursor TEXT NOT NULL,
  PRIMARY KEY (child_cursor, parent_cursor)
);

CREATE TABLE horizon_evidence (
  horizon_id TEXT NOT NULL,
  evidence_id TEXT NOT NULL,
  evidence_class TEXT NOT NULL,
  subject_id TEXT NOT NULL,
  observed_by TEXT,
  lease_until INTEGER,
  PRIMARY KEY (horizon_id, evidence_id)
);
```

The ancestor closure may be materialized for hot horizons, computed through recursive SQL for bounded work, or maintained incrementally. The canonical cursor records remain the authority for ancestry; SQLite projections are rebuildable.

## Dedalus: time and location as logic

Dedalus is a Datalog-like language for distributed systems that makes time explicit. Its rules are commonly explained in three groups:

1. **Deductive rules:** derive facts at the same logical time.
2. **Inductive rules:** persist or produce facts at the next logical time.
3. **Asynchronous rules:** send facts to another location for delivery at some later logical time.

Cursors should borrow this division without copying a single global integer clock.

### Deductive: within one selected horizon

```prolog
candidate_resume(Cursor, Body, H) :-
  checkpoint(Cursor, State, H),
  body_available(Body, H),
  supports(Body, State, H).
```

No cursor advances merely because this relation was derived.

### Inductive: a successor cursor or local generation

```prolog
still_interested(Facet, Pattern, H1) :-
  interest(Facet, Pattern, Lease, H0),
  successor_horizon(H0, H1),
  lease_live(Lease, H1).
```

Persistence is explicit. Leases do not become timeless facts.

### Asynchronous: an envelope separates send from receive

```prolog
envelope_offer(Message, Destination, Hsend) :-
  outbox_intent(Message, Destination, Hsend).

mailbox_admitted(Message, Destination, Hrecv) :-
  envelope_offer(Message, Destination, Hsend),
  admitted_delivery(Message, Destination, Hsend, Hrecv).
```

The send horizon and admitted receive horizon remain visible. Transport delivery is not execution, and either event may be absent from one observer’s horizon.

## One horizon, several projections

The useful model is one durable causal frontier with typed projections:

```text
                     causal horizon H
                            |
          +-----------------+------------------+
          |                 |                  |
          v                 v                  v
   cursor ancestry    authority policy    effect receipts
          |                 |                  |
          v                 v                  v
  material availability   live leases     routes/carriers
```

These views answer different questions:

- **Ancestry:** Which cursor records are accepted predecessors?
- **Authority:** Which trust roots, grants, caveats, and presentations are accepted for this decision?
- **Availability:** Which referenced bytes are currently resolvable, from where, and with what integrity evidence?
- **Live coordination:** Which assertions and interests have unexpired observed leases?
- **Effects:** Which intents, submissions, observations, and receipts are accepted?
- **Transport:** Which carriers were observed, and what did those observations prove?

Do not produce one “complete” gauge by averaging unrelated evidence classes. A fully verified cursor whose checkpoint bytes are unavailable is causally known but not presently resumable.

## Causal cone

Selecting a cursor, effect, assertion, capability, route, or derived logic fact should expose a cone with three regions.

### Upstream

- cursor parents and state roots;
- messages, assertions, or interests that enabled the continuation;
- grants and caveats required for authorization;
- storage and resolution evidence;
- earlier receipts used for duplicate suppression.

### Lateral

- events that may be concurrent;
- other eligible bodies;
- alternative carriers or stores;
- alternative derivations;
- conflicting signed claims;
- branches excluded by the selected curve.

### Downstream

- successor cursors;
- derived assertions;
- outgoing envelopes;
- effect intents, submissions, and receipts;
- replicated material;
- later joins, compensations, revocations, and tombstones.

Every edge needs an evidence class:

| Edge class | Claim |
|---|---|
| `required-cause` | This derivation or transition requires the predecessor under the selected model. |
| `observed-predecessor` | The event is linked and earlier, but necessity was not established. |
| `possible-concurrency` | Neither side is known to precede the other. |
| `alternative-proof` | Another derivation establishes the same result. |
| `correlation` | The events are nearby in time or topology only. |
| `counterfactual-dependency` | A recorded simulation changed the result when this input was removed. |
| `unknown` | Evidence is missing or the observation boundary cannot decide. |

## Why did this happen?

A why query starts from an observed or derived subject and follows accepted derivation and transition edges upstream.

```text
WHY DID MIRROR RESUME CURSOR 83?

successor cursor 84
  because execution receipt r84 was admitted
  because Mirror held execution lease l12
  because capability presentation p7 allowed resume
  because checkpoint state-a91 was hash-verified locally
  because cursor 83 named continuation profile v0
  because parents 77 and 81 were accepted in horizon H
```

This should be a navigable proof graph. A natural-language summary may be generated from that graph, but it must not replace the evidence.

## Why did this not happen?

A why-not query needs four inputs:

1. the expected goal;
2. the selected causal horizon;
3. the curve and authority policy;
4. a completeness policy for every relation whose absence matters.

Example:

```text
WHY DID CURSOR 83 NOT RESUME ON EMBER?

established:
  checkpoint(cursor-83, state-a91)
  supports(Ember, continuation-v0)

failed:
  body lease expired at Ember-local generation 190
  execution capability presentation targeted Mirror, not Ember

unknown:
  no complete remote availability view exists for Ember at H

conclusion:
  resume was not authorized at this horizon;
  remote material availability remains unknown
```

The engine must distinguish:

- **failed prerequisite:** a known condition evaluated false;
- **missing closed-world fact:** the relation is complete for this horizon and contains no match;
- **expired evidence:** a lease or policy record is no longer live;
- **excluded evidence:** the curve or trust policy intentionally hides or rejects it;
- **unavailable material:** a referenced object is known but cannot currently be resolved;
- **open-world unknown:** absence cannot establish falsity;
- **budget/cancellation:** the explanation search did not finish.

## Relation completeness policies

Every relation used under negation needs an explicit policy:

| Policy | Meaning |
|---|---|
| `open` | Missing means “not established here.” |
| `closed-at-horizon` | The relation is complete for this bounded snapshot. |
| `leased-live` | The body has a complete local view of currently live leases it admitted. |
| `derived-closed` | A terminating bounded program derived the complete relation. |
| `authority-closed` | The named accepted roots and policy records form the complete authority set for this decision. |

Negation should be stratified and admitted only over a relation that is closed under one of these policies. Otherwise `not p(x)` is represented as an unresolved anti-goal, not a fact.

## Counterfactual worlds

A counterfactual is a separate experimental horizon derived from a real snapshot plus explicit interventions:

```text
canonical horizon H
      |
      +-- simulated horizon H'
            remove body_available(Mirror)
            expire grant g7
            delay receipt r84
            partition local-store
```

The simulation may answer:

- Which successors disappear?
- Which carrier plan is selected instead?
- Does a duplicate effect become possible?
- Which invariant fails first?
- Which facts remain derivable through alternatives?

A simulated edge must never be styled as observed history. Model-checker counterexamples, Oddity-like execution branches, and operator-created experiments can all use this same representation.

## Cockpit lens

The horizon lens should expose:

```text
HORIZON
  heads / curve / roots / generation

CAUSAL CONE
  upstream / concurrent / downstream

WHY
  selected derivation and alternatives

WHY NOT
  failed, missing, expired, excluded, unavailable, unknown

COUNTERFACTUAL
  interventions and changed consequences
```

Clicking any proof step focuses the actual cursor, grant, assertion, body, store, message, or receipt. Returning to the guide should preserve the exact heading and selected horizon.

## Smallest executable experiment

Use the SQLite + Lua watch-party demo:

1. Create a horizon before a playback assertion.
2. Show that the waiting continuation is not resumable and explain the absent matching assertion as `leased-live` within the local body.
3. Commit a matching leased assertion.
4. Create a successor horizon and show the derivation that wakes the continuation.
5. Expire the assertion and create another horizon.
6. Show that the old durable cursor ancestry remains while the live coordination fact disappears.
7. Add a simulated partition and show a distinct counterfactual branch.

## Acceptance criteria

- [ ] Horizons can contain several concurrent heads.
- [ ] Durable cursor ancestry, live leases, availability, authority, transport, and receipts remain separate projections.
- [ ] Every why answer links to concrete evidence IDs.
- [ ] Every why-not answer names its horizon and completeness assumptions.
- [ ] Open-world absence is never reported as global falsity.
- [ ] Counterfactual and model traces are unmistakably separate from observed history.
- [ ] A body can rebuild horizon projections from canonical cursor records plus accepted observations.
- [ ] Queries are bounded by heads, ancestry depth, rows, proof alternatives, and wall time.

## Research lineage

- [Dedalus: Datalog in Time and Space](https://www2.eecs.berkeley.edu/Pubs/TechRpts/2009/EECS-2009-173.html)
- [The CALM principle](https://arxiv.org/abs/1901.01930)
- [ShiViz](https://homes.cs.washington.edu/~mernst/pubs/shivector-shiviz-icse2014-abstract.html)
- [Whyline](https://doi.org/10.1145/1368088.1368130)
- [Causeway](https://research.google/pubs/causeway-a-message-oriented-distributed-debugger/)
- [Oddity](https://www.usenix.org/conference/nsdi19/presentation/woos)
- [Pivot Tracing](https://www.usenix.org/conference/sosp15/technical-sessions/presentation/mace)
- [Provenance Semirings](https://doi.org/10.1145/1265530.1265535)

## Related guides

- [Cursor Logic](cursor-logic.md)
- [Cursor Records](crypto-cursors.md)
- [Curved Dataspace](dataspace.md)
- [Capabilities](capabilities.md)
- [SQLite + Lua Cursor Machine](sqlite-lua-cursor-machine.md)
- [Cryptofabric Plans and Egglog](cryptofabric-plans-and-egglog.md)