Independently check #4405's refined #4359 ranks and endpoint family: all reproduce; z0 and the exit constant are not levers, the uniform saving is (no new κ)

research/pr4405-refill-check/README.md

@@ -0,0 +1,97 @@
+# Independent check of #4405's refined template ranks and endpoint family
+
+**Claim type:** an independent exact check plus a quantitative lever analysis. **No new κ.** It
+checks 1337isnot1337's [#4405](https://github.com/CrocSwap/integer-mult-bounds/pull/4405), at head
+`873d1b3c96a83b701a5c0bba8e37a861e6672fef`. That PR refines zxv's #4359:
+
+- `TEMPLATE.md` (SHA256 prefix `3778e49c`) gives smaller explicit uniform ranks;
+- `ENDPOINT.md` (`9b8d08cd`) gives a parameter family that admits every rational κ below the
+  complex mixed root.
+
+My #4404 audited #4359's original rank chain. Nothing is imported from #4405 or #4359, and the
+invoices are embedded as printed in #4359.
+
+## Results
+
+**Part A: the refined ranks reproduce.** The refined induction requires only that the exit
+coefficient satisfy `(16·n^{−h})^δ ≤ η = z0·m^{z0−1}`, not that it be at most `1/8 < η/2`. The
+step is `L(n) ≤ A(n^{z0} − ηS + ηS)`, which is valid. With its own certified logarithms, the
+verifier recomputes:
+
+| | `H0` | `H1` | #4359's `H1` |
+| --- | --- | --- | --- |
+| Complex | 335,449 | 1,546,084,442 | 276,540,184,361 |
+| BIT | 69,740 | 42,843,607 | 6,552,928,412 |
+
+Both match #4405. Each `H0` is certified minimal, since one less fails for every value in the
+log enclosure, and each `H1` is minimal. The endpoint's sufficient complex rank exponent,
+2,099,384,703,303,215,709, also reproduces.
+
+**Part B: #4405's suggested levers.** These answer `TEMPLATE.md`'s "next quantitative questions":
+
+- **The intermediate `z0`.** A 199-point rational grid over `(t, z)` finds no `H1` below the
+  midpoint's, in either family. The leading factor is `1/((z0−t)(z−z0))`, which is minimized at
+  the midpoint, so optimizing `z0` gains nothing.
+- **The exit constant 16.** Its `4δ` term is `1.2·10⁻⁴` of `H0` (complex) and `9.2·10⁻⁴` (BIT).
+  Sharpening it is negligible.
+- **The uniform saving.** This is the real lever. `H1` scales like `1/δ²`, where `δ` is half the
+  gap between the tested mixed saving and the uniform saving:
+
+  | Uniform saving | complex `H1` | BIT `H1` |
+  | --- | --- | --- |
+  | 0.002300 | 61,765,945 | 13,943 |
+  | 0.002302 | 171,679,856 | 14,073 |
+  | 0.002303 | 386,399,233 | 14,139 |
+  | as used (0.002304 / 0.002760) | 1,546,084,442 | 42,843,607 |
+
+  #4359 admits BIT at 0.0027 only so that it does not cap the complex supplier. A BIT uniform
+  saving much closer to the complex one would therefore shrink the BIT rank to about `2^14000`.
+  That would hold only if the cover fallback and conversion still leave BIT above the complex
+  saving, which is not checked here.
+
+**Part C: the endpoint family.**
+
+- **The root bound.** The complex mixed moment at `C_test = 0.00230509019` is certified positive,
+  about `4.7·10⁻⁷`, so `C_test < C*`. It is negative at 0.002306, so `C* < 0.002306`.
+- **The gap identities.** These are all exact identities with strictly positive values at
+  `κ = 0.00230509` and at 24 further rational κ between 10⁻⁷ and 0.0023:
+  - `ξ = 29/32 + (1−d)q` and `εq = κ + d(3−q)`;
+  - `λ−τ = d/2`, `λ−σ = 3d/2` and `λ'−λ = d/2`;
+  - `(1−stop)b − a = d(1−b)`;
+  - `ε − ξ = 3/32 − d − (1−d)q`;
+  - `1 − (2ξ−2) − r0 − β = 3/16 − 2(1−d)q + 29d/10`;
+  - the parameter order and the geometric gaps.
+
+## Not covered
+
+- The nine outer cost-row formulas themselves. Only the self-contained identities are checked.
+- Native closure, adapters, the delayed cover and the BIT cover fallback.
+- Whether a smaller uniform saving is admissible at the outer layer.
+
+## Reproduce
+
+```sh
+python3.12 -B scripts/research_package.py --package research/pr4405-refill-check --check-only
+python3.12 -B scripts/research_package.py --package research/pr4405-refill-check
+```
+
+The verifier prints `PASS_PR4405_REFILL_INDEPENDENT_CHECK` in about one second, using only the
+standard library.
+
+## Open next questions
+
+1. **What is the smallest BIT uniform saving that still clears the complex binding row after the
+   cover fallback and conversion?**
+   - *Why it matters:* the BIT rank would drop from `2^42843607` to about `2^14000`.
+   - *First step:* recompute #4359's BIT fallback bill as a function of the uniform saving and
+     of `N`.
+   - *Blocked by:* the fallback formula in `DELAYED-COVER-BRIDGE.md`.
+
+## Credit
+
+- The refinement and endpoint family are 1337isnot1337's (#4405).
+- The construction and invoices are zxv's (#4359).
+- Theorem 1G is Jacob Alan Sussman's (#4268).
+
+Prepared by Ryanson Jonathan with substantial Claude Code (Claude Opus 5.5) assistance.
+Apache-2.0.

