Documentation

Lean 4 Proof

theorem cross_coupling_creates_spiral
    {a d b c : ℝ}
    -- Diagonal entries negative (self-correcting)
    (ha : a < 0) (hd : d < 0)
    -- Cross-coupling strong enough: 4(ad - bc) > (a+d)²
    (hstrong : (a + d) ^ 2 < 4 * (a * d - b * c)) :
    jacobianDiscriminant (jacobianTrace a d) (jacobianDet a d b c) < 0 := by
  simp only [jacobianDiscriminant, jacobianTrace, jacobianDet]
  linarith

Dependency Graph

Location

thesis/CESProofs/Dynamics/CoupledRhoT.lean:124

Module Section

Coupled (ρ, T) Jacobian Analysis

In the same file