negative_eigenvalue_count
plain-language theorem explainer
Exactly one of the four diagonal entries of the metric η is negative. Researchers deriving Lorentzian geometry from J-cost minimization would cite this count to fix the temporal direction. The argument reduces the filtered index set to the singleton at index zero, then applies extensionality and finite case analysis on the signs of the diagonal entries.
Claim. The cardinality of the set of indices $i$ in Fin 4 such that the diagonal entry $η_{ii}$ is negative equals 1.
background
The module derives the complete 4D Lorentzian spacetime structure from the J-cost functional and the T0-T8 forcing chain. J-cost is the strictly convex function J(x) = (x + x^{-1})/2 - 1 whose minimum at x=1 forces positive spatial curvature while the eight-tick recognition operator forces a single negative temporal coefficient. The local setting states that spacetime geometry itself is a theorem of cost minimization rather than a background postulate, with D=3 spatial dimensions fixed by T8 and the octave fixing the temporal direction.
proof idea
Term-mode proof. It first suffices that the filtered set equals the singleton containing index 0, rewrites the cardinality claim, and simplifies. It then applies set extensionality and performs case analysis on each element of Fin 4, invoking the explicit sign facts η_00, η_11, η_22, η_33 to decide filter membership.
why it matters
The result is invoked by lorentzian_signature (SE-004), which asserts the metric signature is (1,3) Lorentzian. It completes one link in the chain from the Recognition Composition Law through T5 J-uniqueness, T7 eight-tick octave, and T8 D=3 to the explicit signature diag(−1,+1,+1,+1). The count thereby supports the claim that the arrow of time and light-cone structure emerge from cost minimization with zero free parameters.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.