Pith. sign in
module module moderate

IndisputableMonolith.Foundation.LedgerTime

show as:
view Lean formalization →

Formalizes recognition time as an append-only ledger on one carrier (a list of entries). Commits only extend the record; the past is immutable and addressable; the write head advances; a causal cone grows with monotone cardinality. Cited as the single-voxel time base before field-level lifting. Structure is elementary list lemmas, not deep analysis.

claimRecognition time on a single carrier is an append-only list $L$ of entries. Commit extends $L$ by one entry; the write head advances (length strictly increases); every past prefix is immutable and addressable; the causal cone after each step grows, and cone cardinality is monotone in the number of commits.

background

In Recognition Science, time is the ordered record of recognition events, not a background continuum parameter. This module treats one carrier's history as a list of entries with strict append-only semantics: new facts are committed at the tip; nothing rewrites earlier addresses.

The write head is the current tip. Commit advances that head and freezes all prior prefixes. Causal reach is packaged as a cone that expands under commit, with cardinality nondecreasing along the commit sequence. Sibling facts cover commit, head advance, past immutability, past addressability, cone step, cone growth, and cone-card monotonicity.

The local setting is Foundation: discrete ledger time for a single List E carrier, before any spatial field structure.

proof idea

Definition-and-lemma module on lists, not a single deep theorem. Commit is append at the tip. Past immutability is prefix stability under append. Write-head advance is strict length increase. Past addressability indexes stable prefixes. Cone step and cone growth are inductive extensions of the reachable set under commit; cone cardinality monotonicity follows by induction on the commit sequence. No heavy tactics beyond standard list reasoning.

why it matters in Recognition Science

Gives the single-carrier append-only time substrate that Foundation.LedgerField imports and lifts. Downstream doc states the point directly: LedgerTime is recognition time for one list; field-scale time-addressing needs an independent append-only ledger per voxel of a spatial index, with single-voxel theorems lifted. Without this module, multi-voxel recognition fields have no time base to generalize. It sits in Foundation, under any later continuum, synchronization, or forcing-chain uses of discrete recognition time.

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)