Pith. sign in
module module high

IndisputableMonolith.Foundation.LedgerField

show as:
view Lean formalization →

Defines a recognition field: one independent append-only ledger per voxel, lifting single-site LedgerTime to a spatial family. Multi-site dynamics and the field-level widening cone cite it. The module packages local commit and write-head operations with immutability and addressability lemmas for the past at each site.

claimA recognition field is a map from voxels to independent append-only ledgers. At each voxel $v$, commit and write-head act only on the ledger at $v$; other sites are unchanged. The past at $v$ is immutable once written and remains addressable from the current head.

background

Upstream, LedgerTime isolates the lived arrow of time from the bare recognition tick. The tick itself is invertible and time-symmetric; asymmetry enters only with the ledger: an append-only record of committed recognition events over an entry type $E$.

This module places one such ledger at each voxel, so a recognition field is a spatial family of independent append-only histories. Local operations (commit at a site, advance the write head) never rewrite foreign voxels. The past at a site stays fixed and readable once committed.

Sibling names mark the main API: the field type itself, pointwise commit and write-head, locality and self-action of commit, past immutability and addressability, write-head advance and non-interference, plus a small certificate bundle for the field ledger laws.

proof idea

Definition-and-API module, not a single deep theorem. The field is the pointwise lift of the LedgerTime structure. Lemmas are mostly equational or by cases on voxel equality: commit and write-head act only at the chosen site; other sites are definitionally unchanged; the past remains immutable and addressable after local writes. A certificate record packages the field ledger laws for downstream use.

why it matters in Recognition Science

Feeds Foundation.LedgerFieldCone, which states two field-level facts on top of this multi-voxel ledger: hub content-emptiness (Cap3 c3_l03) and the field-level widening cone. Cone work needs independent per-voxel histories so addressing can be total while a single carrier's content at the hub stays empty. Without a field of ledgers, the panel's restatement of the time-travel claim and the widening-cone geometry have no carrier. Sits in the Foundation layer that turns abstract recognition time into spatially extended, append-only structure before cone and forcing arguments.

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)