Skip to content

Prove an exact Gaussian boundary determinant and rank obstruction (no κ) - #6404

Open
petalas wants to merge 1 commit into
CrocSwap:mainfrom
petalas:research/w10-1102b-bottleneck
Open

petalas wants to merge 1 commit into
CrocSwap:mainfrom
petalas:research/w10-1102b-bottleneck

Conversation

@petalas

@petalas petalas commented Nov 2, 2026 •

Copy link
Copy Markdown
Contributor

Summary

A scoped mathematical proof gives the exact cross-rim determinant after eliminating a contiguous interior of a truncated Gaussian:

bandwidth b, interior length m>=b, nonzero t, invertible interior A
    det C = (-1)^(bm) t^(b^2(m+b)) / det A
    rank C = b
    every exact factorization C=UV through k scalars has k>=b

The formula holds over every field. A more general outer-band product identity and covariance under nonzero diagonal gauges are proved in research/gaussian-cross-rim-determinant/PROOF.md. The exact rational fixture b=2, m=3, t=1/2 has det A=135/256 and det C=1/552960.

The new result is the exact determinant, including parameters and fields outside the older real positivity range. Full-rank consequences in 0<t<=1/3 already follow from Nick Petalas's PR5207 ordered-minor theorem and remain credited to it. The triangular-minor and block-determinant identities are classical; no general literature-priority claim is made. This is an original boundary question, not a predecessor audit. No new kappa or selected-frontier change is claimed.

Evidence

Earlier bandwidth/support and restricted sign results do not provide this exact determinant. The new direct rational Schur construction and fraction-free host-minor calculation agree in every one of 144 Gaussian, 20 asymmetric banded and 12 signed-gauge cases. Eight invalid inputs reject and three semantic counterexamples pass. The all-size and arbitrary-field claims rest on the written proof; the finite checker runs over Q.

Local CPython 3.12.15 on macOS passes both registered commands, with identical normal/optimized receipts. Individually timed commands take 0.1033 and 0.1041 seconds locally, below their 120-second limits. Generated stdout receipts bind all six package-file hashes. AST/function-size inspection passes, with maximum function length 29 lines. Committed bytes and declared source ancestry pass at 9bb6afaa2b8f6c837bd6ff407e365fdae6382e7e.

Exact reproduction from the repository root:

/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/gaussian-cross-rim-determinant/verify.py
/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -O -B research/gaussian-cross-rim-determinant/verify.py
/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/gaussian-cross-rim-determinant
/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/gaussian-cross-rim-determinant --check-source-history

Expected markers are PASS_GAUSSIAN_CROSS_RIM_DETERMINANT, PASS_REGISTERED_RESEARCH_PACKAGE and PASS_RESEARCH_COMMIT_BYTES. Substitute another CPython 3.12 path if needed. No third-party dependencies, network access or predecessor executable is required by the standalone verifier. The selected metadata orientation separately passes.

Limitations

This only rules out an exact linear factorization of the entire cross-rim map through fewer than b scalar channels. It does not bound recursive calls, machine instructions or an implementation retaining other cross-rim paths. Approximate rank and low displacement rank remain possible. The caller already allows O(b) boundary width, so its asymptotic cost is unchanged.

Actual caller/kernel/truncation admission, useful singular-value bounds, rounded error propagation, native/physical costs and all five framework assumptions remain open. No predecessor scientific replay, selected cold replay, finite-field census, Lean, Docker, independent human review or formal proof-kernel acceptance ran. The arbitrary-field argument is written, not a claimed exhaustive computation.

Open next questions

Can approximate cross-rim compression improve one actual retained solve's complete paid bill? First pin the literal kernel, truncation, gauges and allowed final error, then prove a singular-value tail bound and charge representation, movement and error propagation. Exact full rank alone does not decide this. Research stopped at the first verified formula.

Related open work

  • PR1754 proposes structured boundary solves using displacement rank. The ordinary cross-rim rank proved here does not exclude that representation or audit its cost.

  • PR1758 adds shifted/gauged Gaussian interiors to those structured solves. This proof preserves exact rank under nonzero diagonal gauges and does not check the proposed numerical implementation.

  • PR371 accounts for final-grid Gaussian rounding. This exact determinant does not estimate rounded errors or alter that result.

  • PR3910 proves a physical Gaussian row-norm transfer bound for a different local contract. No row-norm quantity is computed or compared here.

  • PR6405 determines the sharp uniform real range 0<t<=1/2 for ordered minors and Schur-fill signs of the same truncated kernel. This PR gives the exact cross-rim determinant over every field, conditional on interior nonsingularity. No shared determinant value is computed by PR6405, and no extra comparison computation was run.

Credit and coordination

This contribution was produced by Nick Petalas. Credit Cinna Davis PR4100 for the Gaussian caller; unpaidmoon PR4373, James Reed PR4285/4298/4299 and Ryanson Jonathan PR4407 for carve/bandwidth/fill work; and Nick Petalas PR5207 for real-entry signs. All predecessor bytes and credit lines remain unchanged. Apache-2.0.

Advance CLAIM. Canonical main 7c49fe32c55de02c2c873655c804b16e4c3fef0a, priority revision 8, was refreshed before submission. Live open work, claims, local reservations, merged searches and main README searches were checked; unpublished work and historical diffs remain coverage limits.

CI notes

Hosted CI passed at exact head 9bb6afaa2b8f6c837bd6ff407e365fdae6382e7e in run 41527598351. Both plan and replay (research/gaussian-cross-rim-determinant) succeeded. The completed checks were read once, and run metadata confirms the successful conclusion and matching head. Hosted replay certifies the registered finite checks and package validation; the universal theorem rests on PROOF.md. Local normal/optimized replay and committed-byte/source-history checks also pass. Related open work was refreshed against this account's open PRs created since the CLAIM, including PR6405; no common computed number disagrees.

Merge Danger

Door: Two-way.

Blast Radius: Research.

Only six files in one new package are added. Shared code, pinned evidence and the selected frontier are unchanged.

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