Skip to content

Prove endpoint sign criterion for fully crossing helper bills (no κ) - #7460

Open
apoursh wants to merge 1 commit into
CrocSwap:mainfrom
apoursh:codex/proper-terminal-sign-criterion
Open

apoursh wants to merge 1 commit into
CrocSwap:mainfrom
apoursh:codex/proper-terminal-sign-criterion

Conversation

@apoursh

@apoursh apoursh commented Nov 12, 2026

Copy link
Copy Markdown
Contributor

Change and mathematical scope

PR #7331 leaves open whether a proper-terminal helper rank bill can be positive inside a feasible interval while both endpoint bills are nonpositive. This proves no, for every finite number of unit-charged paths reaching the terminal.

For 0<t<1, 0<=a_i<=T<=b_i, A=max a_i, and
G(x)=x^t+(T-x)^t-T^t-sum_i[(x-a_i)^t+(b_i-x)^t-(b_i-a_i)^t]:

There exists x in [A,T] with G(x)>0  iff  G(A)>0.

A self-contained elementary proof shows that each path's split cost divided by the helper's split benefit is nondecreasing. Thus the normalized bill is nonincreasing. The result handles real endpoints, A=0, A=T and every permitted closed subinterval. It preserves #7331's negative interior-maximum counterexample: it decides positivity, not the maximizing dimension. A new exact positive fractional-weight counterexample prevents broadening the zero-endpoint criterion to arbitrary charges.

No new κ, supplier admission, emitted word or selected-frontier change. Paths ending before T, actual cut legality, ordinary charges, native realization, ownership and restoration remain separate.

Task, sources and overlap

Fresh branch from canonical main e54523517d0f03e58352e647c403a5af3e525a57, pulled at entry and refreshed before submission. The revision-8 contextual picker reports its historical PR5599 assessment differs from selected PR7000, κ 363005817/100000000000. Full original p104-side-correction card and explicit changed scope are retained.

Direct predecessor: Nick Petalas / petalas #7331, unchanged head e5383f5c2973c9520918cbe6ebe9c6e6867e5771. Its exact published proof bytes and attribution are retained locally; no predecessor executable is used or source-history ancestry invented. Unpaidmoon's #7283 supplies the rank-bill formula and prior question, retaining CubeJerry's helper-split exploration and DreamingOfClouds's #6902 two-chain lineage.

Live all-state #7331 search found #7332 and #7396's distinct literal-cut/quiet-lift work. Latest 20 PR titles were checked through #7459; the final handoff refresh also read DreamingOfClouds's helper-1077 proposal (comment19569957), which changes a specific word rather than this abstract sign criterion. Local sparse overlap coverage is disclosed, not treated as proof of novelty. Discussion access was signed out, so this bounded session did not post an advance claim.

Validation

CPython 3.12.14, macOS arm64, standard library:

python3.12 -B scripts/research_package.py --package research/proper-terminal-sign-criterion
python3.12 -B scripts/check_research_commit.py --package research/proper-terminal-sign-criterion --check-modes --check-source-history
python3.12 -B scripts/export_research_package.py export --package research/proper-terminal-sign-criterion --ref HEAD --output /tmp/sign-criterion.tar
python3.12 -B scripts/export_research_package.py check /tmp/sign-criterion.tar

All four registered isolated, warning-strict normal/optimized commands passed. Primary exact nth-root bounds cover five rational exponents, 1,440 ratio and 450 normalized-bill comparisons, 225 zero-start bills, 90 endpoint checks and 350 root/domain/direction controls. The separate square-root checker covers 2,900 path multisets, 11,600 normalized comparisons, 11,275 interior signs, the predecessor's four-path example and six scope controls. Mutated predecessor bytes and a false source head were rejected.

All nine committed files, modes and base provenance passed. Official export integrity passed; four direct replays passed from a read-only Git-free export with empty PATH and unchanged file/directory hashes and modes. The source-binding-only selected orientation check passed on 221 paths; the selected scientific cold replay was not run. Proof review by a separate Codex agent found no blocker; this is not independent human or formal-kernel acceptance.

Existing CI blocker

The unchanged upstream navigation test currently fails: test_current_ci_section_matches_selected_record expects make frontier7000-verify, but docs/ci-verification.md still names #6030. Locally the six-test navigation module had that one failure. Pending #7276 already proposes the shared repair; this package does not duplicate it or weaken the test. Package-specific checks passed; hosted CI success is not claimed.

Open next questions and credit

Mixed paths ending before T require a different argument. Applying the criterion to an actual caller first requires authenticating every charged path and its endpoint order; a positive bill still needs the complete legality and implementation invoice.

Prepared by apoursh with substantial OpenAI Codex and subagent assistance in proof discovery, implementation, independent checks and packaging. Predecessor credit is retained above and in the package. Concavity and tangent inequalities are classical; no literature-priority claim. Apache-2.0.

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