type: definition
verification: machine_ready
dependencies: ["D1-1-formal.md"]
verification_points:
- non_negativity
- monotonicity
- additivity
- directionality
TimeMetric(S : SelfReferentialComplete) : Prop ≡
∃τ : Function[StateSpace × StateSpace → Real⁺] .
NonNegative(τ) ∧
Monotonic(τ) ∧
Additive(τ) ∧
Directional(τ)
NonNegative(τ : Metric) : Prop ≡
∀i, j : Time . τ(Sᵢ, Sⱼ) ≥ 0 ∧
(τ(Sᵢ, Sⱼ) = 0 ⟺ i = j)
Monotonic(τ : Metric) : Prop ≡
∀i, j, k : Time . i < j < k →
τ(Sᵢ, Sⱼ) < τ(Sᵢ, Sₖ)
Additive(τ : Metric) : Prop ≡
∀i, j, k : Time . i ≤ j ≤ k →
τ(Sᵢ, Sₖ) = τ(Sᵢ, Sⱼ) + τ(Sⱼ, Sₖ)
Directional(τ : Metric) : Prop ≡
∀i, j : Time . τ(Sᵢ, Sⱼ) > 0 ⟺ i < j
τ_struct(Sᵢ, Sⱼ) : Real⁺ ≡
match (i, j) with
| i = j ⇒ 0
| i < j ⇒ Σ(k=i to j-1) ρ(Sₖ, Sₖ₊₁)
| i > j ⇒ -τ(Sⱼ, Sᵢ)
where
ρ(Sₖ, Sₖ₊₁) := √|Sₖ₊₁ \ Sₖ|
τ_info(Sᵢ, Sⱼ) : Real⁺ ≡
Σ(k=i to j-1) [H(Sₖ₊₁) - H(Sₖ)]
where
H : State → Real⁺ is entropy function
Type Time := ℕ
Type State := System × Time
Type StateSpace := Set[State]
Type Metric := StateSpace × StateSpace → Real⁺
Type Real⁺ := {r ∈ ℝ | r ≥ 0}
Discrete(τ : Metric) : Prop ≡
∃δ > 0 . ∀i ≠ j . τ(Sᵢ, Sⱼ) ≥ δ
Irreversible(S : System) : Prop ≡
∀t : Time . ¬∃φ : Sₜ₊₁ → Sₜ . Surjective(φ)
TotalTime(t : Time) : Real⁺ ≡
Σ(k=0 to t-1) τ(Sₖ, Sₖ₊₁)
def verify_non_negativity(metric, states):
return all(metric(si, sj) >= 0 for si in states for sj in states)
def verify_monotonicity(metric, states):
return all(metric(si, sj) < metric(si, sk)
for si, sj, sk in states if i < j < k)
def verify_additivity(metric, states):
return all(abs(metric(si, sk) - (metric(si, sj) + metric(sj, sk))) < ε
for si, sj, sk in states if i <= j <= k)
def verify_directionality(metric, states):
return all((metric(si, sj) > 0) == (i < j)
for si, sj in states)