IndisputableMonolith.Foundation.LedgerFieldCone
Module formalizing the field cone on a multi-voxel recognition ledger: the set of committed addresses readable at a given field time, together with hub content-emptiness (the present write-head is unwritten). Physicists tracking causal structure on the ledger field cite the card and monotonicity facts. Arguments are lifts of single-carrier append-only lemmas plus elementary finiteness and option reasoning.
claimOn a recognition field (an assignment of an append-only ledger to each voxel $v \in V$), the field cone at time $t$ is the finite set of committed addresses readable by that time. At each voxel's own present write-head the stored value is $\mathsf{none}$ (hub content-empty). Cone cardinality is monotone in $t$. A field-time certificate packages these cone facts for downstream use.
background
Upstream, LedgerField lifts single-carrier recognition time to a field: each spatial voxel carries an independent append-only ledger. Single-voxel time is a growing list of events; field time is a synchronized family of such lists indexed by $V$.
The cone construction asks which addresses are already committed when the field is observed at a global present. Address-completeness says every committed index is readable; content-emptiness at the hub says the frontier itself has no value yet (reading the present write-head returns none). That matches the append-only discipline: the next slot is reserved but unwritten.
Sibling objects in the module package cone cardinality, its monotonicity under time advance, and a small certificate type that bundles the cone facts for later theorems.
proof idea
Definition-heavy module with short supporting lemmas. Hub content-emptiness is option reasoning on the write-head index: the present slot is not yet in the committed prefix, so lookup yields none. Cone cardinality is the size of the finite set of committed field addresses at $t$; monotonicity follows because append-only growth only adds addresses. The field-time certificate is a structure packing these facts, discharged by the preceding lemmas rather than by a deep new argument.
why it matters in Recognition Science
Gives the multi-voxel causal cone that single-carrier LedgerTime cannot express. Downstream work that needs a finite, monotone "what is already written" set at field scale depends on these definitions; the empty used_by list on this page means consumers sit outside the current edge snapshot, not that the cone is idle. In the Recognition forcing picture the cone is the bookkeeping layer under discrete time (eight-tick octave, $D=3$ spatial voxels): it separates address-complete past from content-empty present without smuggling continuum light-cone structure. Hub emptiness is the precise ledger statement that the frontier carries no premature value.
scope and limits
- Does not derive continuum Lorentzian light cones or metric causality.
- Does not fix the spatial index $V$ or prove $D=3$; that lives in the forcing chain.
- Does not construct dynamics or mass formulae; only cone bookkeeping on ledgers.
- Does not assert content at past addresses beyond readability of committed indices.
- Does not discharge global consistency across voxels beyond the packaged certificate.