pith. machine review for the scientific record. sign in
theorem proved term proof

spacetime_emergence_cert_nonempty

show as:
view Lean formalization →

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

generate prose now

formal statement (Lean)

 390theorem spacetime_emergence_cert_nonempty : Nonempty SpacetimeEmergenceCert :=

proof body

Term-mode proof.

 391  ⟨spacetime_emergence_cert⟩
 392
 393/-! ## Summary
 394
 395**The Spacetime Emergence Theorem**: η = diag(−1, +1, +1, +1).
 396
 397The question "Why is spacetime 4D Lorentzian?" has the answer:
 398**Because J(xy) + J(x/y) = 2J(x)J(y) + 2J(x) + 2J(y).** -/
 399
 400end  -- noncomputable section
 401
 402end SpacetimeEmergence
 403end Unification
 404end IndisputableMonolith

used by (2)

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

depends on (8)

Lean names referenced from this declaration's body.