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

research/p112-integer-demand-kernel/NOTICE

@@ -0,0 +1,16 @@
+New integer projection, certificate generation/checking and package metadata:
+ToikY with substantial OpenAI Codex assistance. Apache-2.0.
+
+Three source objects are retained verbatim and authenticated by SOURCE-PINS.json:
+- MATRIX-6425.json: Nick Petalas's PR6425 fixed280-row/14-variable P112 kernel.
+- REAL-RESULT-6455.json: ToikY/OpenAI Codex PR6455 exact real-domain certificate.
+- README-6455.md: PR6455 scope, attribution and open integer-only question.
+
+Retain credit to Jeremy Diviney/PR1422 for the original smaller-family question,
+complete-clique guard, geometry and support caps; Cinna Davis/PR1347/1323, Navinor,
+David Arias, Hanson Sun, DreamingOfClouds, themilkman216 and the retained
+E8/label/decoder lineage. All earlier source headers and credits remain.
+
+No predecessor executable or scientific clique census is replayed. Weak
+compositions/stars-and-bars, monotonicity and finite integer implication are
+classical; no general mathematical priority is claimed.

research/p112-integer-demand-kernel/PROOF.md

@@ -0,0 +1,123 @@
+# Exact integer projection of the fixed P112 demand system
+
+The source matrix has 280 distinct nonempty 14-bit masks `H_t`, each with integer
+demand `1 <= d_t <= 8`. Its row is `sum_(k in H_t) x_k >= d_t`. This proof fixes
+the common domain `x in Z^14`, `x >= 0`, with no upper bounds. Source objects are
+authenticated before parsing. The original clique census and geometry-to-demand
+equivalence remain credited PR6425 premises, not new replays.
+
+## Complete finite projection of a counterexample
+
+An integer vector violating target `(I,d)` has
+
+    sum_(k in I) x_k <= d-1 <= 7.
+
+Thus its inside coordinates are one of the finitely many weak compositions with
+total at most `B=d-1`. This is a consequence of a target violation, not an assumed
+global bound on multiplicities.
+
+For any such inside assignment, set every coordinate outside `I` to 8. Every
+other source row either has support contained in `I`, or has an outside bit. The
+latter row has LHS at least 8 and hence satisfies its demand. Distinct masks mean
+that a different row contained in `I` is a **proper** subset row. Consequently a
+global integer counterexample to the target exists if and only if one of the
+inside weak compositions satisfies every proper-subset source row.
+
+The forward implication follows by restricting any global counterexample. For
+the reverse, extend by 8 as above. Each resulting full vector is nevertheless
+checked literally against all 279 other original rows before acceptance as a
+separating point. No inference from a partial point or solver status is used.
+
+## Enumeration and coverage
+
+For `k=|I|`, the number of nonnegative inside vectors of total at most `B` is
+
+    binomial(k+B,k).
+
+Introduce a slack coordinate equal to `B - sum inside` to obtain ordinary weak
+compositions of exactly `B` into `k+1` parts. Stars and bars gives this count.
+
+The primary traverses coordinate multisets of each total `0..B`; counting the
+multiplicity of each coordinate is a bijection to the inside vectors. The
+separate checker uses an iterative vector-budget tree: at each coordinate assign
+an integer from zero through the remaining budget, then continue with the
+remainder. At depth `k`, each inside vector occurs exactly once; leftover budget
+is the implicit slack. These are distinct executable enumerations of the same
+complete domain.
+
+For a negative classification, every profile must be visited and fail at least
+one proper-subset source inequality. The exact closed-form count and the
+histogram of the first failing row are checked. The count or histogram alone is
+not the proof of exhaustive rejection: both implementations regenerate all
+profiles, and the enumeration bijections justify coverage. Positive search may
+stop early only after producing an actual full integer separating point.
+Capacity exhaustion is UNKNOWN and nonzero; it must not produce a complete
+minimum certificate.
+
+## One integer-only implication
+
+One concrete integer-only deletion illustrates the domain change. Target
+`0x1ada` has demand 5. One half of each source row `0x5a` (demand 4), `0x1a98`
+(demand 3), and `0x1ac2` (demand 2) has **exactly** the target coefficient vector
+and RHS `9/2`. Hence its integer LHS is at least `ceil(9/2)=5`. The corresponding
+real-domain separator from PR6455 has target LHS `9/2` and satisfies the other
+279 rows, so deleting this row over the reals would be unsound. The new complete
+projection independently checks all 495 inside integer profiles for this target.
+The half-sum/rounding example is explanatory; the full result uses complete
+negative projections and literal integer separating points.
+
+## Reused predecessor evidence
+
+PR6455 already supplied 43 exact real-domain deletion certificates and 134
+integral separating points. These are validated as data and credited, not new
+integer discoveries. Each reused deletion is checked as a nonnegative rational
+combination of proper-subset source rows whose coefficient vector is at most
+the target and whose RHS is at least its demand. Each reused integral point is
+parsed as integral/nonnegative and rechecked against all 279 other original
+rows. The new classification resolves the remaining 103 labels.
+
+No predecessor executable, LP solver or 262,928-clique census is imported or
+replayed. The earlier real minimum gives a 237-row candidate integer system;
+the 134 literal integral points force at least those 134 rows. These are existing
+coverage bounds, not the new answer.
+
+## Joint deletion and the restricted integer minimum
+
+Let `R` be the new retained rows. Every deleted row is justified either by a
+reused rational implication or by exhaustive rejection of its finite inside
+counterexample domain. Both types use only proper-subset original rows as
+premises. Induct on support cardinality: an integer solution of `R` satisfies
+each earlier proper-subset row, whether retained or already implied. The rational
+implication then establishes a reused target. For a new negative target, a
+violation would give a visited profile failing one of those already-established
+proper-subset rows, a contradiction. Therefore every integer solution of `R`
+satisfies all original rows. The converse is immediate because `R` is a
+subfamily. Simultaneous deletion has no circular premises.
+
+Every retained row has a full nonnegative integer point satisfying all 279
+other originals and violating that row. Any original-row subfamily equivalent
+to the full integer system must contain that row, since otherwise this point
+would satisfy the subfamily. Hence, once all classifications and witnesses pass,
+`R` is the unique minimum-cardinality and unique inclusion-minimal equivalent
+**subfamily of the original 280 inequalities** over the integer orthant.
+
+This does not minimize arbitrary new inequalities. The minimum claim concerns
+unrestricted integer multiplicities: its witness points need not satisfy an
+additional cost/COPY budget or multiplicity cap. The all-orthant equivalence can
+still be conjoined with any identical additional constraints on both systems;
+the minimum property itself need not persist in that restricted domain.
+
+## Scope and credit
+
+This is a source-bound necessary-condition screen. Integer separating points
+are inequality counterexamples, not decoders or physical call constructions.
+Changed supports require a new matrix and extension bound. Coefficients, full
+decoder/COPY pricing, native/access/dirty restoration/precision/tape/stock/compiler
+and outer admission remain outside scope; no κ or frontier change follows.
+
+Credit Nick Petalas/PR6425, Jeremy Diviney/PR1422, Cinna Davis/PR1347/1323 and the
+retained E8/label/decoder lineage. Credit ToikY with OpenAI Codex/PR6455 for the
+real certificates, literal integral points and explicit integer-domain question.
+Weak compositions, monotonicity and finite integer implication are classical.
+New code/proof uses substantial OpenAI Codex assistance. Separate AI checking
+does not constitute human or formal proof-kernel acceptance.

