causalSimplex4DStatus_flags
plain-language theorem explainer
Status snapshot for the 4D causal-simplex lane: four boolean progress flags (classes defined, Cayley-Menger thresholds certified, Lorentzian negativity proved, action-level continuation still open). Auditors of the Seven-Gaps gravity campaign cite it as a documentation receipt, not as geometry. The proof is four reflexivity steps on hand-set structure fields.
Claim. The 4D causal-simplex status record asserts four equalities: the four-dimensional causal classes are marked defined, the Cayley-Menger thresholds are marked certified, Lorentzian Cayley-Menger negativity is marked proved, and the action-level continuation is marked still open.
background
This module is Phase 3a of the QG Seven-Gaps Lorentzian-sector lane: the 4D CDT-style lift of causal simplex classes. Spatial slices are equilateral tetrahedra of squared edge length $a^2$. Between slices one fills with two 4-simplex types: (4,1) (six spacelike, four timelike edges) and (3,2) (four spacelike, six timelike). Timelike squared lengths are $-\alpha a^2$ with $\alpha>0$; Wick rotation is the algebraic continuation $\alpha\mapsto -\alpha$.
The load-bearing geometry is the bordered Cayley-Menger determinant $\mathrm{cm}_4$ (via the dimension-parametric $6\times 6$ form), evaluated on both classes, with Euclidean non-degeneracy thresholds in $\alpha$ and strict negativity on the Lorentzian side. The status structure is a separate bookkeeping object: its booleans are set by hand next to those theorems and are not derived from them.
proof idea
Pure documentation wrapper. The goal is a four-fold conjunction of field equalities on the status structure. Each conjunct is discharged by rfl against the literal boolean assigned in the structure definition, packaged as a single anonymous constructor ⟨rfl, rfl, rfl, rfl⟩. No geometric lemma is invoked.
why it matters
Inside Recognition Science gravity, this sits in the Seven-Gaps campaign as a honesty-tier receipt for the 4D causal simplex and kinematical Wick-rotation work: combinatorial class definitions, certified $\mathrm{cm}_4$ thresholds, and proved Lorentzian $\mathrm{cm}_4$ negativity are flagged complete, while action-level continuation is explicitly left open. The module doc ties the geometry to Ambjørn-Jurkiewicz-Loll CDT conventions and to the existing Cayley-Menger infrastructure. Nothing downstream currently depends on the flags; the mathematics lives in the determinant and class theorems above. The open flag marks the remaining gap before a dynamical (action-level) continuation can be claimed.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.