negative_eigenvalue_count
The theorem establishes that the spacetime metric η has exactly one negative diagonal entry, isolating the temporal direction as the unique cost-reducing axis. Researchers deriving Lorentzian geometry from J-cost minimization and the T0-T8 chain would cite this to confirm the signature pattern before constructing the light cone. The proof is a term-mode argument that reduces the filtered index set to a singleton via extensionality and finite case analysis on the four indices.
claimThe cardinality of the set of indices $i$ in the finite set of size 4 for which the diagonal entry of the metric tensor η satisfies η_{ii} < 0 equals 1.
background
The Spacetime Emergence module shows that 4D Lorentzian geometry is forced by the J-cost functional J(x) = (x + x^{-1})/2 - 1 together with the T0-T8 chain. The 8-tick recognition operator decreases cost along one axis while the three spatial axes remain positive definite from J''(1) = 1 and D = 3. Upstream structures supply the convexity of J-cost minimization and the spectral forcing of three spatial dimensions from the Q3 lattice.
proof idea
The argument first reduces the claim to equality of the filtered set with the singleton containing index 0. Extensionality then converts the equality into a membership check for each element of Fin 4, which is discharged by exhaustive case analysis on the four indices together with the explicit sign pattern of the diagonal entries.
why it matters in Recognition Science
The result is invoked directly by the lorentzian_signature theorem to establish the (1,3) signature. It fills SE-004 in the Spacetime Emergence registry and confirms that the eight-tick octave (T7) plus D = 3 (T8) produce exactly one negative metric coefficient. This step supports the emergence of the arrow of time from cost reduction and leaves open the derivation of the full causal light-cone structure.
scope and limits
- Does not derive the explicit numerical values of the metric entries.
- Does not prove vanishing of off-diagonal components.
- Does not establish Lorentz invariance or the light-cone structure.
- Does not connect to the mass ladder or coupling constants.
Lean usage
⟨negative_eigenvalue_count, positive_eigenvalue_count⟩formal statement (Lean)
146theorem negative_eigenvalue_count :
147 (Finset.univ.filter (fun i : Fin 4 => η i i < 0)).card = 1 := by
proof body
Term-mode proof.
148 suffices h : Finset.univ.filter (fun i : Fin 4 => η i i < 0) = {(0 : Fin 4)} by
149 rw [h]; simp
150 ext i; fin_cases i <;> simp [Finset.mem_filter, η_00, η_11, η_22, η_33]
151
152/-- Count of positive diagonal entries = 3 (spatial). -/