Pith. sign in
module module moderate

IndisputableMonolith.Foundation.ArrowOfTime

show as:
view Lean formalization →

The ArrowOfTime module defines temporal directionality in Recognition Science through sequences of R-hat steps that accumulate Berry phase. Researchers modeling entropy increase or the forcing chain would cite these objects when establishing an arrow of time. It is a definition-only module with no proofs.

claimThe central object is TemporalSequence, a sequence of R-hat steps $(s_n)$ equipped with accumulated Berry phase $B_n = \sum_{k=1}^n b_k$ at each step $n$.

background

The module IndisputableMonolith.Foundation.ArrowOfTime imports only Mathlib and sits in the Foundation domain. It introduces the arrow of time via definitions including TemporalSequence (the sequence of R-hat steps with Berry accumulation), zAtStep, entropyFromZ, isBefore, before_transitive, before_irrefl, before_asymm, and entropy_monotone. The local theoretical setting is the directed accumulation of Berry phase along recognition steps to produce a temporal ordering and monotonic entropy.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The module supplies the core objects for temporal asymmetry that feed parent results on entropy monotonicity and the forcing chain (T0-T8). It fills the foundational layer for the arrow of time referenced in the Recognition Science framework.

scope and limits

declarations in this module (12)