negative_eigenvalue_count
plain-language theorem explainer
The theorem establishes that the four-dimensional metric η has exactly one negative diagonal entry. Researchers assembling Lorentzian geometry from J-cost minimization would cite this count when confirming the temporal direction in the signature. The argument reduces the filtered set cardinality to an explicit singleton via case analysis on the four indices.
Claim. The Minkowski metric η on four-dimensional spacetime satisfies that exactly one of its diagonal entries is negative: the cardinality of the set of indices i where η_ii < 0 equals 1.
background
The Spacetime Emergence module derives the full Lorentzian structure from the J-cost functional and the T0–T8 forcing chain. J(x) = (x + x^{-1})/2 − 1 is strictly convex with its global minimum at x = 1; the eight-tick recognition operator distinguishes the unique cost-reducing temporal direction while J''(1) = 1 fixes positive curvature on the three spatial axes. Upstream structures supply the required convexity (PhiForcingDerived), dimension count D = 3 (SpectralEmergence), and ledger calibration (LedgerFactorization).
proof idea
The proof first reduces the cardinality claim to the assertion that the filtered set equals the singleton containing index zero. It then applies set extensionality followed by exhaustive case analysis over the four finite indices, invoking the explicit diagonal sign facts η_00, η_11, η_22, η_33 in each branch.
why it matters
The result is invoked directly by lorentzian_signature (SE-004), which assembles the full (1,3) signature as the conjunction of the negative and positive eigenvalue counts. It supplies one concrete step in the chain from the Recognition Composition Law through J-uniqueness (T5), the phi fixed point (T6), the eight-tick octave (T7), and D = 3 (T8) to the metric η = diag(−1, +1, +1, +1). No scaffolding remains.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.