physicalCausalPent
plain-language theorem explainer
Packages the unit-scale physical point (spatial edge length 1, causal ratio 1) as a non-degenerate Euclidean 4-simplex for either CDT type (4,1) or (3,2). Gravity and Regge-calculus workers cite it as the concrete Euclidean witness at the physical parameter values. It is a one-line specialization of the general Euclidean packaging at a=1, alpha=1, using positivity of 1 and the proved bound alphaMin < 1.
Claim. For either causal 4-simplex type $\tau\in\{(4,1),(3,2)\}$, the Euclideanized squared-edge assignment with spatial scale $a=1$ and causal ratio $\alpha=1$ is a non-degenerate 4-simplex: every squared edge is positive and the 4D Cayley–Menger determinant satisfies $\mathrm{cm}_4>0$.
background
This module is Phase 3a of the QG Seven-Gaps Lorentzian lane: CDT-style causal 4-simplex classes in $D=4$, with spacelike edges of squared length $a^2$ and timelike edges of squared length $-\alpha a^2$ (Lorentzian) or $+\alpha a^2$ after Wick rotation. Type $(4,1)$ has four vertices on slice $t$ and one on $t+1$ (6 spacelike + 4 timelike); type $(3,2)$ has three and two (4 spacelike + 6 timelike).
Non-degeneracy is the structure with all ten squared edges positive and $\mathrm{cm}4>0$, where $\mathrm{cm}4$ is the bordered $6\times 6$ Cayley–Menger determinant from Geometry.CayleyMengerN. The Euclidean packaging theorem already shows that whenever $a>0$ and $\alpha>\alpha{\min}(\tau)$ (with $\alpha{\min}=3/8$ for $(4,1)$ and $7/12$ for $(3,2)$), the Euclideanized causal assignment lands in that structure.
The physical point used throughout the campaign is the unit choice $a=1$, $\alpha=1$. Both thresholds lie strictly below 1, so the physical point sits in the open non-degenerate regime for either type.
proof idea
One-line wrapper. Instantiate the general Euclidean packaging at $a=1$ and $\alpha=1$, feeding the positivity proof one_pos for the scale and the already-proved inequality $\alpha_{\min}(\tau)<1$ for the causal ratio. No new algebra: the positivity of squared edges and the strict positivity of $\mathrm{cm}_4$ are inherited from those two hypotheses.
why it matters
Gives a named, type-indexed Euclidean witness at the physical parameter point that downstream Wick-action work can coerce and continue. In WickActionComplexFirst, the endpoint-identification theorem states that at continuation parameter $t=1$ the complex edge tuple equals exactly this module's Euclideanized real tuple (coerced to $\mathbb{C}$); the path-selected continuation realized likewise anchors on that kernel-checked Euclidean data.
Within the Seven-Gaps campaign this closes the kinematical packaging step of Phase 3a: causal classes defined, $\mathrm{cm}_4$ thresholds proved, Lorentzian $\mathrm{cm}_4<0$ established, and a concrete physical-point witness available. The module status note flags the action-level continuation (complex dihedral angles at timelike hinges, boost/sinh sector of the 4d Regge action) as still open wave 3b. Framework-wise it sits in the gravity lane that uses the forced $D=3$ spatial slices of T8 inside a 4D spacetime triangulation, not in the T0–T8 forcing chain itself.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.