Skip to content

Certify the minimum 139-row integer P112 demand subfamily (no κ) - #6484

Open
ToikY wants to merge 1 commit into
CrocSwap:mainfrom
ToikY:codex/b9-p112-integer-demand-kernel
Open

ToikY wants to merge 1 commit into
CrocSwap:mainfrom
ToikY:codex/b9-p112-integer-demand-kernel

Conversation

@ToikY

@ToikY ToikY commented Nov 3, 2026 •

Copy link
Copy Markdown
Contributor

The fixed original280-row P112 demand system has a unique minimum139-row subfamily over unrestricted nonnegative integers. This answers PR6455’s README integer-only question after its237-row real-domain result.

New coverage is98 integer-only deletions and5 new integer separating points. The43 real deletion certificates and134 existing integral points are validated and explicitly credited reuse. All103 previously unresolved labels are resolved. Every retained row has a full14-integer point satisfying all279 other original rows and violating that row, forcing every equivalent original-row subfamily to contain all139.

The completeness bridge is a proof, not an assumed search box: violating target(I,d) forces its inside total<=d-1<=7; setting outside coordinates8 satisfies every row with an outside bit. Proper-subset originals are the only remaining premises. Full weak-composition exhaustion and strict-support induction justify simultaneous old/new deletion. One example is target0x1ada: half of rows0x5a(d4),0x1a98(d3),0x1ac2(d2) gives its exact coefficient vector and RHS9/2, whose integer ceiling is5.

Only research/p112-integer-demand-kernel/ is added. PROOF.md proves projection/coverage/induction/minimality; TASK.json records complex-rank-shape-decoder, scope_status=changed to this integer support-screen implication.

Validation (CPython3.12, standard library):

python3.12 -I -W error -B research/p112-integer-demand-kernel/verify.py
python3.12 -I -W error -B research/p112-integer-demand-kernel/oracle.py
python3.12 -B scripts/research_package.py --package research/p112-integer-demand-kernel
python3.12 -B scripts/check_research_commit.py --package research/p112-integer-demand-kernel --check-source-history --check-modes

Normal/-O emissions and strict defaults pass with identical complete receipts. The primary visits340727 profiles across103 targets;4341 belong to positive early-stop searches. A separately written iterative vector-budget DFS independently regenerates all336386 profiles in98 negative domains and their exact counts/first-miss histograms, then directly checks all139 integer points. It imports no primary/predecessor code and runs no LP. Sixteen rejection controls plus a literal2Dcoverage toy pass. Optional primary ordered-transcript hashes are primary-only provenance; the independent checker regenerates mathematical obstruction fields, not that hash order. Counts/hashes alone are never accepted as exhaustion evidence.

Registered replay, source/commit byte/mode/declared-base history, official export and read-only Git-free/empty-PATH normal/-O replays passed; cold bytes and modes remain unchanged. Static AI review found no material issue in the stated domain. No scientific execution failure occurred.

Source6425 head 092dcbd13d1263e691ad29f34fbf286fea1fac2c; source6455 head 7fdae743973bebb77daf4508d05655dc1e8915c7. Three inert objects are authenticated before parsing by manifest SHA256 c326b2a83adb02af94954c3904ee6e59822bf5fd274c847851abdcb63c1b9c64. Primary receipt SHA256 f4959ac06a189e817a4fc14c428b9bd02dd9f344f20022cd159d8acfd972fa54; independent 5a0ea35df19ee7cc72607fbb4ec8ca51a95ffa1cdea1e73e40214311a5dd47a1. Public tree 87f06cc084d23715ac0ff0a8c402b9cc02e03ca2 equals the tested/exported tree.

The minimum is restricted to these original inequalities on the integer orthant. A fractional source point separates this system from the real237-row system. All-orthant equivalence can be conjoined with identical added constraints; its minimum need not persist under a cost/COPY budget. Changed caps require a new matrix. Coefficients, decoder/COPY pricing and physical/native/access/restoration/precision/tape/stock/compiler/outer admission remain open. No κ or selected-frontier change; all five selected assumptions remain. Original262928-clique census/geometry equivalence is credited predecessor coverage, not replayed. Selected/native/Lean/Docker replays were not run.

Canonicalmain 7c49fe32c55de02c2c873655c804b16e4c3fef0a, revision8/selected6030 and source heads unchanged at submission refresh. Overlap:425deduplicated open bodies from non-atomic pages pluslatest30,15boundedall-state queries and visible Discussion claims. Truncated broad query,6458PR404, sparse/history/hidden/unpublished limits remain. No novelty certificate.

Credit Nick Petalas6425; Jeremy Diviney1422; Cinna Davis1347/1323 and retained E8/label/decoder lineage; ToikY/OpenAI Codex6455 for the43/134 reuse and explicit integer question. Weak compositions, monotonicity and integer implication/rounding are classical. New work uses substantial OpenAI Codex assistance; AI checking is not human/formal acceptance.

Canonical claim. Science froze2026-11-03T00:37:44Z; at least15minutes reserved for verification/handoff within the60minute budget. Maintainer edits disabled; no auto-merge or merge requested.

Hosted CI: run41555251128 passed for exact head eb919ae6caba5dd81dce8eff41765db3a71429d5: plan / 711 onboarding tests, both scientific commands and unchanged inputs. The hosted synthetic PR test commit was 5e5da9c1e21c3691dc2a87d1d49f35a5f842007a; its tree equals the frozen/public tree. No actual merge occurred. All seven optimized-Python external source/receipt corruption cases also failed closed on disposable copies.

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