Successor problems

problems{ P1. Necessity of the record equation. Does a strategy in Assumption ass:strategy-class satisfy $(\mathrm{C}{)}^{\star },(\mathrm{NS}{)}^{\star },(\mathrm{N}{)}^{\star },(\mathrm{K}{)}^{\star }$ but fail $(\mathrm{R}{)}^{\star }$? Separate: (i) possible freedom in coherent outcome laws; and (ii) possible freedom in conditional updates once the complete Born outcome law is fixed. No equivalence between these subquestions is presumed.

P2. A weaker route to record-free uniqueness. Without assuming the record equation, can a strictly weaker, independently motivated operational condition identify coherent laws and updates from diagonal anchoring? The fixed language already defines the record term using allocation and CNOT. Removing that definable construction would change the structural problem. “Record-free” here means omitting its observational equation.

P3. Internal context-refinement discipline. Add syntax for observer judgments, refinement certificates, and permitted transports. Under a specified encoding, prove soundness and underivability of the Frauchiger–Renner certainty chain. Section sec:contexts supplies the finite projector obstruction, not this internalization.}