Lorentzian_1_3
plain-language theorem explainer
The Lorentzian (1,3) master-theorem clause is the conjunction of carried metric content (four dimensions, one timelike and three spacelike directions, with metric normalizations) and inhabitance of the full spacetime-emergence certificate. Gravity Track 7.A authors cite it as the M4 signature clause inside the twelve-clause quantum-gravity master statement. It is a pure Prop definition, not a proved claim.
Claim. The Lorentzian $(1,3)$ clause holds when the carried metric content is true: spacetime dimension equals $4$, the emergent metric $\eta$ has exactly one negative and three positive diagonal entries, and the stated trace and determinant normalizations hold; and when the spacetime-emergence certificate (forced $4$D Lorentzian structure from the $J$-cost and the T0--T8 chain) is inhabited.
background
Gravity Track 7.A authors the quantum-gravity master statement as a twelve-clause conjunction. Closed clauses are discharged from existing certificates; open clauses remain hypothesis inputs. This definition is the named Prop for the Lorentzian-signature clause (M4).
The carried half requires spacetime_dim = 4, exactly one timelike and three spacelike diagonal signs of the emergent metric $\eta$, plus trace/determinant normalization. The certificate half is SpacetimeEmergenceCert, which "verifies the full structure of 4D Lorentzian spacetime is forced by the $J$-cost functional and the RS forcing chain T0--T8" (including temporal dimension one and spatial dimension three).
In the RS primer, T8 forces $D = 3$ spatial dimensions and T7 the eight-tick octave; together they pin the $(1,3)$ signature that this clause packages for the master theorem.
proof idea
Definitional abbreviation only: the Prop is the conjunction of the carried metric content and Nonempty of the spacetime-emergence certificate. No tactics, no lemmas applied at this site. The sibling theorem that inhabits it unpacks fields of the existing emergence certificate (dimension, signature, metric trace, metric determinant) and the certificate's nonemptiness witness.
why it matters
This is one of the twelve clauses of RSQuantumGravityMaster, the Track 7.A master statement matching the master-plan template verbatim: the opening block is (T0_T8_holds ∧ CostUniqueness ∧ Lorentzian_1_3) ∧ .... Downstream, Lorentzian_1_3_proven discharges it from the spacetime-emergence certificate, and the non-circularity audit lists it among the six closed certificate clauses (closed_certs_hold) while disclosing that the clause is exactly carried M4 content conjoined with certificate nonemptiness.
Framework landmark: it packages the T8 $D = 3$ spatial result (with one time direction) into the gravity master theorem, so strong-field and continuum-EH clauses sit on a forced Lorentzian base rather than an assumed GR background. It does not itself close open tracks (Page curve, PTA, strong-field distinctness from GR); those remain separate hypothesis inputs to the conditional master theorem.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.