Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
1,717 changes: 1,717 additions & 0 deletions research/p104-all-projections-seed67/CERTIFICATE.json

Large diffs are not rendered by default.

13 changes: 13 additions & 0 deletions research/p104-all-projections-seed67/CLAIM.md
Original file line number Diff line number Diff line change
@@ -0,0 +1,13 @@
# Sprint claim and handoff

- Assignment seed: **67** (Python OS-backed `secrets.randbelow(100)`, obtained 2026-10-13).
- Assigned track: 60–74, adversarial mathematical audit.
- Repository base pinned: `ba82555c64e1879e4b7decce28186f208fcb8262` (main at beginning of investigation).
- Investigated predecessor: PR #1125 at `9f7c0679d64bab954b7161d8586dc626a59b92ee`; source certificate blob `9a2cd574df48361579167e39aa6198f39059f70c`.
- Three candidates: (1) independently replicate 0/1-survivor-loss widths; (2) classify two-erasure widths; (3) complete all-survivor width spectrum with automorphism and dual witnesses. Selected (3), encompassing (1) and (2) in a new finite statement.
- Claim: exact widths of the 255 nonempty projections of the frozen 104-mask cube support family; no claims outside term-preserving carrier interface.
- Method: induced-tree enumeration; exact bipartite matching to construct chain partitions; alternating-path antichains; independently verified dual witnesses; cube symmetry under 48 explicitly checked automorphisms.
- Expected deliverable: self-contained Python 3.10+ standard-library package, 21-orbit certificate, proof, negative controls and review notes.
- Coordination: no pinned sprint issue was found in available issue search. This claim was recorded locally, not posted to GitHub.
- Status: ready for focused review; PR not submitted because the connected GitHub account has no push rights to this repository and no supported fork action was available.
- All inherited assumptions and explicit provenance are recorded in PROOF.md and SOURCES.json.
13 changes: 13 additions & 0 deletions research/p104-all-projections-seed67/LICENSE
Original file line number Diff line number Diff line change
@@ -0,0 +1,13 @@
Copyright 2026 contributors.

Licensed under the Apache License, Version 2.0 (the "License");
you may not use this file except in compliance with the License.
You may obtain a copy of the License at

http://www.apache.org/licenses/LICENSE-2.0

Unless required by applicable law or agreed to in writing, software
distributed under the License is distributed on an "AS IS" BASIS,
WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
See the License for the specific language governing permissions and
limitations under the License.
74 changes: 74 additions & 0 deletions research/p104-all-projections-seed67/PROOF.md
Original file line number Diff line number Diff line change
@@ -0,0 +1,74 @@
# Exact widths of every P104 survivor projection

