Skip to content

Construct exact uniform two-capacity completions (no κ) - #6607

Open
petalas wants to merge 2 commits into
CrocSwap:mainfrom
petalas:research/w5-1102j-native-obstruction
Open

petalas wants to merge 2 commits into
CrocSwap:mainfrom
petalas:research/w5-1102j-native-obstruction

Conversation

@petalas

@petalas petalas commented Nov 3, 2026 •

Copy link
Copy Markdown
Contributor

Correction

Commit 0abcc978aa8ec083c0017ee50d7788e85f1cba1a corrects the auxiliary count bound reported in the FINDING. PROOF.md now states |GL_n(F_q)| <= q^(n^2), with equality only at n=0, and uses O(1+n^2 log q) bits on the full domain. The strict inequality and original asymptotic bit bound remain valid for n>=1. The zero-dimensional rank/unrank and M=1 sampling cases are explicit. Checking count storage, conditional partitions, rank/unrank, sampling and the finite cardinality guard confirms every downstream conclusion without narrowing the claim. Only PROOF.md changes; no executable or predecessor bytes change.

Summary

Construct an exact rank/unrank bijection for invertible prime-field maps extending a prescribed injection and satisfying two arbitrary simultaneous capacities. A finite fair-bit interface produces a uniform completion conditional on success and reports entropy exhaustion explicitly. Claim type: scoped written constructive proof with exact finite corroboration. No new kappa.

partial injection
  partition by the next image vector using PR6539's exact coupled count
  decode one integer rank through the consecutive intervals
  reconstruct the unique admissible complete map

For N admissible maps and b independent fair bits, exhaustion has exact probability (2^b mod N)/2^b. Every map has the same successful probability. On an unlimited stream, expected bits are below ceil(log2 N)+2. Rank or unrank uses at most 1+(n-dim U)q^n conditional-count calls, including initialization, rather than enumerating complete matrices. This remains exponential in n.

This answers the uniform-sampling opening in Ali Romman's PR6539, exact head 96c63f994af628f574c71dca0d7ed219cbfc70c2. Its count theorem is a cited premise. Credit ToikY / PR6535 for coupled feasibility, Ali Romman / PR6533 for general capacity rank counts and construction, Nick Petalas / PR6489 for the nested count, Brian / JoyboyBrian / PR5020, Cao Yifan / intqwq / PR4610, codyw912 / PR4735, and the retained native/compiler lineage. Classical self-reduction, interval coding, entropy recycling and linear algebra are not claimed as new general methods. This contribution was produced by Nick Petalas.

Evidence

  • Before: the cited two-capacity theorem counts completions and explicitly leaves uniform sampling open. After: PROOF.md supplies the enumerative construction, inverse proof, exact finite-bit distribution and operation bounds; codec.py implements it.
  • Rank and unrank agree with literal ordered matrix sets at all 2,118 admissible endpoints in 1,954 contracts. This includes the full normalized F2 dimension 0–2 and F3 dimension-1 contract domains, plus 14 further contracts over F3/F5 in dimension 2 and F2 in dimension 3. Ten selected dimension-eight ranks also round-trip and satisfy the endpoint constraints. This is not an exhaustive dimension-eight census.
  • Every output frequency and exact exhaustion count passes for 24,564 bit strings across 132 cardinality/budget pairs. For GL2(F2), all 256 eight-bit strings give 42 occurrences of each of six matrices and four exhausted strings. Fourteen domain/semantic rejection controls pass. Four external optimized mutants reject wrong rank offsets, a wrong interval boundary, biased bit reduction and corrupted predecessor proof bytes.
  • CPython 3.12.15, macOS arm64, standard library only. Both warning-strict registered commands passed locally after correction in 6.990 s and 6.442 s. These are check durations, not a speedup claim. Direct normal and optimized checks also passed.
  • Registered metadata/provenance and committed-byte/mode/source-history preflight pass for all eleven files at 0abcc978aa8ec083c0017ee50d7788e85f1cba1a. The official export passes integrity and declared-input coverage. Optimized replay from a read-only, Git-free, empty-PATH export passes after correction, leaving all twelve exported files unchanged.
  • The predecessor proof and NOTICE are verbatim and match the immutable source's SHA256 and Git blob digests. The external head is not a local Git object; the generic source-history check certifies main-based provenance, not that head's ancestry. The standalone verifier checks the retained external bytes. No predecessor executable or scientific suite was imported or replayed.

From the worktree root:

