Documentation

Lean 4 Proof

theorem correlation_leads_volatility
    {ρ : ℝ} (hρ : ρ < 1) (hρne : ρ ≠ 0) :
    -- The escort Fisher eigenvalue (fast-world curvature) and the
    -- log-Hessian eigenvalue (slow-world curvature) are linked by
    -- the bridge ratio. Changes in fast-world curvature propagate
    -- to slow-world adjustment via this bridge.
    -- Statement: bridge ratio is positive when rho < 1 (complement regime),
    -- ensuring the information cascade direction is well-defined.
    0 < bridgeRatio ρ := by
  simp only [bridgeRatio]
  apply div_pos
  · linarith
  · exact sq_pos_of_ne_zero hρne

Dependency Graph

Location

thesis/CESProofs/Dynamics/TemporalOrdering.lean:73

Module Section

Temporal Ordering Rules from Two-World Timescale Separation

In the same file