theorem proved term proof

`negative_eigenvalue_count`

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

formal statement (Lean)

 146theorem negative_eigenvalue_count :
 147    (Finset.univ.filter (fun i : Fin 4 => η i i < 0)).card = 1 := by

proof body

Term-mode proof.

 148  suffices h : Finset.univ.filter (fun i : Fin 4 => η i i < 0) = {(0 : Fin 4)} by
 149    rw [h]; simp
 150  ext i; fin_cases i <;> simp [Finset.mem_filter, η_00, η_11, η_22, η_33]
 151
 152/-- Count of positive diagonal entries = 3 (spatial). -/

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

lorentzian_signature in IndisputableMonolith.Unification.SpacetimeEmergence decl_use

depends on (5)

Lean names referenced from this declaration's body.

of in IndisputableMonolith.Astrophysics.NucleosynthesisTiers decl_use
of in IndisputableMonolith.Foundation.DAlembert.LedgerFactorization decl_use
of in IndisputableMonolith.Foundation.PhiForcingDerived decl_use
of in IndisputableMonolith.Foundation.SpectralEmergence decl_use
of in IndisputableMonolith.Information.PhysicsComplexityStructure decl_use