/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -W error -B scripts/research_package.py --package research/two-capacity-uniform-codec
/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -W error -B scripts/check_research_commit.py --package research/two-capacity-uniform-codec --check-source-history --check-modes
/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -W error -B research/two-capacity-uniform-codec/verify.py
/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -W error -O -B research/two-capacity-uniform-codec/verify.py

A different CPython 3.12 installation may replace the absolute interpreter path. Expected markers are PASS_TWO_CAPACITY_UNIFORM_CODEC, PASS_REGISTERED_RESEARCH_PACKAGE and PASS_RESEARCH_COMMIT_BYTES. Optional receipts are generated outside the checkout and bind every package file hash.

Limitations and unrun obligations

The executable enforces n≤12, prime q≤31, q^n≤4,096 and at most 4,096 supplied bits. The written reduction extends to finite fields with an ordered element representation and exact count oracle; extension-field arithmetic is not implemented. Empty completion sets cannot be sampled. Finite-bit success may have probability below one, and uniformity assumes independent unbiased supplied bits. No physical randomness generator is supplied.

The all-dimension statement rests on the written proof and cited count theorem. This is unrestricted GL construction, not a native/symplectic or signed-phase implementation. Actual contacts, scalar/basis prices, legal access, dirty restoration, physical routing, precision, stock, tapes, compiler and complete outer closure remain open. All five selected framework assumptions remain. No supplier admission, complete multiplication theorem or selected-frontier change follows. No Lean, Docker, selected cold replay or predecessor scientific suite ran. Independent human and formal proof-kernel review are unclaimed.

Open next questions

  1. Remove the q^n candidate factor by directly sampling the predecessor's quotient/lift factors. Start with a uniform common injection having the prescribed quotient discrepancy; exact lift multiplicities are the blocker.
  2. Bind one sampled map to an actual shared native contact and price its full caller. Specify exact bases and chronology first; symplectic/signed restrictions and physical costs remain blockers.

Related open work

  • PR6539 supplies the exact two-capacity count oracle and poses uniform sampling. This PR constructs the new bijection and sampler; it does not re-audit that theorem.
  • PR6535 proves the all-field two-capacity feasibility criterion. Its coupled prescription survives every conditional branch here.
  • PR6533 counts arbitrary capacity families at all ranks and constructs maximum-rank witnesses. This PR samples invertible completions for exactly two capacities using the faster cited oracle.
  • PR6489 proves the prior nested-capacity criterion/count. It remains predecessor credit; the sampling question taken here is explicitly PR6539's.

The final completion refresh inspected all 160 open account PRs, including the fifteen other open contributions created since the advance CLAIM. None of those new submissions studies the same prescribed two-capacity completion contract or computes its sampling distribution. The four directly related open packages above retain their stated roles. No additional scientific computation checked another contribution or compared unrelated numbers.

The advance CLAIM matches the delivered scope. Canonical main 7c49fe32c55de02c2c873655c804b16e4c3fef0a, priority revision 8 and selected PR6030 were refreshed before committing. The formal-interface-lemma card changes to this constructive finite-field side result. Live open PRs, recent account work, active Discussions, local reservations and main/merged formula/object searches were checked. The cached search covered 555 open PR bodies and 6,596 Discussion records; most sparse local notes were omitted, with separate Git README searches for the distinctive object. These checks do not establish global novelty or cover unpublished work.

CI notes

Both hosted checks, plan and replay (research/two-capacity-uniform-codec), passed at exact corrected head 0abcc978aa8ec083c0017ee50d7788e85f1cba1a in run 41639653353. The completed checks were read once with gh pr checks 6607 --repo CrocSwap/integer-mult-bounds: planning took 4m33s and replay took 1m52s.

Every local check from the contribution brief was rerun successfully after correction, including direct normal/optimized verification, fourteen rejection controls, four external corruption controls, selected-baseline bindings, committed bytes/modes/source history, official export integrity and read-only Git-free empty-PATH replay. The scientific receipt fields match the earlier published result; only the corrected PROOF.md source digest differs.

Hosted replay certifies execution of the registered normal and optimized finite checks and package bindings. The auxiliary bound reported in the FINDING was corrected in commit 0abcc978a without narrowing the claim. Independent human and formal proof-kernel acceptance remain unclaimed. No check failed.

Merge Danger

Door: two-way. Blast radius: isolated. Eleven files are added in one opt-in research package. Shared implementations, frozen predecessor packages and the selected record retain their bytes.

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