[petalas]

Change and mathematical scope

NO VERIFIED GAIN. Exact conditional κ change 0%. The selected exponent stays 363005817/100000000000. No word is emitted and no cut is declared legal.

This answers Open next question 1 of unpaidmoon's #7283: does the endpoint maximum of the contact-free helper-split rank bill survive when the helper terminal T is strictly inside the ambient D (so 0 < T < D) and a paid path leaves the boundary (b > T)? The bill is

G(x) = x^t + (T-x)^t - T^t - Σ_i ( (x-a_i)^t + (b_i-x)^t - (b_i-a_i)^t ),

with 0 < t < 1, integers 0 ≤ a_i ≤ b_i ≤ D, and 0^t = 0. This is the #7283 formula with the helper dimension replaced by the terminal.

Theorem 1. For one path with b > T, G is strictly decreasing on [a, T], so its maximum is G(a); if a = 0 then G(0) = 0 and G(x) < 0 on (0, T). The endpoint maximum survives in the strongest form for the case named in #7283's first step: the only candidate is the path's own lower endpoint.

Proposition 2. G(T) ≤ 0 for every path set with a_i ≤ T ≤ b_i, with equality exactly when T is an endpoint of every path.

Proposition 3. If every a_i = 0 and at least one path crosses, then G(x) < 0 on (0, T) for every m ≥ 1.

Proposition 4 (counterexample). At t = 1/2, D = 26, T = 24 and paths (3,25), (17,26), (0,25), (6,25), the interior dimension x0 = 3819/160 beats both endpoints:

G(17) = -3.747477... < G(x0) = -3.554274... > -3.734846... = G(24).

The two comparisons are certified by exact integer square-root arithmetic, not floating point. So the endpoint maximum does not extend to four crossing paths. The witness has a negative interior value: it shows that the two-endpoint comparison can understate the maximum, not that a gain exists.

Claim type: scoped written proof with an exact finite counterexample and finite censuses. No finite census is used as a proof for larger parameters.

Task and overlap

Card p104-side-correction, priority revision 8, base e54523517d0f03e58352e647c403a5af3e525a57, selected record unchanged. Scope status: changed. The card asks whether a legal causal split improves the complete P104 productive/paid invoice. This package answers one boundary case of the rank-bill factor that #7283 explicitly left open. It does not emit a cut, price an ordinary bill, or change the selected exponent, so the invoice question stays open.

Only research/proper-terminal-helper-rank-bill/ is new scientific work. #7283's formula, zero-to-D endpoint theorem and one-path normalization are cited premises; they are not replayed or re-audited here. #7283 credits CubeJerry's shared-native helper-split exploration and the two-chain word from DreamingOfClouds in #6902; that lineage is retained.

Validation

From the repository root, CPython 3.12, standard library:

/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B research/proper-terminal-helper-rank-bill/verify.py
/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/proper-terminal-helper-rank-bill
/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/proper-terminal-helper-rank-bill --check-source-history

Observed locally:

PASS_PROPER_TERMINAL_HELPER_RANK_BILL power_pairs=4500 one_path=3960 zero_start=5628 terminal=4004 two_path=7938 three_path=9780 counterexample=D26,T24,x=3819/160 controls=4 kappa=363005817/100000000000 no_new_kappa=true
PASS_REGISTERED_RESEARCH_PACKAGE research/proper-terminal-helper-rank-bill outcome=partial
PASS_RESEARCH_COMMIT_BYTES {"commit": "e5383f5c2973c9520918cbe6ebe9c6e6867e5771", "files": 6, ...}

The direct verifier also passes under -O and -I. The registered replay takes about 0.4 s locally, well inside the 120 s manifest timeout. Exact comparisons use math.isqrt with a certified truncation whose error is strictly less than one unit per term; like radicands are combined first. Four control claims are rejected: a flipped endpoint comparison at the witness, a one-path decrease applied to the four-path witness, a positive terminal bill, and a violated strict subadditivity.

