Documentation

Lean 4 Proof

theorem detection_asymmetry_bridge (J : ℕ) [NeZero J] (hJ : 0 < J)
    {ρ : ℝ} (hρ : ρ ≠ 0) {c : ℝ} (hc : 0 < c) :
    -- At symmetry, the aggregate is rho-invariant (no information
    -- in the slow/aggregate channel) while the fast/price channel
    -- in 1-perp carries all curvature information.
    powerMean J ρ hρ (symmetricPoint J c) = c ∧
    fisherInfoRho (symmetricPoint J c) ρ = 0 :=
  ⟨powerMean_symmetricPoint hJ hρ hc,
   fisherInfoRho_zero_at_symmetry hc ρ⟩

Dependency Graph

Location

thesis/CESProofs/Dynamics/TemporalOrdering.lean:241

Module Section

Temporal Ordering Rules from Two-World Timescale Separation

In the same file