feat(Order/Causal): add Causal ordering for stream functions

Mathlib.lean

@@ -5747,6 +5747,8 @@ public import Mathlib.Order.Category.PartOrd
 public import Mathlib.Order.Category.PartOrdEmb
 public import Mathlib.Order.Category.Preord
 public import Mathlib.Order.Category.Semilat
+public import Mathlib.Order.Causal.Basic
+public import Mathlib.Order.Causal.Defs
 public import Mathlib.Order.Circular
 public import Mathlib.Order.Circular.ZMod
 public import Mathlib.Order.Closure

Mathlib/Order/Causal/Basic.lean

@@ -0,0 +1,30 @@
+/-
+Copyright (c) 2026 Matt Hunzinger. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Matt Hunzinger
+-/
+module
+
+public import Mathlib.Order.Causal.Defs
+
+/-!
+# Causal stream functions
+-/
+
+@[expose] public section
+
+universe u v
+
+variable {α : Type u} {β : Type v}
+
+namespace Stream'
+
+theorem map_causal {f : α → β} : Causal (map f) := by
+  intro x y t h
+  simpa [map] using congrArg f (h t (Nat.le_refl t))
+
+theorem enum_causal : Causal (enum (α := α)) := by
+  intro x y t h
+  simpa [enum] using congrArg (fun a => (t, a)) (h t (Nat.le_refl t))
+
+end Stream'

Mathlib/Order/Causal/Defs.lean

@@ -0,0 +1,47 @@
+/-
+Copyright (c) 2026 Matt Hunzinger. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Matt Hunzinger
+-/
+module
+
+public import Mathlib.Data.Stream.Defs
+public import Mathlib.Order.Defs.PartialOrder
+
+/-!
+# Causal stream functions
+-/
+
+@[expose] public section
+
+universe u v w
+
+variable {α : Type u} {β : Type v} {δ : Type w}
+
+/-- A stream function is causal if the output at time `t` depends only on inputs up to time `t`. -/
+def Causal (f : Stream' α → Stream' β) : Prop :=
+  ∀ (x y : Stream' α) (t : ℕ), (∀ s, s ≤ t → x s = y s) → f x t = f y t
+
+instance
+    {f : Stream' α → Stream' β}
+    [i : Decidable
+          (∀ (x y : Stream' α) (t : ℕ),
+            (∀ s, s ≤ t → x s = y s) → f x t = f y t)] :
+    Decidable (Causal f) := i
+
+theorem causal_id : Causal (id (α:=Stream' α)) := by
+  intro x y t h
+  exact h t (Nat.le_refl t)
+
+theorem causal_comp
+    {f : Stream' α → Stream' β}
+    {g : Stream' β → Stream' δ}
+    (hf : Causal f)
+    (hg : Causal g) :
+    Causal (g ∘ f) := by
+  intro x y t h
+  apply hg
+  intro s hs
+  apply hf
+  intro s' hs'
+  exact h s' (Nat.le_trans hs' hs)