lorentzian_from_det
plain-language theorem explainer
The product of the four diagonal entries of the metric η is negative, confirming Lorentzian signature (−,+,+,+). Researchers deriving spacetime geometry from J-cost minimization and the T0–T8 chain would cite this as the terminal step that fixes the metric signature. The proof is a one-line term reduction that rewrites the determinant definition and evaluates the resulting arithmetic expression.
Claim. $∏_{i=0}^3 η_{ii} < 0$, where η is the diagonal metric diag(−1,+1,+1,+1) forced by J-cost minimization together with the eight-tick octave and D=3 spatial dimensions.
background
The Spacetime Emergence module derives 4D Lorentzian geometry from the J-cost functional without any background postulate. The Recognition Composition Law together with the forcing chain T0–T8 yields J-uniqueness (T5), the golden-ratio fixed point φ (T6), the eight-tick temporal operator (T7), and exactly three spatial dimensions (T8). The metric η is then fixed as diag(−1,+1,+1,+1) because temporal displacements lower cost while spatial displacements raise it quadratically, producing the opposite sign on the time component. The module states: “The complete structure of 4D Lorentzian spacetime — metric signature (−,+,+,+), causal light-cone, Lorentz factor, arrow of time — is FORCED by the J-cost functional and the forcing chain T0–T8.” Upstream definitions of the active-edge count A supply the φ-power balance at D=3 that enters the cost calculation.
proof idea
The proof is a one-line term-mode wrapper. It rewrites the product via the determinant definition of η and then applies numerical normalization to obtain the explicit negative value.
why it matters
This theorem supplies the final metric signature required by the module’s central claim that spacetime itself is a theorem of cost minimization. It realizes the T0–T8 chain landmarks (J-uniqueness, φ fixed point, eight-tick octave, D=3) and the explicit statement that η = diag(−1,+1,+1,+1). No direct downstream uses are recorded, yet the result closes the derivation of causal structure, proper time, and the mass-shell relation E² = p² + m² within the Recognition framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.