Pith. sign in
module module moderate

IndisputableMonolith.Foundation.LedgerFieldCone

show as:
view Lean formalization →

Module formalizing the field-level past cone of a multi-voxel append-only ledger: at each voxel the present write-head is content-empty (reads return none), while every committed past index remains address-complete. Introduces cone cardinality, its monotonicity under extension, and field-time certificates. Cited by anyone lifting single-carrier LedgerTime facts to spatial fields. Mostly definitional scaffolding plus short monotone/emptiness lemmas.

claimA recognition field assigns an independent append-only ledger to each voxel $v \in V$. The field cone at a global time is the collection of all committed entries strictly before each voxel's write-head. The hub (present write-head index) is content-empty: reading it yields $\mathsf{none}$. Cone cardinality is monotone under ledger extension, and field-time certificates package these facts for downstream use.

background

Upstream, LedgerField lifts single-carrier recognition time to a spatial index: a recognition field is an assignment of an independent append-only ledger to each voxel of $V$. Single-voxel LedgerTime already encodes that time is append-only and that the present write-head has no committed value.

This module works at field scale. The past cone collects, across voxels, every index that has already been written. Address-completeness says every committed index is readable; content-emptiness at the hub says the frontier itself still holds nothing. Cone cardinality counts those committed cells; monotonicity records that extending any voxel ledger can only enlarge the cone.

The local setting is pure foundation: discrete multi-voxel ledgers before continuum or dynamics are imposed.

proof idea

Definition-heavy module. Hub emptiness is the pointwise lift of the single-ledger fact that reading at the write-head returns none. Cone cardinality is a finite sum/card over voxels of committed prefix lengths. Monotonicity is by componentwise inclusion of prefixes under append. Field-time certificates are thin packaging structures that bundle emptiness, address-completeness, and card facts for later import; no deep new arithmetic.

why it matters in Recognition Science

Supplies the multi-voxel cone language needed before continuum or causal-structure layers can talk about "what has been recognized so far" on a spatial lattice. Feeds any downstream development that needs field-scale time certificates or monotone cone growth (none recorded yet in the local used-by graph). Sits directly on the LedgerField generalization of single-carrier LedgerTime, keeping the append-only, present-empty discipline that Recognition time demands. Does not itself touch the T0–T8 forcing chain, J-cost, or phi-ladder; it is infrastructure for later field dynamics.

scope and limits

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (5)