Process-level ↔ path-law bridges for exchangeability

This file connects the process-level FullyExchangeable/Exchangeable predicates with the path-space ExchangeableLaw predicate: a process is fully exchangeable exactly when its pathLaw is an exchangeable path-space law, and (under a finite base law) finite exchangeability is the same statement. It also connects process-level contractability with the path-space ContractableLaw predicate.

Contractable.coordinate_pathLaw packages the form path-space arguments use: contractability transferred to the coordinate process under pathLaw μ X, so an argument may be run on path space and its conclusion carried back. It needs no finiteness hypothesis: contractability is a family of finite-dimensional map equalities.

The bridges realize the Layer 0 roadmap item asking for process-level ↔ path-law bridges in both directions. They reuse the existing FullyExchangeable path-law bridge from FullyExchangeable.lean and the contractability bridge from Contractability.lean; no measure-theoretic infrastructure is vendored.

theorem TauCeti.Probability.FullyExchangeable.exchangeableLaw_pathLaw {Ω : Type u_1} {α : Type u_2} [MeasurableSpace Ω] [MeasurableSpace α] {μ : MeasureTheory.Measure Ω} {X : ℕ → Ω → α} (hX : FullyExchangeable μ X) (hX_meas : ∀ (i : ℕ), AEMeasurable (X i) μ) : ExchangeableLaw (pathLaw μ X)

A fully exchangeable process has an exchangeable path law.

theorem TauCeti.Probability.fullyExchangeable_iff_exchangeableLaw_pathLaw {Ω : Type u_1} {α : Type u_2} [MeasurableSpace Ω] [MeasurableSpace α] (μ : MeasureTheory.Measure Ω) {X : ℕ → Ω → α} (hX_meas : ∀ (i : ℕ), AEMeasurable (X i) μ) : FullyExchangeable μ X ↔ ExchangeableLaw (pathLaw μ X)

A process is fully exchangeable iff its path law is an exchangeable path-space measure.

theorem TauCeti.Probability.exchangeable_iff_exchangeableLaw_pathLaw {Ω : Type u_1} {α : Type u_2} [MeasurableSpace Ω] [MeasurableSpace α] {μ : MeasureTheory.Measure Ω} {X : ℕ → Ω → α} [MeasureTheory.IsFiniteMeasure μ] (hX_meas : ∀ (i : ℕ), AEMeasurable (X i) μ) : Exchangeable μ X ↔ ExchangeableLaw (pathLaw μ X)

For finite laws, finite exchangeability of a process is equivalent to exchangeability of its path law.

theorem TauCeti.Probability.fullyExchangeable_of_exchangeableLaw_pathLaw {Ω : Type u_1} {α : Type u_2} [MeasurableSpace Ω] [MeasurableSpace α] {μ : MeasureTheory.Measure Ω} {X : ℕ → Ω → α} (hX_meas : ∀ (i : ℕ), AEMeasurable (X i) μ) (hρ : ExchangeableLaw (pathLaw μ X)) : FullyExchangeable μ X

A process whose path law is exchangeable is fully exchangeable.

theorem TauCeti.Probability.exchangeable_of_exchangeableLaw_pathLaw {Ω : Type u_1} {α : Type u_2} [MeasurableSpace Ω] [MeasurableSpace α] {μ : MeasureTheory.Measure Ω} {X : ℕ → Ω → α} [MeasureTheory.IsFiniteMeasure μ] (hX_meas : ∀ (i : ℕ), AEMeasurable (X i) μ) (hρ : ExchangeableLaw (pathLaw μ X)) : Exchangeable μ X

A process whose path law is exchangeable is finitely exchangeable under a finite base law.

theorem TauCeti.Probability.Contractable.contractableLaw_pathLaw {Ω : Type u_1} {α : Type u_2} [MeasurableSpace Ω] [MeasurableSpace α] {μ : MeasureTheory.Measure Ω} {X : ℕ → Ω → α} [MeasureTheory.IsFiniteMeasure μ] (hX : Contractable μ X) (hX_meas : ∀ (i : ℕ), AEMeasurable (X i) μ) : ContractableLaw (pathLaw μ X)

A contractable process has a contractable path law.

theorem TauCeti.Probability.contractable_iff_contractableLaw_pathLaw {Ω : Type u_1} {α : Type u_2} [MeasurableSpace Ω] [MeasurableSpace α] {μ : MeasureTheory.Measure Ω} {X : ℕ → Ω → α} [MeasureTheory.IsFiniteMeasure μ] (hX_meas : ∀ (i : ℕ), AEMeasurable (X i) μ) : Contractable μ X ↔ ContractableLaw (pathLaw μ X)

Contractability of a process is equivalent to contractability of its path law.

theorem TauCeti.Probability.contractable_of_contractableLaw_pathLaw {Ω : Type u_1} {α : Type u_2} [MeasurableSpace Ω] [MeasurableSpace α] {μ : MeasureTheory.Measure Ω} {X : ℕ → Ω → α} [MeasureTheory.IsFiniteMeasure μ] (hX_meas : ∀ (i : ℕ), AEMeasurable (X i) μ) (hρ : ContractableLaw (pathLaw μ X)) : Contractable μ X

If a process has a contractable path law, then the process is contractable.

theorem TauCeti.Probability.Contractable.coordinate_pathLaw {Ω : Type u_1} {α : Type u_2} [MeasurableSpace Ω] [MeasurableSpace α] {μ : MeasureTheory.Measure Ω} {X : ℕ → Ω → α} (hX : Contractable μ X) (hX_meas : ∀ (i : ℕ), AEMeasurable (X i) μ) : Contractable (pathLaw μ X) fun (j : ℕ) (p : ℕ → α) => p j

The coordinate process under a contractable process's path law is contractable. This is the form path-space arguments need: transfer the hypothesis to pathLaw μ X, work there — path space being standard Borel whenever the state space is — and carry the conclusion back.