Foundation Ledger Field Cone

The ledger field cone

A ledger is a discrete record of events, one entry per step. A field here is a collection of such ledgers, one at each point of a space, like a weather map where every grid cell keeps its own log. The cone at a point is the set of all possible future continuations from the current state, the branching tree of what could happen next.

Two facts hold for any such field. First, the present frontier is always empty: reading the entry at the current write-head, the next unwritten position, returns no value. The ledger is address-complete, every committed index is readable, but content-empty at the frontier, there is no committed value to retrieve. So no information can be pulled from the future; the hub supplies addressing, a field supplies content, and the two never mix.

Second, the cone never shrinks. If you count the admissible continuations over a finite set of points, that count is nondecreasing as the horizon extends. The future widens, it never contracts. The proof is a direct lifting of the single-ledger result to the field: the total over voxels inherits monotonicity from each voxel's own cone.

In Recognition Science, these are theorems in the machine-checked library, not assumptions. The identification of the abstract voxels and entries with physical space and events is a modeling choice, but the two structural facts themselves are proved from the definitions. The module packs them into a single certificate, FieldTimeCert, which states both properties together.

What this changes: any framework that uses ledgers as its substrate gets a guarantee about time. The future is open, never closed, and the present is always a boundary, never a fixed content. That is the structural basis for why the framework treats time as an expanding possibility space rather than a pre-written script.

/-- **Hub content-emptiness.** Reading a voxel at its own present write-head index returns
`none`: the frontier is unwritten. The hub is address-complete (every committed index is
readable) but content-empty at the present (no committed value to retrieve from the
future). -/
theorem hub_content_empty (F : LedgerField V E) (v : V) :
    (F v)[writeHeadAt F v]? = none := by
  unfold writeHeadAt writeHead
  exact List.getElem?_eq_none (le_refl _)

/-- **Field-level widening cone.** The total admissible-continuation count over a finite
voxel set is nondecreasing under one cone step at every voxel: the field future cone never
shrinks. -/
theorem fieldCone_card_monotone (next : E → Finset E) [DecidableEq E]
    (S : V → Finset E) (vs : Finset V) :
    fieldConeCard next S vs ≤ fieldConeCard next (fun v => coneStep next (S v)) vs := by
  unfold fieldConeCard
  apply Finset.sum_le_sum
  intro v _
  exact cone_card_monotone next (S v)

theorem fieldTimeCert : FieldTimeCert where
  content_empty := fun F v => hub_content_empty F v
  cone_widens := by
    intro V E _ next _ S vs
    exact fieldCone_card_monotone next S vs

What this page does not claim

The identification of V and E with physical voxels and recognition entries is a model, not a theorem. The cone widening does not imply that every continuation is physically realized. No claim is made about the rate at which the cone widens, only that it never shrinks.

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