pith. machine review for the scientific record. sign in
def definition def or abbrev high

arrow_of_time

show as:
view Lean formalization →

Recognition Science defines the arrow of time between two ledger snapshots as the conjunction of strict temporal precedence by tick index and non-increasing defect. A physicist deriving emergent spacetime from ledger dynamics would cite this when aligning the thermodynamic arrow with discrete time steps. The definition is introduced as a direct conjunction of the before relation and the defect inequality with no auxiliary lemmas.

claimThe arrow of time holds between ledger states $s_1$ and $s_2$ when the tick index of $s_1$ is strictly smaller than that of $s_2$ and the defect of $s_2$ satisfies $d(s_2) ≤ d(s_1)$, where $d$ denotes the recognition cost functional.

background

The TimeEmergence module treats time as the discrete tick counter on the ledger rather than a continuous background parameter. A LedgerSnapshot records a tick index together with its nonnegative defect value; the before relation orders two snapshots strictly by increasing tick index. Defect itself is the J-cost functional, which vanishes at unity and is drawn from the LawOfExistence module.

proof idea

The definition is a direct conjunction of the before predicate on snapshots and the defect inequality. No lemmas or tactics are invoked; it functions as the primitive relation supplied to the subsequent well-definedness theorem.

why it matters in Recognition Science

This supplies the primitive temporal direction used in arrow_well_defined (F-006), which shows that defect monotonicity makes the thermodynamic arrow coincide with tick ordering. It registers the F-006 item on the arrow of time and feeds the SpacetimeEmergence result that temporal dimension equals one with monotonic advance, consistent with the eight-tick octave.

scope and limits

formal statement (Lean)

  87def arrow_of_time (s₁ s₂ : LedgerSnapshot) : Prop :=

proof body

Definition body.

  88  before s₁ s₂ ∧ s₂.defect ≤ s₁.defect
  89
  90/-- **Theorem (F-006)**: The arrow of time is well-defined.
  91    If defect decreases along the tick sequence, the temporal
  92    ordering and the thermodynamic arrow agree. -/

used by (2)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (19)

Lean names referenced from this declaration's body.