Certify the pooled R437 carrier moment ceiling: 0.00173678297, unreachable 17/5000 below width 28571 (no new κ)

research/r437-pooled-moment-ceiling/README.md

@@ -0,0 +1,135 @@
+# Moment ceiling of the pooled R437 carrier profile
+
+**Finite exact certificate for a fixed profile. No new κ, supplier admission
+or frontier change.** This contribution is produced by Nick Petalas.
+
+ToikY's [PR #5810](https://github.com/CrocSwap/integer-mult-bounds/pull/5810)
+(`research/r437-unpooled-budget-obstruction`) shows that the unpooled #4067
+host fails the retained moment test at the admitted BIT target `17/5000`. It
+leaves other invoices open: "a different invoice, productive normalization,
+target allocation ... needs its own bound". Chris R / Clear1nsight's
+[PR #4176](https://github.com/CrocSwap/integer-mult-bounds/pull/4176)
+(`research/r437-carrier-integration`) fixes the pooled profiles C (original
+R437 with the 63 pooled owner moves) and D (the #4067 carrier with the same
+moves). Its BILL.md says "No new decimal root is needed". This package computes
+that root as a certified ceiling.
+
+## Result
+
+Use #5810's moment with every added charge omitted:
+
+    M(c) = Σ_r n_r · r/(64·28416) · (64/r)^c.
+
+Every rank in C and D is below 64, so each term increases with `c`. A
+nonnegative surcharge `S(c)` only raises the left side of `M(c)+S(c) <= 1`.
+The certificate proves `M(lo) < 1 < M(hi)` exactly. Therefore **every
+`c >= hi` fails for every nonnegative surcharge**, and the fixed contract cannot
+pass above the ceiling `hi`.
+
+| Profile | Source | Certified crossing bracket of M |
+|---|---|---|
+| U, unpooled #4067 host | #5810 README | (0.0017366903544672, 0.0017366903544673) |
+| C, pooled original | #4176 `PROFILE_C` | (0.0017367386530996, 0.0017367386530997) |
+| **D, pooled carrier** | #4176 `PROFILE_D` | **(0.0017367829682417, 0.0017367829682418)** |
+
+- **The carrier keeps its gain under pooling.** The D ceiling exceeds C by
+  4.4315142e-8 (exact interval in RESULT.json). The C ceiling exceeds U by
+  4.83e-8.
+- **The admitted BIT target is out of reach at this normalization.** For D,
+  `M(17/5000)` lies in an interval around `1.005440413297699` and exceeds 1.
+- **The required width is 28571.** With D's paid profile unchanged, `M(17/5000) <= 1`
+  holds exactly when the productive normalization is at least
+  `Σ n_r r (64/r)^{17/5000} / 64`. The certificate places that number strictly
+  between 28570 and 28571. The smallest integer width is **28571**, 155 more
+  than 28416. C and U give the same integer.
+
+All three profiles have 903456 paid calls, rank mass 1808352 and
+`M(0) = 18837/18944`. That matches #5810's constant `A`.
+
+**Consistency with reported values.** Two reported values should lie below
+these ceilings, since their invoices include surcharges that this package
+omits. Both do. #4067's passing grid point 0.001736690352456612377607 lies
+2.0e-12 below the U bracket. Rohan Arun's closed #3959 pooled crossing
+0.001736738651088946052684 lies 2.0e-12 below the C bracket. Neither
+predecessor was replayed.
+
+## Method
+
+`verify.py` uses only the standard library and exact `Fraction` intervals.
+Every endpoint is rounded outward to the grid `2^-256`.
+
+- `log 2, log 3, log 5, log 7, log 13` come from `atanh(1/q)` series for
+  `q = 3, 5, 9, 15, 25`, each with an explicit geometric tail bound.
+  `log(64/r)` is assembled by factoring `r`.
+- `exp(t)` on `0 <= t <= 1/2` uses the Taylor partial sum. The Lagrange tail is
+  bounded by twice the next term.
+- The profiles are read from #4176's `numerical.py` with `ast` and from #5810's
+  README text. No predecessor code is executed. Both files are pinned by
+  SHA256 in the verifier and in SOURCES.json. The verifier also checks the
+  call count, rank mass, the #4176 normalization `W = 28416` and `M = 64`.
+
+Controls must reject:
+- D's bracket applied to C;
+- the physical width 28425 in place of the productive width 28416;
+- one D rank-42 call moved to rank 1;
+- the carrier delta `{1:+288, 2:-576, 3:+288}` reversed on D.
+
+The log intervals are also checked against floating-point `log` and must be
+narrower than `10^-60`. The normal run requires byte equality with the
+committed [RESULT.json](RESULT.json); `--emit` prints the recomputation.
+
+## Reproduce
+
+From the repository root, CPython 3.12, standard library only:
+
+```sh
+python3.12 -B research/r437-pooled-moment-ceiling/verify.py
+python3.12 -O -B research/r437-pooled-moment-ceiling/verify.py
+python3.12 -B scripts/research_package.py --package research/r437-pooled-moment-ceiling
+```
+
+Each direct run prints `PASS_R437_POOLED_MOMENT_CEILING` and takes under one
+second.
+
+## Scope and limits
+
+- This is a **ceiling for one fixed moment test**. It assumes #5810's contract:
+  productive normalization `64·28416` and the retained gate `M + S <= 1`. It is
+  not a runtime lower bound, and it does not price D's complete invoice. It is
+  not admission of the pooled compiler, physical caller, precision or stock
+  boundaries, which #4176 and the family status keep open.
+- The width threshold is a statement about normalization only. Adding productive
+  columns would change the word, the caller and the paid profile. No such
+  construction is proposed.
+- The R437 line is not the selected supplier. The selected conditional κ stays
+  `0.00310045` (#5599). The BIT budget there is admitted at `.0034` from a
+  different supplier.
+
+## Open next questions
+
+1. **What is D's complete pooled crossing?** It matters because the ceiling
+   omits the 864 added ADDs, the finite invoice term and the pooled-routing
+   premise that #4176 retains. First step: add #4176's complete D invoice
+   charges to `M(c)` and bisect with the same interval arithmetic. Blocked by
+   #4176's retained absolute 77-factor routing premise, which has no
+   source-bound proof.
+2. **Which change of paid profile could close the gap to `17/5000`?** It
+   matters because one carrier exchange per call moves the ceiling by only
+   about 4.4e-8, while D still needs `M(17/5000)` lowered by about 0.544%.
+   First step: compute the exact per-call moment change of each available
+   local exchange at `c = 17/5000`, then compare the needed total with the
+   903456 paid calls. Blocked by: no inventory of further exchange-eligible
+   calls beyond #4067's 288.
+
+Structured versions are in [TASK.json](TASK.json).
+
+## Credit
+
+ToikY (#5810) supplied the fixed moment contract, the unpooled profile and the
+open pooled question. Chris R / Clear1nsight supplied the #4067 carrier, the
+#4176 pooled C/D profiles and normalization, and the earlier pooled-allocation
+audit. Rohan Arun supplied the #3959 pooled crossing. The retained R437 lineage
+credited in those packages is unchanged: ai-nanachi/#3647, Ali Romman/#1043,
+Sagar Thakrar/#3700, unpaidmoon/#4147, zxv/#3690 and others. The new work is
+the certified pooled ceilings, the carrier gain under pooling and the
+width threshold. Apache-2.0.

research/r437-pooled-moment-ceiling/RESULT.json

@@ -0,0 +1,103 @@
+{
+  "ceiling_gain_C_minus_U": [
+    "482986323/10000000000000000",
+    "19319453/400000000000000"
+  ],
+  "ceiling_gain_D_minus_C": [
+    "22157571/500000000000000",
+    "221575711/5000000000000000"
+  ],
+  "controls_rejected": [
+    "D bracket applied to C",
+    "physical width 28425 instead of productive 28416",
+    "one D rank-42 call moved to rank 1",
+    "carrier delta reversed on D",
+    "log intervals tight and consistent with float log"
+  ],
+  "normalization": "64*28416",
+  "profiles": {
+    "C": {
+      "M0": "18837/18944",
+      "M_at_target_interval_decimal": [
+        "1.005440697467206",
+        "1.005440697467206"
+      ],
+      "crossing_bracket": [
+        "0.0017367386530996",
+        "0.0017367386530997"
+      ],
+      "extra_productive_columns": 155,
+      "min_productive_width_at_target": 28571,
+      "profile": {
+        "1": 380160,
+        "14": 1,
+        "2": 400877,
+        "3": 22176,
+        "4": 26592,
+        "42": 403,
+        "5": 29376,
+        "6": 17375,
+        "7": 26496
+      }
+    },
+    "D": {
+      "M0": "18837/18944",
+      "M_at_target_interval_decimal": [
+        "1.005440413297699",
+        "1.005440413297699"
+      ],
+      "crossing_bracket": [
+        "0.0017367829682417",
+        "0.0017367829682418"
+      ],
+      "extra_productive_columns": 155,
+      "min_productive_width_at_target": 28571,
+      "profile": {
+        "1": 380448,
+        "14": 1,
+        "2": 400301,
+        "3": 22464,
+        "4": 26592,
+        "42": 403,
+        "5": 29376,
+        "6": 17375,
+        "7": 26496
+      }
+    },
+    "U": {
+      "M0": "18837/18944",
+      "M_at_target_interval_decimal": [
+        "1.005441005045044",
+        "1.005441005045044"
+      ],
+      "crossing_bracket": [
+        "0.0017366903544672",
+        "0.0017366903544673"
+      ],
+      "extra_productive_columns": 155,
+      "min_productive_width_at_target": 28571,
+      "profile": {
+        "1": 380448,
+        "2": 400288,
+        "26": 32,
+        "3": 22464,
+        "4": 26592,
+        "42": 384,
+        "5": 29376,
+        "6": 17376,
+        "7": 26496
+      }
+    }
+  },
+  "reported_3959_pooled_crossing": {
+    "below_ceiling_of": "C",
+    "gap_to_bracket_lo": "502663486829/250000000000000000000000",
+    "value": "0.001736738651088946052684"
+  },
+  "reported_4067_unpooled_grid_point": {
+    "below_ceiling_of": "U",
+    "gap_to_bracket_lo": "2010587622393/1000000000000000000000000",
+    "value": "0.001736690352456612377607"
+  },
+  "target": "17/5000"
+}

research/r437-pooled-moment-ceiling/SOURCES.json

@@ -0,0 +1,30 @@
+{
+  "schema_version": 1,
+  "base_commit": "19fdb086ea96af9a9f87936a2b888e10af4ed810",
+  "files": [
+    {
+      "path": "certificates/selected-result.json",
+      "usage": "provenance",
+      "git_blob": "581f8d87008354eb5b869f7ed9de1317ad837ce8",
+      "sha256": "2a0220e866417774606e0f991e41b9c1d26b1f43b97857238cf478dbc7d330b5"
+    },
+    {
+      "path": "docs/research/agent-task-catalog.json",
+      "usage": "provenance",
+      "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec",
+      "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81"
+    },
+    {
+      "path": "research/r437-carrier-integration/numerical.py",
+      "usage": "input",
+      "git_blob": "d3411758be96f22f8d64e02ba278dc46b21639c5",
+      "sha256": "83f2b60a90ab2d0354c5c84f48af246ab416605c3ae4bd62368bbe5f23bb53bb"
+    },
+    {
+      "path": "research/r437-unpooled-budget-obstruction/README.md",
+      "usage": "input",
+      "git_blob": "6b1a2a36a7f0dd69261a25bb32faf131a60126f8",
+      "sha256": "f41669bda70e75a91471539303011766b7348353e88a3ef9774865d3dd24e512"
+    }
+  ]
+}

research/r437-pooled-moment-ceiling/TASK.json

@@ -0,0 +1,90 @@
+{
+  "schema_version": 1,
+  "task_id": "r437-carrier-integration",
+  "priority_revision": 8,
+  "base_commit": "19fdb086ea96af9a9f87936a2b888e10af4ed810",
+  "original_card": {
+    "id": "r437-carrier-integration",
+    "question": "Can the paid R437 two-window carrier improvement be admitted by the actual pooled compiler and physical caller?",
+    "starting_points": [
+      "docs/research/research-family-status.md",
+      "certificates/selected-result.json",
+      "research/r437-two-window-carrier/README.md",
+      "research/r437-reverse-row-coefficient/README.md"
+    ],
+    "methods": [
+      "Close one compiler/request, caller or precision/stock implication for the pinned paid exchange.",
+      "Falsify that exact interface with an arbitrary-dirty-state or chronology counterexample."
+    ],
+    "acceptance_gate": "Pin the complete source and destination contracts, exact paid and scalar deltas, and all remaining assumptions. A local moment gain is not a physical or all-size supplier admission.",
+    "first_step": {
+      "command": [
+        "python3",
+        "-B",
+        "scripts/research_selected_baseline.py"
+      ],
+      "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY",
+      "inspect": "Resolve the current selected review, separate complex/ordinary BIT/admitted BIT/outer budgets, and compare the card against live handoffs before starting. Historical ceilings require exact source/model equivalence.",
+      "scope": "Source-binding orientation only; not a scientific replay or all-size proof. Materialize selected inputs if this checkout is sparse."
+    },
+    "first_experiment": "Choose one unclaimed obligation: pooled compiler codebook/request alignment, actual physical caller, or precision/stock envelope using the already reported reverse coefficient. Pin the input and receiver, preserve dirty/source windows, and test one binding with a rejection control. Stop at unresolved dependencies; do not rederive the coefficient or quote the local moment as a completed bound.",
+    "bottleneck_link": "The exchange changes the paid profile; integration must establish that its gain survives the complete caller.",
+    "allowed_variations": [
+      "One compiler rebind, one actual caller boundary, or one precision/stock implication."
+    ],
+    "scope_change_triggers": [
+      "Ignoring added ADDs, retaining an obsolete reverse coefficient, or declaring global admission from the local histogram."
+    ],
+    "overlap_terms": [
+      "R437",
+      "two-window carrier",
+      "4067",
+      "4147",
+      "pooled compiler",
+      "request alignment",
+      "reverse row coefficient"
+    ],
+    "existing_checks": [
+      {
+        "scope": "PR #4067: source-bound two-window carrier with (2,2) to (1,3) paid exchange and fixed OQ4 host.",
+        "evidence": "research/r437-two-window-carrier/README.md",
+        "remaining": "Pooled compiler/request rebind, physical caller and precision/stock admission.",
+        "status": "author-checked",
+        "source_commit": "a95f11c52e3ca1e4c5171b3c20d8f4b0815aee2e",
+        "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129"
+      },
+      {
+        "scope": "PR #4147: reverse row coefficient follow-up.",
+        "evidence": "research/r437-reverse-row-coefficient/README.md",
+        "remaining": "Use the exact coefficient in a caller-bound precision/stock proof rather than repeat the arithmetic.",
+        "status": "author-checked",
+        "source_commit": "72e7bb797adf82aeb525a399f56ab8adbab8e93c",
+        "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129"
+      }
+    ]
+  },
+  "scope_status": "refined",
+  "actual_scope": "Certified ceiling of the retained fixed moment test (PR #5810 contract, productive normalization 64*28416, surcharges omitted) for the pooled R437 C and D profiles fixed by PR #4176, with the unpooled #4067 host as a comparison row and the smallest productive normalization at which D's paid profile could meet the admitted BIT target 17/5000.",
+  "scope_change_reason": "The card asks for admission of the carrier through the pooled compiler and caller. This package settles one necessary pricing implication of that admission, the pooled moment ceiling that PR #4176 left uncomputed, and does not attempt compiler, caller, precision or stock admission.",
+  "bottleneck_link": "Side result on a non-selected BIT supplier: it shows that the pooled carrier keeps its moment gain (+4.43e-8 over pooled C) and that no surcharge allocation lets the fixed pooled profile reach the current admitted BIT budget 17/5000 without about 155 more productive columns.",
+  "budget_minutes": 60,
+  "stop_rule": "Stop after the first exact interval certificate for the D ceiling and the width threshold; do not search for a changed allocation or price the complete invoice.",
+  "outcome": "completed",
+  "evidence": "Exact outward-rounded rational interval certificate: M_D(0.0017367829682417) < 1 < M_D(0.0017367829682418); M_D(17/5000) > 1; 28570 < sum n_r r (64/r)^(17/5000)/64 < 28571. Same certificates for C and U; four rejecting mutation controls; RESULT.json byte equality.",
+  "author": "Nick Petalas",
+  "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.",
+  "open_questions": [
+    {
+      "question": "What is the complete crossing of the pooled D invoice once its 864 added ADDs, finite invoice term and pooled-routing premise are charged?",
+      "why_it_matters": "The certified ceiling omits every surcharge; only the complete invoice gives D's actual fixed-contract crossing.",
+      "first_step": "Add PR #4176's complete D invoice charges to M(c) and bisect with the same interval arithmetic.",
+      "blocked_by": "PR #4176 retains an absolute 77-factor routing/primitive premise without a source-bound proof."
+    },
+    {
+      "question": "Which change of paid profile could close the gap between the pooled D profile and 17/5000?",
+      "why_it_matters": "One carrier exchange per call moves the ceiling by about 4.4e-8, while D still needs M(17/5000) lowered by about 0.544%.",
+      "first_step": "Compute the exact per-call moment change of each available local exchange at c = 17/5000 and compare the needed total with the 903456 paid calls.",
+      "blocked_by": "No inventory of further exchange-eligible calls beyond #4067's 288."
+    }
+  ]
+}

research/r437-pooled-moment-ceiling/VERIFY.json

@@ -0,0 +1,31 @@
+{
+  "schema_version": 1,
+  "status": "ready",
+  "python": "3.12",
+  "requirements": [],
+  "inputs": [
+    "research/r437-carrier-integration/numerical.py",
+    "research/r437-unpooled-budget-obstruction/README.md"
+  ],
+  "commands": [
+    {
+      "argv": [
+        "{python}",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 120,
+      "checks": "Pinned C/D/U profiles and normalization; exact interval brackets for each crossing; M(17/5000)>1; width threshold 28571; reported #4067/#3959 values below ceilings; four rejecting mutation controls; RESULT.json byte equality."
+    },
+    {
+      "argv": [
+        "{python}",
+        "-O",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 120,
+      "checks": "Same certificate under -O; the verifier uses explicit Fail checks, not assert."
+    }
+  ]
+}