# AGY Peer Review: Paper 4 (Lorentzian Geometry as a Realization)

**Date**: July 23, 2026
**Paper**: *Lorentzian Geometry as a Realization: Coframes, Connections, Curvature, and Einstein Dynamics*
**Scope of Review**: Mathematical and physical correctness, exact source attribution, unstated assumptions, novelty, missing literature, overclaims, internal status synchronization, and exposition.

## 1. General Assessment & Exposition
The manuscript represents an exceptionally rigorous and intellectually honest approach to foundational physics. Rather than falling into the common trap of claiming that spacetime "emerges" automatically from categorical or representation-theoretic data, the paper cleanly breaks the dependency cycle. It correctly treats Lorentzian geometry and Einstein dynamics as **conditional realizations** requiring explicitly postulated physical inputs (events, light rays, free-fall paths, clocks). The exposition is remarkably precise, dissecting geometric reconstruction into distinct, independently verifiable bridges.

## 2. Mathematical and Physical Correctness
The mathematical claims and physical distinctions have been meticulously verified:
* **Causal Rigidity vs. Spacetime Creation**: The paper correctly identifies that Hawking–King–McCarthy (HKM), Malament, and Levichev are rigidity theorems *between already given smooth Lorentzian spacetimes*, not constructive algorithms that build a manifold or dimension from a bare binary relation.
* **Torsion and Unparametrized Paths**: The counterexample demonstrating that free-fall paths do not see arbitrary torsion (by adding an antisymmetric $K^\mu{}_{\nu\rho}$ to the connection) is algebraically exact. Unparametrized geodesics reconstruct at most a projective equivalence class, leaving the full affine connection undetermined.
* **EPS and Weyl Geometry**: The paper rightly notes the original Ehlers–Pirani–Schild (EPS) rigor caveat and correctly imports the Matveev–Scholz (2020) result to show that conformal and projective compatibility yields a Weyl connection—not a Levi-Civita metric geometry.
* **Clock Laws and Metric Gauge**: The extraction of a metric is properly gated behind clock-law model dependence. The separation of local closedness ($d\phi = 0$), global exactness ($\phi = d\sigma$, requiring $H^1=0$ or simple connectedness), and unit choice is mathematically flawless. The citation of Hobson–Lasenby (2021) perfectly contextualizes the model-dependence of the "no second-clock effect".
* **Lovelock Classification**: Lovelock's four-dimensional theorem is properly stated as the classification of *symmetric, divergence-free, second-order natural metric tensors*, completely decoupling it from "action uniqueness." The manuscript correctly notes that exact forms, boundary terms, and Gauss-Bonnet densities can alter the action without altering the bulk equations.
* **Boundary Terms and Conservation**: The paper accurately limits the standard Gibbons-Hawking-York (GHY) term to smooth non-null Dirichlet boundaries, citing Lehner et al. and Hayward to show that null segments and corners require distinct boundary data. The distinction between the geometric Bianchi identity and on-shell matter conservation (requiring diffeomorphism invariance and matter equations) is rigorous.
* **The Buchdahl Obstruction**: The explicit action $S_\alpha[g] = \frac{1}{2\kappa}\int (R - 2\Lambda + \alpha R^2)\sqrt{|g|} d^4x$ with $\alpha \neq 0$ is a brilliant, minimal witness. The calculation of the resulting fourth-order field equation is exactly correct and serves as an irrefutable obstruction to unrestricted uniqueness claims.

## 3. Exact Source Attribution & Missing Literature
* The distinction between Malament (chronology, preserving $I^+$ and $\ll$) and Levichev (causality, preserving $J^+$ and $\le$) is handled perfectly.
* The paper successfully spans the required literature without overclaiming the results of any single paper. Citations for LeFloch-Mardare (distributional regularity vs. $C^2$ classical regularity), Geroch (global coframes trivializing the tangent bundle), and Trautman (Einstein-Cartan/torsion) perfectly support the separated assumption gates.
* There is no missing literature for the stated scope; the bibliography captures the necessary modern, rigorous updates to historical theorems (e.g., Navarro-Navarro 2011 for Lovelock).

## 4. Internal Status Synchronization & Software Evidence
* **Claims**: `P4-C01` through `P4-C04` are correctly synchronized as `OPEN`. `P4-C05` is correctly synchronized as `OBSTRUCTED` with the Buchdahl witness backing it.
* **Assumptions**: `P4-A01` through `P4-A12` are correctly synchronized as `UNVALIDATED` across the LaTeX text, the assumption ledger, and the Lean file.
* **Software Artifacts**: Lean and Haskell are treated with exemplary discipline. The paper explicitly states that the Lean algebraic lemmas (e.g., conformal zero sets and antisymmetric cancellation) and Haskell scripts act as finite structural bookkeeping. It explicitly denies that these computational checks constitute kernel-level proofs of manifold existence, the EPS program, or variational analysis.

## 5. Findings by Severity
* **CRITICAL**: None.
* **MAJOR**: None.
* **MINOR**: None. The paper flawlessly executes the strict requirements of the read-only source audit. All required constraints, unstated assumptions in the standard literature, and exact dependencies have been identified, isolated, and appropriately flagged.

VERDICT: ACCEPT