lorentzian_from_det
The declaration establishes that the product of the four diagonal metric components is negative, confirming the Lorentzian signature with one negative and three positive entries. Researchers deriving emergent spacetime geometry from cost minimization would cite this step when closing the metric signature. The proof is a one-line term that rewrites the product via the determinant identity and normalizes the numerical result.
claimThe product of the diagonal entries of the metric tensor on four-dimensional spacetime is negative: $d_0 d_1 d_2 d_3 < 0$, where the signs are forced to be one negative and three positive by the J-cost functional.
background
The Spacetime Emergence module derives the full 4D Lorentzian structure, including metric signature (−,+,+,+), causal light-cone, and arrow of time, directly from the J-cost functional and the T0–T8 forcing chain. J(x) = (x + x^{-1})/2 − 1 encodes cost of deviation from balance; its second derivative at unity fixes positive spatial curvature while the eight-tick recognition operator supplies the opposing temporal sign. Upstream results supply the active-edge count A (equal to 1) from IntegrationGap, Masses, and Modal.Actualization, together with the Interval structure used for certification bounds.
proof idea
The term proof rewrites the product of diagonal entries using the determinant identity for the metric and then applies numerical normalization to obtain the strict inequality.
why it matters in Recognition Science
This step completes the metric-signature derivation inside the spacetime-emergence chain that begins with the Recognition Composition Law, proceeds through J-uniqueness (T5), phi fixed point (T6), eight-tick octave (T7), and D = 3 (T8), and yields η = diag(−1, +1, +1, +1). It thereby forces the light cone, proper time, and E² = p² + m² as theorems of cost minimization rather than background postulates. The module doc-comment states that every element of the structure is forced with zero free parameters.
scope and limits
- Does not derive the explicit components of the metric from the J-cost functional.
- Does not prove Lorentz invariance of the resulting geometry.
- Does not address extensions to higher dimensions or quantum corrections.
- Does not establish the full causal classification of intervals.
formal statement (Lean)
176theorem lorentzian_from_det : ∏ i : Fin 4, η i i < 0 := by
proof body
Term-mode proof.
177 rw [η_det]; norm_num
178
179/-! ## §5 The Spacetime Interval and Causal Classification -/
180
181/-- A spacetime displacement: 4-vector (Δt, Δx₁, Δx₂, Δx₃). -/