Foundation Ledger Time Cone Step

The cone step

A ledger is a discrete record of events, written one entry at a time and never altered in place. In Recognition Science, the framework models time itself on this pattern: the bare recognition tick, the smallest unit of awareness, is reversible, so it carries no direction. The asymmetry between a fixed past and an open future enters only with the ledger, the append-only record of committed recognition events. The declaration coneStep, one step of the admissible future cone, is the operation that takes the current frontier of possible states and adds every state reachable from it in one move under a given relation next. In plain terms, it answers: from where we are now, what could happen next, and what could happen after that, all collected together.

The operation itself is simple: coneStep next S = S ∪ S.biUnion next. It takes a set S of states, applies the successor relation next to each member, and unions the results back into S. The framework's library proves three structural facts about it, all standard results about finite sets and lists. First, the cone never shrinks: the current frontier is always contained in its successor cone (cone_grows). Second, the count of admissible states never decreases as the horizon extends (cone_card_monotone). Third, the committed past is immutable and addressable: truncating the extended ledger back to its old length returns the old ledger exactly, and every past index reads the same value after a new commit (past_immutable, past_addressable). The write-head, the present index, advances by exactly one per commit (writeHead_advances). These are the formal bones of a time that accumulates rather than erases.

What coneStep does not claim is just as important as what it proves. The identification of the abstract entry type E with actual recognition events, and of coneStep with the set of continuations admissible under the framework's cost function J, is a modeling choice argued in a companion paper, not a result in the machine-checked library. The structural lemmas are proved; the bridge from them to physical time is not. The framework also does not claim that the future is predetermined: the cone grows, but it never selects a single path. The openness of the future, in this account, is the cone's failure to shrink, not a prediction of which branch will be taken.

This matters because it gives a precise, checkable meaning to a phrase that usually stays vague. When someone says the past is fixed and the future is open, coneStep and its lemmas say exactly what that means in one formal setting: the past is a list that append-only commits cannot change, and the future is a set of states that only grows. The framework's contribution is not the intuition, which is ancient, but the discipline of stating it as a finite-set operation with proved monotonicity. That lets a reader see, in a few lines of formal code, which parts of the intuition are results and which parts are choices still awaiting their argument.

/-- **The cone never shrinks.** The frontier is contained in its successor cone.

Strategy: `unfold coneStep; exact Finset.subset_union_left`. -/
theorem cone_grows (next : E → Finset E) (S : Finset E) :
    S ⊆ coneStep next S := by
  unfold coneStep; exact Finset.subset_union_left

/-- **Admissible count nondecreasing.** The number of admissible states is
nondecreasing in horizon.

Strategy: `exact Finset.card_le_card (cone_grows next S)`. -/
theorem cone_card_monotone (next : E → Finset E) (S : Finset E) :
    S.card ≤ (coneStep next S).card := by
  exact Finset.card_le_card (cone_grows next S)

/-- **Past immutability.** Truncating the extended ledger back to the old length
returns the old ledger exactly: committing a new entry cannot alter the past.

Strategy: `unfold commit; exact List.take_left l [e]` (or
`simp [commit, List.take_left]`). -/
theorem past_immutable (l : List E) (e : E) :
    (commit l e).take l.length = l := by
  unfold commit; simp

/-- **Past addressability.** Every committed past index reads the same value after
a new commit: the past is read-only and addressable by index.

Strategy: `unfold commit; exact List.getElem?_append_left hi` (find the exact
`getElem?_append` lemma for the index-in-left-segment case via the premises). -/
theorem past_addressable (l : List E) (e : E) (i : ℕ) (hi : i < l.length) :
    (commit l e)[i]? = l[i]? := by
  unfold commit; rw [List.getElem?_append_left hi]

/-- **Write-head advance.** The present index moves forward by exactly one per
commit.

Strategy: `simp [writeHead, commit, List.length_append]`. -/
theorem writeHead_advances (l : List E) (e : E) :
    writeHead (commit l e) = writeHead l + 1 := by
  unfold writeHead commit; simp

/-- One step of the admissible future cone: the current frontier together with all
its admissible successors under `next`. -/
def coneStep (next : E → Finset E) (S : Finset E) : Finset E :=
  S ∪ S.biUnion next

What this page does not claim

The framework does not claim that coneStep selects which future branch actually occurs. The framework does not claim that the physical identification of E with recognition events is proved in the machine-checked library. The framework does not claim that the cone's growth rate is bounded or that the future is finite.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Foundation/LedgerTime.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: