positive_eigenvalue_count
plain-language theorem explainer
Exactly three diagonal entries of the metric η are positive. Researchers deriving Lorentzian geometry from J-cost minimization under the T0-T8 chain would cite this count to fix the spatial dimension. The argument reduces the cardinality statement to an explicit set equality on Fin 4 and verifies membership by exhaustive case analysis on the indices.
Claim. The cardinality of the set of indices $i$ in $0,1,2,3$ such that the diagonal entry $η_{ii}>0$ equals 3.
background
The Spacetime Emergence module shows that 4D Lorentzian spacetime is forced by the J-cost functional and the T0-T8 chain. J satisfies the Recognition Composition Law, forces φ as the self-similar fixed point (T6), produces an eight-tick temporal direction (T7), and yields D=3 spatial dimensions (T8). The metric η carries signature (−,+,+,+) because spatial directions increase cost quadratically while the temporal direction reduces it. The local setting is given by the module statement that the full Lorentzian structure, including light cones and proper time, follows from cost minimization with zero free parameters.
proof idea
A suffices tactic reduces the claim to equality of the filtered set with the explicit set of the three positive indices. Extensionality then splits into four cases via fin_cases on i, each simplified by the known diagonal signs η_00, η_11, η_22, η_33. The cardinality is recovered by rewriting and a decide tactic.
why it matters
The result supplies the positive count used by lorentzian_signature (SE-004), which asserts the metric signature is (1,3). It realizes the D=3 spatial count from T8 together with the single temporal octave from T7, confirming that spacetime geometry itself is a theorem of the forcing chain rather than a background assumption. No open scaffolding remains at this step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.