arrow_of_time
plain-language theorem explainer
The theorem asserts that time has dimension one, the recognition period is eight ticks, and the natural numbers increase strictly. It would be cited by anyone deriving the thermodynamic arrow from J-cost minimization in the T0-T8 chain. The proof is a term-mode construction that applies reflexivity to the two equalities and the successor lemma to the inequality.
Claim. The temporal dimension equals one, the forced recognition period equals eight ticks, and every natural number $t$ satisfies $t < t + 1$.
background
Module SpacetimeEmergence derives the full Lorentzian metric signature from the J-cost functional and the T0-T8 forcing chain. The arrow of time appears as SE-009 inside that derivation. Upstream, eight_tick is defined as the constant 8 (DimensionForcing.eight_tick), while the TimeEmergence module supplies the defect-based definition: arrow_of_time(s1,s2) holds when s1 precedes s2 and defect decreases.
proof idea
The term proof uses rfl on the two equalities temporal_dim = 1 and eight_tick = 8. The universal quantifier is witnessed by the lambda that applies Nat.lt_succ_of_le le_rfl to any natural number.
why it matters
The result supplies the basic arithmetic facts required by arrow_of_time and arrow_well_defined in TimeEmergence. It closes the T7 eight-tick octave step inside the spacetime emergence chain (RCL to J-uniqueness to eight-tick to D=3). No open scaffolding remains at this node.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.