Skip to content

Prove common30 P112 span bound and exclude the 2^5,6,7^5 caller - #3973

Merged
Mister-Meeseeks merged 1 commit into
CrocSwap:mainfrom
Clear1nsight:research/c5-common30-geometry-20261019
Oct 20, 2026
Merged

Mister-Meeseeks merged 1 commit into
CrocSwap:mainfrom
Clear1nsight:research/c5-common30-geometry-20261019

Conversation

@Clear1nsight

@Clear1nsight Clear1nsight commented Oct 19, 2026 •

Copy link
Copy Markdown
Contributor

Result and literal caller

For ONE common set S of at most30 live P112 coordinates, the normals over every characteristic-zero field whose residual binary support rank is at most7 span at most three dimensions. An explicit independent triple at30 attains the bound. The complete triple inventory also proves that at most two projective directions qualify when |S|<=29; the triple at30 makes this span-two cut threshold sharp.

This excludes the actual historical TWOSIDE (b,t)=(5,6) eleven-piece profile 2^5,6,7^5 at code-intersection dimension at least5. The six small pieces have support-cap sum5*2+20=30<distance53, forcing quotient dimension6 and intersection dimension5. The five remaining rank7 pieces then give five independent code directions after the SAME cut, contradicting5>3. All462 six-piece subsets are checked;30 is the minimum certified capacity sum, not a lower bound on the actual support union. The authenticated retained PR3154 necessary filter contains this literal strict-deficit-one row.

No full cell reconciliation, full C5, decoder floor, native/restoration/consumer/all-size/supplier admission, multiplication theorem or new kappa is claimed. The separate concurrent caller-inventory contribution can use this named exclusion as an explicitly pinned additional dependency.

Proof and finite coverage

PROOF.md includes the finite reflection-group chamber argument and rational-kernel scalar extension. Off(h)<=30+36=66 gives at least46 perpendicular live roots;46>42 isolates the root-normal face. All120 root normals, including eight frame normals, are retained. No embedding of K into R or frame preservation under Weyl moves is assumed.

The exact finite graph contains43,435 binary seven-spaces,5,212,200 normal/space pairs,24,264 completion records and9,828 compatible distinct-owner pairs. Every admitted triple has union size30:896 rank2 and3,584 rank3. The primary enumerates independent prefixes and tests2,688 four-node continuations, all rank3. Every independent four-tuple would have independent prefixes, so this pruning is complete for the claimed bound. Total common union<=30 is explicitly tested, not inferred from pairwise compatibility.

The separate checker imports no primary or predecessor executable. It uses shell/Cramer/Bareiss reconstruction,10,795 six-spaces with four affine cosets plus255 leading-zero spaces, and direct Gram determinants on all3,360 compatible quadruples, including672 with dependent first triples. Full flat, record, node and edge digests agree. Its shell/coordinate routines are adapted with explicit credit from #3960; this is same-donor computational corroboration, not newly independent provenance or human/formal-kernel acceptance.

Sources, overlap and credit

Canonical main refreshed unchanged before publication:20ecf2891d80b5acf18d980b2164fb44ea7faa90, priority revision6. Parent coordination checked671 live open PR bodies and rendered C5/start/handoff/active-board discussions at entry; no overlapping common30 result was found. This worker reread the exact caller source, current #3960 head/body and checked a live lexical common30 PR query at entry and publication. The local helper searched2,490 records but could not refresh remote snapshots because gh was unavailable. Closed-work, arbitrary-diff, discussion-wide and private-work coverage remains partial; no novelty certificate.

Credit Nick Petalas for global capacities, root-shortening and common-cut predecessors, including #3269/#3163/#3282/#3289; DreamingOfClouds/#3154 for TWOSIDE/C5; David Arias, joaqcoo and the retained E8/P112 lineage. Exact predecessor heads and roles are in PREDECESSORS.json. This donor's #3951 head9aacf01037f6e19cabb95ccbea15fcc2965dcd4d supplies the preceding dependency audit and field argument. #3960 head7e8d98e351ac153d81943218bf168dc8548b1cea supplies the prior common24 theorem, adapted model/reconstruction code and this caller handoff. Frozen predecessors and selected records are untouched; no pending predecessor Git object or executable is needed at runtime.

Validation and remaining obligations

Commit 1e77152, tree83b19e6ebef0a9f33423877c69279704f528e06b, adds11 files only under research/p112-common30-span. CPython3.12.3, standard library only:

python3.12 -I -Werror -B scripts/research_package.py --package research/p112-common30-span

All three optimized registered commands pass. Controls screen all1,024 five-vertex graphs and compare577 qualifying graphs against a direct subset oracle, verify the real attaining triple, reject a synthetic fourth independent normal, expose the characteristic-two boundary, and reject actual optimized CLI source/manifest corruption. The primary also rechecks the global rank6 capacity20 on all788,035 six-spaces. Metadata/pins, syntax/JSON/whitespace and committed-source-history preflight pass. The official committed export passes integrity checking and all three optimized commands from read-only files with Git absent from PATH: primary45.700s, separate34.658s, controls2.555s. All16 exported hashes stay unchanged; archive SHA2565e213d31300064103b9b2f05f4b5a8a73f6c430d0353c5e9ccbe111ab4d4a7fc. Hosted CI39217108765 passed at2026-10-19 07:41:22UTC for exact head1e77152b14dd94ca3f99ce1afba280ba13225d9c. Planning, replay, all four expected theorem/independent/control/registered PASS markers and committed-inputs-unchanged succeeded. Parent independently rechecked the run/head and empty comments at07:44:34UTC; worker review/inline-thread checks were also empty.

A parent agent separately checked the actual table/label witness without importing worker or predecessor executables: Gram determinant256,30 distinct live cut labels and three residual ranks7. Its proof review found no objection to the stated coverage and quotient transfer. All agents remain in the same donor/assistant context. Independent human/formal review and the broader C5 obligations remain open. The session stops at this named caller; no ongoing reservation.

Prepared by Chris R / Clear1nsight with substantial OpenAI Codex assistance, including parallel agents; Apache-2.0. No merge, closure or selected-frontier change.

Task complex-rank-shape-decoder; changed scope to a uniform common30 span law bound to the actual remaining literal caller. The separate source-bound inventory is #3972, and the independent common24 graph audit is #3971. The parent refreshed all673 open PR bodies at07:30:28UTC and the newest100 at07:36:13UTC; no conflicting common30 contribution was found in that coverage. Open next questions and stop rules are in TASK.json/README.md.

The other two scoped agents also completed read-only cross-review of the independent-prefix completeness, direct all-quadruple coverage, characteristic-zero bridge and exact quotient transfer; no objection was found. The graph-audit agent independently replayed the attaining triple from its own table reconstruction. These are same-session automated checks, not human/formal acceptance.

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.

2 participants