lorentzian_signature
Why this theorem is linked from Hamiltonian Analysis of Pre-geometric Gravity echoes
Pith linked this Lean declaration because the review connected a specific passage in the paper to this theorem. The relation tag says how strong that connection is; it is not a generic placeholder.
the pre-geometric field content of this formulation consists of the gauge field A^{AB}_µ of the group SO(1,4) or SO(3,2) and a Higgs-like scalar field ϕ^A. Once the latter acquires a nonzero vacuum expectation value... the ensuing SSB reduces the gauge group of spacetime to the Lorentz group SO(1,3)
ECHOES: this paper passage has the same mathematical shape or conceptual pattern as the Recognition theorem, but is not a direct formal dependency.
plain-language theorem explainer
lorentzian_signature establishes that the metric η on 4D spacetime has exactly one negative diagonal entry and three positive ones, matching the temporal and spatial dimensions forced by the J-cost chain. Researchers deriving spacetime geometry from recognition principles would cite this to confirm the (1,3) signature. The proof is a one-line wrapper that pairs the negative_eigenvalue_count and positive_eigenvalue_count theorems.
Claim. The metric η satisfies |{i ∈ Fin 4 | η_{ii} < 0}| = temporal dimension and |{i ∈ Fin 4 | η_{ii} > 0}| = spatial dimension, confirming Lorentzian signature (−, +, +, +).
background
The SpacetimeEmergence module derives 4D Lorentzian geometry from J-cost minimization and the T0–T8 forcing chain rather than postulating background spacetime. J(x) = (x + x^{-1})/2 − 1 is the cost functional whose second derivative at 1 fixes positive spatial curvature while the 8-tick operator supplies the unique negative temporal direction. Upstream, negative_eigenvalue_count proves the negative diagonal count equals 1 and positive_eigenvalue_count proves the positive count equals 3; spatial_dim and temporal_dim are the constants 3 and 1 fixed by T8 and T7. The module states: 'The complete structure of 4D Lorentzian spacetime — metric signature (−,+,+,+) … is FORCED by the J-cost functional and the forcing chain T0–T8.'
proof idea
The proof is a one-line wrapper that applies negative_eigenvalue_count and positive_eigenvalue_count to discharge the two cardinality conjuncts directly.
why it matters
This fills SE-004 and supplies the signature_lorentzian field to spacetime_emergence_cert, which certifies the full emergence of Lorentzian spacetime with zero free parameters. It closes the chain segment from Recognition Composition Law through J-uniqueness (T5), 8-tick octave (T7), and D = 3 (T8) to the explicit metric signature diag(−1, +1, +1, +1). No open scaffolding remains.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.
papers checked against this theorem (showing 3 of 3)
-
Lattice Weyl fermion gets an exact chiral symmetry, no doubling
"a single Weyl fermion ... protected by an emanant U(1) chiral symmetry which is also ultralocally generated but not quantized in the UV"
-
Neural net reads a holographic metric off the lattice quark potential
"f(r) = 1 − (1/r_h^4 + μ²/r_h²) r^4 + (μ²/r_h^4) r^6; AdS/RN background with deformation factor"
-
Pre-geometric gravity has three modes: graviton plus one scalar
"the pre-geometric field content of this formulation consists of the gauge field A^{AB}_µ of the group SO(1,4) or SO(3,2) and a Higgs-like scalar field ϕ^A. Once the latter acquires a nonzero vacuum expectation value... the ensuing SSB reduces the gauge group of spacetime to the Lorentz group SO(1,3)"