Repository navigation
Conversation
This was referenced Nov 6, 2026
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
Scoped proof with exact finite corroboration. Arbitrary polynomial constant terms cannot improve a labelled linear-operator call minimum when every allowed operator has constant row sum. Dirty inputs, required workspace returns and chronological labels are preserved.
Merged PR #6017 establishes the zero-preserving case and asks about nonzero trajectories. This answers that question for the constant-row-sum alphabet. Width-independent row sums also yield one uniform extracted word. The chain rule is classical; the new step is the homogeneous orbit and its explicit profile and uniform-family consequences. The contribution was produced by Nick Petalas. Predecessor and contextual credit are retained in the package.
Only
research/homogeneous-polynomial-profile/is added. No new kappa or selected-frontier change is claimed.Evidence
Before, the cited theorem requires every polynomial to fix zero. After, the proof permits arbitrary constant terms under the stated operator hypothesis. It does not audit or replay the predecessor.
Local CPython 3.12.15 on macOS arm64 passes
PASS_HOMOGENEOUS_POLYNOMIAL_PROFILE:From the worktree root:
Any absolute CPython 3.12 interpreter path can replace this local path. Expected final markers are
PASS_REGISTERED_RESEARCH_PACKAGEandPASS_RESEARCH_COMMIT_BYTES. No third-party packages or runtime predecessor inputs are required. Scientific base and refreshed canonical main are7c49fe32c55de02c2c873655c804b16e4c3fef0a, priority revision eight. The source-history preflight passes at head6d38d4c55bf81afec80cc422c98d9b588432acf1.Advance claim. Live overlap checks cover open PR metadata, the handoff discussion, a paginated cache of 734 open PR bodies and 6,836 discussion records, main-tree README searches and targeted merged searches. Unpublished work and arbitrary historical code diffs remain coverage limits.
Limitations and unrun obligations
The theorem requires an infinite field, coordinatewise scalar polynomials, exact linear endpoints on independent inputs, fixed topology and a linear comparison permitting scalar multiples at the original charge. Arbitrary vector constants, coordinate-dependent polynomials, nonconstant row sums, restricted grids, branching and rounded operations are outside it. Width-dependent row sums retain pointwise domination but do not automatically give uniform coefficients.
No native realization, physical supplier, scalar/tape/precision/storage/stock bill, complete signed invoice, selected cold replay, Lean or Docker run is supplied. The five selected assumptions remain. Independent human and formal proof-kernel review are unclaimed. The written proof is the universal claim; finite checks only corroborate it.
Open next questions
Related open work
No open PR studying this homogeneous polynomial call-profile question was found in the stated overlap coverage. The direct predecessor #6017 is merged. The merged #6025 fixed nonlinear role-recoding theorem and #1757 finite-alphabet cut theorem use different contracts; neither is rechecked here. No common numerical minimum is compared.
The closeout check read this account's seven other open PRs created since the advance claim: #6785, #6787, #6788, #6789, #6790, #6791 and #6792. None computes a competing homogeneous-polynomial call-profile minimum. No additional computations were run to compare them.
CI notes
Both hosted checks passed at exact head
6d38d4c55bf81afec80cc422c98d9b588432acf1in run 42223022774:plan(4m52s) andreplay (research/homogeneous-polynomial-profile)(1m24s). The completed checks were read once and both report pass. Hosted replay certifies execution of the registered finite checks and metadata at this commit; the universal written proof and physical obligations retain their stated scope. All listed local checks also passed.Merge Danger
Door: two-way
Blast Radius: isolated
Six new package files. Shared scripts, frozen evidence, existing credits and selected records are unchanged.