Skip to content

Prove exact dyadic cyclic balancing and grid cost (no κ) - #6468

Open
petalas wants to merge 1 commit into
CrocSwap:mainfrom
petalas:research/w14-1102e-original-step
Open

petalas wants to merge 1 commit into
CrocSwap:mainfrom
petalas:research/w14-1102e-original-step

Conversation

@petalas

@petalas petalas commented Nov 3, 2026 •

Copy link
Copy Markdown
Contributor

Summary

Scoped all-length proof with exact finite corroboration. For dyadic diagonal balancing of a weighted cyclic recurrence to coefficient cap beta, put d_i=ceil(log_2(|a_i|/beta)).

sum d_i > 0:  no dyadic balancing exists
sum d_i <= 0: minimum scale span = max(0, proper cyclic interval sums)

An explicit suffix-sum constructor attains the minimum. The least diagonal condition number is exactly 2^H. With minimum scale exponent zero, direct rescaling of arbitrary binary-grid inputs needs H additional common-grid fractional bits, and reverse scaling has sharp error gain 2^H.

For a=(2^k,2^(-k-2)) at cap 1/2, H=k+1. For a=(3/5,2/5), real scales attain cap 1/2 but no dyadic scales do, despite a strict product margin. These are scoped proofs, not search failures or a complete multiplication theorem. No new kappa or selected-frontier change.

This contribution was produced by Nick Petalas. Credit Sricharan Vagvala / theon199's PR1481, head 753c1b6, for Open next question 2 and its weighted expansive-cycle setting; Chafik Boukhalfa / PR628 and PR905, Charles Bethin / PR764, and the retained cyclic-kernel/precision lineage. Difference constraints and longest-path potentials are classical; general optimization or literature priority is unclaimed. The predecessor's scientific verifier was not replayed.

Advance CLAIM. The delivered result is the scale-range and grid-cost subproblem; the full physical balancing invoice remains open.

Evidence

Before, PR1481 left the scaling and two-grid cost of balancing unresolved. After, the written theorem gives the exact dyadic minimum and an attaining construction for every length.

Local CPython 3.12.15 checks pass at head 25d72c3:

  • 19,530 demand vectors, including 10,886 feasible constructors. Exhaustive smaller-span optimization covers all 445 feasible cases through length four and rejects all 5,428 smaller candidate vectors.
  • 5,600 rational coefficient/cap cases; every basis column of all 2,159 feasible conjugacies passes, totaling 8,255 columns and 32,005 entries.
  • 25,000 coordinate grid checks, 1,110 sharp grid/error witnesses, 402 logarithmic ceiling boundary checks, 64 expansive-family members and 17 rejection or semantic controls.
  • Both registered warning-strict normal and optimized commands pass and emit identical generated source-hash receipts. Each timed command finished in under one second, within its 120-second cap.
  • Package metadata, registered replay, exact committed bytes/modes and source-history checks pass. Official six-file export integrity and input coverage pass. Optimized replay of the read-only export with Git absent from PATH produces the same receipt.
  • Syntax/function-size inspection and staged whitespace checks pass. No separate static analyzer is claimed.

From the repository root, reproduce with this local interpreter path or substitute another CPython 3.12 executable:

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

The direct marker is PASS_DYADIC_CYCLE_BALANCING. The runner reports PASS_REGISTERED_RESEARCH_PACKAGE, and publication preflight reports PASS_RESEARCH_COMMIT_BYTES. Receipts are generated, not handwritten or committed. Canonical main was refreshed unchanged before publication at 7c49fe3, priority revision 8.

Limitations

The universal assertion rests on the written proof, supported by the finite domains. Complex phases are covered by the proof; conjugacy fixtures use signed real rationals. The implementation has explicit finite capacities.

Relative grid span and norm transfer do not establish an optimal rounded solver. Nonuniform grids, different algorithms and non-dyadic scales may change the cost. Physical scale instructions, reversible acquisition, arbitrary dirty restoration, complete numerical heights, scratch, tape/storage, coefficient preparation, the complete supplier invoice and selected-caller admission remain unproved. All five selected assumptions remain. Independent human and formal proof-kernel review are unclaimed. Lean, Docker and selected scientific cold replay were not run; every registered command ran locally.

Open next questions

  1. Build one reversible balanced cyclic inverse with explicit nonuniform grids, scaling instructions, rounded errors and complete restoration/movement costs.
  2. Bind the exact minimum span to one actual coefficient table, cap and caller, then compare its complete precision/storage allowance.

Related open work

No open PR on this exact dyadic balancing minimum was found in the inspected live PR bodies, handoffs and targeted searches. Sparse notes, arbitrary diffs and unpublished work remain coverage limits.

  • PR6426 studies degree growth of polynomial cyclic inverse row norms. This result concerns diagonal balancing of weighted first-order recurrences and computes no shared value. No additional computation was run to check that work.

The completion refresh covered this account's twelve open PRs created since the advance CLAIM, including this PR. The eleven others, PR6460 through PR6471 excluding PR6468, concern nilpotent-Schur and characteristic-five replay, a ternary COPY floor, helper-channel capacities, a stopped-recursion coefficient, tensor reconstruction, observable-mask preparation, a fixed matcher, triangular parity cuts and compatible fitting flags. None studies this dyadic balancing minimum or reports a competing value computed here. No additional mathematical computation was run to check those contributions.

CI notes

Both hosted checks passed at exact head 25d72c368430c2e5ab494de6bef6ade08fde9b8c in run 41551117193: plan in 4m7s and replay (research/dyadic-cycle-balancing) in 1m21s. The checks were read once; run metadata confirms completed success and the matching head. Hosted replay certifies the registered normal and optimized finite checks, not independent human or formal proof-kernel acceptance of the all-length proof. All local checks listed above passed. No CI failure required repair.

Merge Danger

Door: two-way

Six new files in one isolated research package. No shared implementation, predecessor archive or selected record changes.

Blast Radius: research

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