lorentzian_clause_is_cert
plain-language theorem explainer
The Lorentzian (1,3) master-theorem clause is definitionally the carried metric content M4 conjoined with nonemptiness of the spacetime-emergence certificate. Auditors of the unconditional QG master theorem cite this to confirm the field is not a True placeholder and does not smuggle in the master conclusion. The proof is a one-line rfl disclosure of the clause definition.
Claim. The Lorentzian-signature atom of the master theorem is definitionally equal to the conjunction of the carried metric proposition (spacetime dimension $4$, exactly one negative and three positive diagonal entries of the emergent metric $\eta$, plus its trace/determinant normalization) with the assertion that a spacetime-emergence certificate exists.
background
This module is a field-by-field non-circularity audit of rs_quantum_gravity_master_unconditional. A formal-methods referee objected that witness structures of shape $\Sigma(P:\mathrm{Prop}),P$ carry no content unless the plugged-in propositions are genuine physics rather than True or the master conclusion itself. For each atom the audit therefore supplies an rfl-level disclosure of what the field actually is, plus a standalone proof that it holds.
The Lorentzian clause is the M4 spacetime-emergence atom. Its carried content asserts four spacetime dimensions, signature $(1,3)$ read off the diagonal of the emergent metric $\eta$ (one timelike, three spacelike directions), and the trace/determinant normalization of that metric. The second conjunct is mere nonemptiness of the full spacetime-emergence certificate structure.
Upstream, the master theorem defines the clause exactly as that conjunction; the carried proposition is the concrete metric content, not a self-reference to the master statement.
proof idea
One-line term proof by rfl. The left-hand side is the master-theorem definition of the Lorentzian clause; the right-hand side is that definition unfolded. Definitional equality discharges the disclosure with no lemmas and no tactics beyond reflexivity.
why it matters
Peer-review finding F1 / Rec 2 demanded that every atom of the QG master conjunction be inspectably non-circular. This disclosure places the Lorentzian field in the inhabitedCert class: carried metric content plus Nonempty of a certificate, not a True placeholder and not the master conclusion.
It sits beside sibling disclosures for the T0–T8 forcing chain, cost-uniqueness, BMV positivity, Hawking temperature, and $c_{\mathrm{RS}}$. Together they underwrite the audit claim that after M1–M3 the master statement is assembled from independently named, non-self-referential propositions. Framework-wise it records the D=3 spatial (plus one time) landmark of the forcing chain (T8) as the metric signature the master theorem actually carries, rather than as prose aspiration.
No downstream consumers are wired yet; the declaration is an audit artifact for referees, not a computational lemma.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.