feat(uc): sampler-level coherence shapes and the scheduled theory's laws

[dtumad]

One commit on top of dtumad/uc-activation-coherence: the coherence shapes of the previous PR, now up to OpenProcessSamplerEquiv R, and the laws of the mass-aware scheduled theory as their instances.

OpenProcessSamplerCoherence.lean proves the shapes of interleave up to OpenProcessSamplerEquiv R (left and right plug factorization, commutation, re-homing, and a derived reassociation) for identically decorated leaves and internal scheduler nodes, with the two nested scheduler draws of a regrouping as the only transport hypothesis. Draws take two samplers per nesting so that the shared sampler of openTheory and the mass-dependent samplers of scheduledOpenTheory are both instances. Sampler equivalence is a congruence for interleave and mapHom once the relation family is bind-congruent on the right (MonadRelFamily.IsBindCongr; instances for eq and top) and the injections relabel traces (OpenNodeContext.EmitsAlong).

OpenProcessSamplerFactorization.lean becomes instances of the shapes with its hypotheses unchanged, plus the congruence laws of the theory. ScheduledSamplerFactorization.lean identifies the mass-aware draws with the nested draws, restates IsCoherent in the form the shapes consume, proves the five plug laws of scheduledOpenTheory from coherence alone, and packages them as Observation.scheduledSampler respecting factorization; scheduledOpenTheory is now IsLawful.

Public API delta

• New module Interaction/UC/OpenProcessSamplerCoherence: the shapes interleave_factorLeft_samplerEquiv, interleave_factorRight_samplerEquiv, interleave_comm_samplerEquiv, interleave_rehome_samplerEquiv, interleave_assoc_samplerEquiv; the congruences OpenProcess.interleave_congr_{left,right}_samplerEquiv, OpenProcess.mapHom_congr_samplerEquiv; the nested draws nestedDrawLeft, nestedDrawFactorLeft, nestedDrawFactorRight with their _bind lemmas; the path equivalences leftBranchPathEquiv, rightBranchPathEquiv and the named trees nestedLeftTree, factorLeftTree, factorRightTree.
• Moved with names kept: schedulerFlip (and its _up_* lemmas), flipInterleavePathEquiv, parLeftPathEquiv, parRightPathEquiv, samplePath_interleave_flip, samplePath_interleave_congr_scheduler, and OpenProcessFactorization.Leaf to OpenProcessSamplerCoherence; OpenNodeContext.IsInternalNode, OpenNodeContext.EmitsAlong (exposed; instances for the six structural homs and composition), and boundaryTrace_map_of_emitsAlong to OpenProcessInterleave; the silence and boundary-trace unfoldings of composite-step branches to OpenProcessCoherence; PFunctor.TraceList.mapPartial (with mapPartial_one, mapPartial_mul) to PFunctor/Trace.
• New class MonadRelFamily.IsBindCongr with instances for MonadRelFamily.eq and MonadRelFamily.top.
• OpenProcessSamplerFactorization: the five openTheory_plug_*_sampler_equiv laws and openTheory_{par_comm,par_assoc,wire_comm}_sampler_equiv keep their statements and hypotheses; new openTheory_{map,par,wire,plug}_congr_{left,right}_sampler_equiv; closed-composite (close_comp_*) and tensor-reindexing lemmas the instances use.
• ScheduledSamplerFactorization: BinaryScheduler.{sourceDraw_eq_nestedDrawLeft, leftDraw_eq_nestedDrawFactorLeft, rightDraw_eq_nestedDrawFactorRight}, BinaryScheduler.IsCoherent.{flip_rel, nestedDrawLeft_rel_factorLeft, nestedDrawLeft_rel_factorRight}, scheduledOpenTheory_plug_{comm,par_left,par_right,wire_left,wire_right}_sampler_equiv, Observation.scheduledSampler, Observation.respectsFactorization_scheduledSampler; samplePath_interleave_assoc_{left,right} and the *Draw_bind lemmas keep their statements. scheduledOpenTheory gains IsLawful.
• Nothing public is removed beyond the moves.