Checked scope: Lemma 1's integer power form; Theorem 1 for D ≤ 10 on a rational grid of eighths; Lemma 4 for D ≤ 8, m ≤ 3; Lemma 3 for D ≤ 8, m ≤ 2; the exact counterexample; and endpoint-maximum censuses for two paths (D ≤ 8) and three paths (D ≤ 7). Not run: make frontier7000-verify, Lean, Docker, and any 68-split or native replay.

Limits and open obligations

The rank bill G is one factor. Native legality, arbitrary-input identity, ownership, restoration, ordinary cost, precision and the complete target/paid invoice remain where the selected record left them. The two-path and three-path cases are not proved, only censused on the stated grids. The sign question is not settled: whether a positive interior value can appear when both endpoint values are nonpositive is open. A floating-point search over four million random integer configurations (D ≤ 24, m ≤ 8, nine rational exponents) found none, but that is search evidence, not a proof, and it is not part of the verifier. No independent human or formal-kernel review is claimed.

Open next questions

1. Positive interior bill with nonpositive endpoints. If none exists, the two-endpoint comparison still decides whether a proper terminal gives a rank-bill gain even though it does not give the maximum. Fix m = 4 and determine the sign structure of the interior critical point, or prove a maximum principle for the tent decomposition.
2. Exact crossing threshold. Theorem 1 proves one path and Proposition 4 gives four. Resolving two and three paths for all D would make the threshold exact.
3. One pinned helper. Evaluate G at both endpoints for a helper of the published 68-split word whose terminal is proper. A positive value would still need legality, ownership and the paid profile.

Related open work

• Prove the zero-to-D helper-split rank bill is maximized at an endpoint. #7283 (unpaidmoon): direct predecessor. Proves the zero-to-D endpoint maximum and poses this proper-terminal question; this PR answers that question for one crossing path and gives a four-path counterexample. Its proof and verifier are cited, not replayed.
• Certify fixed-profile helper-split first-crossing ceilings for #7000 (no κ) #7175 (petalas): fixed-profile helper-split first-crossing ceilings for Conditional κ = 0.00363005817 (+0.0838% over #6936): shared wires and two helper splits #7000. Different object: a profile ceiling, not the abstract proper-terminal rank bill; no number is compared.
• Exclude fixed-word singleton P104 helper splits (0% κ change) #7303 (ToikY): excludes fixed-word singleton P104 helper splits. Different scope: a word-level exclusion, not the rank-bill factor; no number is compared.
• dillona's open helper-split κ PRs (Conditional κ = 0.00363216151 (+9.932e-8 over #7004) #7105, Conditional κ = 0.00363233825 (+1.7674e-7 over #7105) #7107-Conditional κ = .003641239650184 (+4.78276042e-7 over #7122): recharted helper split #7123 lineage): they price recursive invoices on specific charts; this package prices only the abstract rank-bill term and makes no invoice or κ claim.

CI notes

Hosted CI did not certify this package. The head commit is e5383f5c2973c9520918cbe6ebe9c6e6867e5771. Local checks passed there: the registered package replay, the commit byte/source check, and the direct verifier under -B, -O and -I.

Run 43110001543, job 130823229175, failed the plan job at the "Onboarding helper tests" step on exactly one test of 760 (24 skipped):

tests/test_research_current_status.py
test_research_current_status.CurrentCiNavigationTests.test_current_ci_section_matches_selected_record
AssertionError: '`make frontier7000-verify`' not found in the CI verification doc

certificates/selected-result.json names make frontier7000-verify, while docs/ci-verification.md still describes #6030 and make frontier6030-verify. I reproduced the same failure locally at this PR's head:

cd tests && /Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B -m unittest test_research_current_status.CurrentCiNavigationTests.test_current_ci_section_matches_selected_record -v

The package replay job was skipped because plan failed, so no hosted run checked this package. The same single test fails on the other runs I verified: 42905094314 and 42903313790 (other contributors' PRs) and 43107374986, 43107826591 and 43108616300 (this account's other PRs). Each shows plan failure with replay skipped. This is a repository-level documentation mismatch, not caused by this package. No fix or retrigger commit was pushed here; the maintainers own the docs/ci-verification.md repair.