causalSimplex4DStatus
plain-language theorem explainer
Status record for the 4D causal (CDT) simplex kinematical layer: classes defined, exact cm4 thresholds certified, Lorentzian cm4 negativity proved, and action-level continuation still open. Downstream honesty theorems and Wick-action modules cite these flags. The body is a plain structure instance with four hand-set booleans; the mathematics lives in the theorems above, not here.
Claim. The deliverable status of the 4D Lorentzian causal-simplex module is the record with four flags: four-dimensional causal classes are defined; the exact Cayley--Menger thresholds $\alpha > 3/8$ (type $(4,1)$) and $\alpha > 7/12$ (type $(3,2)$) are certified; Lorentzian tuples satisfy strict $cm_4 < 0$; and the action-level continuation (complex dihedral angles at timelike hinges) remains open.
background
This module is Phase 3a of the QG Seven-Gaps Lorentzian lane: the 4D lift of causal-simplex machinery. Spatial slices are equilateral tetrahedra of squared edge length $a^2$. Between slices one fills with two CDT 4-simplex types: $(4,1)$ (six spacelike + four timelike edges) and $(3,2)$ (four spacelike + six timelike). Spacelike edges carry $a^2$; timelike edges carry $-\alpha a^2$ with $\alpha > 0$. Wick rotation is the algebraic continuation $\alpha \mapsto -\alpha$ on squared lengths.
The status structure packages four booleans for that kinematical layer: combinatorial class definitions, exact Euclidean non-degeneracy thresholds in $\alpha$ via the bordered $6\times 6$ Cayley--Menger determinant $cm_4$, strict Lorentzian $cm_4$ negativity, and whether the action-level (boost/sinh) continuation is closed. The structure doc states the embeddability upgrade from $cm_4 < 0$ to non-realizability is classical and not formalized here.
proof idea
Not a proof. The definition is a structure instance that sets the four status booleans by hand: classes defined, cm4 thresholds certified, and Lorentzian negativity proved are true; action-level continuation open is true. A sibling documentation theorem then re-reads those flags by rfl. As the module notes, nothing forces the flags; the real content is in the combinatorial and determinant theorems above this record.
why it matters
Gives a single citation point for what the 4D kinematical Wick layer has closed versus left open in the Seven-Gaps campaign. Downstream, causalSimplex4DStatus_flags freezes the four values by rfl. WickHingeDataComplete.action_level_still_open quotes the open flag explicitly and states that hinge-data continuation deliberately does not flip it. WickActionComplexFirst.realized sits on the same honesty boundary: path-selected hinge continuation with a branch certificate, not full action-level closure.
In framework terms this is the D=4 Lorentzian simplex kinematics supporting Regge/CDT-style gravity, not a forcing-chain (T0--T8) step. It records that the combinatorial and $cm_4$ layer is done while complex dihedral/action continuation stays open.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.