Skip to content

Bound signed invoice classes by a polarized extreme (no κ) - #7325

Open
petalas wants to merge 1 commit into
CrocSwap:mainfrom
petalas:research/w1-1111f-polarized-invoice-ceiling
Open

petalas wants to merge 1 commit into
CrocSwap:mainfrom
petalas:research/w1-1111f-polarized-invoice-ceiling

Conversation

@petalas

@petalas petalas commented Nov 11, 2026 •

Copy link
Copy Markdown
Contributor

Result

Claim type: scoped written proof with exact finite corroboration.

On the documented signed concave invoice screen (scripts/compare_recursive_invoices.py), the net of a declaration at exponent x = 1 - C is

N(x) = sum_paid r^x - sum_target s^x,   0 < x < 1.

This PR answers the question the comparator does not: over the whole class of declarations sharing the four numbers (paid entry count Kp, paid rank mass Mp, target entry count Kt, target rank mass Mt), which declaration is the most favourable, and is that extreme independent of x?

Theorem. For ambient rank m >= 2, the pointwise-in-x minimum of N over the class is attained by the polarized declaration:

  • paid ranks spread to the ambient extremes — j copies of m, one remainder r0, the rest 1, with j = min(Kp-1, (Mp-Kp)//(m-1)) and r0 = Mp - Kp + 1 - j(m-1);
  • target ranks balanced — q = Mt//Kt and q+1.

Every declaration in the class satisfies N(x) >= N_canonical(x) for all 0 < x < 1 simultaneously, with equality exactly at the canonical declaration. Because the canonical declaration depends only on (Kp, Mp, Kt, Mt, m), one two-rank declaration bounds a whole class.

Two consequences that need no construction replay:

  1. Necessary condition. A candidate in class (Kp, Mp, Kt, Mt) can beat an incumbent with net Psi(x) only if Lambda(x) < Psi(x); the mass-only form is Mt > Mp m^(x-1) - Psi(x).
  2. Sufficient class certificate. With U the antipodal declaration of the incumbent class (paid balanced, targets spread), Lambda_candidate(x) > U_incumbent(x) for all x implies every candidate declaration is uniformly worse than every incumbent declaration. Both sides are two-rank declarations, so the existing hinge comparator verifies the hypothesis exactly in constant time.

The proof is an exchange argument: increments of a strictly concave power are strictly decreasing, so spreading paid mass and equalizing target mass never hurt, and the terminal configurations are unique (PROOF.md, Lemmas 1-3, Propositions 1-2, Theorem). The exponent range is sharp: at x = 1 the inequality is an equality for every declaration with the same masses, and at x = 0 it degenerates to entry counts, so 0 < x < 1 is exactly where the polarized extreme exists.

Evidence

  • PROOF.md — written proof, uniqueness of both extreme declarations, sharpness of the exponent range, and the two screening consequences.
  • verify.py — integer interval arithmetic only (rank powers bracketed by integer k-th roots, 24 digits; no floating point). It checks both exchange lemmas for every admissible pair with m <= 6 and five exponents 1/2, 1/3, 2/3, 1/5, 3/7; Propositions 1 and 2 exhaustively over every integer multiset in the boxes (m, max entries) = (5,3), (4,4), (6,2), (3,5); the class theorem on every ordered pair in those boxes (40,705 strict comparisons, 16,995 equality cases); the x = 1 and x = 0 boundary controls; and mutation/hypothesis controls.
  • Comparator composition, which is an independent implementation (its hinge criterion is not the exchange argument): a non-canonical declaration against its canonical replacement is classified uniformly_worse with a strictly positive power sign, the reverse uniformly_better, identical canonical declarations equal, a rank above the declared ambient rank is rejected, and the antipodal class certificate is confirmed on concrete declarations.
  • RESULT.json — generated census with source hashes, rewritten by the verifier.

Reproduction from the repository root, with the pinned interpreter:

~/git/integer-mult-bounds/.venv/bin/python3.12 -B research/invoice-class-polarization/verify.py
~/git/integer-mult-bounds/.venv/bin/python3.12 -W error -B research/invoice-class-polarization/verify.py
~/git/integer-mult-bounds/.venv/bin/python3.12 -O -W error -B research/invoice-class-polarization/verify.py
~/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/invoice-class-polarization
~/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/invoice-class-polarization --check-source-history

All of the above pass locally on commit a9b48385719c50b2a710906b70e975585e24a631; the verifier runs in about 0.2 s.

Limitations and unrun obligations

  • No physical, native, compiler, precision, hosting, ownership or supplier admission. Ranks are declared histogram entries, exactly as in the comparator, whose assurance block records the same restriction.
  • No paid call count, scalar instruction count, or charge outside the raw signed moment; the theorem is about the declared arithmetic screen.
  • No kappa change, and no claim that a canonical declaration is realizable by a word. The bound is over declarations and is sharp inside the declared class only.
  • The finite corroboration is exhaustive in the four stated boxes and at five exponents, not over all m or all x; the universal statement rests on the written exchange proof.
  • No formal-kernel proof is supplied.

Open next questions

  1. Per-rank target multiplicity caps. With at most c hostable targets of a given rank, the target maximum becomes a bounded-composition problem. First step: compute the exact maximum of sum s_j^x under per-rank caps. Blocked by: no declared cap inventory bound for a concrete word.
  2. Achievable summary quadruples. Which (Kp, Mp, Kt, Mt) a fixed controller can realize. First step: count the four numbers for one audited declaration and compare against its own class ceiling. Blocked by: no source inventory is bound in this package.
  3. Distinct-rank budget. A bound that also fixes the number of distinct ranks per side could separate proposals the four numbers cannot. First step: solve the extremal problem with a distinct-rank budget and a tie-breaking rule. Blocked by: the extremal vector is no longer unique.

Related open work

  • PR Keep selected invoice stdout bytes consistent with its receipt #5973 (josecarlosgonzalezroque-design) keeps selected-invoice stdout bytes consistent with its receipt: the invoice tooling's output contract, not the signed moment or its class extremum.
  • PR Certify fixed-profile helper-split first-crossing ceilings for #7000 (no κ) #7175 (petalas) certifies fixed-profile helper-split first-crossing ceilings for the selected frontier: a different model (one fixed helper-split profile at one crossing), not comparable with the class ceiling here without expressing that profile as a declared paid/target invoice.
  • PR Bound the paid-fusion moment ceiling exactly (no κ) #7326 (petalas) bounds the paid-fusion moment: strict subadditivity of x^c, a sharp single-fusion cap and a total fusion budget for a fixed partition. It changes the paid multiset of one declared invoice; this PR bounds the signed net over a whole class of declarations. The two are complementary and share no computed number, so no numeric comparison is made here.
  • docs/research/recursive-invoice-preflight.md records the signed-invoice comparison procedure and its "not a new theorem" disclaimer for the concave-order interface; this PR supplies the class-extremal theorem there and changes nothing in that document.

CI notes

Head a9b48385719c50b2a710906b70e975585e24a631, run
https://github.com/CrocSwap/integer-mult-bounds/actions/runs/43107053327.

  • plan failed. The replay job was then skipped, so CI did not certify this package.
  • The only failing test is
    test_research_current_status.CurrentCiNavigationTests.test_current_ci_section_matches_selected_record
    (760 tests, 24 skipped, 1 failure), with
    AssertionError: 'make frontier7000-verify' not found in '# CI verification ...'.
  • Cause is on main's own files, not in this PR. At base e54523517,
    certificates/selected-result.json has "reproduce": "make frontier7000-verify",
    while docs/ci-verification.md still describes make frontier6030-verify
    (line 9), and the test compares those two. This PR touches neither file and
    adds only research/invoice-class-polarization/.
  • I verified the same single test failing in run 43105433200, run 43105694304,
    run 43105875821, and in another contributor's run 42905094314.
  • Locally, every registered VERIFY.json command,
    scripts/research_package.py and
    scripts/check_research_commit.py --check-source-history pass at this head
    (verifier runtime about 0.2 s).

Apache-2.0.

Prove that on the documented signed concave invoice screen, every invoice
with fixed paid/target entry counts and rank masses is pointwise bounded by
its polarized canonical invoice: paid ranks spread to the ambient extreme,
target ranks balanced. The extreme is independent of the exponent, so one
two-rank declaration bounds a whole class, gives an O(1) necessary condition
and an O(1) sufficient uniformly-worse certificate that composes with the
hinge comparator. The written proof is corroborated by exhaustive certified
interval checks over four count/rank boxes and by the comparator itself.
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