arrow_of_time
plain-language theorem explainer
The arrow of time theorem asserts that the temporal dimension equals one, the recognition period equals eight ticks, and the natural numbers are strictly ordered. It would be cited when closing the T0-T8 forcing chain to Lorentzian signature in cost-minimization derivations. The proof is a term-mode construction that applies reflexivity twice and the successor inequality lemma.
Claim. The temporal dimension equals $1$, the eight-tick recognition period equals $8$, and for every natural number $t$, $t < t + 1$.
background
The Spacetime Emergence module derives 4D Lorentzian geometry from the J-cost functional and the T0-T8 chain. Spatial curvature follows from J''(1) = 1 while the eight-tick operator supplies the cost-reducing temporal direction, yielding signature (-,+,+,+). The eight_tick definition from DimensionForcing fixes the period at 8. The arrow_of_time definition in TimeEmergence states that time flows from higher to lower defect: before s1 s2 and s2.defect ≤ s1.defect.
proof idea
The proof is a term-mode construction. It pairs reflexivity for the two equalities with the lambda that maps any natural number to Nat.lt_succ_of_le le_rfl.
why it matters
This theorem supplies SE-009 and feeds the arrow_of_time and arrow_well_defined results in TimeEmergence. It instantiates the T7 eight-tick octave and the temporal component of the derivation chain RCL → J unique (T5) → 8-tick (T7) → D = 3 (T8). It touches the alignment between defect monotonicity and the thermodynamic arrow.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.