euclideanSqEdges_scale
plain-language theorem explainer
Squared edge lengths of a Euclideanized causal 4-simplex at spacing a equal a² times the unit-spacing lengths, edge by edge. Cited when factoring overall scale out of Cayley-Menger determinants or Wick-rotated CDT (4,1)/(3,2) volumes. Proof is extensionality, a timelike/spacelike case split, and ring.
Claim. For either causal 4-simplex type $\tau\in\{(4,1),(3,2)\}$ and real $a,\alpha$, the Euclidean squared-edge assignment at spacing $a$ equals $a^{2}$ times the unit-spacing assignment: for every edge $e$ among the ten lexicographic edges, $\mathrm{eucl}(\tau,a,\alpha)(e)=a^{2}\,\mathrm{eucl}(\tau,1,\alpha)(e)$.
background
This module is the 4D Lorentzian lift in the QG Seven-Gaps campaign (Phase 3a): CDT-style causal 4-simplices between adjacent spatial slices, plus the kinematical Wick map on squared edge lengths. Spatial slices are equilateral tetrahedra of squared edge $a^{2}$. Two fill types appear: $(4,1)$ (six spacelike, four timelike) and $(3,2)$ (four spacelike, six timelike); reflections share the same edge multiset.
CausalPentType is the inductive label for those two types. Squared lengths are indexed by Fin 10 in lexicographic vertex-pair order. In the Euclideanized assignment, spacelike edges carry $a^{2}$ and timelike edges carry $\alpha a^{2}$ (the Wick image of the Lorentzian $-\alpha a^{2}$). The companion map euclideanSqEdges packages that assignment as a function of type, spacing, and $\alpha$.
The claim is the elementary homogeneity of that map in the spacing parameter: every squared length scales as $a^{2}$ relative to the unit-spacing tuple.
proof idea
Pointwise extensionality on the ten edges, then unfold the Euclidean squared-edge definition. Case-split on whether the edge is timelike for the given type. In the timelike branch both sides hit the $\alpha a^{2}$ arm of the conditional, so ring gives $a^{2}\cdot(\alpha\cdot 1^{2})=\alpha a^{2}$. In the spacelike branch both sides hit the pure $a^{2}$ arm, and ring again closes. No external lemmas beyond the definition and the boolean edge-type predicate.
why it matters
Homogeneity in $a$ is the first step toward factoring scale out of the 4-simplex Cayley-Menger determinant cm4 (the bordered $6\times 6$ form from Geometry.CayleyMengerN). The 3D sibling campaign uses the identical pattern: rewrite by the scale law, then apply the existing CM scaling identity to obtain $\mathrm{cm}\propto (a^{2})^{d}$. The same rewrite is what downstream 4D non-degeneracy thresholds need so that positivity/negativity statements can be stated at unit spacing and transferred.
In the module plan this sits under the Wick-rotation block: after edges are Euclideanized, scale factors cleanly, and the algebraic continuation $\alpha\mapsto -\alpha$ can be studied independently of lattice spacing. It is pure kinematics (no dynamics, no measure), but it is required scaffolding for the exact Euclidean non-degeneracy thresholds in $\alpha$ that the module targets for both causal classes.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.