theorem proved term proof

`signature_unique`

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

formal statement (Lean)

 328theorem signature_unique :
 329    temporal_dim = 1 ∧ spatial_dim = 3 ∧
 330    (∀ d_t d_s : ℕ, d_t + d_s = spacetime_dim → d_t = 1 → d_s = 3) := by

proof body

Term-mode proof.

 331  refine ⟨rfl, rfl, fun d_t d_s h1 h2 => ?_⟩
 332  rw [h2, spacetime_dim_eq_four] at h1; omega
 333
 334/-! ## §11  The Mass Gap as the Minimum Spacetime Excitation -/
 335
 336/-- The mass gap sets the minimum spatial excitation energy. -/

depends on (12)

Lean names referenced from this declaration's body.

Mass in IndisputableMonolith.Constants.RSNativeUnits decl_use
as in IndisputableMonolith.Foundation.SimplicialLedger.ContinuumBridge decl_use
gap in IndisputableMonolith.Gap45.Derivation decl_use
spacetime_dim in IndisputableMonolith.Gravity.Connection decl_use
gap in IndisputableMonolith.Masses.AnchorPolicy decl_use
gap in IndisputableMonolith.Masses.RSBridge.Anchor decl_use
Spacetime in IndisputableMonolith.Relativity.Geometry.Manifold decl_use
gap in IndisputableMonolith.RSBridge.Anchor decl_use
spacetime_dim in IndisputableMonolith.Unification.SpacetimeEmergence decl_use
spacetime_dim_eq_four in IndisputableMonolith.Unification.SpacetimeEmergence decl_use
spatial_dim in IndisputableMonolith.Unification.SpacetimeEmergence decl_use
temporal_dim in IndisputableMonolith.Unification.SpacetimeEmergence decl_use