threeTwoCosPath_apply_symm
plain-language theorem explainer
The split-form dihedral cosine along the physical (3,2) Wick arc is symmetric under swap of the opposite vertex pair. Anyone tracking hinge labels on the threeTwo causal 4-simplex can cite this to treat (p,q) and (q,p) as the same cosine path. The proof is a one-line application of the generic split-cosine symmetry.
Claim. For all opposite vertex indices $p,q \in \{0,1,2,3,4\}$ and real arc parameter $t$, the split-form dihedral cosine of the hinge opposite $(p,q)$ along the physical threeTwo continuation arc equals that opposite $(q,p)$: $\mathrm{cos}_{3,2}(q,p;t)=\mathrm{cos}_{3,2}(p,q;t)$.
background
Lane B2 of the QG Seven-Gaps campaign continues the (3,2) causal 4-simplex (lower slice ${0,1,2}$, upper ${3,4}$) along the canonical upper-half-plane arc at the physical point $a=1$, $\alpha=1$. Hinges are labeled by opposite pairs $(p,q)$ among the five vertices; the ten triangular hinges fall into spacelike, mixed, and upper-pair classes with closed cofactor formulae.
The path threeTwoCosPath evaluates the split-form dihedral cosine on the complex edge-length package obtained by continuing the threeTwo simplex along that arc. The split cosine is built from complex Cayley-Menger cofactors and a split denominator, so it is a priori ordered in $(p,q)$.
Upstream, dihedralCosSplitC_symm already proves that the generic split-form cosine is invariant under swapping the opposite pair, by cofactor symmetry and commutativity of multiplication in the denominator.
proof idea
One-line term proof: unfold the path definition (cosine of the continued threeTwo edge package at $(p,q)$) and apply dihedralCosSplitC_symm to that package. No arc-specific algebra is needed; the symmetry is inherited from the generic split cosine.
why it matters
In the all-hinge Wick package for the (3,2) simplex, opposite pairs are unordered geometric labels, yet the cosine path is written with ordered indices. This lemma licenses free reordering when assembling branch certificates, minor tables, or transport of the boundary-continuation package across a pair swap (as the adjacent doc-comment states).
It sits inside the Gravity Seven-Gaps finishing charter rather than the T0-T8 forcing chain: it is bookkeeping that keeps the ten-hinge complex-first continuation coherent. No downstream consumers are recorded yet; the natural parents are the branch-regularity and continuation statements that quantify over unordered hinges.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.