Audit per-axis lattices for structural-vs-lattice Eq mismatches (PR 4b-D.2 D24 follow-up)

[bashandbone]

PR 4b-D.2 commit 11 (decisions.md D24) dropped impl JoinSemilattice for CapcoMarking + impl MeetSemilattice for CapcoMarking after Copilot R1 surfaced an idempotence-law violation driven by RelToBlock's tetragraph expansion. The lattice consultant's verdict was Option D-extended: cross-axis folds are projections, not lattice ops; the lattice claim moves to the per-axis types.

The D24 fix is surgical — it removes the false claim at the cross-axis layer. The remaining per-axis types still need a systematic audit for the same structural-vs-lattice-Eq mismatch pattern. PR #456 already split Lattice into JoinSemilattice + MeetSemilattice halves and identified several per-axis types as carrying observational state:

DissemSet, JointSet, and SupersessionSet implement only JoinSemilattice (these types have join-side observational state — relido_observed_unanimous, Mixed/DisunityCollapse, and the post-join supersession overlay — that makes meet either undefined or non-idempotent).

The systematic-audit question this issue tracks:

1. DissemSet::relido_observed_unanimous: does this flag survive join(a, a) == a on the join side? PR marque-scheme: split Lattice into JoinSemilattice+MeetSemilattice OR weaken DissemSet/JointSet trait impls #456 retired the meet impl; the join side needs proptest coverage analogous to the new RelToBlock laws in crates/capco/tests/proptest_lattice.rs.

2. JointSet::Mixed / DisunityCollapse: do these variants preserve idempotence on structural Eq? DisunityCollapse carries a non-US producer set; if from_attrs_iter normalizes the producer list, the same expand-on-construct hazard RelToBlock had may apply.

3. SupersessionSet: the post-join overlay state — does the overlay re-application on join(a, a) produce structurally-equal output? Or does the overlay introduce a non-idempotent transformation that's hidden by the current test surface (only covered in fixed-sample tests, no proptests)?

Acceptance criteria

For each of the three per-axis types above:

• Add a proptest in crates/capco/tests/proptest_lattice.rs covering the join laws (idempotence/commutativity/associativity) on the type's own structural Eq.
• If any law fails, file the failure with a counterexample and propose either (a) a representation change to make the law hold, (b) a stronger structural Eq impl that ignores the observational state for the lattice claim, or (c) a documented "this is not actually a lattice — drop the impl per D24 precedent" verdict.
• Verify the test suite is green post-audit.

Related

• PR marque-scheme: split Lattice into JoinSemilattice+MeetSemilattice OR weaken DissemSet/JointSet trait impls #456 (Join/Meet split + observational-state framing)
• PR 4b-D.2 commit 11 / decisions.md D24 (CapcoMarking trait removal)
• marque-applied.md §3 (PR 3b stall walkthrough — the framing this issue extends)
• crates/capco/tests/proptest_lattice.rs::rel_to_* (the proptest template the audit should follow)

Scope notes

• NOT in scope: revisiting whether per-axis lattices SHOULD have observational state. The state is load-bearing for §H.8 pp155-156 RELIDO unanimity, §H.3 p57 JOINT disunity, etc. The audit asks "is the trait claim sound given the state we keep?" not "should we keep the state?"
• NOT in scope: CapcoMarking itself (resolved by D24).
• Out-of-scope per PR brief: This work was deferred from PR 4b-D.2 to a follow-up PR per Constitution VII scope-discipline.

[bashandbone]

closed by #538