research/pr4405-refill-check/SOURCES.json

@@ -0,0 +1,18 @@
+{
+  "schema_version": 1,
+  "base_commit": "12fa8c5c844be21bfefb38a19503fbd867a11244",
+  "files": [
+    {
+      "path": "certificates/selected-result.json",
+      "usage": "provenance",
+      "git_blob": "b1fea0c94436b236cc2b7d41a7be032811b94c81",
+      "sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129"
+    },
+    {
+      "path": "docs/research/agent-task-catalog.json",
+      "usage": "provenance",
+      "git_blob": "64bfc5af6709ed9811171e0a2108f05e1219cb65",
+      "sha256": "352a6184713b8843d96fd2c2071eb7aeaa655906b7c51d45ad444912666c8a96"
+    }
+  ]
+}

research/pr4405-refill-check/TASK.json

@@ -0,0 +1,100 @@
+{
+  "schema_version": 1,
+  "task_id": "independent-moment",
+  "priority_revision": 7,
+  "base_commit": "12fa8c5c844be21bfefb38a19503fbd867a11244",
+  "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": "Independently check #4405's refined template ranks and endpoint slack family for #4359, and quantify its suggested levers.",
+  "scope_change_reason": "The card asks for independent coverage of a new paid-profile claim; #4405 refines the largest open conditional claim and had no review.",
+  "bottleneck_link": "#4359/#4405's uniform savings rest on these explicit-rank and slack-family steps.",
+  "budget_minutes": 30,
+  "stop_rule": "Stop at self-contained arithmetic; do not audit outer row formulas or native closure.",
+  "outcome": "completed",
+  "evidence": "verify.py: H0/H1 reproduced and minimal for both families and the endpoint; midpoint z0 optimal on a 199-point grid; exit constant 16 is 1e-4..1e-3 of H0; H1 falls to 61,765,945 (complex) / 13,943 (BIT) at uniform saving 0.0023; C_test < C* < 0.002306 certified; gap identities exact at 25 kappa.",
+  "author": "Ryanson Jonathan, with Claude Code (Claude Opus 5.5) assistance",
+  "ai_assistance": "Substantial Claude Code (Claude Opus 5.5) assistance; no independent human review.",
+  "open_questions": [
+    {
+      "question": "What is the smallest BIT uniform saving that still clears the complex row after cover fallback and conversion?",
+      "why_it_matters": "The BIT rank would fall from 2^42843607 to about 2^14000.",
+      "first_step": "Recompute #4359's BIT fallback bill as a function of the uniform saving and N.",
+      "blocked_by": "The fallback formula in DELAYED-COVER-BRIDGE.md."
+    }
+  ]
+}

research/pr4405-refill-check/VERIFY.json

@@ -0,0 +1,18 @@
+{
+  "schema_version": 1,
+  "status": "ready",
+  "python": "3.12",
+  "requirements": [],
+  "inputs": [],
+  "commands": [
+    {
+      "argv": [
+        "{python}",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 120,
+      "checks": "Embedded #4359 invoices; certified log2(eta) enclosure; #4405 H0/H1 (complex 335449/1546084442, BIT 69740/42843607) reproduced and minimal; endpoint H1 2099384703303215709; z0 grid, exit-constant share and uniform-saving curve; mixed moment sign at C_test and 0.002306; ENDPOINT.md gap identities at 25 rational kappa."
+    }
+  ]
+}