Semantics

• The hypotheses of the sampler shapes are "the composite injections are equal per leaf" (ContextHom.comp g₁ f₁ = g₁' and so on), scheduler nodes that are IsInternalNode (including re-decorated ones), and one draw relation. This is stronger than necessary (equal boundaries would do) but it is the literal content of "a regrouping only moves scheduler nodes", and every instance in the model is rfl-level or a tensor reindexing.
• IsBindCongr is needed only by the congruence theorems and the derived par_assoc; the plug laws, IsCoherent, and everything VCVio #572 consumes need nothing new. VCVio's outputRel (equality of output distributions) should satisfy it, since bind with pointwise output-equal continuations gives equal output distributions; that is to be checked when VCVio bumps its pin (to note on VCVio#633).
• BinaryScheduler.{sourceDraw, leftDraw, rightDraw}, IsFlat, IsCoherent, scheduledOpenTheory, and the MonadRelFamily fields are unchanged; codex/uc-scheduler-denotation (VCVio #572) uses exactly these plus the _bind lemmas of ScheduledSamplerFactorization, which keep their statements.
• The unit and zig-zag laws have no sampler-level version (ledger row in uc.md). A new gotchas.md entry records why the tree shapes are named abbreviations: pattern-matching lambdas inside statements elaborate to declaration-local matchers, so rw and simp cannot match them across declarations.

Tests

• Ordinary-import canaries in PolyFunTest/ModuleAPI/Interaction.lean: nestedDrawLeft_bind, IsBindCongr.bind_congr_right, interleave_comm_samplerEquiv, respectsFactorization_scheduledSampler, openTheory_wire_comm_sampler_equiv.
• PolyFunTest/Interaction/UC/SamplerCoherenceExamples.lean: the shapes on both instances, openTheory (laws conditional on the scheduler-transport facts) and scheduledOpenTheory (laws from IsCoherent alone); at MonadRelFamily.top every hypothesis is trivial, so both sampler observations respect factorization outright and the whole Emulates suite applies; sampler equivalence is a congruence for the theory at the exact and forgetful families.

Validation

• Rebased linearly onto dtumad/uc-activation-coherence (itself on main at e4099b4). The Lean sources are byte-identical to the version validated during development; only the wiki ledger row and the canary file were merged.
• At this tip: git diff --check, scripts/check-imports.sh, scripts/check-modules.sh, both docs-integrity checks, lake build && lake test.
• ./scripts/validate.sh --lint --test --axioms at the tip of the stack (dtumad/uc-quotient-theory, which contains this PR): lint passes for PolyFun and ToCslib; the axiom sweep reports 11255 declarations across 291 modules with zero sorry and zero non-standard axioms.
• The base-branch-filtered workflows only run for PRs against main; CI for this head is dispatched manually with gh workflow run.

Audit note

• Attacked: whether one draw relation suffices for both plug factorizations (it does, with the flipped draw for the right one); whether the congruence needs bind-congruence on both sides (only the right; the left is never rebound); whether the shared-sampler instance and the mass-aware instance can share the shapes (two samplers per nesting); whether EmitsAlong holds for the composite injections (instances and .comp).
• Hardened: scheduledOpenTheory is now IsLawful with its five plug laws proved from coherence alone; the sampler-aware laws of openTheory no longer carry their own path-bijection proofs.
• Outside the result: unit and zig-zag laws at sampler equivalence (impossible); a derived par_assoc without IsBindCongr; any probabilistic instance (VCVio).

Stack

2 of 3: dtumad/uc-activation-coherence → this PR → dtumad/uc-quotient-theory. Based on dtumad/uc-activation-coherence; review this PR's single commit only, and merge it after its base, once it is retargeted to main.

🤖 Generated with Claude Code

https://claude.ai/code/session_01EtHsoefgvyzMtfdyqjLVhT