Formal: optimal linear and log pooling, Dobrushin consensus contraction (FORM-S13)

[docxology]

Refs #96 (FORM-S13). Not closing: fep-110..113 dispositions change only after independent review.

Collective inference used one fixed two-agent mixing matrix, and fep-110's pooled mass was rfl. New section in collective_inference.lean (39 declarations):

(a) The linear pool is the KL-optimal consensus.

• linearPool_kl_decomposition: ∑wᵢ KL(pᵢ‖q) = ∑wᵢ KL(pᵢ‖q*) + KL(q*‖q) for q* = ∑wᵢpᵢ.
• linearPool_kl_minimal and linearPool_kl_unique_minimiser: q* is the minimiser, uniquely.

(b) The log pool (product of experts) is optimal for the reverse objective.

• logPool_kl_decomposition: ∑wᵢ KL(q‖pᵢ) = KL(q‖q_log) − log Z.
• logPool_kl_minimal and logPool_kl_unique_minimiser.
• This explains why each pool is the right consensus, depending on which way the KL runs.

(c) Dobrushin contraction for any row-stochastic W on any finite set of agents.

• valueSpread_mixStep_le: spread(Wx) ≤ (1 − δ)·spread(x), where δ is the scrambling coefficient min_{i,j} ∑ₖ min(W_ik, W_jk).
• valueSpread_mixStep_lt: strict contraction when δ > 0.
• Only unit row sums are needed.

(d) Witnesses.

• consensus_spread_le_half: the existing ¼/¾ two-agent kernel is an instance with δ ≥ ½.
• asymMatrix3_strict_contraction: an asymmetric 3-agent W with δ ≥ 3/5 strictly contracts (1,0,0).
• identityMixing2_no_contraction: the identity has δ = 0 and no contraction, so the scrambling hypothesis is necessary.

Evidence:

• lake --wfail build FepSketches passes, and all 39 declarations use only the standard three axioms.
• Projections were regenerated by their owners, and every --check passes, as do check_render_log --verify-receipt, theorem_ref_audit and check_orphan_compiles.
• Pins: collective_inference 13 → 41, lexical 1,953 → 1,981.
• 181 tests and ruff pass.