arrow_of_time
plain-language theorem explainer
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.
Claim. The 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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.