Repository navigation
Prove the sharp four-term pair-reader floor - #3489
Merged
Mister-Meeseeks merged 1 commit intoOct 18, 2026
Merged
Conversation
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.
Summary
This closes PR3472's four-query continuation. The new rank-three/rank-three case transfers the four queries and two distinguished targets to GF16 through a complete nine-type six-point incidence classification. All original source and reader zeros survive. The expanded identity then gives the sharp bill. Original terms attain equality, so disjoint pair replacements retain literal P112 total 224.
Only
research/p112-four-term-reader-floor/is added, with the self-contained proof, exact incidence templates, unchanged attributed fixture, source pins, receipt, two arithmetic implementations, actual CLI controls and replay instructions. No supplier, new kappa or selected-frontier update is claimed.Evidence
877ea00e462a4d306babb9867651d9fd9a1f74b1.# Set TMPDIR to a private existing external directory. python3.12 -Werror -B scripts/research_package.py \ --package research/p112-four-term-reader-floor python3 -Werror -B scripts/check_research_commit.py \ --package research/p112-four-term-reader-floor --check-source-historyCanonical source and submission refresh remain
6f100d4bb5083f8c35d96fd95a539811c62f245c, priority revision 6. Public proof comparisons have exact head/blob/SHA receipts separate from ancestry pins. Replay needs only the retained package and its one declared canonical input. Credit Tekalign/PR3370, Philippe Van Velzen/PR3345, PR3398/3414/3463/3472/3475, ctoth and the retained P112/E8/native/compiler/supplier lineage. Scope, sources and full limits are in README.md, PROOF.md and VALIDATION.md.Independent human and formal proof-kernel review are unclaimed. Five-term synthesis, changed matrices, larger target blocks, native acquisition/coefficients/frames/restoration, hosting, stock, precision, all-size/compiler and outer transfer remain open. Selected cold replay, Lean, Docker and hosted CI were not run.
Merge Danger
Door: two-way
One isolated opt-in research package. Frozen predecessor bytes and existing verifiers are unchanged.
Blast Radius: research
Archiving the result does not admit a supplier or change the selected frontier.