Skip to content

Prove the sharp rectangular native-fusion approximation floor (no κ) - #7249

Open
petalas wants to merge 1 commit into
CrocSwap:mainfrom
petalas:research/w5-1111d-frontier-obstruction
Open

petalas wants to merge 1 commit into
CrocSwap:mainfrom
petalas:research/w5-1111d-frontier-obstruction

Conversation

@petalas

@petalas petalas commented Nov 11, 2026 •

Copy link
Copy Markdown
Contributor

Summary

Scoped written proof with exact finite corroboration: the sharp relaxed error for replacing two independent rank-one Gaussian tensor targets through one rank-r child, norm-bounded rectangular adapters and a column-sparse bypass is

d = 2^f, alpha = 2^(-(r-1)f/2)
min max-column error = min normalized-Frobenius error
                     = sqrt(1-h/d) max(0,1-M alpha)

Here r>=2, the adapter maximum-column-sum/maximum-row-sum norm product is at most M, and the bypass has at most h nonzeros per column. Every column obeys the lower bound. A two-spectator projected construction attains both minima simultaneously in the relaxation.

For fixed M and sublinear bypass support, the error tends to one. At f=8, r=2 and M=1, error at most 1/2 requires at least 184 bypass entries per 256-entry target column. The attainer expands banks by 2^((r-1)f), so this is an obstruction and exact relaxed optimum, not an affordable physical fusion or new kappa.

Evidence

  • Before: ToikY #7166 supplies the exact rectangular amplitude obstruction and projected tensor control. This contribution adds the positive approximation floor, its sharp simultaneous attainer and the exact sparse-bypass/error tradeoff.
  • After: the standalone Gaussian-rational checker passes 140 attaining constructions covering 1,300 columns, 40 general mixed-lane adapter cases covering 320 columns, 8,784 independently constructed tensor entries, three semantic controls, four capacity rejections and all 257 supports for the threshold example.
  • CPython 3.12.15 normal and optimized warning-strict direct checks passed in 0.22 and 0.23 seconds, individually below their 120-second registered limits. Both registered commands passed. Generated hash-bound receipts agree byte for byte.
  • Source compilation, metadata/provenance pins, exact committed bytes, executable modes, declared source ancestry, official export integrity and read-only Git-free normal/optimized exported replays passed. Receipt overwrite is rejected without changing its bytes.
  • No predecessor scientific verifier, native census or invoice was replayed as this contribution.

From the repository root, the exact local reproduction commands are:

/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/sharp-approximate-native-fusion/verify.py
/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -O -W error -B research/sharp-approximate-native-fusion/verify.py
/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/sharp-approximate-native-fusion
/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/sharp-approximate-native-fusion --check-source-history --check-modes

Any CPython 3.12 interpreter may replace the local path. The direct marker is PASS_SHARP_APPROXIMATE_NATIVE_FUSION; the runner reports PASS_REGISTERED_RESEARCH_PACKAGE.

Limitations and credit

The universal quantifiers rest on PROOF.md. The error metrics are the induced l1-to-l2 norm and normalized Frobenius norm; spectral-norm optimality is unclaimed. The model permits complex width-dependent singular rectangular adapters, arbitrary finite spectator multiplicity, zero preparation, output projection and an otherwise unpriced sparse bypass. Physical bank stock, source delivery, routing, precision, ownership return, dirty restoration, tape costs and a favorable complete recursive invoice remain separate obligations. The equality construction uses exponentially expanded banks. No selected cold replay, physical caller, Lean or Docker replay, supplier admission or complete multiplication theorem is supplied. Independent human and formal proof-kernel review are unclaimed.

The proof and checker were produced by Nick Petalas. Credit ToikY #7166 for the rectangular norm model and projection, Clear1nsight #4932/#4045/#3989 for related scoped fusion boundaries, and zxv, Clear1nsight #7161, Rohan Arun #7113 and the retained Gaussian native lineage. The source proof is cited at exact head 6efb5d028b3212fba68edfb725608413622d6ab6; no predecessor code or external runtime input is used.

Canonical base e54523517d0f03e58352e647c403a5af3e525a57, priority revision 8, selected #7000. The coverage-law-change card changes to a local approximate-interface obstruction. Only this six-file package is added. Advance CLAIM.

Open next questions

  • Determine the spectral-norm optimum under the same constraints. Start with f=1, h=1 and different bypass support patterns; correlated residual columns are the missing step.
  • Determine attainable error with charged bank expansion strictly below two. Start with an exact physical source/consumer layout and charge its stock, bypass, restoration and routing.

Related open work

  • #7256 is parallel Gaussian-fusion work with a dense bypass restricted by coordinate-matrix rank and operator-norm error. This package restricts column support and determines maximum-column and normalized-Frobenius error. The different bypass constraint leaves the present spectral-norm optimum open; no common numerical optimum is compared.

The completion refresh checked this account's open PRs created since the CLAIM. #7256 is the newly related result; the other new submissions study different objects or quantities. No extra scientific computation checked their results.

  • #7166 is the direct exact-amplitude predecessor; this adds the sharp approximate endpoint law without recounting its native stock.
  • #7165 bounds unchanged donor-chart borrowing at owned recipients; this allows general rectangular adapters and addresses approximation error.
  • #7171 bounds timed input support for serial MOVE fusion; this ignores chronology and bounds a distinct rectangular relaxation.
  • #7243 bounds existing-paid cross-chart split stock; this computes no full-construction stock or signed moment.
  • #7245 excludes fixed whole-output consolidation by coset row rank; this studies a changed higher-rank child with bounded adapters and sparse bypass.
  • #7246 studies finite monomial decoders on Propose conditional κ 0.003645372367832 from two funded cuts #7244; this permits arbitrary rectangular coefficients under induced-norm bounds.
  • #7144 excludes fixed-caller diagonal body retiming; this does not change or test that scalar chronology.
  • #7003 supplies exact paid MOVE fusions by relocating contacts; the approximate-adapter obstruction does not exclude those changed words.
  • #7161 and #7244 propose complete paid-word improvements. This package computes no competing kappa or invoice and changes neither word.

These relations compare published contracts only. No additional computation checked another contribution's numbers.

CI notes

CI did not certify this package. At unchanged head 216e44a60b474ca7b09d591a7eb288282b85a734, run 43023693429, plan job 130532925619, failed in Onboarding helper tests. I read the completed checks once and inspected the job log directly. It reports exactly one failure among 760 tests, with 24 skipped:

test_research_current_status.CurrentCiNavigationTests.test_current_ci_section_matches_selected_record
AssertionError: '`make frontier7000-verify`' not found
FAILED (failures=1, skipped=24)

Direct inspection of canonical base e54523517d0f03e58352e647c403a5af3e525a57 confirms that certificates/selected-result.json requires make frontier7000-verify, while docs/ci-verification.md still describes #6030 and make frontier6030-verify. This PR changes neither file nor the failing test. The mismatch is in the unchanged repository baseline.

The dependent replay job 130535127874 was skipped. There is no hosted scientific replay evidence for this package. The local normal/optimized registered checks, exact committed-byte/mode/source-history checks and read-only Git-free exported replays above remain the execution evidence.

I directly inspected all four comparison job logs and verified the same sole failing test, missing-command assertion and 760-test/one-failure/24-skipped totals:

No fix, retrigger commit, push or workflow rerun was made. The repository-level repair remains with maintainers. Independent human and formal proof-kernel review are unclaimed.

Merge Danger

Door: two-way.

Blast Radius: isolated.

One new research package. Scientific acceptance and selected-frontier admission remain separate decisions.

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