Foundation Ledger Field

The field ledger

A recognition field is a way of organizing time and memory across space. In the Recognition Science framework, reality keeps a ledger: a discrete record of events, one entry appended after another. A single ledger works for one location. A field extends that idea to many locations at once. Formally, a ledger field assigns to every voxel, or spatial cell, its own independent append-only list of entries. The type is simply a function from voxels to lists, written V → List E, where V is the spatial index and E is the type of recognition entries.

The central operation is a commit: writing a new entry to one voxel. The framework's library proves five properties of this operation, each a theorem in a machine-checked collection of formal proofs. First, locality: a commit at voxel v leaves every other voxel w untouched. Second, past immutability: committing at v cannot change the history that v already had; the old entries remain readable. Third, the write-head at the written voxel advances by exactly one. Fourth, the write-heads at all other voxels stay fixed. Fifth, addressability: after a new commit, every old index at the written voxel still reads the same value as before.

These properties together form a certificate, a single packaged theorem asserting that the field is append-only, local, and has an immutable addressable past. The theorems are axiom-clean: they follow from the definitions with no extra assumptions. What is not proved is that physical space is made of such voxels, or that recognition entries are the right kind of events. Those identifications are modeling choices, argued in a companion paper. The module itself establishes the mathematical structure, not the physical claim.

The consequence is a precise sense in which space can hold independent histories. A write at one voxel does not edit another, and the past at any voxel is fixed once written. This is the foundation for later results about content emptiness and widening cones, which build on this type. For a reader, the useful picture is simple: a field ledger is a grid of private timelines, and the framework proves that no timeline can rewrite another.

/-- **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 immutability.** Committing at `v` cannot alter the committed past of `v`. -/
theorem past_immutable_at (F : LedgerField V E) (v : V) (e : E) :
    (commitAt F v e v).take (F v).length = F v := by
  rw [commitAt_self]
  exact past_immutable (F v) e

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

/-- **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 identification of V with physical voxels and E with recognition entries is not proved here; it is a modeling choice.

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: