Repository navigation
DONE: native rounded butterfly contract #5475
JoyboyBrian
started this conversation in
General
Replies: 0 comments
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Uh oh!
There was an error while loading. Please reload this page.
Uh oh!
There was an error while loading. Please reload this page.
DONE — contribution submitted: 5485. Maintainer review remains pending.
Exact head
47c4e95f2aad7b33637aca3ac0dde0a0a2a9ebfe; 3 substantive commits. Local validation and independent agent review are evidence for this scoped contribution, not human or formal-kernel acceptance.A concrete fixed-grid nearest-even butterfly backend now supplies the completed-call tolerance assumed by the actual PR4743 C0/C2 port analysis. For rho=2^-q, g=q+ceil(f/2)+1 grid bits suffice uniformly. The proof includes internal numerator ranges, actual stored inputs, adjoints, every two/three-call forward/reverse schedule and w=H+g+2f+ceil(f/2)+9 signed component bits. Deterministic nonzero rounding is executed rather than injected.
The exact source pins, all-width proof, executable controls and open next questions are in
research/native-rounded-butterfly-contract/. This closes a named source-bound implementation handoff; it does not admit a supplier or change selected κ.Validation: 20,003 signed half-rounding cases;36 completed-call cases at widths1/2/3 across C0/C2 and adjoints;12 actual forward/reverse port cases with nonzero rounding and off-grid input quantization; every actual completed-call input/output; overflow/axis/adjoint controls;625 one-butterfly residue fixtures. Registered Python3.12 normal/optimized checks pass, as do actual on-disk source/receipt/scientific-code rejection controls. Final committed-byte/source-history preflight and official export integrity checks pass. Both normal and optimized direct science pass from a read-only Git-free export with PATH empty; payload hashes are unchanged. Separate AI peer review found no blocking issue.
Limits: The direct backend costs O(fN), N=8^f, and does not inherit an accelerated recursive rank-one tariff. The source-ordered external channel bounds are reused with attribution, not claimed as a new norm calculation. Concrete fault patterns obey additional parity constraints; no attainability of the earlier independent-ball sharp constant is claimed. Accelerated recursion, fixed tapes, native supplier/outer admission and selected-frontier replay remain open.
Prepared by JoyboyBrian with substantial OpenAI Codex assistance; Apache-2.0. All predecessor credit is retained in README/PROOF and exact copied sources. Independent human, formal-kernel, hosted-CI and full selected-supplier verification are unclaimed. Canonical investigation: #5475.
Claim base
32890bc5de034ab8fc93ac88ead7279a6a416d04. Selected frontier unchanged.All reactions