Prove single crossing for every fixed p16 fragmentation invoice

research/fragmentation-single-crossing/PROOF.md

@@ -0,0 +1,164 @@
+# Single crossing for every fixed p16 fragmentation invoice
+
+This proof discharges S1 from [PR #5226](https://github.com/CrocSwap/integer-mult-bounds/pull/5226)
+for the fixed p16 positive-partition class below. The retained source checked
+S1 on a grid. Here the monotonicity proof covers the whole interval and every
+partition in the class. No native word or complete kappa improves.
+
+The caller and current invoice come from Cao Yifan's
+[PR #4610](https://github.com/CrocSwap/integer-mult-bounds/pull/4610).
+SOURCES.json pins the retained ARITHMETIC.json and the S1 statement at canonical
+main ff3cc58e370d0f678e529246f8c73e8094e18fcf. This is a theorem about complete
+finite invoices, not acceptance of the physical or compiler premises.
+
+## Exact class
+
+Fix p=16, a=7 or8, v=112 and d=8. There are 18 native calls. Each call has
+224 main fields of net increment 8 and 408 independent helper fields, with
+endpoint census `{4:28,7:7,8:47,9:326}`. It also pays eight rank-8 center jobs.
+For each main and helper field, replace its one net increment R by any
+positive integer partition of R. The partition can differ between fields
+and calls. No extra native jobs are permitted. The complete target inventory
+and controller jobs remain those in the source invoice.
+
+These are exactly the numerical hypotheses used in this proof. They cover
+nested ascending paths whose transport ranks equal their dimension gains.
+They do not cover descents, nonnested costs exceeding the dimension gain,
+changed endpoints, extra jobs, sharing, or coded interfaces. Mathematical
+partitions are not asserted to have realizable native words.
+
+Let `f(t)=sum_T n_r r^t-sum_P m_r r^t`, with positive ranks and their integer
+multiplicities. Put `c_r=n_r-m_r`. The largest rank is 145. Define weighted tails
+
+```text
+B_k = sum_(r>=k) r c_r.
+```
+
+The comparison invoice uses one unsplit job R per main/helper field. We call
+it the unsplit invoice. It is a numerical comparison, not a new construction.
+Helper paid jobs cancel their same-rank credits in this invoice. Each call
+then has 232 paid rank-8 jobs from mains and centers. The controller adds:
+
+- 224 target jobs of rank 145;
+- 1,680 paid rank-1 jobs;
+- for j=1,...,7 and separately j=1,...,8, 224 targets of rank `8(j+1)+1`
+  and 224 paid jobs of rank `8(j+1)`.
+
+This formula reproduces the source complete invoice when the unsplit native
+profile is replaced by the source local paid profile.
+
+## Positive weighted tails survive every partition
+
+For a partition `R=r1+...+rs`, at every integer k the sum of parts at least k
+is at most `R [R>=k]`. Substituting the partition for the unsplit paid job
+therefore cannot decrease any B_k. This statement uses mass, not concavity
+or a comparison at selected exponent values.
+
+For the unsplit invoice and 2<=k<=8, all 15 controller pairs contribute their
+rank difference 224. The final target contributes `224*145=32480`. The main
+and center cost is `18*232*8=33408`. Thus
+
+```text
+B_k = 32480 + 15*224 - 33408 = 2432   (2<=k<=8).
+```
+
+For 9<=k<=145, the native rank-8 cost is below the threshold. A controller
+pair has nonnegative weighted tail at every threshold: it contributes 224
+below its paid rank, only its positive target at the next rank, and zero
+after that. The rank-145 targets remain. Hence `B_k>=32480` on this range.
+Every fragmented invoice consequently has `B_k>=2432>0` for all 2<=k<=145.
+Its total rank mass is unchanged:
+
+```text
+f(1) = 2432 - 1680 = 752.
+```
+
+The current source invoice has minimum B_k equal to 32480 for k>=2. This
+independent numerical certificate gives it the same monotonicity even
+without a new native trace replay.
+
+## Interval monotonicity
+
+For 4/5<=t<=1, define `h_t(x)=x^(t-1) ln(x)` on 1<=x<=145. Its derivative is
+
+```text
+h_t'(x) = x^(t-2) [1-(1-t) ln(x)] > 0.
+```
+
+For a fully rational check of the strict inequality, the exponential series
+has positive terms and
+
+```text
+exp(5) > sum_(j=0)^12 5^j/j! = 2837864809/19160064 > 145.
+```
+
+Thus ln(145)<5 and `(1-t)ln(x)<1`. Summation by parts now gives
+
+```text
+f'(t) = sum_(r=1)^145 (r c_r) h_t(r)
+      = sum_(k=2)^145 B_k [h_t(k)-h_t(k-1)] > 0.
+```
+
+The term at rank 1 vanishes because h_t(1)=0. This proves strict monotonicity
+on the entire interval, for every partition in the stated class. It is not
+a grid extrapolation. The same argument is a reusable sufficient test for
+any finite invoice with nonnegative weighted tails, at least one positive
+tail, and a rank bound that keeps h_t increasing.
+
+## An exact endpoint sign gives one crossing
+
+At t=19/20, splitting a positive paid rank cannot reduce its moment:
+`(a+b)^t<=a^t+b^t` for a,b>0 and 0<t<1. Thus every fragmented invoice has
+f(19/20) no larger than the unsplit invoice.
+
+The checker encloses each r^(19/20) by integer powers. With Q=2^24, it finds
+an integer z such that
+
+```text
+z^20 <= r^19 Q^20 < (z+1)^20.
+```
+
+Then `z/Q <= r^(19/20) < (z+1)/Q`. Signed interval addition gives the exact
+unsplit endpoint enclosure
+
+```text
+-997308605/262144 <= f_unsplit(19/20) <= -1994616351/524288 < -3804.
+```
+
+There is no floating-point logarithm or root in this check. All fragmented
+invoices have f(19/20)<0 and f(1)=752>0. Continuity and strict monotonicity
+give exactly one zero in (19/20,1), and no other zero in [4/5,1]. Therefore
+the raw saving variable C=1-t has exactly one crossing in (0,1/20).
+
+For every bar in (0,1/20], the raw crossing is at least bar if and only if
+`f(1-bar)>=0`. For a homogeneous native word used 18 times, PR #5226's
+identity `f(t)=18[Lambda_star(t)-Lambda_word(t)]` therefore gives its
+p16 necessary-and-sufficient loss test without an extra S1 assumption.
+The numerical value of Lambda_star and the all-p controller optimum are
+separate source claims; this package does not reprove those. It does not
+extend the result to arbitrary p or to native jobs outside the partition
+class.
+
+## Evidence, credit and next question
+
+The checker binds the complete source invoice through the local profiles
+and an independent controller formula. It checks all 144 weighted tails,
+the fixed rank mass, all 96 positive integer partitions of totals 1,...,9,
+22 integer-root enclosures, and the rational exponential lower bound.
+Controls reject an added high-rank cost, removed helper credit and a wrong
+partition total. The written mass and summation proofs cover every assignment
+of partitions; those assignments are not enumerated. No native, Lean,
+compiler, outer-ledger or selected replay was run.
+
+PR #5226 supplies the fragmentation framework and names S1. Its retained
+README attributes the text to Claude Opus 5.5 via Claude Code; no human
+identity is inferred from its submission account. Cao Yifan supplies the
+PR #4610 invoice. Cinna Davis, zxv and the retained controller/native authors
+keep their source credit. The weighted-tail proof, class-wide S1 discharge
+and exact checker are new here. Ali Romman with substantial OpenAI Codex
+assistance. Apache-2.0; author-checked, not independent acceptance.
+
+A future changed invoice can first test its weighted tails. If extra jobs or
+changed endpoints make a tail negative, this sufficient certificate does
+not apply; that is not a proof of multiple crossings. Derive an appropriate
+interval bound or a new invoice before using a sufficiency claim.

research/fragmentation-single-crossing/README.md

@@ -0,0 +1,42 @@
+# Prove the fixed p16 fragmentation invoice has one crossing
+
+Every positive-integer fragmentation of the stated main/helper increments
+has a strictly increasing moment on t in [4/5,1], and exactly one crossing
+in C=1-t in (0,1/20). This removes S1 from the p16 sufficiency test in
+[PR #5226](https://github.com/CrocSwap/integer-mult-bounds/pull/5226) for this
+class. It does not improve kappa or prove a new native word.
+
+[PROOF.md](PROOF.md) gives the class, weighted-tail argument and exact endpoint
+sign. [RESULT.json](RESULT.json) records the certificate. [SOURCES.json](SOURCES.json)
+pins the source invoice and S1 statement at canonical main
+ff3cc58e370d0f678e529246f8c73e8094e18fcf, priority 7. The
+[claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19151239)
+excludes descents, extra jobs, coded interfaces and changed endpoints.
+
+## Reproduce
+
+Use CPython 3.12 and the standard library:
+
+```sh
+python3.12 -B scripts/research_package.py --package research/fragmentation-single-crossing
+python3.12 -I -O -W error -B research/fragmentation-single-crossing/verify.py
+```
+
+Expected marker: PASS_FRAGMENTATION_SINGLE_CROSSING. Both modes check the
+complete invoice, 144 weighted tails, 96 integer partitions, 22 root intervals
+and a rational exponential bound. The quantified proof covers every partition
+assignment. No native, Lean, compiler, outer-ledger or selected replay ran.
+
+## Open next questions
+
+Test the weighted tails of one specified changed invoice. A negative tail
+means this sufficient test does not apply; it does not prove multiple roots.
+Then derive a suitable interval proof. TASK.json records this next step.
+
+## Credit
+
+Cao Yifan's PR #4610 supplies the source invoice. PR #5226 supplies the
+fragmentation framework and S1 question; its README attributes the text to
+Claude Opus 5.5 via Claude Code. The proof links these sources and retains
+controller/native credit. New proof and checks: Ali Romman with substantial
+OpenAI Codex assistance. Apache-2.0; author-checked, not independent acceptance.

research/fragmentation-single-crossing/RESULT.json

@@ -0,0 +1,40 @@
+{
+  "status": "PASS_FRAGMENTATION_SINGLE_CROSSING",
+  "controller": {
+    "p": 16,
+    "a": [
+      7,
+      8
+    ],
+    "v": 112,
+    "d": 8,
+    "native_calls": 18
+  },
+  "max_rank": 145,
+  "rank_mass_surplus": 752,
+  "skeleton_min_weighted_tail": 2432,
+  "current_min_weighted_tail": 32480,
+  "monotone_t_interval": [
+    "4/5",
+    "1"
+  ],
+  "unique_crossing_C_interval": [
+    "0",
+    "1/20"
+  ],
+  "skeleton_moment_at_19_over_20": [
+    "-997308605/262144",
+    "-1994616351/524288"
+  ],
+  "power_denominator": 16777216,
+  "power_intervals": 22,
+  "exp5_rational_lower": "2837864809/19160064",
+  "positive_integer_partitions_checked": 96,
+  "controls": [
+    "extra_high_rank_cost",
+    "missing_helper_credit",
+    "wrong_partition_total"
+  ],
+  "native_replay_run": false,
+  "new_kappa_claimed": false
+}

research/fragmentation-single-crossing/SOURCES.json

@@ -0,0 +1,36 @@
+{
+  "schema_version": 1,
+  "base_commit": "ff3cc58e370d0f678e529246f8c73e8094e18fcf",
+  "files": [
+    {
+      "path": "certificates/selected-result.json",
+      "usage": "provenance",
+      "git_blob": "c35482cd9035843b15a634cc8276a7e1e40e8395",
+      "sha256": "6fe0a099b89aa2aed796a13c3a21dafc63f3388ebf397464e44e0451893b9375"
+    },
+    {
+      "path": "docs/research/agent-task-catalog.json",
+      "usage": "provenance",
+      "git_blob": "f126dd2e2dad2b669e75d1d0d0bd05c600725602",
+      "sha256": "f7a48bfa2659b88378282a8eee7d9fe52cdf505594124c4d1686b58510fffd72"
+    },
+    {
+      "path": "research/fragmentation-ceiling/PROOF.md",
+      "usage": "input",
+      "git_blob": "c4033090d7cd35d9c80744922c587ae115b1de8a",
+      "sha256": "28be45a551ed8491be1ebb8c64acba2834aaa402452cb02e3c71c83e49232264"
+    },
+    {
+      "path": "research/fragmentation-ceiling/README.md",
+      "usage": "input",
+      "git_blob": "236e94ea255ebace3cebd37b2f2e9258b31c622e",
+      "sha256": "fc10b61fbceceedc6e764ad5fb8506aacf01e1de4b60b08e83fa38d8ee86dc97"
+    },
+    {
+      "path": "research/kappa-round3-warp-20261022/ARITHMETIC.json",
+      "usage": "input",
+      "git_blob": "c89e009ca4a5ad316c69f0371d885d72045ba415",
+      "sha256": "ab10f6a4a8a4f589d4b094aac663e002c43ec44774e6bd181c51915c7fa7e521"
+    }
+  ]
+}

research/fragmentation-single-crossing/TASK.json

@@ -0,0 +1,100 @@
+{
+  "schema_version": 1,
+  "task_id": "independent-moment",
+  "priority_revision": 7,
+  "base_commit": "ff3cc58e370d0f678e529246f8c73e8094e18fcf",
+  "original_card": {
+    "id": "independent-moment",
+    "question": "Does a new paid-profile or mixture-ceiling claim have independent source-bound coverage of its actual changed ledger?",
+    "starting_points": [
+      "docs/research/research-family-status.md",
+      "certificates/selected-result.json",
+      "research/staged544-mixed-fourth-entry/README.md",
+      "research/staged-fourth-mixture-ceiling/README.md",
+      "research/r437-two-window-carrier/README.md"
+    ],
+    "methods": [
+      "Independently reconstruct one changed paid ledger or pooled dual with exact source and model binding.",
+      "Check a genuinely uncovered moment implication with a different enclosure method and semantic controls."
+    ],
+    "acceptance_gate": "Demonstrate independence, source binding, positive cases and semantic failure controls. Name the existing checks and the missing coverage. More digits or another equivalent evaluation of an unchanged root is not by itself new verification coverage.",
+    "first_step": {
+      "command": [
+        "python3",
+        "-B",
+        "scripts/research_baseline.py"
+      ],
+      "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY",
+      "inspect": "Choose one uncovered implication in #4088 literal mixed fill, #4091 pooled dual/model binding or #4067 changed frame/host bill. #4091 pins an earlier #4088 head: validate word, capacity and stock equivalence before applying that ceiling to the later fill.",
+      "scope": "Source-binding orientation only; no scientific replay, theorem acceptance or supplier admission. Budget any heavy replay separately."
+    },
+    "first_experiment": "Independently reconstruct one changed ledger or pooled certificate with a positive case and a semantic failure control. Compare exact sources and name what existing checks miss. Keep this separate from supplier-boundary-audit (ordinary/outer dispatch) and uniform-transfer-audit (all-size proof). Stop after the chosen implication; more digits of an unchanged root are not additional mechanism coverage.",
+    "bottleneck_link": "Independent pricing prevents unsupported frontier claims and can reveal genuine accounting slack.",
+    "allowed_variations": [
+      "Reconstruct either a source ledger or a numeric enclosure with a different method."
+    ],
+    "scope_change_triggers": [
+      "Importing the primary function and calling its output independent verification.",
+      "Calling an aggregate histogram or source archive an independently accepted physical supplier."
+    ],
+    "overlap_terms": [
+      "independent moment",
+      "rank histogram",
+      "exact enclosure",
+      "2979",
+      "rank7 joint endframes",
+      "paired extraction",
+      "joint lowering",
+      "4088",
+      "4091",
+      "4067",
+      "staged544-mixed-fourth-entry",
+      "staged-fourth-mixture-ceiling",
+      "r437-two-window-carrier"
+    ],
+    "existing_checks": [
+      {
+        "scope": "PR #4088: mixed local/owner/phase ledger and moment reported.",
+        "evidence": "research/staged544-mixed-fourth-entry/README.md",
+        "remaining": "Independent binding of changed construction to paid histogram, distinct from full admission.",
+        "status": "author-checked",
+        "source_commit": "72d7efc181edb21806a878f174847c96dd410ab0",
+        "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129"
+      },
+      {
+        "scope": "PR #4091: sharp pooled ceiling proposed for fixed THREE/FOUR words and inventory.",
+        "evidence": "research/staged-fourth-mixture-ceiling/README.md",
+        "remaining": "Validate dual, exhaustive pattern scope and exact source equivalence before applying to newer fills.",
+        "status": "author-checked",
+        "source_commit": "a29bdd8f56cd18b805917775cdec09ff935eddc4",
+        "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129"
+      },
+      {
+        "scope": "PR #4067: paid (2,2) to (1,3) exchange and fixed OQ4 host reported.",
+        "evidence": "research/r437-two-window-carrier/README.md",
+        "remaining": "Independent full cost delta; remaining caller/precision/stock obligations are separate.",
+        "status": "author-checked",
+        "source_commit": "a95f11c52e3ca1e4c5171b3c20d8f4b0815aee2e",
+        "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129"
+      }
+    ]
+  },
+  "scope_status": "refined",
+  "actual_scope": "Prove S1 for every positive-partition invoice of the fixed p16 controller.",
+  "scope_change_reason": "The retained fragmentation ceiling assumes a single crossing and checks it on a grid. Weighted rank tails give a quantified interval proof for the stated complete invoice class.",
+  "bottleneck_link": "A native loss target needs a valid sufficient raw-moment test. This proof removes one sampled assumption without changing the invoice.",
+  "budget_minutes": 60,
+  "stop_rule": "Stop after the class-wide single-crossing proof and exact certificate; do not construct a native word or claim a new kappa.",
+  "outcome": "completed",
+  "evidence": "PROOF.md and RESULT.json: exact weighted tails, integer-root endpoint enclosure and a quantified partition/monotonicity proof.",
+  "author": "Ali Romman with OpenAI Codex assistance",
+  "ai_assistance": "Substantial OpenAI Codex assistance; no subagents or independent human review.",
+  "open_questions": [
+    {
+      "question": "Does a changed invoice outside the positive-partition class retain an interval monotonicity certificate?",
+      "why_it_matters": "Extra costs or changed endpoints can invalidate the sufficient tail test.",
+      "first_step": "Compute the new weighted tails and test the actual rank bound before using single-crossing sufficiency.",
+      "blocked_by": "A specified changed complete invoice."
+    }
+  ]
+}