classDot_add
plain-language theorem explainer
Additivity of the edge-class covector pairing in its matrix argument: pairing a fixed class weight vector against the edge loads of A+B splits as the sum of the pairings against A and B. Cited when proving left-additivity of the zero-momentum true-weight bilinear form and the quadratic polarization identity. Proof is a short term rewrite: unfold the two dots, apply class-coefficient additivity, then distribute multiplication and finite sums.
Claim. For any class covector $v:\mathrm{Fin}\,15\to\mathbb{R}$ and any $A,B\in\mathrm{Mat}_4(\mathbb{R})$, if $c(H)$ denotes the edge-class coefficient covector of a matrix $H$, then $\sum_{d} v(d)\,c(A+B)_d = \sum_{d} v(d)\,c(A)_d + \sum_{d} v(d)\,c(B)_d$.
background
This module assembles the committed per-orbit star deficit kernels with Heron area gradients into the flat second-variation class quadratic of the 4D Regge action, at zero momentum only (constant edge-class perturbation). Edge classes live on Fin 15; each matrix $H$ is reduced to a class covector $c(H)$ by summing edge loads within each class.
The scalar pairing used throughout is the ordinary Euclidean dot of two class covectors, $\sum_{d:15} v_d w_d$. The object proved additive here is that pairing with $v$ fixed and $w = c(H)$ varying in $H$. Upstream, class coefficients themselves are already additive in the matrix: $c(A+B)_d = c(A)_d + c(B)_d$, via edge-load additivity on the 4D stencil.
Local deliverable A of the module includes polarization and bilinearity of the orbit-count-weighted true-weight Hessian; this lemma is the elementary linear algebra step those identities rest on.
proof idea
Unfold the definitions of the class pairing and the coefficient dot so the goal is an equality of finite sums $\sum_d v_d,c(A+B)_d = \sum_d v_d,c(A)_d + \sum_d v_d,c(B)_d$. Rewrite the summand with class-coefficient additivity, then apply real multiplication distributing over addition and the standard finite-sum additivity lemma. No case splits or geometry-specific facts beyond the already-proved additivity of class coefficients.
why it matters
In the QG full-theory campaign this module replaces the provisional weight-1 aggregate by true orbit-count weights (72/48/48/24/24/24 over the six $S_4$ types). Polarization of the resulting zero-momentum quadratic is listed as deliverable A.4; both parent results call this lemma directly.
trueWeightZeroMomBilinear_add_left unfolds the bilinear form and rewrites each orbit summand by this additivity, then pulls the sum apart. trueWeightZeroMomQuadratic_add expands the quadratic via bilinearity of the same pairing. Those identities underwrite the evaluations that true weights kill pure gauge at zero momentum (axis TT-plus, decoy gauge, and decoy trace all give 0), improving on the provisional weight-1 decoy value 32.
Scope remains zero-momentum only: finite-momentum Bloch phase folding is open, and this does not prove continuum EH recovery or flip gap-action recovery.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.