Repository navigation
[FORM-S13] Optimal pooling and Dobrushin consensus for collective inference (fep-110..113) #96
Description
Scope ID: FORM-S13. Size: Medium. Scoped on 2026-10-08 in SCOPE-2026-10-08.md; acceptance remains open.
Owner: collective-inference bodies.
Dependencies: FORM-D3
Work
Consensus uses one fixed 2-agent mixing matrix and fep-110's pooled mass is rfl. Prove the log-pool and linear pool are the unique minimisers of the two weighted-KL objectives (via the Gibbs principle), and Dobrushin contraction for any scrambling row-stochastic W.
Acceptance
A 3-agent asymmetric W witness and a non-scrambling countermodel; the fixed 2-agent kernel is an instance.
Failure controls and claim boundary
No disposition promotion from compilation, import or numerical agreement; the maturity record changes only after independent semantic review. No duplicate topics and no automatic sealed-roster expansion.
Canonical references
Closure requires actual exact-source commands, results and retained receipts, with independent review where specified. Remove its open TODO row only after acceptance; retain delivery facts in changelog/history. Size describes implementation scope, not a semantic-version promise.
Activity
docxology commentedon Oct 9, 2026
Status update (2026-10-09). Delivered in #162 (via #164), merged to
main: Linear-pool and log-pool KL decompositions with unique-minimiser theorems, Dobrushin contractionspread(Wx) ≤ (1−δ)·spread(x)for any finite row-stochastic W, the existing 2-agent kernel as an instance, an asymmetric 3-agent strict-contraction witness, and an identity countermodel.Evidence:
lake --wfail build FepSketchespasses at the pin (Lean v4.34.1, Mathlibd13f23b7), every new declaration depends only onpropext/Classical.choice/Quot.sound, and all generator--checks plus hosted CI pass.Remaining for closure: independent semantic review of the delivered statements against the topic's theorem proxy. Per this issue's claim boundary, no disposition in
config/theorem_maturity.yamlwas changed, and none may change without that review.docxology commentedon Oct 11, 2026
Accepted on
mainvia #171. InFEP.CollectiveInference:linearPool_kl_unique_minimiserandlogPool_kl_unique_minimiser;valueSpread_mixStep_lefor any row-stochastic W; the 3-agent asymmetric witnessasymMatrix3_strict_contraction; the non-scrambling countermodelidentityMixing2_no_contraction; and the 2-agent kernel as an instance (consensus_spread_le_half). Any maturity change still needs independent review. Row retired.