From 5048b6b28d929d9990b5e88bb745de2f62e1f438 Mon Sep 17 00:00:00 2001 From: Quang Dao Date: Fri, 28 Aug 2026 21:31:07 -0700 Subject: [PATCH] feat(uc): lift scheduled draws through factorization --- PolyFun.lean | 1 + .../UC/ScheduledSamplerFactorization.lean | 280 ++++++++++++++++++ docs/wiki/repo-map.md | 5 + docs/wiki/uc.md | 5 +- 4 files changed, 290 insertions(+), 1 deletion(-) create mode 100644 PolyFun/Interaction/UC/ScheduledSamplerFactorization.lean diff --git a/PolyFun.lean b/PolyFun.lean index 6ff0b49..f04a82d 100644 --- a/PolyFun.lean +++ b/PolyFun.lean @@ -133,6 +133,7 @@ public import PolyFun.Interaction.UC.OpenTheory.Family public import PolyFun.Interaction.UC.Realizability public import PolyFun.Interaction.UC.SamplerObservation public import PolyFun.Interaction.UC.ScheduledOpenProcessModel +public import PolyFun.Interaction.UC.ScheduledSamplerFactorization public import PolyFun.Interaction.UC.Scheduler public import PolyFun.Interaction.UC.SecureEmulation public import PolyFun.Interaction.UC.SubTheory diff --git a/PolyFun/Interaction/UC/ScheduledSamplerFactorization.lean b/PolyFun/Interaction/UC/ScheduledSamplerFactorization.lean new file mode 100644 index 0000000..103376f --- /dev/null +++ b/PolyFun/Interaction/UC/ScheduledSamplerFactorization.lean @@ -0,0 +1,280 @@ +/- +Copyright (c) 2026 PolyFun Contributors. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Quang Dao +-/ + +module + +import all PolyFun.Interaction.UC.OpenProcessSamplerFactorization +import all PolyFun.Interaction.UC.Scheduler +public import PolyFun.Interaction.UC.OpenProcessSamplerFactorization +public import PolyFun.Interaction.UC.Scheduler + +/-! +# Path-sampler factorization for mass-aware scheduling + +The structural UC factorization maps already identify the leaves of the +source and reassociated binary process trees. This module proves the missing +sampler statement for the mass-aware scheduler: after applying those path +maps, both hierarchical samplers bind the same component sampler whenever the +binary scheduler satisfies `BinaryScheduler.IsCoherent`. + +This is the generic bridge between the scheduler algebra and process-level UC +factorization. It remains independent of probability; downstream models only +need to prove the scheduler coherence law for their observation relation. +-/ + +public section + +universe w w' + +namespace Interaction +namespace UC + +open Concurrent OpenProcessFactorization + +namespace BinaryScheduler + +/-- Binding the source-shaped mass-aware draw against a continuation exposes +the two scheduler calls used by the nested process sampler. -/ +theorem sourceDraw_bind {m : Type w → Type w'} [Monad m] [LawfulMonad m] + (scheduler : BinaryScheduler m) (first second context : ScheduleMass) + {α : Type w} (h : ULift.{w, 0} Leaf → m α) : + sourceDraw scheduler first second context >>= h = + scheduler (first + second) context >>= fun outer => + if outer.down then + scheduler first second >>= fun inner => + if inner.down then h ⟨.first⟩ else h ⟨.second⟩ + else + h ⟨.context⟩ := by + simp only [sourceDraw, bind_assoc] + refine bind_congr fun outer => ?_ + obtain ⟨choice⟩ := outer + cases choice + · simp only [Bool.false_eq_true, ↓reduceIte, pure_bind] + · simp only [↓reduceIte, bind_assoc] + refine bind_congr fun inner => ?_ + obtain ⟨choice⟩ := inner + cases choice <;> simp only [Bool.false_eq_true, ↓reduceIte, pure_bind] + +/-- Binding the left-factored mass-aware draw exposes the scheduler calls used +by the left-reassociated process sampler. -/ +theorem leftDraw_bind {m : Type w → Type w'} [Monad m] [LawfulMonad m] + (scheduler : BinaryScheduler m) (first second context : ScheduleMass) + {α : Type w} (h : ULift.{w, 0} Leaf → m α) : + leftDraw scheduler first second context >>= h = + scheduler first (context + second) >>= fun outer => + if outer.down then + h ⟨.first⟩ + else + scheduler context second >>= fun inner => + if inner.down then h ⟨.context⟩ else h ⟨.second⟩ := by + simp only [leftDraw, bind_assoc] + refine bind_congr fun outer => ?_ + obtain ⟨choice⟩ := outer + cases choice + · simp only [Bool.false_eq_true, ↓reduceIte, bind_assoc] + refine bind_congr fun inner => ?_ + obtain ⟨choice⟩ := inner + cases choice <;> simp only [Bool.false_eq_true, ↓reduceIte, pure_bind] + · simp only [↓reduceIte, pure_bind] + +/-- Binding the right-factored mass-aware draw exposes the scheduler calls +used by the right-reassociated process sampler. -/ +theorem rightDraw_bind {m : Type w → Type w'} [Monad m] [LawfulMonad m] + (scheduler : BinaryScheduler m) (first second context : ScheduleMass) + {α : Type w} (h : ULift.{w, 0} Leaf → m α) : + rightDraw scheduler first second context >>= h = + scheduler second (context + first) >>= fun outer => + if outer.down then + h ⟨.second⟩ + else + scheduler context first >>= fun inner => + if inner.down then h ⟨.context⟩ else h ⟨.first⟩ := by + simp only [rightDraw, bind_assoc] + refine bind_congr fun outer => ?_ + obtain ⟨choice⟩ := outer + cases choice + · simp only [Bool.false_eq_true, ↓reduceIte, bind_assoc] + refine bind_congr fun inner => ?_ + obtain ⟨choice⟩ := inner + cases choice <;> simp only [Bool.false_eq_true, ↓reduceIte, pure_bind] + · simp only [↓reduceIte, pure_bind] + +end BinaryScheduler + +/-! ## Reassociated path samplers -/ + +/-- The source-shaped and left-factored nested path samplers are related after +applying the structural left-reassociation path equivalence. -/ +theorem samplePath_interleave_assoc_left {m : Type w → Type w'} + [Monad m] [LawfulMonad m] (R : MonadRelFamily m) + (scheduler : BinaryScheduler m) (coherent : scheduler.IsCoherent R) + (firstMass secondMass contextMass : ScheduleMass) + (firstTree secondTree contextTree : TypeTree.{w}) + (firstSampler : TypeTree.Sampler m firstTree) + (secondSampler : TypeTree.Sampler m secondTree) + (contextSampler : TypeTree.Sampler m contextTree) : + R.rel + ((fun path => parLeftPathEquiv firstTree secondTree contextTree path) <$> + TypeTree.samplePath _ + (TypeTree.Sampler.interleave + (scheduler (firstMass + secondMass) contextMass) + (TypeTree.Sampler.interleave (scheduler firstMass secondMass) + firstSampler secondSampler) + contextSampler)) + (TypeTree.samplePath _ + (TypeTree.Sampler.interleave + (scheduler firstMass (contextMass + secondMass)) firstSampler + (TypeTree.Sampler.interleave (scheduler contextMass secondMass) + contextSampler secondSampler))) := by + let continuation : ULift.{w, 0} Leaf → + m (TypeTree.Path (TypeTree.node (ULift.{w, 0} Bool) fun + | ⟨true⟩ => firstTree + | ⟨false⟩ => TypeTree.node (ULift.{w, 0} Bool) fun + | ⟨true⟩ => contextTree + | ⟨false⟩ => secondTree)) := fun leaf => + match leaf with + | ⟨.first⟩ => TypeTree.samplePath _ firstSampler >>= fun path => + pure ⟨⟨true⟩, path⟩ + | ⟨.second⟩ => TypeTree.samplePath _ secondSampler >>= fun path => + pure ⟨⟨false⟩, ⟨⟨false⟩, path⟩⟩ + | ⟨.context⟩ => TypeTree.samplePath _ contextSampler >>= fun path => + pure ⟨⟨false⟩, ⟨⟨true⟩, path⟩⟩ + have source_eq : + ((fun path => parLeftPathEquiv firstTree secondTree contextTree path) <$> + TypeTree.samplePath _ + (TypeTree.Sampler.interleave + (scheduler (firstMass + secondMass) contextMass) + (TypeTree.Sampler.interleave (scheduler firstMass secondMass) + firstSampler secondSampler) + contextSampler)) = + BinaryScheduler.sourceDraw scheduler firstMass secondMass contextMass >>= + continuation := by + rw [BinaryScheduler.sourceDraw_bind] + simp only [TypeTree.Sampler.interleave, TypeTree.samplePath, map_bind] + refine bind_congr fun outer => ?_ + obtain ⟨choice⟩ := outer + cases choice + · simp only [Bool.false_eq_true, ↓reduceIte, map_pure] + rfl + · simp only [↓reduceIte, TypeTree.samplePath, bind_assoc, map_pure, + pure_bind] + refine bind_congr fun inner => ?_ + obtain ⟨choice⟩ := inner + cases choice <;> rfl + have target_eq : + TypeTree.samplePath _ + (TypeTree.Sampler.interleave + (scheduler firstMass (contextMass + secondMass)) firstSampler + (TypeTree.Sampler.interleave (scheduler contextMass secondMass) + contextSampler secondSampler)) = + BinaryScheduler.leftDraw scheduler firstMass secondMass contextMass >>= + continuation := by + rw [BinaryScheduler.leftDraw_bind] + simp only [TypeTree.Sampler.interleave, TypeTree.samplePath] + refine bind_congr fun outer => ?_ + obtain ⟨choice⟩ := outer + cases choice + · simp only [Bool.false_eq_true, ↓reduceIte, TypeTree.samplePath, bind_assoc, + pure_bind] + refine bind_congr fun inner => ?_ + obtain ⟨choice⟩ := inner + cases choice <;> rfl + · simp only [↓reduceIte] + rfl + have draws_related := R.bind_congr continuation + (coherent.left firstMass secondMass contextMass) + exact Eq.mp + (congrArg₂ (fun left right => R.rel left right) + source_eq.symm target_eq.symm) + draws_related + +/-- The source-shaped and right-factored nested path samplers are related after +applying the structural right-reassociation path equivalence. -/ +theorem samplePath_interleave_assoc_right {m : Type w → Type w'} + [Monad m] [LawfulMonad m] (R : MonadRelFamily m) + (scheduler : BinaryScheduler m) (coherent : scheduler.IsCoherent R) + (firstMass secondMass contextMass : ScheduleMass) + (firstTree secondTree contextTree : TypeTree.{w}) + (firstSampler : TypeTree.Sampler m firstTree) + (secondSampler : TypeTree.Sampler m secondTree) + (contextSampler : TypeTree.Sampler m contextTree) : + R.rel + ((fun path => parRightPathEquiv firstTree secondTree contextTree path) <$> + TypeTree.samplePath _ + (TypeTree.Sampler.interleave + (scheduler (firstMass + secondMass) contextMass) + (TypeTree.Sampler.interleave (scheduler firstMass secondMass) + firstSampler secondSampler) + contextSampler)) + (TypeTree.samplePath _ + (TypeTree.Sampler.interleave + (scheduler secondMass (contextMass + firstMass)) secondSampler + (TypeTree.Sampler.interleave (scheduler contextMass firstMass) + contextSampler firstSampler))) := by + let continuation : ULift.{w, 0} Leaf → + m (TypeTree.Path (TypeTree.node (ULift.{w, 0} Bool) fun + | ⟨true⟩ => secondTree + | ⟨false⟩ => TypeTree.node (ULift.{w, 0} Bool) fun + | ⟨true⟩ => contextTree + | ⟨false⟩ => firstTree)) := fun leaf => + match leaf with + | ⟨.first⟩ => TypeTree.samplePath _ firstSampler >>= fun path => + pure ⟨⟨false⟩, ⟨⟨false⟩, path⟩⟩ + | ⟨.second⟩ => TypeTree.samplePath _ secondSampler >>= fun path => + pure ⟨⟨true⟩, path⟩ + | ⟨.context⟩ => TypeTree.samplePath _ contextSampler >>= fun path => + pure ⟨⟨false⟩, ⟨⟨true⟩, path⟩⟩ + have source_eq : + ((fun path => parRightPathEquiv firstTree secondTree contextTree path) <$> + TypeTree.samplePath _ + (TypeTree.Sampler.interleave + (scheduler (firstMass + secondMass) contextMass) + (TypeTree.Sampler.interleave (scheduler firstMass secondMass) + firstSampler secondSampler) + contextSampler)) = + BinaryScheduler.sourceDraw scheduler firstMass secondMass contextMass >>= + continuation := by + rw [BinaryScheduler.sourceDraw_bind] + simp only [TypeTree.Sampler.interleave, TypeTree.samplePath, map_bind] + refine bind_congr fun outer => ?_ + obtain ⟨choice⟩ := outer + cases choice + · simp only [Bool.false_eq_true, ↓reduceIte, map_pure] + rfl + · simp only [↓reduceIte, TypeTree.samplePath, bind_assoc, map_pure, + pure_bind] + refine bind_congr fun inner => ?_ + obtain ⟨choice⟩ := inner + cases choice <;> rfl + have target_eq : + TypeTree.samplePath _ + (TypeTree.Sampler.interleave + (scheduler secondMass (contextMass + firstMass)) secondSampler + (TypeTree.Sampler.interleave (scheduler contextMass firstMass) + contextSampler firstSampler)) = + BinaryScheduler.rightDraw scheduler firstMass secondMass contextMass >>= + continuation := by + rw [BinaryScheduler.rightDraw_bind] + simp only [TypeTree.Sampler.interleave, TypeTree.samplePath] + refine bind_congr fun outer => ?_ + obtain ⟨choice⟩ := outer + cases choice + · simp only [Bool.false_eq_true, ↓reduceIte, TypeTree.samplePath, bind_assoc, + pure_bind] + refine bind_congr fun inner => ?_ + obtain ⟨choice⟩ := inner + cases choice <;> rfl + · simp only [↓reduceIte] + rfl + have draws_related := R.bind_congr continuation + (coherent.right firstMass secondMass contextMass) + exact Eq.mp + (congrArg₂ (fun left right => R.rel left right) + source_eq.symm target_eq.symm) + draws_related + +end UC +end Interaction diff --git a/docs/wiki/repo-map.md b/docs/wiki/repo-map.md index ec4247b..be47ab2 100644 --- a/docs/wiki/repo-map.md +++ b/docs/wiki/repo-map.md @@ -269,6 +269,11 @@ Interaction/UC/{OpenProcessModel, Scheduler} additive mass-aware open-process theory; concrete proportional sampling and distributional adequacy remain downstream) +Interaction/UC/{OpenProcessSamplerFactorization, Scheduler} + -> Interaction/UC/ScheduledSamplerFactorization + (the scheduler coherence law lifted through arbitrary component samplers + along the existing left/right structural path reassociations) + Interaction/UC/{OpenProcessModel, OpenProcessFactorization, OpenProcessSamplerEquiv} -> Interaction/UC/OpenProcessSamplerFactorization diff --git a/docs/wiki/uc.md b/docs/wiki/uc.md index 23bae7e..414a550 100644 --- a/docs/wiki/uc.md +++ b/docs/wiki/uc.md @@ -122,7 +122,10 @@ relation family `MonadRelFamily` atomic frontier, binary nodes receive both subtree masses, and a downstream scheduler proves that all hierarchical three-way draws denote one flat choice. Probability and the concrete proportional scheduler remain VCVio - responsibilities. + responsibilities. `samplePath_interleave_assoc_left` and + `samplePath_interleave_assoc_right` lift the resulting coherence law through + arbitrary component samplers along the existing structural path + reassociations. 2. **Initial-state correspondence.** The totality fields of `OpenProcessSamplerEquiv` expose the regrouping bijection on states, so corresponding initial states are chosen definitionally.