**Status:** scoped mathematical extension / independently checkable finite certificate; **no new κ**. This builds on the *conditional* delivery interface and terminal-read theorem of [PR #1125](https://github.com/CrocSwap/integer-mult-bounds/pull/1125) (Ali Romman). It is **not** a new decoder, supplier, frame schedule, all-size theorem, or claim that PR #1125 is already merged.

## 1. Frozen finite object

Write the 8 vertices of the three-dimensional Boolean cube as integer labels `0,...,7`, where two vertices are adjacent iff their XOR has Hamming weight one. Represent vertex subsets by 8-bit masks. The exact 104-term support family `F` is the 12 edges, 24 induced 3-vertex trees, 32 induced 4-vertex trees, 24 induced 5-vertex trees, and 12 complements of edges. The explicit 104 masks agree with the pinned `cube_supports` array in PR #1125, at blob `9a2cd574df48361579167e39aa6198f39059f70c`. `generate.py` reconstructs them *independently* by cube edge enumeration, induced connectivity and tree edge counts, rather than importing the predecessor's checker.

For any nonempty surviving term set `K`, define

F_K = {S ∩ K : S ∈ F, S ∩ K != ∅},

with duplicates removed. Order `F_K` by inclusion and denote its width by `w(K)`, the largest antichain size. There are 255 nonempty `K`. The degenerate empty `K` has width zero.

## 2. Orbit reduction is exact

Every cube automorphism has the form `v -> permute_coordinates(v) XOR t`, where the coordinate permutation has six choices and `t` has eight, giving 48 distinct permutations. The checker exhaustively verifies each permutation maps **the entire original family** `F` onto itself. Therefore for every `S` and `K`,

p(S ∩ K) = p(S) ∩ p(K),

and hence the posets `F_K` and `F_{p(K)}` are isomorphic, with identical widths. All 255 nonempty `K` split into exactly **21** cube-automorphism orbits, explicitly listed in `CERTIFICATE.json`. No orientation or geometric equivalence is assumed without finite verification.

## 3. Dual width witnesses

For each of the 21 orbit representatives, `CERTIFICATE.json` contains:

- an antichain of exactly `w` distinct members, giving `width >= w`;
- a partition of **every** member of the projected support poset into `w` strictly increasing chains, giving `width <= w`.

Both certificates are checked by `verify.py` without importing `generate.py`, solving optimization problems, or trusting recorded width values. Every member is accounted for once and every asserted inclusion is recomputed bitwise. Since an antichain meets each chain in at most one point, the two finite witnesses prove equality. Symmetry transports the proof to all 255 nonempty survivor sets.

The resulting **complete width census** is:

| Erased terms q | Remaining | Number of K | Exact widths (number of K) |
|---:|---:|---:|---|
| 0 | 8 | 1 | 32 (1) |
| 1 | 7 | 8 | 26 (8) |
| 2 | 6 | 28 | 18 (24), 20 (4) |
| 3 | 5 | 56 | 10 (56) |
| 4 | 4 | 70 | 6 (70) |
| 5 | 3 | 56 | 3 (56) |
| 6 | 2 | 28 | 2 (28) |
| 7 | 1 | 8 | 1 (8) |
| 8 | 0 | 1 | 0, trivial degenerate case |

For exactly two erased terms, **width 20 occurs iff the erased pair comprises opposite vertices of the cube**, i.e. their XOR equals `7`. The other 24 pairs have width 18. The six-vertex cases belong to three distinct automorphism orbits, though only two width values occur.

## 4. Consequences for the inherited delivery theorem

PR #1125's terminal-read theorem, with its full assumptions and endpoint / carrier / payment definitions, states:

L >= q + 2 max(0, width(F_K) - P_K),

where `q` distinct terms lose their survivor, `P_K` counts continuous term-preserving paths assigned to surviving terms, and `L` is excess paid frame-move rank. This contribution does **not** reprove the physical/scheduling premises of that theorem. Substituting the now-exact widths yields additional conditional obstructions for every `q = 2,...,7`.

In particular, for **two erased terms**:

L >= 2 + 2 max(0, 18 - P_K) (non-opposite erased pair)
L >= 2 + 2 max(0, 20 - P_K) (opposite erased pair).

If `P` counts all delivery paths, and every erased term has at least one path, then `P_K <= P - 2`. Thus

L >= 2 + 2 max(0, 20 - P) (non-opposite pair)
L >= 2 + 2 max(0, 22 - P) (opposite pair).

For example, **P <= 18** forces **L >= 6** for non-opposite pairs and **L >= 10** for opposite pairs, provided exactly two terms are erased. These bounds improve the previously used generic `L >= q = 2` for this scoped path budget. They are necessary conditions, not constructs of any legal schedule. For `q >= 3`, substitute the row-specific widths in the same inequality. All transformations retain the original separate source, restoration, finite-invoice and analytic assumptions.

## 5. What was and was not established

- **Proved by finite witnesses:** the complete 255-case projection width table in the frozen 104-support cube model.
- **Conditional corollaries:** sharpened rank/path lower bounds assuming PR #1125's terminal-read theorem and *its precise interface*, rather than an arbitrary mixing or changed-COPY decoder.
- **Not claimed:** a new conditional exponent, a direct correction to an accepted frontier, a proof of all 7,168 geometrically labeled decoders independent of PR #1125's support-uniformity assertion, an unrestricted impossibility theorem, or a complete integer multiplication algorithm.

An optional SciPy sparse-matching oracle independently repeats all 255 cases and checks the opposite-pair condition. The 21 antichain/chain-cover certificates are exact finite proofs of these poset widths; they are not a formal proof of the physical terminal-read theorem. `verify.py` also exercises ten adversarial corruptions and rejects all ten. The full P104 path-price obligation for new constructions remains open.
33 changes: 33 additions & 0 deletions research/p104-all-projections-seed67/PR_BODY.md
Original file line number Diff line number Diff line change
@@ -0,0 +1,33 @@
## Status

**Mathematical audit / scoped finite proof extension; no new κ.** Independent all-survivor width classification in the P104 fixed cube-support family. Depends on the currently open PR #1125's support-uniformity claim and term-preserving terminal-read theorem for its delivery-cost interpretation; it does not change the selected frontier.

## New finite result

- Classifies all **255 nonempty survivor masks** using 21 exact cube-automorphism orbits and antichain/chain-cover dual certificates.
- Erasing two opposite cube vertices leaves width **20**; the other 24 pairs leave width **18**. With 3, 4, 5, 6 or 7 erasures the widths are respectively **10, 6, 3, 2, 1**, independent of the deletion geometry.
- The inherited inequality `L >= q + 2 max(0, width(F_K)-P_K)` now has exact finite width inputs for every `q` from 0 through 7. For exactly two erasures and `P <= 18`, this implies `L >= 6`, or `L >= 10` for opposite erased vertices, under #1125's explicit interface.

## Reproduce

```sh
python3 -I -B research/p104-all-projections-seed67/verify.py
```

Expected `PASS_P104_ALL_PROJECTIONS orbits=21 subsets=255 negative_controls=10 no_new_kappa`.

Optionally, with SciPy installed:

```sh
python3 -I -B research/p104-all-projections-seed67/independent_scipy.py
```

Expected `PASS_SCIPY_INDEPENDENT_MATCHING subsets=255 antipodal_pairs=4 no_new_kappa`.

The default acceptance is standard-library only, checks every literal antichain, chain partition and cube symmetry, and deliberately rejects 10 corrupted certificates. The optional SciPy implementation uses a disjoint matching backend. The 104-mask data is pinned to source PR1125 at head `9f7c0679d64bab954b7161d8586dc626a59b92ee`, certificate blob `9a2cd574df48361579167e39aa6198f39059f70c`, and also reconstructed independently from induced cube trees.

## Scope and credit

Base `ba82555c64e1879e4b7decce28186f208fcb8262`, refreshed main `ce7ad1b6ab09452c3478723a2e96ed5ff212dc08` at check. No changes to `upstream/` or selected frontier; no full theorem or runnable supplier claimed. The PR should be reviewed after or alongside PR #1125; if #1125 changes, reconfirm pins and assumptions.

Prepared for `@Chrisbryan17` with substantial GPT-6 assistance. Source decoder, theorem and initial widths: Ali Romman (#1125). Additional context: #1071 and #968. Licensed under Apache-2.0.
45 changes: 45 additions & 0 deletions research/p104-all-projections-seed67/README.md
Original file line number Diff line number Diff line change
@@ -0,0 +1,45 @@
# P104 all-survivor projection width audit (seed 67)

**Research audit, finite proof certificates, no new κ.** Extends [Ali Romman's PR #1125](https://github.com/CrocSwap/integer-mult-bounds/pull/1125) from zero/one erasures to the full nonempty survivor family in the P104 cube-support model.

## Reproduce

Requires Python 3.10+ and only its standard library, from any working directory:

```sh
python3 -I -B research/p104-all-projections-seed67/verify.py
```

Expected terminal header:

```text
PASS_P104_ALL_PROJECTIONS orbits=21 subsets=255 negative_controls=10 no_new_kappa
```

Regenerate (developer-only) and compare the file exactly with the committed certificate:

```sh
python3 -I -B research/p104-all-projections-seed67/generate.py
python3 -I -B research/p104-all-projections-seed67/verify.py
```

`generate.py` derives the 104 supports from cube connectivity, solves the exact 255 finite posets, and writes 21 orbit-compressed antichain/chain-cover witnesses. `verify.py` does **not** import the generator and checks each witness and orbit action directly. An optional, separately implemented SciPy sparse-matching oracle is available as `python3 -I -B research/p104-all-projections-seed67/independent_scipy.py` (requires SciPy and NumPy); it repeats all 255 width calculations independently. The pin for the 104 source masks is independently committed in the checker as SHA-256 of compact JSON.

## Result

| Erasures | Width(s) | Multiplicity |
|---|---|---|
| 0 | 32 | 1 |
| 1 | 26 | 8 |
| 2 | 18 or 20 | 24 or 4, respectively |
| 3 | 10 | 56 |
| 4 | 6 | 70 |
| 5 | 3 | 56 |
| 6 | 2 | 28 |
| 7 | 1 | 8 |

For two erasures, the stronger width 20 holds precisely when the deleted vertices are opposite on the cube. See `PROOF.md` for the proof, conditional delivery-rank corollaries and remaining assumptions.

**Scope:** no selected frontier edits; `upstream/` unchanged; no κ claim or all-size theorem; PR #1125 is an open predecessor as of this handoff. This package is an independent finite extension, but it depends on #1125's terminal-read premise to draw scheduling conclusions.

**Attribution:** Prepared for GitHub user `@Chrisbryan17` with substantial OpenAI GPT-6 assistance (analysis, implementation, verification and documentation). Original P104 support uniformity, theorem and initial width certificates: Ali Romman, PR #1125. Prior fixed-delivery findings and underlying frames: PR #1071 and PR #968 and their predecessors. Apache-2.0 repository license applies; retain all predecessor credits.
12 changes: 12 additions & 0 deletions research/p104-all-projections-seed67/SOURCES.json
Original file line number Diff line number Diff line change
@@ -0,0 +1,12 @@
{
"license": "Apache-2.0",
"research_base": "ba82555c64e1879e4b7decce28186f208fcb8262",
"source_pr": "https://github.com/CrocSwap/integer-mult-bounds/pull/1125",
"source_pr_head": "9f7c0679d64bab954b7161d8586dc626a59b92ee",
"source_path": "research/p104-asynchronous-carrier-bound/CERTIFICATE.json",
"source_blob_sha": "9a2cd574df48361579167e39aa6198f39059f70c",
"source_supports_compact_json_sha256": "adc1b55add8d480dbe1a6baf2c8322495a7176eca698bb6899cb698fce1de087",
"dependency_note": "Uses the 104 cube support masks and the term-preserving terminal-read theorem from Ali Romman's PR1125, which was open at the time of this audit. Independently reconstructs the cube supports for the finite combinatorial calculation. No independent proof of PR1125's physical decoder uniformity or scheduling theorem is asserted.",
"contributor": "@Chrisbryan17 with substantial OpenAI GPT-6 assistance",
"additional_predecessor_prs": [1071, 968]
}
22 changes: 22 additions & 0 deletions research/p104-all-projections-seed67/VALIDATION.json
Original file line number Diff line number Diff line change
@@ -0,0 +1,22 @@
{
"status": "pass",
"date_utc": "2026-10-13",
"track": "adversarial-mathematical-audit",
"assignment_seed": 67,
"base_commit": "ba82555c64e1879e4b7decce28186f208fcb8262",
"refresh_main_commit": "ce7ad1b6ab09452c3478723a2e96ed5ff212dc08",
"audited_pr": 1125,
"audited_pr_head": "9f7c0679d64bab954b7161d8586dc626a59b92ee",
"certificate_sha256": "2a78bac08cefd16ef14c7c1face1ea990ea6d8d04d5e88978ba0fac7843bf809",
"tests": [
{"command": "python3 -I -B verify.py", "result": "PASS_P104_ALL_PROJECTIONS orbits=21 subsets=255 negative_controls=10 no_new_kappa"},
{"command": "python3 -I -O -B verify.py", "result": "pass"},
{"command": "python3 -I -B independent_scipy.py", "result": "PASS_SCIPY_INDEPENDENT_MATCHING subsets=255 antipodal_pairs=4 no_new_kappa"},
{"command": "python3 -I -B generate.py", "result": "byte-identical CERTIFICATE.json"},
{"command": "python3 -I -B /mnt/data/tmp_verify_relocated/analysis/verify.py", "result": "pass from relocated directory"}
],
"proof_scope": "Exact widths of all nonempty projections of frozen 104-mask cube support family. Uses accepted finite dual witnesses and orbit-symmetry transport; delivery ranks are conditional on PR1125 theorem.",
"github_submission": "not submitted: connected account lacks upstream push permission and no fork exists",
"independent_human_review": false,
"substantial_ai_assistance": true
}
Loading