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

research/p112-farkas-kernel/NOTICE

@@ -0,0 +1,17 @@
+New finite-kernel generator, certificate checker, proof and package metadata:
+ToikY, with substantial OpenAI Codex assistance. Apache-2.0.
+
+The two source files are retained verbatim from Nick Petalas's PR6425, exact
+head092dcbd13d1263e691ad29f34fbf286fea1fac2c. Their original headings and credit
+remain. SOURCE-PINS.json records exact Git blob identities, byte lengths and
+SHA256 digests; no predecessor executable is imported or replayed.
+
+Retain predecessor credit to Jeremy Diviney/PR1422 for the complete-clique guard,
+geometry/caps and smaller-family question; Cinna Davis/PR1347/1323 for the support
+model and geometry; Navinor, David Arias, Hanson Sun, DreamingOfClouds,
+themilkman216 and the retained E8/label/decoder lineage.
+
+PR5767 is related exact-certificate tooling, not the source of an optimization
+solver here. Its shared limits and code are unchanged. Linear programming,
+nonnegative implication/Farkas certificates, simplex and Bland's rule are
+classical methods; no literature priority is claimed.

research/p112-farkas-kernel/PROOF.md

@@ -0,0 +1,105 @@
+# Exact implications in the fixed P112 demand system
+
+This is a finite, source-bound inequality result, quantified over all nonnegative
+real multiplicity vectors. No predecessor executable or clique census is replayed.
+The source matrix is the literal 280-row kernel in Nick Petalas's PR6425 at
+`092dcbd13d1263e691ad29f34fbf286fea1fac2c`, authenticated by `SOURCE-PINS.json`.
+Its 14 ordered cap rectangles, source clique witnesses and earlier completeness
+claims retain their original meaning and attribution.
+
+## Matrix and domain
+
+For each saved pair `(H_i,d_i)`, let `a_i` be the 14-dimensional 0/1 indicator of
+hit mask `H_i`. The row is `a_i x >= d_i`, with the common baseline `x >= 0`.
+The source rows have distinct nonempty 14-bit masks and positive integer demands
+at most 8. These conditions are checked, not inferred from a row count.
+
+PR6425's [proof](https://github.com/petalas/integer-mult-bounds/blob/092dcbd13d1263e691ad29f34fbf286fea1fac2c/research/p112-demand-kernel/PROOF.md)
+defines the hit predicate and proves equivalence of this kernel to its full
+262,928-clique demand screen. That earlier theorem is a credited premise when
+composing the present result with the full geometry. The present standalone
+certificate establishes equivalence of the literal 280-row matrix and its new
+retained subfamily; it does not independently certify the source clique census,
+the witnesses' geometric validity, decoder coefficients or physical admission.
+
+## Checkable deletion implication
+
+For each omitted row `t`, the certificate supplies nonnegative rational weights
+`lambda_j`, with every donor `j` in the **final retained family** `R`. The exact
+checks are
+
+    sum_j lambda_j a_j <= a_t       (coordinatewise),
+    sum_j lambda_j d_j >= d_t.
+
+For any nonnegative `x` satisfying the retained rows,
+
+    a_t x >= (sum_j lambda_j a_j) x
+          >= sum_j lambda_j d_j >= d_t.
+
+Thus the retained system implies every omitted row. Conversely a solution of
+all original rows satisfies their retained subfamily. This proves equivalence
+for all nonnegative real vectors, including unbounded integer vectors. No LP
+solver status or floating tolerance enters this acceptance argument.
+
+## Generation and simultaneous deletion
+
+A positive donor weight cannot use a row having a 1 outside `H_t`, because the
+target coefficient there is zero and all donor coefficients/weights are
+nonnegative. Restrict candidate donors to strict subsets of `H_t`. Process
+targets by increasing support size, retaining a row whenever it is not certified
+implied by the already retained strict subsets. Retained rows are never deleted
+later. Consequently every deletion refers directly to rows in final `R`;
+simultaneous deletion is justified without circular premises.
+
+The bounded generator uses exact rational packing simplex: maximize
+`sum_j d_j lambda_j`, subject to coefficient capacities at most 1 on `H_t` and
+`lambda >= 0`. Zero weights plus slacks form an initial feasible basis. Bland
+entering/leaving rules include nonbasic slack columns. A feasible packing reaching
+`d_t` already certifies deletion; full optimality is unnecessary for that case.
+Explicit bounds reject exhausted work instead of truncating coverage.
+
+The generator is a discovery mechanism. The elementary coefficient checks above
+and the explicit points below independently establish the result even if the
+simplex implementation is not trusted.
+
+## Separating points and the restricted minimum claim
+
+For every retained row `t`, the certificate supplies a full 14-dimensional
+rational vector `x^(t) >= 0` which satisfies **all 279 other original rows** and
+strictly violates row `t`. This is checked literally against the original matrix,
+not just against `R`, a restricted LP, or an objective value.
+
+A packing dual optimum below `d_t` can suggest the coordinates on `H_t`.
+Setting each coordinate outside `H_t` to 8 covers any source row touching an
+outside bit, since every demand is at most 8. Original rows wholly inside `H_t`
+are covered by retained rows and their certified implications. This explains a
+construction of the points; their literal checks are the acceptance evidence.
+
+Given the full-original checks, any subfamily `S` of the original 280 rows
+equivalent to the full system must contain every `t` in `R`: otherwise `x^(t)`
+would satisfy `S` but fail the full system. Since `R` is itself equivalent, it is
+the unique minimum-cardinality and unique inclusion-minimal **subfamily of these
+original rows**, with the baseline `x >= 0` fixed. This claim is conditional on
+every retained point passing the stated full-original checks.
+
+No minimum over arbitrary new inequalities or alternative representations is
+claimed. Fractional separating points do not establish integer-only
+indispensability. Changing caps, adding rectangles or trimming actual supports
+changes the matrix and requires new certificates.
+
+## Credit and limits
+
+Credit Nick Petalas/PR6425 for the fixed matrix, pairwise kernel and explicit
+combined-implication handoff; Jeremy Diviney/PR1422 for the complete-clique guard,
+source geometry, caps and smaller-family question; Cinna Davis/PR1347/1323 and
+the retained E8/label/decoder lineage. Exact LP certificate semantics also have
+repository precedent in PR5767; no shared solver or 128-variable cap is changed.
+Nonnegative implication, packing/covering duality, simplex and Bland's rule are
+classical. No general mathematical priority is asserted for them.
+
+New work uses substantial OpenAI Codex assistance. A separately implemented
+certificate checker is independent code verification of a frozen certificate,
+not blind rediscovery or independent human/formal proof-kernel acceptance.
+No coefficient synthesis, complete COPY floor, native/physical supplier,
+restoration/access/precision/stock/compiler closure, signed invoice, outer
+integration, κ improvement or selected-frontier change follows.

