Skip to content

Prove exact radical reachability through a common flag (no κ) - #6628

Open
petalas wants to merge 1 commit into
CrocSwap:mainfrom
petalas:research/w5-1102k-new-obstruction
Open

petalas wants to merge 1 commit into
CrocSwap:mainfrom
petalas:research/w5-1102k-new-obstruction

Conversation

@petalas

@petalas petalas commented Nov 3, 2026 •

Copy link
Copy Markdown
Contributor

Summary

Prove the complete reachability criterion requested in PR5854, Open next question 1. Claim type: scoped written algebraic proof with exact finite corroboration.

R=K[t_0,...,t_s]/(all t_i*t_j), C_0 invertible, n>=1
M=sum_j t_j C_j on exactly n roles
paid: I+u v^T, u in R^n, v in K^n; free: GL_n(K)

M is reachable <=> C_0^-1 C_1,...,C_0^-1 C_s share a complete K-invariant flag
when reachable, exact paid cost = n
otherwise, no finite word reaches M

The new chronological-cut lemma proves C_0 ker H = im S for 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.

  • Two finite descriptions, projective lines/planes and every invertible adapted basis, agree on all 256 binary two-role pairs, 6,561 ternary two-role pairs and 262,144 binary three-role pairs. Reachable counts are respectively 148, 2,457 and 47,968.
  • Exact endpoints pass for 5,062 attaining words; a separate literal interpreter checks 2,272 arbitrary-input basis columns. All 1,150 tested chronological cuts satisfy the coefficient, rank, image and invariant-subspace identities. The abstract cut domain has 58 scalar pairs and 1,584 indexed coefficient cases. Twelve boundary, omission and semantic controls pass.
  • Warning-strict CPython 3.12.15 normal and optimized commands pass locally on macOS arm64, each in under two seconds. Both registered checks are far below the five-minute target and produce identical generated hash-bound receipts.
  • Registered metadata/replay and committed-byte, executable-mode and full source-history preflight pass at 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:

/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -X dev -B research/radical-common-flag/verify.py
/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -O -W error -X dev -B research/radical-common-flag/verify.py
/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/radical-common-flag
/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/radical-common-flag --check-source-history --check-modes

Another CPython 3.12 executable can replace the interpreter path. Expected markers include PASS_RADICAL_COMMON_FLAG, PASS_REGISTERED_RESEARCH_PACKAGE and PASS_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-lemma card 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 are 7c49fe32c55de02c2c873655c804b16e4c3fef0a, 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

  • Can one restored additional role enable an excluded target? Start with diag(M,1) for the four-role fixture and retain every dirty-input column. The scalar endpoint becomes nonzero and the distinguished coefficient becomes singular, blocking this proof.
  • Which zero-residue targets without an invertible coefficient are reachable? Start with one singular coefficient tuple and complete source/image flags. Excess dimension in the cut image prevents the current rank equality.

Related open work

No other open PR studying this pure square-zero common-flag criterion was found in the refreshed inventory. Adjacent work is:

  • PR6563 computes cost statistics for invertible two-role F_q[t] targets in the right-vector alphabet; its coefficient algebra, endpoints and counted quantity differ from this radical reachability criterion.
  • PR6560 compiles a nilpotent chain using fixed-involution rank-one idempotent calls and restored workspace; its identity-residue endpoint and paid alphabet differ. No shared target minimum is compared.

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 d1041a1273f46a473ba3168b64a108f18822ba75 in 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.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant