Joint continuation values in zero-sum extensive-form games: a history-value obstruction and aggregate convexity

Working draft 2 for public review; not peer reviewed. We distinguish jointly realizable frontier-history continuation values from conditional own-information-set aggregates. An explicit hidden-label example gives a nonconvex continuous history-value class on a singleton input domain, with positive frontier reach and fully mixed witnesses. The aggregate theorem proves convexity of the class of existing continuous selections under explicit augmented-recall, own-activity and public-trunk assumptions. It does not assert selection existence or convexity of every boundary fiber. The positive-support convexity mechanism follows from standard zero-sum equilibrium geometry once the game-specific root-value correspondence is supplied. No priority for that mechanism is claimed. Interpretation of Problem A.2 and novelty remain open to review; a general translation for arbitrary stopping trunks and off-path counterfactual conditions is not established here. This revision clarifies the definitions and realization-plan constraints, displays the bilinear payoff formulas, gives a direct saddle-mixture proof, and makes the prior-art discussion more conservative. The v6 finite-game certificate is unchanged. A separate saddle-mixture addendum contains two checked generic Lean lemmas with explicit hypotheses and reproduction instructions. Supplementary exact-rational checks accompany the calculation of the original paper's example, which already implies unrestricted history nonconvexity. Substantial AI assistance is disclosed. Lean checks establish the encoded statements, not their interpretation or novelty. No independent researcher endorsement is claimed. Feedback on definition mismatches, omitted premises, proof errors, reproduction failures and equivalent prior results is welcome. The manuscript and LaTeX source are licensed CC BY 4.0. The code retains its stated notices; no additional software license is introduced.