Repository navigation
[4/7] Refinement and Framed machinery; Split and NSplit rules - #5
Open
zilberstein wants to merge 4 commits into
Open
zilberstein wants to merge 4 commits into
zilberstein wants to merge 4 commits into
Conversation
A distribution refines a space exactly when the space is below the discrete space ProbSpace.ofPMF of a representation of the distribution. With this, the laws of the order give Refines.pad: a refined space can be extended, without adding probabilistic information, by variables that the distribution allocates. Also move Distr.Owns next to it. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_019Gipsr3EwstFw5DuwGNoug
Refines.split: a distribution that refines a sum is the average of its conditionings, which refine the summands. Refines.sum: conversely, refinements of the summands glue into a refinement of the sum. These are the semantic content of the Split rule. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_019Gipsr3EwstFw5DuwGNoug
Framed-level versions of the refinement lemmas, as needed by the Split rule: a distribution framed with a sum is an average of distributions framed with the summands (split), and conversely (glue, which relabels the summands to disjoint outcomes and rebuilds a common invariant space). pad extends a framed space by allocated variables, and shrink_inv takes the invariant space to own only the invariant's variables. Also sure_forget and disjoint_support_product'. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_019Gipsr3EwstFw5DuwGNoug
wp_split splits the initial distribution along the outcome conjunction of the precondition (Framed.split), runs each conditioning separately, pads each postcondition space back to the variables of the precondition (Framed.pad, using that programs do not deallocate variables), and glues the results (Framed.glue). wp_nsplit follows. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_019Gipsr3EwstFw5DuwGNoug
zilberstein
force-pushed
the
claude/happy-noether-41vna7-part4
branch
from
October 8, 2026 16:56
ba32300 to
a1655c9
Compare
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Part 4 of the stack splitting #1 (based on part 3).
Contents
Refines.lean: refinement via discrete spaces, padding a refined space; refinements of sums split and glue.Framed: shrinking the invariant space, padding, splitting and gluing.SplitandNSplitrules.🤖 Generated with Claude Code
https://claude.ai/code/session_019Gipsr3EwstFw5DuwGNoug
Generated by Claude Code