Repository navigation
Prove doubled centre Gram degree at least 410 (no new κ) - #5120
Merged
Mister-Meeseeks merged 1 commit intoOct 23, 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
A new finite exact certificate and scoped all-positive-tensor-size proof answer Open next question 1 of Ali Romman's #4958 negatively: the full historical doubled centre Gram cannot have minimal-polynomial degree exactly 409.
The new certificate uses the invariant direct sum of Bell blocks c=1 and c=11. It uses new seeds and does not import or rerun the predecessor's 409 certificate. The inverse statement assumes alpha I+beta A is invertible and beta is nonzero. Only
research/centre-gram-degree410/is added.Produced by Nick Petalas. Credit Ali Romman #4958 at c8c48ef for the operator, Bell identities, invariant tensor embedding and open question; #4720 for the retained actual query; #1719 for the doubled representation. The unchanged historical notices retain icekylinx, Gauge44 and the native/helper/compiler/upstream lineage. Krylov/Hankel minors and modular nonvanishing are standard methods.
Evidence
The new 410-by-410 moment minor has determinant 58805 modulo 65537. Both operator implementations agree on all 1,638 block Krylov vectors, and modular Gaussian elimination and integer fraction-free condensation agree on the determinant. The receipt regenerates all 819 direct-sum moments, both component lists and seven source hashes. Eight dependence, pivoting, source and truncation controls pass.
On CPython 3.12.15 / NumPy 2.5.4 / macOS arm64, both warning-strict registered modes pass. Direct normal/optimized checks took 6.70/7.04 seconds, below each 180-second limit. Metadata, committed-byte/full-source-history preflight, official seven-file export integrity and read-only Git-free normal/optimized replays pass. All seven exported payload files retain the source-bound receipt hashes. The selected source-binding orientation also passes; it is metadata orientation only.
From the repository root:
Any equivalent Python 3.12 installation with the declared NumPy pin can replace that local path. Direct output is
PASS_CENTRE_GRAM_DEGREE410 degree>=410 inverse_degree>=409 det=58805 mod=65537. Add--emit-resultto the direct command for the generated JSON receipt; write it outside the checkout.Limitations
The exact full degree and an upper annihilator remain unknown. The all-size deduction uses #4958's cited Bell identities and common fixed vector. General ADD circuits, rational expressions, matrix-valued encodings, native access, rounding, dirty restoration, physical movement, recursive prices and complete supplier admission are outside this scalar-polynomial result. No new kappa or selected-frontier change is claimed.
All registered checks ran locally. Lean, Docker, predecessor scientific replays and the selected cold replay were not run. Independent human and formal proof-kernel review are unclaimed. The finite certificate and written scope are distinct from a complete multiplication theorem.
Open next questions
Related open work
No other open PR studying this doubled Gram's scalar minimal-polynomial degree was found in the pre-commit refresh. Merged #4958 is the direct predecessor; #4720's source-span bounds and #1719's lift have different claims. The complete remote overlap snapshot covers 323 open PRs and 4,243 Discussion records; sparse local coverage was supplemented with all-main README and merged-PR searches. Arbitrary diffs and unpublished work are not exhaustively covered.
Canonical advance claim. Scientific base 81e9bd6, priority revision 7; canonical main was refetched unchanged before submission. TASK.json declares the changed formal-interface-lemma scope.
CI notes
CI blocked upstream for head
34f5c3aa8c9df2f9f1c587c6bca0c4ea7af0c36e. The plan job failed in Onboarding helper tests; package selection and the hosted package replay were skipped. The log reports 408 tests, eight failures and 17 skips. The checked-out merge wasb616414606fc3c6cb811b4cc955b9bf4e12b143f, merging this head into upstream20a1e31bc6009b9b3f4d084bbaadc6350e34fcba.The eight failure entries have two shared causes, confirmed from the failed logs and exact merge-tree files:
test_research_descendant_source_roles.DescendantSourceRoleTestsstop onworking source drift: scripts/check_research_commit.py. The historicalresearch/isolated-descendant-bytecode/SOURCES.jsonstill marks that checker as a live input with SHA256ecf206a82bf1f4e748efb6cc639919582050d173b3537ec12f7265a4f7b55ead; the merge-tree checker has SHA25628fed1e156fe8601633ed453f682a158cb15e94981e6c89ed96ae72ffc9d0c6f. This earlier rejection prevents the intended helper/history corruption or acceptance checks. The seven entries comprise bothgit_blob/sha256subtests for each of the two historical corruption tests, plustest_live_history_guard_is_not_a_historical_source_substitution,test_original_gate_rejects_but_correct_role_accepts_current_helperandtest_original_history_input_role_rejects_live_guard_successor.test_research_onboarding.OverlapTests.test_report_survives_a_cp1252_stdoutfails withModuleNotFoundError: No module named 'research_package'. Its temporary fixture copies onlyscripts/find_overlap.pyat test line 39; that script now importsgit_source_envfromresearch_packageat line 24, and the copied fixture lacks the module.I compared all eight failure names/subtest labels and terminal error signatures with these other failed plan logs; all eight signatures agree exactly:
Their changed-file lists, like this PR's six-file package addition, contain no shared script or test changes. This is a shared upstream fixture breakage, not a failure of the new Gram certificate. No shared scripts/tests were modified, no new commit was pushed, and no DONE was posted. The previously passed local registered normal/optimized, source-history and export checks remain the available package execution evidence; hosted replay has not certified the package. Scratch logs and exports are retained for the upstream repair and rerun.
Merge danger
Door: two-way. Blast radius: isolated research package. Shared code, predecessor sources, frozen evidence and the selected frontier are unchanged.