research/p112-farkas-kernel/README.md

@@ -0,0 +1,99 @@
+# A 237-row exact P112 demand system
+
+For the fixed 14-variable, 280-row cap-demand matrix of Nick Petalas's
+[PR6425](https://github.com/CrocSwap/integer-mult-bounds/pull/6425), exact
+nonnegative rational combinations remove 43 rows. The retained 237 rows are
+equivalent for every nonnegative real multiplicity vector. Each retained row has
+a rational point satisfying all 279 other original rows and strictly violating
+that row. Together these certificates establish the **unique minimum subfamily
+of the original 280 rows**, with `x >= 0` fixed.
+
+This answers PR6425's first Open next question. Its pairwise reduction, source
+clique census and geometry-to-demand equivalence remain credited predecessor
+results; no predecessor executable or census is replayed. The present result is
+an exact reduction of the literal source matrix. It supplies no coefficients,
+decoder, physical supplier, COPY floor or κ improvement.
+
+## Concrete implication
+
+The first deleted mask is `0x1d1a`, demand 3. One half of each of the retained
+rows `0x1412`, `0x1818` and `0xd0a`, each demand 2, gives RHS 3. The resulting
+coefficient is 1 on target coordinates 1, 3, 4, 10, 11 and 12, and one half on
+coordinate 8 (zero-based); all are at most the target's coefficients. The
+missing half of coordinate 8 is supplied by `x_8 >= 0`. No single retained row
+dominates this target: the source family was already pairwise nondominated.
+`RESULT.json` retains all 43 exact combinations and all 237 full separating
+points; `PROOF.md` gives the universal implication and restricted minimum proof.
+
+## Replay
+
+CPython 3.12 and the standard library suffice. No Git executable, network, solver
+package or predecessor executable is needed for the package's two replays.
+
+```sh
+python3.12 -I -W error -B research/p112-farkas-kernel/verify.py
+python3.12 -I -W error -B research/p112-farkas-kernel/oracle.py
+```
+
+Also run with `-O`. Default commands require strict complete retained JSON;
+`--emit` prints regenerated output without overwriting files. The primary
+regenerates the certificate with bounded exact `Fraction` packing simplex and
+checks every implication and separator literally. The separate checker treats
+the sealed primary result as untrusted certificate data and computes all
+coefficient/RHS budgets and full-original-row separations independently. It does
+not import the generator, solve an LP or claim blind rediscovery.
+
+The generator uses 2,272 pivots, at most 49 per target, on this exact instance.
+Explicit time/pivot/coefficient bounds fail closed. These are generation counts,
+not a general runtime improvement. `VERIFY.json` registers the two bounded checks.
+`SOURCE-PINS.json` authenticates both inert source files before parsing them.
+`SOURCES.json` pins the originating current-main card/selected record as
+provenance; all runtime bytes are package-local.
+
+## Scope, evidence and limitations
+
+The equivalence covers nonnegative real vectors and therefore preserves all
+nonnegative integer tests too. Fractional separating points do **not** establish
+integer-only indispensability or the smallest integer-only screen. The minimum
+claim is over subfamilies of these original inequalities; it does not minimize
+arbitrary newly introduced normals or alternative descriptions.
+
+The independent checker exercises actual coefficient, demand, premise and
+separator corruptions, along with source/schema controls. `VALIDATION.md`
+records the actual run evidence, corrections and remaining obligations. Passing
+this finite necessary-condition screen does not construct coefficient vectors
+or pay for access, dirty restoration, precision, tape, stock, compiler or outer
+integration. No native, Lean, Docker, selected cold supplier or complete
+multiplication replay was run.
+
+Orientation was frozen at canonical main
+`7c49fe32c55de02c2c873655c804b16e4c3fef0a`, priority revision 8,
+selected PR6030, selected-record SHA256
+`9b8d0eea95b3bf0dfcb7938a732a6439b87a2685dec2a5ab9e525b3b34debbfa`.
+The broader `complex-rank-shape-decoder` card is explicitly changed to this fixed
+support-screen implication. Main/overlap are rechecked before submission;
+sparse/history/hidden/unpublished coverage limits are not novelty evidence.
+
+## Open next questions
+
+1. Can integer multiplicity implications remove further rows? Specify the
+   integer domain and produce integer implication/separation certificates;
+   fractional witnesses alone do not answer that question.
+2. For changed support caps, what is the new exact demand screen? Rebuild the
+   complete changed quotient before applying or attempting new combinations.
+3. Can a passing vector admit actual coefficients and a fully charged decoder?
+   Specify one vector and its full interface before synthesis and pricing.
+
+## Credit
+
+Credit Nick Petalas/PR6425 for the fixed matrix, pairwise reduction and explicit
+combined-implication question; Jeremy Diviney/PR1422 for the complete-clique
+guard, pinned geometry/caps and smaller-family question; Cinna Davis/PR1347/1323
+and Navinor, David Arias, Hanson Sun, DreamingOfClouds, themilkman216 and the
+retained E8/label/decoder lineage. PR5767 is related exact-certificate tooling;
+its code and 128-variable cap are unchanged. Nonnegative implication,
+packing/covering duality, simplex and Bland's rule are classical.
+
+New work is ToikY with substantial OpenAI Codex assistance. Separate AI
+certificate checking is not independent human review or formal proof-kernel
+acceptance. `NOTICE` preserves attribution; the two source files remain verbatim.

research/p112-farkas-kernel/SOURCE-PINS.json

@@ -0,0 +1,20 @@
+{
+  "files": {
+    "README-6425.md": {
+      "git_blob": "d9ce3b644cff65dadd88663189638a4bfd52bac3",
+      "sha256": "f35f0a30796e94ced74686bc3614b4478f5460bac0adb7c8d80827991f70ed0c",
+      "bytes": 7410,
+      "repository": "petalas/integer-mult-bounds",
+      "commit": "092dcbd13d1263e691ad29f34fbf286fea1fac2c",
+      "path": "research/p112-demand-kernel/README.md"
+    },
+    "RESULT-6425.json": {
+      "git_blob": "e18f92e001b8ce9d44287760516bf6ea002bcbcd",
+      "sha256": "f8d15306112914af299acca8720779fbc9f6f07bb1336c51e99304fdea5caf89",
+      "bytes": 22234,
+      "repository": "petalas/integer-mult-bounds",
+      "commit": "092dcbd13d1263e691ad29f34fbf286fea1fac2c",
+      "path": "research/p112-demand-kernel/RESULT.json"
+    }
+  }
+}

research/p112-farkas-kernel/SOURCES.json

@@ -0,0 +1,19 @@
+{
+  "schema_version": 1,
+  "base_commit": "7c49fe32c55de02c2c873655c804b16e4c3fef0a",
+  "files": [
+    {
+      "path": "docs/research/agent-task-catalog.json",
+      "usage": "provenance",
+      "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec",
+      "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81"
+    },
+    {
+      "path": "certificates/selected-result.json",
+      "usage": "provenance",
+      "git_blob": "d59b5035e7b4cbaa9d688a1d32dd0d6eb79c466a",
+      "sha256": "9b8d0eea95b3bf0dfcb7938a732a6439b87a2685dec2a5ab9e525b3b34debbfa"
+    }
+  ],
+  "note": "Canonical catalogue/selected are provenance only. Runtime inputs are the package-local source pair and result certificate. SOURCE-PINS.json authenticates the external source data; no predecessor executable is imported or replayed."
+}