temporal_dim
plain-language theorem explainer
temporal_dim assigns the temporal dimension count to exactly one, matching the octave advance in the recognition cycle. Researchers deriving Lorentzian geometry from J-cost minimization reference it to fix the metric signature. The definition is a direct constant assignment aligned with T7 of the unified forcing chain.
Claim. The number of temporal dimensions is defined to be $1$.
background
The module derives 4D Lorentzian spacetime from the J-cost functional and forcing chain T0–T8. J(x) = (x + x^{-1})/2 - 1 is strictly convex with minimum at x=1; the eight-tick operator R̂ decreases cost along the temporal direction while spatial directions carry positive curvature from J''(1)=1. The local setting states that spacetime is a theorem of cost minimization, not a background postulate, with c=1 as a tautology and η = diag(−1,+1,+1,+1). Upstream structures supply the J-cost calibration and 8-tick local dynamics that underwrite the octave advance.
proof idea
Direct constant definition assigning the value 1, consistent with the eight-tick octave (T7) stated in the module documentation.
why it matters
This definition supplies the temporal component for the spacetime dimension count and feeds directly into lorentzian_signature (which equates negative eigenvalues to temporal_dim) and arrow_of_time (which pairs temporal_dim=1 with the monotonic advance). It completes the central derivation of η from RCL → T5 (J uniqueness) → T7 (eight-tick) + T8 (D=3 spatial), yielding the light cone and proper time without free parameters. It touches the open question of whether the octave advance can be relaxed while preserving the arrow of time.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.