Skip to content

Certify the minimum 237-row P112 demand subfamily (no κ) - #6455

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

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

Conversation

@ToikY

@ToikY ToikY commented Nov 3, 2026 •

Copy link
Copy Markdown
Contributor

For the fixed 14-variable/280-row P112 demand matrix in Nick Petalas’s PR6425, exact nonnegative combinations remove 43 rows. The retained 237 rows are the unique minimum equivalent subfamily of those original280 inequalities, over nonnegative real multiplicities with x>=0 fixed.

Each deletion has a rational coefficient/RHS certificate using only final-retained rows. Each retained row has a full14-coordinate rational point satisfying all279 other original rows and strictly violating that row. These two certificate forms establish equivalence and force every equivalent original-row subfamily to contain all237. The proof does not trust simplex status or floating tolerances.

A concrete example: target 0x1d1a, demand3, follows from half each of retained 0x1412, 0x1818 and 0xd0a, all demand2. The weighted coefficients fit inside the target; nonnegativity supplies the remaining half-coordinate slack.

Only research/p112-farkas-kernel/ is added. PROOF.md, RESULT.json and TASK.json / next questions delimit the scope. This takes PR6425’s first Open next question. complex-rank-shape-decoder has scope_status=changed: a finite support-screen implication replaces the broader full-supplier task. No coefficient synthesis, COPY floor, physical supplier, κ or selected-frontier change is claimed.

Validation (CPython3.12, standard library only):

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

Normal/-O emissions and strict defaults pass, with identical full receipts. The exact bounded generator uses2272 pivots, maximum49 per target. A separately implemented checker consumes the sealed certificate as untrusted data, without importing the generator or solving an LP; all43 implications,237×279 full-original-row comparisons and14 corruption/schema controls pass. This is independent certificate checking, not blind rediscovery. The registered replay, committed bytes/modes/declared-base history, official export and read-only Git-free/empty-PATH normal/-O replays pass; cold bytes and modes remain unchanged. Static AI review found no material issue in the stated domain.

Exact source: PR6425 head 092dcbd13d1263e691ad29f34fbf286fea1fac2c; inert source RESULT Git blob e18f92e001b8ce9d44287760516bf6ea002bcbcd, SHA256 f8d15306112914af299acca8720779fbc9f6f07bb1336c51e99304fdea5caf89. Both source files are authenticated before parsing; no predecessor executable or clique census is replayed. Primary receipt SHA256 b477f2a8d144ed884c78ee29ac76fd88c95b076eb2dd290ef2431dd7e4969704; independent receipt 02c89eed3237e401b4b16563529de77cba8925439f2e67c86021a27846fccc81. Public tree b842829a950addc20da16bbac83b32b2aa036608 equals the tested/exported tree.

The source262928-clique equivalence is a credited PR6425 premise when composing with the larger geometry, not new independent census coverage. The minimum excludes arbitrary replacement inequalities and integer-only minima;134 displayed separators are integral, which does not settle the integer-only screen. Changed caps require a rebuilt quotient. Actual coefficients, access/restoration, precision/tape, stock, compiler, native and outer integration remain open; all five selected assumptions remain. Selected/native/Lean/Docker replays were not run.

Canonical main 7c49fe32c55de02c2c873655c804b16e4c3fef0a, revision8, selected6030 unchanged. Main/guidance/source and live overlap were refreshed before submission:405open PR bodies plus a latest30 refresh, bounded all-state queries, visible claims and pinned ledger. Sparse notes, hidden/unpublished work and arbitrary history remain coverage limits. PR6430 uses another P112 screen; PR6424 another B2 model. PR5767 verifies supplied LP certificates and supplies no optimizer; its shared128-variable cap/code are unchanged.

Credit Nick Petalas/PR6425; Jeremy Diviney/PR1422 for the guard, geometry/caps and smaller-family question; Cinna Davis/PR1347/1323; Navinor, David Arias, Hanson Sun, DreamingOfClouds, themilkman216 and retained E8/label/decoder lineage. LP duality, simplex/Bland and nonnegative implication are classical. New work is ToikY with substantial OpenAI Codex assistance. AI corroboration is not human or formal proof-kernel acceptance.

Canonical claim. Science froze2026-11-02T23:56:05Z; at least15minutes are reserved for verification/handoff within the60minute budget. Maintainer edits disabled; no auto-merge or merge requested.

Hosted CI: run41549688777 passed for exact head 7fdae743973bebb77daf4508d05655dc1e8915c7: plan / 711 onboarding tests, both package commands and unchanged inputs. The hosted synthetic PR test commit was 3166feacd234891589b674a98904e7c4a36ca84a; its tree equals the frozen/public tree. No actual merge occurred. Seven additional optimized-Python external source/receipt corruption cases 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