Repository navigation
Qualify PR5285's h8 family closure with exact coverage - #5558
Merged
Mister-Meeseeks merged 1 commit intoOct 25, 2026
Merged
Mister-Meeseeks merged 1 commit into
Mister-Meeseeks merged 1 commit into
Conversation
Prepared for @CubeJerry with substantial OpenAI Codex assistance. Credit Matarener's PR5285 census, eumemic's source geometry/generator, and DreamingOfClouds' PR589 word. No new kappa.
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.
PR5285's recorded search does not by itself establish its whole-family closure. An independent stdlib checker reconstructs all 17,478 admissible puncture sets and finds 43,122 represented set/receiver pairs out of 344,019,474 (343,976,352 absent). It reproduces 6,000 sampling draws, supplies an omitted allowed input, and identifies Stage C's saved effort 50 versus documented/spot-replay effort 2000.
New relative to Matarener's PR5285: source-derived domain enumeration, deduplicated coverage certificate, and a precise scope/provenance correction. Original census files and selected result are unchanged.
No new κ. This identifies a missing exclusion/equivalence argument, not a better word or a counterexample to optimality. No omitted word was built/priced; producer, transfer, compiler and outer proofs were not replayed. The historical Stage C invocation remains unresolved; inherited framework assumptions remain.
Base: 13be6ac.
PR5285 source head: 440550b. Exact Git/SHA256 pins, scope, local seed-95 claim and supporting detail are in the package.
Reproduce (Python 3.12, no third-party dependencies):
python3.12 -B scripts/research_package.py --package research/h8-census-coverageExpected: PASS_H8_CENSUS_COVERAGE, represented=43122, unrepresented=343976352; 16 tests; PASS_REGISTERED_RESEARCH_PACKAGE.
Executed: normal/-O replay, metadata/source-history checks, Git-free export with empty PATH and unchanged hashes, and 15 rejecting controls (including forged full-coverage/effort receipts and source-byte corruption). Hosted CI was not run.
Published commit: 3ce75dc. Its complete tree 1507411197bd009db71622658357e98a236a7749 matches the tested tree, checked by GitHub objects and a fresh Git fetch/full-tree diff. No upstream PR submitted.
Prepared for @CubeJerry with substantial OpenAI Codex assistance. Credit Mark/Matarener's PR5285, eumemic's PR555/PR543/PR493 geometry and generator, DreamingOfClouds' PR589, and the retained lineage. Apache-2.0.
Research package and validation