Foundation Ledger Field Commit At Self

The local write

A ledger, in the Recognition Science framework, is a discrete record of events that only ever grows. The framework models a spatial field of such ledgers: each point, or voxel, carries its own append-only history. The declaration commitAt_self is a small but load-bearing theorem about this field structure. It states that when a new entry is committed at a specific voxel, the value at that voxel after the commit is exactly the result of appending the entry to that voxel's previous history.

This is a statement of locality. The theorem guarantees that a write at one voxel does not edit any other voxel. A companion theorem, commitAt_local, makes this explicit: for any voxel w different from the written voxel v, the field at w is unchanged. Together, these theorems establish that the act of recording an event at one location has no effect, no side effect, on the record at any other location. The framework's library of machine-checked theorems proves this as a formal result, not as a convention.

The theorem also underpins the immutability of the past. Because a commit at v only appends to the list at v, the previous entries at that voxel remain readable at their old indices. The past is not rewritten; it is extended. This is the property the framework calls an addressable past: after a new commit, every previously committed index at the written voxel still reads the same value.

The theorem does not claim that the field's voxels correspond to physical points in space, nor that the entries are physical events. Those identifications are modeling choices, argued in a companion paper, not formal results. The theorem operates purely on the abstract structure: a function from a voxel type to a list of entries. What it establishes is internal consistency: the field-level commit behaves exactly as the single-voxel commit does, and nothing more.

/-- The value of the field at the written voxel after a commit is the single-voxel commit. -/
theorem commitAt_self (F : LedgerField V E) (v : V) (e : E) :
    commitAt F v e v = commit (F v) e := by
  unfold commitAt
  rw [Function.update_self]

/-- **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]

/-- **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

What this page does not claim

The theorem does not identify voxels with physical points in space. The theorem does not say that recognition entries are physical events. The theorem does not prove that a commit at one voxel affects any other voxel.

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: