before_transitive
Why this theorem is linked from Timer-S1: A Billion-Scale Time Series Foundation Model with Serial Scaling echoes
Pith linked this Lean declaration because the review connected a specific passage in the paper to this theorem. The relation tag says how strong that connection is; it is not a generic placeholder.
Forecasting into the long term accumulates uncertainty, as the prediction of each step depends on all preceding estimations, which positions time series forecasting as a serial problem
ECHOES: this paper passage has the same mathematical shape or conceptual pattern as the Recognition theorem, but is not a direct formal dependency.
plain-language theorem explainer
The before relation on real numbers, defined by strict inequality of Z-complexity, is transitive. Researchers modeling emergent time from Berry phase accumulation cite this to guarantee ordered temporal sequences without external thermodynamics. The proof is a one-line term that unfolds the definition and applies linear arithmetic.
Claim. If $z_1 < z_2$ and $z_2 < z_3$ then $z_1 < z_3$, where each $z_i$ is the absolute Berry phase complexity at successive snapshots.
background
The module derives the arrow of time from Berry phase monotonicity on the ledger. The relation isBefore is defined directly as $z_1 < z_2$ for real numbers $z$ that track absolute accumulated phase. Upstream, the before predicate on LedgerSnapshot compares tick indices: $a.tick.index < b.tick.index$. The module states that Z-complexity is monotonically non-decreasing, supplying an intrinsic before-after distinction.
proof idea
The term proof unfolds isBefore on the hypotheses and goal, then invokes linarith to obtain transitivity of the strict order on the reals.
why it matters
This result confirms that the Z-induced temporal order is transitive, supporting directed time in the Recognition framework. It underpins entropy_monotone and related claims in the same module. The module doc notes that forward R-hat steps accumulate phase while reversal does not decrease absolute Z, yielding the asymmetry.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.
papers checked against this theorem (showing 8 of 8)
-
Stake weights deliver pBFT in leaderless async DAG
"StakeDag protocol achieves global consistent view via layer assignment with probability one in pBFT condition"
-
Max-entropy relaxation solves multiway k-cut on graphs
"treat it as a control Lyapunov function … ˙F ≤ 0 … non-positiveness of the time derivative"
-
Causal attention lifts time-series classification to 98.6 percent
"The CTA module ... enforces autoregressive consistency (h_t = f({x_τ}_τ≤t)). ... By enforcing causality, our CTA module functions as a Structural Noise Filter. ... enforcing physical time-arrow constraints"
-
Hydrodynamics alone violates causality without extra modes
"Theorem 2 (Decay rate). ... Γ(v)>0 for all v≠cs ... monotonic in |v−cs|."
-
Serial scaling boosts time series model to top forecasting scores
"Forecasting into the long term accumulates uncertainty, as the prediction of each step depends on all preceding estimations, which positions time series forecasting as a serial problem"
-
Video models ground robot control in causal prediction
"causal attention masking over the unified sequence ensures that both predicted visual states and action commands are governed by preceding states"
-
Next-token learning selects world-tracking encodings matching training ecologies
"under explicit heredity, variation, and selection assumptions... inter-model selection pushes toward lower ecological excess loss"
-
Expanding quantum gas shows Mpemba effect in density relaxation
"the relaxation dynamics of the ground and excited symmetry sectors exhibit a clear crossing in time"