Skip to content

Prove the sharp rank-only P104 support floor 96 (no κ) - #6275

Merged
Mister-Meeseeks merged 1 commit into
CrocSwap:mainfrom
petalas:research/w9-1030b-original-obstruction
Oct 31, 2026
Merged

Mister-Meeseeks merged 1 commit into
CrocSwap:mainfrom
petalas:research/w9-1030b-original-obstruction

Conversation

@petalas

@petalas petalas commented Oct 30, 2026

Copy link
Copy Markdown
Contributor

Summary

Scoped written proof with exact finite corroboration: the P104 rank-only owned-delivery relaxation has exact minimum NEED = 96 at rank cap 56. This sharpens the inherited lower bound 90 and classifies every minimizer.

unit diagonal + rank <= 56 + P104 allowed mask
  -> NEED >= 2(104-56) = 96
  -> equality: 48 reciprocal rank-one pairs + 8 singletons

DreamingOfClouds's #6170 supplies the P_M identity, rank-to-paid premise, prior bound and abstract 96-entry example. The new contribution is exact optimality, equality rigidity and a witness in the actual orthogonality mask. Gruber's random-order acyclic-set bound and elementary rank/graph facts are classical; no literature-wide priority is claimed for those ingredients. This contribution was produced by Nick Petalas. Credit Ali Romman for PR5599's retained ports and Matarener / #6267 for distinguishing the matrix and physical premises, with the retained P104/native/helper/controller/caller lineage.

Only research/p104-rank-support-extremizers/ is added. Canonical base is 2485805a6d47f36ea83ddde6327d453ac82d44dc, priority revision 8. Advance claim.

Evidence

  • Before: the cited continuous Jensen relaxation gives NEED >= 90. After: the written integral-degree argument gives the exact minimum 96 and all equality cases over every field. The 104-port witness has exactly 96 off-diagonal nonzeros, rank 56 over Q/F2/F3 and the correct mask. A rational reciprocal-weight witness also has rank 56.
  • Local warning-strict normal and optimized checks cover all 4,165 unit-diagonal binary matrices through dimension four, all 739 ternary matrices through dimension three, independent XOR-basis/Leibniz-minor rank routes, 5,460 degree cases and nine controls. Both modes print PASS_P104_RANK_SUPPORT_EXTREMIZERS and identical generated hash-bound receipts.
  • Metadata/pins and both registered commands pass. Each VERIFY command was timed locally: normal 0.11 s, optimized 0.12 s, well within the 120 s limits. These are execution-budget observations, not performance-improvement claims.
  • Exact committed bytes, modes and declared source-history ancestry pass for eight package/input files at 681c547a36e742eceebbde04cb427bcd10cd3293. Official export and declared-input coverage pass. Both modes pass in a read-only Git-free export with empty PATH; all nine exported files retain bytes/modes. Actual source corruption rejects in both modes.

Reproduce from the worktree root with CPython 3.12 and the standard library:

/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -W error -B research/p104-rank-support-extremizers/verify.py
/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -W error -O -B research/p104-rank-support-extremizers/verify.py
/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/p104-rank-support-extremizers
/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/p104-rank-support-extremizers --check-source-history --check-modes

Another CPython 3.12 path can replace the local interpreter. The verifier reads the hash-pinned source's port field and never executes its program. No predecessor scientific suite is the deliverable.

Limitations and unrun obligations

The attaining matrix is not a legal owned layer of paid cost 56. The P_M identity and rank-to-paid implication remain cited premises and are not transferred to P' accounting. The exact relaxed optimum shows that rank, diagonal and mask alone stop at 96; it does not settle the physical NEED >= 3597 objective. Gather/landing geometry, shared ancestry, source reads, lifetimes and the complete paid/productive invoice still matter.

No native supplier, selected-frontier change, new kappa or complete multiplication theorem is claimed. All five selected framework assumptions remain. Independent human and formal proof-kernel review are unclaimed. Selected cold replay, historical suites, Lean and Docker were not run. Every registered local obligation ran; none is deferred to CI alone.

Related open work

  • #6267 studies the same P_M owned-delivery matrix and physical floor through lineage factorization, branching and scoped source review. This proves the exact matrix support relaxation and its equality cases; it does not recompute its word counts or resolve its physical NEED premise.

The current open-PR, Discussion, recent-account, main README and merged object/formula searches found no other submission computing this exact extremum. Sparse local-note and unpublished-work coverage remain incomplete; no novelty certificate is implied.

Open next questions

Which extra owned-geometry condition excludes every 48-pair matrix extremizer under paid <= 56? Start with one actual gather/landing or source-content constraint, retaining shared ancestors and public reads. A complete physical bound is the blocker. This package stops at the first exact relaxation improvement.

CI notes

CI pending at head 681c547a36e742eceebbde04cb427bcd10cd3293. All registered checks passed locally. No hosted result is claimed yet.

Merge Danger

Door: two-way.

Blast Radius: isolated. Seven new package files and one unchanged declared input; no shared checker or selected-frontier edits.

@Mister-Meeseeks
Mister-Meeseeks merged commit 94ad794 into CrocSwap:main Oct 31, 2026
2 checks passed
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.

2 participants