time
plain-language theorem explainer
Every ledger state is assigned a discrete time stamp equal to zero. The map is a pure placeholder on the RecognitionOperator ledger type (an eight-tick signal), not a dynamical clock. Downstream Noether and Hamiltonian code cite it as the time coordinate of a state; the body is the constant zero function, so no evolution is encoded yet.
Claim. Define a time coordinate on ledger states by $t(s) := 0$ for every ledger state $s$. Here a ledger state is an eight-component recognition signal (the local `Signal8` type).
background
In the RecognitionOperator module, the working state type is LedgerState, an abbreviation for an eight-tick signal. That choice matches the forced eight-tick octave (period $2^3$) from the foundation chain. Sibling fields on the same namespace (global phase, active bonds, bond multipliers, Z-patterns) describe the instantaneous configuration; time is the remaining coordinate that should index successive ticks.
Other modules carry richer ledger notions: variational dynamics pairs a configuration with an explicit tick counter; information-as-ledger stores a list of recognition events; the thermodynamic ledger tracks active bonds and positive multipliers. The present definition is the thin Foundation stand-in: a total function from that signal type into $\mathbb{N}$.
No dynamics are imposed here. The constant value simply occupies the API slot so that action, Noether, and chemistry modules can mention "the time of a state" without depending on a full evolution operator yet.
proof idea
There is no proof. The declaration is a one-line definition: ignore the state argument and return the natural number $0$. No lemmas are applied.
why it matters
The definition supplies the time coordinate used across the Action layer. Downstream, total energy is written $E(t)=H(\gamma(t),p(t))$; time-translation invariance is the statement that a J-action is unchanged under $\gamma\mapsto\gamma(\cdot+dt)$; the associated one-parameter flow and the concrete Noether status string (energy conservation for time-independent potentials) all thread through this slot. Glass-transition material also reads relaxation time off ledger states via the same accessor.
In the broader RS picture this is scaffolding for the discrete tick that the eight-tick octave and the recognition operator are supposed to advance. Until a non-constant clock (or an evolution that increments tick) replaces the zero body, energy conservation and time-translation arguments remain formal in the continuous RealAction setting and only nominally attached to Foundation ledger states.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.