Item 120: Exhaustive sharing on trace-constitutive dockets: what exchange equalizes live sets

*Re-filed 2026-10-21 by the rebuttal-and-end-to-end round from branch round/2026-09-17-convergence-measure, where it was item 96; content unchanged; the branch round is landed under projects/normativity/seed/rounds/2026-09-17-convergence-measure/.*

H3 of the convergence-measure round holds under exhaustive sharing read as "the reasoners' live substantive-and-warrant row sets eventually coincide". Sharing every warrant does not give this: a warrant defeated on one docket and live on another is a one-sided defeater (the consensus fixture), and the landed defeat calculus fixes the live docket per trace. Say which exchange protocol — sharing warrants and their disposals, a shared docket, or a synchronization event — makes live sets coincide on DefeatTrace, state it on the existing docket types, and prove H3's eventual constancy against it in Lean (the round composes it from eventually_const_of_finite in prose).

Deliverable shape: the protocol as a predicate on a family of traces, the theorem that it equalizes liveSub ++ W, and H3 stated and proved on IntervalData from it. Acceptance check: the Lean audits clean.

Context: DYNAMICS.md §3 of the round; the seed round's CONFINEMENT.md §2 (the calculus computes no extension). Consumed by: any claim that persistent discord is never an artifact of order. A solution ships: the predicate and the two theorems.