Pith. sign in
module module high

IndisputableMonolith.Foundation.LedgerField

show as:
view Lean formalization →

Defines a recognition field as a family of independent append-only ledgers, one per voxel, built on the abstract LedgerTime structure. Physicists tracking multi-site recognition events and causal cones cite this module. It packages commit and write-head operations with locality, immutability of the past, and addressability lemmas, plus a field-level certificate.

claimA recognition field assigns to each voxel an independent append-only ledger of recognition entries. At each site one has a commit map and a write-head advance; the past at a site is immutable under local writes, writes advance only the local head, and past entries remain addressable. A field-ledger certificate packages these structural facts.

background

Recognition time begins from an invertible bare tick, which is time-symmetric. Lived asymmetry (fixed readable past versus open future) enters only with the ledger: the append-only record of committed recognition events. The upstream module LedgerTime formalizes that structure abstractly over an entry type $E$.

This module lifts the single-ledger picture to a spatial field. A recognition field is an independent append-only ledger at each voxel, so multi-site recognition can be stated without sharing mutable state across locations. The sibling API centers on commit-at-site, write-head-at-site, locality of commits, self-consistency of commits, immutability of the past under local writes, head advance, non-interference at other sites, and past addressability.

The setting is Foundation: discrete recognition structure before continuum limits or dynamics are imposed.

proof idea

This is primarily a definition-and-structure module. It introduces the field type as a voxel-indexed family of ledgers, then proves elementary lemmas about commit and write-head operations: locality, self-action, past immutability, head advance, non-interference elsewhere, and past addressability. A bundled certificate packages the structural facts for downstream use. There is no deep analytic argument; the work is type design plus short algebraic or by-definition proofs over the LedgerTime primitives.

why it matters in Recognition Science

Downstream, Foundation.LedgerFieldCone imports this module to state hub content-emptiness and the field-level widening cone. That work rests on the multi-voxel ledger: the hub vantage is address-complete but content-empty for a single carrier, and the cone of widening future is a field-level fact. Without independent per-voxel append-only ledgers, those Cap3-style claims cannot even be typed.

In the broader Recognition framework this is the spatial ledger layer that turns abstract append-only time into a field on voxels, feeding causal-cone and emptiness arguments rather than continuum field equations. It sits under Foundation, upstream of cone and certificate consumers, and does not itself force $D=3$, $\varphi$, or the eight-tick octave.

scope and limits

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (11)