research/p112-integer-demand-kernel/README.md

@@ -0,0 +1,107 @@
+# An exact 139-row integer P112 demand subfamily
+
+The fixed 280-row, 14-variable P112 demand system has a **unique minimum
+139-row original subfamily over nonnegative integers**, with no upper bounds.
+This resolves [PR6455](https://github.com/CrocSwap/integer-mult-bounds/pull/6455)'s
+integer-only question after its 237-row real-domain minimum.
+
+The new work removes 98 additional rows by complete integer projections and
+finds five new integer separating points. The 43 earlier real-domain deletions
+and 134 existing integral points are authenticated, validated and credited reuse.
+Thus all 103 previously unresolved labels are decided. Every one of the 139
+retained rows has a full integer point satisfying all 279 other original rows
+and violating that row; these force every equivalent original-row subfamily to
+contain all 139. No minimum over arbitrary new inequalities is claimed.
+
+## Why a finite test covers unrestricted integer multiplicities
+
+For a violated target `(I,d)`, integrality forces the total of the target
+coordinates to at most `d-1 <= 7`. Set every outside coordinate to 8: every row
+with an outside bit is then satisfied. The remaining constraints have proper
+subset supports. Exhausting the inside weak compositions therefore decides
+whether a global counterexample exists, despite unrestricted multiplicities.
+Support-cardinality induction makes simultaneous old/new deletions sound.
+`PROOF.md` states the complete projection, enumeration and minimum arguments.
+
+For example, half of source rows `0x5a` (demand 4), `0x1a98` (3) and `0x1ac2`
+(2) gives exactly the coefficient vector of target `0x1ada` with RHS `9/2`.
+Its integer LHS is therefore at least 5, the target's demand. The source's
+real separating point has LHS `9/2`, showing why the row was needed over reals.
+The new projection checks all 495 inside integer profiles for this target.
+
+## Replay and evidence
+
+CPython 3.12 and the standard library suffice; no Git, network, LP solver or
+predecessor executable is required for these two package replays.
+
+```sh
+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
+```
+
+Both also pass with `-O`. Default commands require complete strict retained
+JSON; `--emit` prints candidates without overwriting files. All three inert
+source objects are authenticated before parsing. The primary uses coordinate
+multisets; the separate checker uses iterative vector-budget DFS and imports
+no primary or predecessor code.
+
+All 98 new negative domains exhaust 336,386 profiles, independently regenerated
+with exact closed-form counts and first-miss histograms. The primary visits
+340,727 profiles across all 103 new targets, including 4,341 positive early-stop
+profiles. The separate checker validates positive witnesses directly and does
+not reproduce that first-positive search order. It checks 16 rejection cases
+and a literal two-dimensional DFS coverage toy. Saved-count/histogram mutations
+test receipt drift; they do not remove profiles from the enumerator.
+
+Primary `profile_sha256` values describe its ordered multiset transcript and
+are regenerated by the primary only. The separate checker ignores these
+optional order-specific hashes and independently regenerates all mathematical
+obstruction fields and histograms. Neither a hash nor a count alone certifies
+exhaustion. Profile/time/input capacities reject instead of silently truncating.
+`VALIDATION.md` records source identities, actual runs and remaining obligations.
+
+## Scope and limits
+
+The result concerns exactly the original PR6425 masks and unrestricted
+`Z^14 >= 0`. The inside total bound is derived from violating a particular row;
+it is not a global cap on multiplicities. The all-orthant equivalence remains
+valid if identical extra constraints are conjoined to both systems. The minimum
+claim itself need not persist under a cost/COPY budget or multiplicity caps,
+because its separating points may fail those extra constraints.
+
+The source clique census and geometry-to-demand equivalence are credited
+predecessor coverage and are not replayed. Passing the screen produces no
+coefficients, decoder, physical calls, COPY floor, paid supplier or κ. Native,
+access, dirty restoration, precision/tape, stock, compiler and outer integration
+remain open. No selected supplier, native, Lean or Docker replay was run.
+
+Canonical orientation: main `7c49fe32c55de02c2c873655c804b16e4c3fef0a`,
+priority revision 8, selected PR6030, selected-record SHA256
+`9b8d0eea95b3bf0dfcb7938a732a6439b87a2685dec2a5ab9e525b3b34debbfa`.
+The broader `complex-rank-shape-decoder` card is explicitly changed to this
+integer support-screen implication. Main/overlap are refreshed before submission;
+bounded searches and sparse/hidden/unpublished/history gaps are not novelty
+certificates. All five selected framework assumptions remain.
+
+## Open next questions
+
+1. What is the minimum original-row subfamily under one exact cost/COPY budget?
+   State that domain first; the unrestricted witness points do not settle it.
+2. Can a passing integer vector admit actual coefficients and a fully charged
+   decoder? Freeze one vector/interface before synthesis and complete pricing.
+3. For changed support caps, rebuild the complete quotient and establish its
+   valid integer projection/extension bound before reducing rows.
+
+## Credit
+
+Credit Nick Petalas/PR6425 for the original kernel; Jeremy Diviney/PR1422 for
+the guard, geometry/caps and smaller-family question; Cinna Davis/PR1347/1323,
+Navinor, David Arias, Hanson Sun, DreamingOfClouds, themilkman216 and the retained
+E8/label/decoder lineage. Credit ToikY/OpenAI Codex/PR6455 for the real reduction,
+literal integral points and explicit integer-only question. Weak compositions,
+monotonicity and integer implication/rounding are classical.
+
+New work uses substantial OpenAI Codex assistance. Separate AI checking is not
+human review or formal proof-kernel acceptance. `NOTICE` and `SOURCE-PINS.json`
+retain exact source heads, Git blobs and attribution; predecessor files remain
+verbatim. No merge or selected-frontier change is part of this contribution.

research/p112-integer-demand-kernel/SOURCE-PINS.json

@@ -0,0 +1,28 @@
+{
+  "files": {
+    "MATRIX-6425.json": {
+      "git_blob": "e18f92e001b8ce9d44287760516bf6ea002bcbcd",
+      "repository": "petalas/integer-mult-bounds",
+      "commit": "092dcbd13d1263e691ad29f34fbf286fea1fac2c",
+      "path": "research/p112-demand-kernel/RESULT.json",
+      "bytes": 22234,
+      "sha256": "f8d15306112914af299acca8720779fbc9f6f07bb1336c51e99304fdea5caf89"
+    },
+    "REAL-RESULT-6455.json": {
+      "git_blob": "1ee2f6269556d155b5d265b8c1a0ace6b0e13e22",
+      "repository": "ToikY/integer-mult-bounds",
+      "commit": "7fdae743973bebb77daf4508d05655dc1e8915c7",
+      "path": "research/p112-farkas-kernel/RESULT.json",
+      "bytes": 31660,
+      "sha256": "b477f2a8d144ed884c78ee29ac76fd88c95b076eb2dd290ef2431dd7e4969704"
+    },
+    "README-6455.md": {
+      "git_blob": "27aea79adbd206d95ffe94f01fa69d8ca478ab5e",
+      "repository": "ToikY/integer-mult-bounds",
+      "commit": "7fdae743973bebb77daf4508d05655dc1e8915c7",
+      "path": "research/p112-farkas-kernel/README.md",
+      "bytes": 5522,
+      "sha256": "dd2849071a27cf4fa8023a8d3cba767199afeb977cc7e5c5acab361e5006804d"
+    }
+  }
+}

research/p112-integer-demand-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 metadata is provenance only. Runtime closure is three inert source data/documents plus the new certificate, all package-local and independently authenticated. No predecessor executable or clique census is run."
+}