pith. sign in
module module high

IndisputableMonolith.Foundation.ArrowOfTime

show as:
view Lean formalization →

The ArrowOfTime module defines temporal sequences as chains of R-hat steps that accumulate Berry phase, supplying the core objects for an intrinsic arrow of time. It introduces zAtStep, isBefore, entropyFromZ and related monotonicity lemmas. A physicist deriving time asymmetry from the Recognition Composition Law would cite these constructions. The module advances via successive definitions and elementary ordering lemmas.

claimA temporal sequence is a chain of R-hat steps $z_n$ with accumulated Berry phase $B_n = B_{n-1} + J(z_n)$, where $J$ denotes the J-cost function and the sequence satisfies the forward accumulation rule.

background

The module belongs to the Foundation domain and introduces the arrow of time directly from the Recognition Science functional equation. Central definitions are TemporalSequence for the directed chain, zAtStep for the rung value at each step, and entropyFromZ for the entropy extracted from the z sequence. Supporting lemmas establish non-negativity of z, forward accumulation, reverse subtraction, and immunity of the absolute z value to reversal. These rest on the J-uniqueness and phi fixed-point results from the upstream forcing chain.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The module supplies the base layer for parent results on entropy monotonicity and irreversibility within the Recognition framework. It fills the chain step that converts the eight-tick octave and Berry creation threshold into a directed temporal order. It touches the question of how the T7 period and D=3 dimensions produce macroscopic time asymmetry.

scope and limits

declarations in this module (12)