sin_add_sub_sin

The ambient module is the Wave-4 plane-wave attachment of the Euclidean $4\times 4$ TT/gauge/transverse-trace split to axis-edge loadings on the 4-torus. Edge load of a matrix $H$ along axis $a$ is simply the diagonal entry $H_{aa}$; the midpoint plane-wave perturbation multiplies that load by $\cos(m\cdot x+m_a/2)$, matching the 3D midpoint convention.

A named target in the module header is the exact lattice identity linking matrix gauge to discrete Lie loading: for the plane-wave vertex field $\xi_b(x)=v_b\sin(m\cdot x)$, the finite difference $2(\xi_a(x+e_a)-\xi_a(x))$ expands to a product of $\sin(m_a/2)$ and a midpoint cosine. The present lemma is the pure trigonometric step that converts $\sin(\theta+\varphi)-\sin\theta$ into that product form.

It sits downstream of Mathlib's difference-of-sines formula and upstream of the discrete-Lie axis expansion; the noisy short-name import edges (active-edge counts, polarized birth interfaces, gap-2 edge complexes) are not mathematical inputs here.

One short tactic proof. Instantiate Mathlib's Real.sin_sub_sin at $A=\theta+\varphi$ and $B=\theta$, which supplies $$\sin A-\sin B=2\sin\frac{A-B}{2}\cos\frac{A+B}{2}.$$ Two ring goals identify the half-difference with $\varphi/2$ and the half-sum with $\theta+\varphi/2$. Rewrite the three equalities and close.

Feeds discreteLieAxis_eq, the exact trig expansion of discrete Lie loading on an axis edge: after unfolding the gauge vertex field and midpoint phase, the finite difference of sines is rewritten via this identity into $2 v_a\cdot(2\sin(m_a/2))\cdot\cos(\text{midpoint phase})$. That expansion is the lattice half of the module's gauge $\leftrightarrow$ discrete-Lie comparison, which then equates the matrix-gauge plane-wave edge perturbation to $(m_a/(2\sin(m_a/2)))$ times the discrete Lie loading whenever $\sin(m_a/2)\neq 0$.

In the QG campaign this is a kernel-checked increment on lane W4-1 after the algebraic EdgeTTDecomposition4D layer. It does not touch continuum Einstein-Hilbert recovery, the full ledger name edge_tt_decomposition, or gap_action_recovery; it only supplies the finite-difference trig step those later claims will need.