Documentation

Lean 4 Proof

theorem bridge_in_two_worlds {J : ℕ} {ρ : ℝ} (hρ : ρ ≠ 0)
    {c : ℝ} (hc : c ≠ 0) (hJ : (↑J : ℝ) ≠ 0) :
    -- The bridge theorem: same curvature, two observation speeds
    -hessLogFEigenvalue J ρ c =
    bridgeRatio ρ * escortFisherEigenvalue J ρ c :=
  bridge_theorem hρ hc hJ

Dependency Graph

Location

thesis/CESProofs/Dynamics/TemporalOrdering.lean:269

Module Section

Temporal Ordering Rules from Two-World Timescale Separation

In the same file