docs(formal-model): add weight renormalisation remark to def:agg-drift

Applies foldback from verisim-modular-experiment (FOLDBACK.adoc item 2).

When a federation operates over a subset modset' ⊊ modset of modalities,
aggregate-drift comparisons require per-federation weight renormalisation
ŵ_{m1,m2} = w_{m1,m2} / Σ w_{m'1,m'2} over {m'1,m'2} ⊆ modset'. Without
this, PROOF CONSISTENCY thresholds shift silently between full-octad and
partial-octad federations.

The per-octad d(·,⊥)=0 convention is sound; this remark addresses the
complementary aggregate-comparison concern across federations with
different modality subsets.

Source: nextgen-databases/verisim-modular-experiment/docs/FOLDBACK.adoc

Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>

Author: hyperpolymath

arcvix-octad-data-model.tex

@@ -502,6 +502,30 @@ \subsection{Formal Drift Metrics}
 In practice, not all pairs have meaningful distance functions; we define
 metrics for the most important pairs.
 
+\begin{remark}[Per-federation weight renormalisation]\label{rem:agg-drift-renorm}
+When a federation or deployment operates over a subset
+$\modset' \subsetneq \modset$ of modalities, Definition~\ref{def:agg-drift}
+must be applied with care. The per-octad convention
+$d_{m_1, m_2}(\cdot, \bot) = 0$ from
+Definition~\ref{def:pairwise-drift} handles \emph{per-octad} absence
+soundly --- each absent modality contributes zero drift to its pairs.
+However, for aggregate-drift comparisons to remain meaningful
+\emph{across federations} with different modality subsets, the weights
+must be renormalised over the pairs actually present:
+\[
+  \widehat{w}_{m_1, m_2} = \frac{w_{m_1, m_2}}{\sum_{\{m'_1, m'_2\} \subseteq \modset'} w_{m'_1, m'_2}},
+  \quad \text{for } \{m_1, m_2\} \subseteq \modset',
+\]
+so that $\sum_{\{m_1, m_2\} \subseteq \modset'} \widehat{w}_{m_1, m_2} = 1$.
+Without this renormalisation, thresholds in downstream judgements (e.g.\
+\texttt{PROOF CONSISTENCY}) shift silently between full-octad and
+partial-octad federations, since absent-pair weights effectively vanish
+from the denominator. Equivalently, absent-pair weights may be treated
+as contributing to a \emph{no-drift term}; the two formulations agree
+when the $d_{m_1, m_2}(\cdot, \bot) = 0$ convention is combined with
+renormalisation over $\modset'$.
+\end{remark}
+
 \subsection{Modality-Pair Distance Functions}\label{sec:drift-metrics}
 
 \paragraph{Vector--Document drift ($d_{\mathsf{V},\mathsf{D}}$).}