positive_eigenvalue_count
The declaration shows that exactly three of the four diagonal entries of the metric η are positive. Researchers assembling derivations of Lorentzian geometry from J-cost minimization would cite it to confirm the spatial sector. The proof reduces the filtered cardinality claim to an explicit set equality on Fin 4 via case analysis and decidable equality.
claimThe number of indices $i$ in Fin 4 such that the diagonal entry $η_{ii}$ is positive equals 3.
background
The Spacetime Emergence module derives 4D Lorentzian geometry as a theorem of cost minimization under the Recognition Composition Law and the T0–T8 forcing chain. The metric η is fixed to diag(−1, +1, +1, +1) once J-uniqueness (T5), the self-similar fixed point φ (T6), the eight-tick octave (T7), and D = 3 spatial dimensions (T8) are in place; the temporal direction carries the negative sign because the recognition operator decreases cost along that axis. Upstream results supply the structural assumptions: OptionAEmpiricalProgram.is ensures collision-free counting, SimplicialLedger.EdgeLengthFromPsi.is guarantees algebraic tautology for edge lengths, and the remaining two is-structures close the combinatorial setup without new axioms.
proof idea
A suffices tactic equates the filtered Finset to the explicit set {(1 : Fin 4), (2 : Fin 4), (3 : Fin 4)}. Rewriting and decide then settle the cardinality. The set equality is discharged by extensionality followed by fin_cases on i, with simp using the four precomputed diagonal signs η_00 < 0, η_11 > 0, η_22 > 0, η_33 > 0.
why it matters in Recognition Science
The result is invoked by lorentzian_signature to complete the (1,3) signature statement. It supplies the spatial half of SE-004, confirming that the T8-forced count of three positive directions emerges directly from J-cost positivity. The declaration therefore closes one link in the chain from RCL through the eight-tick octave to the emergence of causal structure and the mass formula.
scope and limits
- Does not derive the explicit diagonal values of η from the J-functional.
- Does not treat off-diagonal metric components or curvature tensors.
- Does not establish Lorentz invariance or light-cone structure.
- Does not connect the count to the phi-ladder mass formula or the alpha band.
formal statement (Lean)
153theorem positive_eigenvalue_count :
154 (Finset.univ.filter (fun i : Fin 4 => 0 < η i i)).card = 3 := by
proof body
Term-mode proof.
155 suffices h : Finset.univ.filter (fun i : Fin 4 => 0 < η i i) =
156 {(1 : Fin 4), (2 : Fin 4), (3 : Fin 4)} by
157 rw [h]; decide
158 ext i; fin_cases i <;>
159 simp [Finset.mem_filter, η_00, η_11, η_22, η_33, Fin.ext_iff]
160
161/-- **SE-004: The metric signature is (1, 3) — Lorentzian.** -/