Repository navigation
Clarify finite stopped-channel terminology - #815
Merged
Merged
Conversation
Replace O14 with a description of the balanced stopped-channel formula in the live census note and Lean doc comment. Replace the absent AvailableChannelApproximation name with a plain statement that no sequence of available channels is assumed. No theorem statement, proof, premise, module disposition, manuscript anchor or frozen round record changes. Local validation: JSON scope check and diff check pass; all 45 native receipts hold; all 303 legacy records in 75 closed namespaces remain intact.
First parent is the existing editorial branch f323348; second parent is accepted main 9fea39a. Resolve the shared census by preserving every accepted family, including OI-PAIR-MAXCONE-1, and applying only the finite family's existing terminology correction. Relative to accepted main, exactly two wording lines change: the finite family note and a finite protocol doc comment. Theorem statements, proofs, premises, kernel-only dispositions, manuscript anchors, both adopted rounds' records and receipts remain unchanged. Fresh CI is required before landing this follow-up.
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.
The finite-protocol census note cited the absent name
AvailableChannelApproximation, and both that note and a Lean doc comment used the private labelO14. These two live wording lines now describe the balanced stopped-channel formula and state plainly that no sequence of available channels is assumed.This editorial follow-up to #812 changes exactly two lines in two files against accepted main. Main was merged into the branch after #811 landed; the census resolution preserves the pair family and every accepted family. Theorem statements, proofs, premises, registry dispositions, manuscript anchors and frozen round records remain unchanged. Independent review is clean.
Validation: fresh run 38283803926 on updated head
fe994df094cad242a774a0a8b1eb29a8ae301a2dpassed 21 jobs with one expected dispatch-only skip. The logged synthetic checkout has the updated head's exact tree. The complete release gate passes; all 46 native receipts hold and all 303 legacy records across 75 closed namespaces remain intact. The census reports 222 modules, 106 families, 197 cited identifiers and 16 supersessions.Merged through an ordinary merge at
a40205746784a14f008b5c0dcadf9dd329ed175eafter the owner's stated conditions were met. Post-merge receipt and legacy checks pass on that actual main object.