Repository navigation
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
Prove the complete reachability criterion requested in PR5854, Open next question 1. Claim type: scoped written algebraic proof with exact finite corroboration.
The new chronological-cut lemma proves
C_0 ker H = im Sfor each scalar prefix H and suffix S. Every normalized coefficient preserves ker H, and rank-one scalar drops supply every flag dimension. An explicit column-replacement word attains n. A four-role example has a split homogeneous determinant and common left eigenrow but no complete common flag, so the earlier common-row condition is strictly weaker.Only six new files in
research/radical-common-flag/are added. This contribution was produced by Nick Petalas. No new kappa, native supplier or selected-frontier change is claimed.Evidence
Before, PR5854 supplies one necessary common eigenrow and leaves a complete flag open. After, PROOF.md proves the criterion for every field, positive role count and finite coefficient tuple, with exact paid cost. No predecessor scientific result or executable is audited or replayed.
d1041a1273f46a473ba3168b64a108f18822ba75. Official export/integrity checks pass. Both modes also pass with-I -S, empty PATH and a read-only Git-free export; all seven exported files retain their hashes. The committed and exported receipts agree exactly.From the repository root:
Another CPython 3.12 executable can replace the interpreter path. Expected markers include
PASS_RADICAL_COMMON_FLAG,PASS_REGISTERED_RESEARCH_PACKAGEandPASS_RESEARCH_COMMIT_BYTES. Each direct run generates its receipt from the executed checks and six current file hashes. No handwritten receipt is committed.Task and overlap
The
formal-interface-lemmacard is changed to this algebraic side question. A reachability screen can reject proposed formal coefficient interfaces before unbounded word search, but it does not establish a physically priced native interface. Base and refreshed canonical main are7c49fe32c55de02c2c873655c804b16e4c3fef0a, priority revision 8, selected PR6030. The selected source-binding orientation passed.Advance CLAIM. Direct question source: PR5854 at
e70246e3aabe63aacbddb41dfa2253e865798d1d; PR4776 supplies the two-generator antecedent. SOURCES.json pins their main-tree texts, catalogue and selected record as provenance, with no runtime dependency on predecessor code or foreign Git objects. Main/merged general-form searches, live open work, handoffs and reservations were refreshed before committing. Cached coverage had 572 open PRs and 6,639 Discussion records with complete remote pagination; sparse local notes, arbitrary historical diffs and unpublished work remain coverage limits.Limitations and unrun obligations
An invertible distinguished coefficient, zero scalar endpoint, square-zero radical, exactly n roles and the stated paid/free alphabet are required. Restored extra roles, higher nilpotency and targets without an invertible coefficient remain open. Paid factors may discard data in this formal model. Coefficient preparation, reversible physical realization, access, restoration, precision, stock, tape, complete recursive invoice, compiler and outer admission are not supplied. All five selected framework assumptions remain.
The universal claim rests on the written proof. Finite replay and hosted CI do not independently prove it. Independent human and formal proof-kernel review are unclaimed. Selected cold replay, Lean and Docker were outside scope and unrun. Managed Python allocation is the documented Power of Ten deviation; fixed dimensions and finite inventories bound live collections. No unrelated historical suite was run.
Credit
Produced by Nick Petalas. Credit Nick Petalas / PR5854 for the question and common-row obstruction, PR4773 for the first-zero argument, PR4776 for the two-generator classification, and PR4243 for the free-map normal form. Retain Wentao Li / PR4099 following PR2513 and ToikY / PR4334 for the alphabet and shared-chart lineage. Rank-nullity, rank-one perturbation bounds and adapted bases are classical; no general literature-priority claim is made. Predecessor files and credit are unchanged. Apache-2.0.
Open next questions
Related open work
No other open PR studying this pure square-zero common-flag criterion was found in the refreshed inventory. Adjacent work is:
Their titles and bodies were read without additional scientific computations. Merged PR5854 and PR4776 are the direct predecessors, not competing open work.
The completion refresh listed all 16 account open PRs created since the advance CLAIM at 2026-11-03T13:56:02Z, including this PR. The other fifteen concern different objects or quantities. None studies this pure square-zero common-flag criterion or reports a competing value for its finite pair counts or exact cost. No additional scientific computation checked another contribution.
CI notes
Both hosted checks passed at exact contribution head
d1041a1273f46a473ba3168b64a108f18822ba75in run 41650404715: plan in 4m35s and registered package replay in 1m28s.The completed checks were read once. Separate run metadata confirms the matching head, completed status and success. Both warning-strict normal and optimized registered commands, committed-byte/source-history checks and read-only Git-free export replay passed locally. Hosted replay certifies execution of the bounded registered checks; independent human and formal proof-kernel acceptance of the universal written proof remain unclaimed. No failed or waived check remains.
Merge danger
Door: two-way.
Blast radius: isolated. This adds one self-contained research package. Shared code, frozen evidence and the selected result are unchanged.