Foundation Ledger Field Past Addressable At

Addressable past

An append-only record, like a logbook whose pages are never torn out or rewritten, has a simple guarantee: once an entry is written, it stays there. The Recognition Science declaration past_addressable_at states this guarantee precisely for a ledger, a discrete record of events, when that ledger is spread across many locations. It proves that after a new entry is added at a particular location, every previously committed entry at that same location can still be read back with exactly the same value as before. In plainer terms, the past is read-only and addressable: you can point to any old entry by its position and get the same answer you would have gotten before the latest write.

The declaration is a theorem in the framework's machine-checked library of formal theorems, meaning its proof is verified by a computer and rests on no framework-specific assumptions. It is the field-level version of a single-location result: where a single ledger guarantees its own history is immutable, this theorem extends the guarantee to a field, an assignment of an independent ledger to each voxel, or point in a spatial index. The key word is independence. A commit, or write, at one voxel leaves every other voxel untouched, and the write-head, the marker of the present moment, advances by exactly one at the written voxel and nowhere else. The addressable-past theorem then follows: because the write only appends, it cannot shift or overwrite what came before.

What the declaration does not claim is just as important. It does not say that the voxels correspond to physical space or that the entries correspond to physical events. That identification is a modeling choice, argued separately in a companion paper, not a proved result. The theorem operates on an abstract type: any set of locations and any type of entry. It also does not claim that the past is meaningful in any causal or temporal sense beyond the formal structure of the ledger. It establishes a property of a data structure, not a statement about the nature of time or memory in the physical world.

The practical consequence is that the framework can build on a stable foundation: any process that reads the past can do so without fear of mutation, and any reasoning about the past can treat it as fixed. This is the keystone for later results about content-emptiness and widening cones, which assume that the past is a reliable, unchanging reference. For a reader, the takeaway is simple: in this framework, history is not rewritten, it is accumulated, and the addressable-past theorem makes that accumulation safe to use.

/-- **Field past addressability.** Every committed past index at the written voxel reads the
same value after a new commit: the field past is read-only and addressable. -/
theorem past_addressable_at (F : LedgerField V E) (v : V) (e : E) (i : ℕ)
    (hi : i < (F v).length) :
    (commitAt F v e v)[i]? = (F v)[i]? := by
  rw [commitAt_self]
  exact past_addressable (F v) e i hi

/-- **Locality.** A commit at voxel `v` leaves every other voxel `w ≠ v` exactly as it was. -/
theorem commitAt_local (F : LedgerField V E) (v : V) (e : E) (w : V) (hw : w ≠ v) :
    commitAt F v e w = F w := by
  unfold commitAt
  rw [Function.update_of_ne hw]

/-- **Write-head advance (written voxel).** The present index at `v` moves forward by one. -/
theorem writeHeadAt_advances (F : LedgerField V E) (v : V) (e : E) :
    writeHeadAt (commitAt F v e) v = writeHeadAt F v + 1 := by
  unfold writeHeadAt
  rw [commitAt_self]
  exact writeHead_advances (F v) e

/-- **Write-head unchanged (other voxels).** No other voxel's present index moves. -/
theorem writeHeadAt_other (F : LedgerField V E) (v : V) (e : E) (w : V) (hw : w ≠ v) :
    writeHeadAt (commitAt F v e) w = writeHeadAt F w := by
  unfold writeHeadAt
  rw [commitAt_local F v e w hw]

What this page does not claim

The voxels are physical points and the entries are physical events. The past has any causal or temporal meaning beyond the formal ledger structure.

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/LedgerField.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: