formal: end-to-end stream correctness of the incremental reduce model - #777
Merged
frankmcsherry merged 1 commit intoJul 2, 2026
Merged
Conversation
frankmcsherry
force-pushed
the
reduce-model-lean
branch
from
July 2, 2026 11:51
b3d3dc7 to
e0d9d57
Compare
… model Adds Differential/Model.lean and formal/TARGETS2.md. TARGETS2.md states the incremental model in prose: rounds delimited by antichain frontiers, a truncated join-closure enumeration with a carried pending set, and logical compaction modeled as an adversary that may re-represent the stored input and output arbitrarily, subject only to preserving accumulations at or beyond the frontier. Model.lean renders it sentence by sentence and proves the goal theorem unconditionally (Model.Run.stream_correct, Model.streamCorrectness_holds): every run, under every such adversary, emits corrections that accumulate to the reduction of the true input at every finalized time, and once the frontier empties the emitted stream is the unique difference trace of the output. One amendment to the model, recorded in TARGETS2.md step 2: the enumeration's ground set includes the stored (post-consolidation) output support, as the implementation's does. The pending coverage is then re-derived each round from current representatives and never crosses the adversary boundary. Whether the output-free enumeration also suffices remains open, per the amendment note. TARGETS2.md's cancellation scenario is checked end to end (scenario1Run), and the file builds with no sorries on the standard axioms. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
frankmcsherry
force-pushed
the
reduce-model-lean
branch
from
July 2, 2026 13:06
e0d9d57 to
9007d67
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
1 participant
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.
Adds
formal/TARGETS2.md(the incremental model, in prose) andformal/Differential/Model.lean(the model in Lean, with its goal theorem proved).The model (TARGETS2.md, following on from #776's per-round
Coverage.lean): rounds delimited by antichain frontiers; a truncated join-closure enumeration (joins beyond the round's frontier are deferred to a pending set and closed no further); and logical compaction modeled adversarially — between rounds the stored input and output may be re-represented arbitrarily (times advanced, merged, cancelled; support added or dropped), subject only to preserving accumulations at or beyond the frontier.advance_byplus consolidation is one instance (acc_mapDomain, with #776'sCompaction.advance_le_iff).The theorem (
Model.Run.stream_correct, quantified asModel.streamCorrectness_holds): every run — every choice of rounds, frontiers, compliant emissions, and adversary — emits corrections that accumulate to the reduction of the true input at every finalized time. Unconditional; the only hypothesis anywhere isf 0 = 0. Once the frontier empties, the emitted stream is the difference trace of the output (update_ext,Run.emitted_unique). TARGETS2's cancellation scenario is checked end to end as a concrete two-round run (scenario1Run), and a nonvacuity witness guards the quantified statements.One amendment, recorded in TARGETS2.md step 2: the enumeration's ground set includes the stored (post-consolidation) output support, as the implementation's enumeration does. The pending coverage is then re-derived each round from the current representatives (
staleness_rederived), so nothing is carried across an adversary boundary and the re-representation question dissolves (transfer_always). Whether the output-free enumeration also suffices — the empirical finding that output times are not needed for determination — remains open, per the amendment note; it is separately backed by ~48M adversarial rounds of a decidable per-round check in an executable twin of this model.Checking:
cd formal && lake build(no sorries);#print axioms Model.streamCorrectness_holdsreports onlypropext,Classical.choice,Quot.sound. The file header carries a sentence-by-sentence correspondence table to TARGETS2.md.🤖 Generated with Claude Code