Pith. sign in
module module moderate

IndisputableMonolith.Foundation.LedgerTime

show as:
view Lean formalization →

Append-only recognition time for a single carrier: a ledger is a list of entries, and time advances only by committing new heads. Past prefixes are immutable and addressable; causal cones grow monotonically in cardinality. Downstream field-level ledgers import this single-voxel core. The module is mostly definitions plus short monotonicity and immutability lemmas.

claimA single-carrier recognition ledger is an append-only list $L$ of entries. Committing appends a new head; the write-head index strictly advances. Every past prefix is immutable and addressable. The causal cone after each step contains the previous cone, and cone cardinality is monotone nondecreasing.

background

Recognition time is not a real parameter; it is the discrete record of commits on a carrier. This module treats one carrier as a List E: each commit appends an entry, never rewriting earlier cells. The write-head is the current length (or tip index); advancing it is the only allowed time step.

Immutability of the past means that once a prefix is written, later commits leave that prefix unchanged. Addressability means any earlier index remains a valid lookup into that frozen prefix. Causal structure is packaged as a cone: the set of ledger addresses (or entries) in the past light-cone of the current head. Cone growth and cardinality monotonicity are the discrete stand-ins for causal order and nondecreasing information.

The local setting is Foundation: single-voxel ledger time before multi-voxel fields. Downstream LedgerField assigns one such ledger to each spatial voxel.

proof idea

Definition-heavy module. Core operations (commit, writeHead) are list append and length. Immutability and addressability of the past are immediate from list-prefix lemmas: appending does not alter earlier indices. Write-head advance is length increase by one. Cone step includes the prior cone by construction; cone growth and cardinality monotonicity follow from set inclusion and finite-cardinality monotonicity on the growing address set. No deep analytic argument; list and finset facts close the lemmas.

why it matters in Recognition Science

Single-carrier append-only time is the primitive that multi-voxel recognition fields reuse. Foundation.LedgerField imports this module and lifts the same theorems to an assignment of independent ledgers over a spatial index $V$, so field-scale time-addressing inherits past immutability, head advance, and monotone cones voxelwise.

In the broader Recognition chain, discrete ledger time supports the eight-tick octave and causal bookkeeping without continuum clocks: commits are the ticks; cones encode what a carrier may still depend on. Parent use is structural (module import into LedgerField), not a single named theorem, but every field-level append-only claim rests on this single-list core.

scope and limits

used by (1)

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

declarations in this module (8)