Item 105: Belief–decision compatibility: W1 as a theorem of record, and the unresolved implication

projects/decision-theory/rounds/2026-09-29-li-bria-synthesis-spec/PROBLEM_STATEMENT.md §5 states the compatibility relation in two forms. The established form W1: under LI recovery relative to the observation stream (M2(c), item 91), a post-selection forecast F⁺_k of the selected option's realized score published as a market state after the selection is in the stream, and settlement within a computable deferral, limsup (1/K) Σ_{k≤K} (e_k − F⁺_k) ≤ 0 — from no overestimation and thm:wubaff on the trivial weighting. The strong form: the same on every P-generable weighting. The first pass's derivation of the strong form from M2(c) and M3 is invalid (the subsequence gap; the cumulative-loss gap, repaired by ε-shifted bidders; the access gap — a weighting must be computable at forecast time, so a selection-based weighting serves post-selection forecasts and serves pre-selection forecasts only where the selection is predictable from the market state, and publicity of the selection does not make an internal test set recognizable; the semantic gap — a forecast for an unselected option settles against nothing), and no countermodel to the implication exists: its status is unresolved. Two deliverables. (i) W1 as a statement of record with its hypotheses exact and its witness (the paper's auction over a logical inductor on a finite environment). (ii) The implication settled: a proof under added hypotheses (weighted no-overestimation; a sound market-reading bidder for the selected option on a recognizable test set), or a countermodel — the belief-disagreement environment A1 of §7 is the candidate for one.

Deliverable shape: paper-level theorems with named hypotheses and witnesses; Lean for the algebraic core where the pinned formalization admits it; or the countermodel with its fixture. Acceptance check: python3 tests/run.py green; Lean audits clean if any. Context: the round's PROBLEM_STATEMENT.md §3, §5, §7 (A1); TEST_SUITE.md T11; the cross-subsidy and heads-tracker fixtures in projects/decision-theory/rounds/2026-09-29-li-bria-synthesis-spec/tests/test_cm.py; items 91, 102. Consumed by: item 106; item 102 (a bid checked against prices is the strong form's lower half stated on priced claims). A solution ships: W1 of record and the implication's status, either way.