threeTwoCosPath_symm
plain-language theorem explainer
The split-form dihedral cosine along the physical (3,2) Wick arc is symmetric under swap of the opposite-pair indices. Anyone proving boundary continuation for all ten triangular hinges of the threeTwo causal 4-simplex cites this to avoid double-counting ordered pairs. The proof is a one-line funext of the generic split-cosine symmetry.
Claim. For all opposite-pair indices $p,q \in \{0,1,2,3,4\}$, the split-form dihedral cosine path of the physical threeTwo arc at pair $(q,p)$ equals the path at pair $(p,q)$, as functions of the arc parameter $t \in \mathbb{R}$.
background
Lane B2 of the QG Seven-Gaps campaign treats the all-hinge complex-first Wick continuation of the (3,2) causal 4-simplex. Vertices are labeled by $\mathrm{Fin},5$; the lower slice is ${0,1,2}$ and the upper slice ${3,4}$, with the six cross edges timelike. Each triangular hinge is labeled by its opposite pair $(p,q)$.
The model path threeTwoCosPath p q evaluates the split-form dihedral cosine on the continued edge data of type threeTwo at the physical point $a=1$, $\alpha=1$, along the canonical upper-half-plane arc. The underlying split cosine is the ratio of the off-diagonal Cayley–Menger cofactor to the product of the two diagonal cofactors (with a fixed denominator convention).
Upstream, the generic identity dihedralCosSplitC_symm already asserts that this split cosine is symmetric in the opposite pair for arbitrary complex squared-edge data, by cofactor symmetry and commutativity of multiplication.
proof idea
Term-mode one-liner. Apply functional extensionality in the arc parameter $t$, then invoke the upstream theorem that the split-form dihedral cosine is symmetric under swap of the opposite pair, instantiated at the continued threeTwo edge data. No case split on hinge class is needed.
why it matters
Feeds directly into boundary32_symm, which transports the boundary-continuation package (continuity on $[0,1]$ plus the Lorentzian endpoint value $-1/4$) across the unordered pair. Without this symmetry one would have to re-prove continuity and the endpoint identity for every ordered pair rather than every hinge.
In the module's hinge taxonomy there are ten hinges (one spacelike, six mixed, three upper-pair). Symmetry halves the bookkeeping for the six mixed and three upper-pair classes when assembling the full branch certificate at the physical point. This is scaffolding closure inside lane B2 of the finishing charter, not a new forcing-chain step; it sits downstream of the complex-first Wick arc and the closed-form cofactor table already kernel-checked by 5×5 minors.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.