Independently check #4416's moment and paid-tail inequalities at κ = 0.00268647: all hold; the tested saving sits 9.05e-9 below this invoice's limit (no new κ)

research/pr4416-moment-check/README.md

@@ -0,0 +1,99 @@
+# Independent check of #4416's moment and paid-tail inequalities
+
+**Claim type: an independent certified finite check. No new κ.** This does
+not accept #4416. It checks none of its native audit, outer ledger or
+inherited premises.
+
+## Object
+
+[PR #4416](https://github.com/CrocSwap/integer-mult-bounds/pull/4416)
+(1337isnot1337, head `e9058860`) claims a conditional κ = 0.00268647, the
+highest open claim when this check ran. Its strictification (TENSOR.md §3–4)
+needs, at saving `C = 0.00268648` with `τ = 1 − C`:
+
+```text
+alpha = P_tau/T_tau < 1 - 1/10^8,
+gamma = P_1/(10^C T_tau) < 4991/5000,
+delta = 7688*11/(10^C T_tau) < 2/3,
+alpha^6240 + 2 gamma^6240 + 2 delta^6240 < 1.
+```
+
+Here `X_τ = Σ n_r r^τ`, over the raw p7 invoices `T` (7,688 targets) and `P`
+(55,998 paid calls). No outside check existed.
+
+## Results
+
+Every link holds, recomputed with exact rationals and enclosure widths below
+`10⁻³⁰`:
+
+| Link | Value | Required |
+| --- | --- | --- |
+| `alpha` | `0.999999984403908…`, so `1 − alpha = 1.56·10⁻⁸` | `< 1 − 10⁻⁸` |
+| `gamma` (`c = 10`) | `0.998191712473…` | `< 4991/5000` |
+| `delta` (`b = 11`) | `0.643824709152…` | `< 2/3` |
+| `(4991/5000)^390 < 1/2`, `(2/3)² < 1/2`, `6240 = 16·390` | exact | — |
+| Normalized bound `1/(1 + 6240/10⁸) + 4/2¹⁶` | `10240625039/10240638976` | `< 1` |
+| Gap | exactly `13937/10240638976 = 1.36095…·10⁻⁶` | as stated |
+
+**Binding.** The invoices in RESULT.json's strictification block equal its
+native-inventory block and the two lines in TENSOR.md:
+
+- the counts are 7,688 and 55,998;
+- the rank-one moments are 131,723 and 131,115, a surplus of 608;
+- the ambient is 121.
+
+All three enclosures overlap #4416's recorded intervals.
+
+**Headroom: the tested saving is at this invoice's ceiling.** As the tensor
+power grows, the construction works for every `C` with `alpha < 1`; `gamma`
+and `delta` stay below 1 there. The limit saving, where `alpha = 1`, is
+
+```text
+C* = 0.002686489049…,      C* − 0.00268648 = 9.05·10⁻⁹.
+```
+
+So #4416's κ = 0.00268647 uses essentially all the headroom of this native
+p7 invoice. A higher κ on this route needs a different invoice, not a larger
+tensor power.
+
+**Controls.**
+
+- Completing every target to the full ambient (`b = 121`) gives `delta > 1`.
+- The undamped rank-one tail `P_1/T_τ` exceeds 1.
+
+So both damping choices are needed, as TENSOR.md says.
+
+## Not covered
+
+- The native audit that produces `T` and `P`. These are taken from #4416's
+  inventory, not rebuilt from the word.
+- The tensor composition, completion and splitting proofs, which are written
+  arguments.
+- The compiler ranks, the nine outer cost rows and every inherited physical,
+  precision and analytic premise.
+
+## Reproduce
+
+```sh
+python3.12 -B research/pr4416-moment-check/verify.py
+```
+
+It prints `PASS_PR4416_MOMENT_CHECK` in about 90 seconds, using only the
+standard library. `vendor/` holds #4416's TENSOR.md and RESULT.json,
+byte-identical and SHA256-checked.
+
+## Open next questions
+
+1. **Rebuild `T` and `P` from #4416's native word.**
+   - *Why it matters:* the moment margin is only `5.6·10⁻⁹` above what
+     `alpha` needs. One extra paid call of rank 1 changes `alpha` by about
+     `1/131723`, far more than that margin.
+   - *First step:* census #4416's p7 native word with separate code.
+   - *Blocked by:* nothing.
+
+## Credit
+
+The construction and the invoices are #4416's (1337isnot1337, with OpenAI
+Codex assistance), building on zxv's #4359, #4405, #4412 and #4414, and Jacob
+Alan Sussman's Theorem 1G. Prepared by Ryanson Jonathan with substantial
+Claude Code (Claude Opus 5.5) assistance. Apache-2.0.

research/pr4416-moment-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/pr4416-moment-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 certify #4416's strictification inequalities (alpha, gamma, delta at saving 0.00268648, the v = 6240 closing argument and the gap) from its recorded p7 invoice, and compute the invoice's limit saving.",
+  "scope_change_reason": "The card asks for independent coverage of a new paid-profile or moment claim; #4416 is the highest open conditional kappa and had no outside check.",
+  "bottleneck_link": "#4416 raises the conditional kappa to 0.00268647; its moment inequalities must hold before its native and outer premises are worth review.",
+  "budget_minutes": 30,
+  "stop_rule": "Stop once every stated inequality is certified or fails.",
+  "outcome": "completed",
+  "evidence": "verify.py: invoices bound across RESULT.json and TENSOR.md (7,688 / 55,998, rank-one 131,723 / 131,115); alpha = 0.9999999844 < 1 - 1e-8, gamma = 0.99819 < 4991/5000, delta = 0.64382 < 2/3 with enclosures below 1e-30 overlapping #4416's; integer comparisons and Bernoulli bound; normalized bound 10240625039/10240638976 and gap 13937/10240638976 exact; limit saving C* = 0.002686489049, 9.05e-9 above the tested saving; b = 121 and undamped-tail controls fail.",
+  "author": "Ryanson Jonathan, with Claude Code (Claude Opus 5.5) assistance",
+  "ai_assistance": "Substantial Claude Code (Claude Opus 5.5) assistance in reading, verifier implementation and writing; no independent human or proof-kernel review.",
+  "open_questions": [
+    {
+      "question": "Rebuild #4416's T and P invoices from its native word with separate code.",
+      "why_it_matters": "alpha clears its 1e-8 requirement by only 5.6e-9; one extra rank-one paid call moves alpha by about 7.6e-6.",
+      "first_step": "Census #4416's p7 native word independently.",
+      "blocked_by": "None."
+    }
+  ]
+}

research/pr4416-moment-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": 600,
+      "checks": "Vendored TENSOR.md and RESULT.json hashes and phrases; invoice binding and aggregates; certified alpha, gamma, delta at 0.00268648; integer comparisons, Bernoulli step, exact normalized bound and gap; limit saving by bisection; completion-base and undamped-tail controls."
+    }
+  ]
+}

research/pr4416-moment-check/vendor/NOTICE.md

@@ -0,0 +1,9 @@
+# Vendored files
+
+Byte-identical copies of `research/pr4359-p7-padding/TENSOR.md` (Git blob
+`8ecfd3e4d0bcb449ecb1e150c4f1f4fbb39ca656`) and `research/pr4359-p7-padding/RESULT.json`
+(Git blob `ebb30a9b3b94fb159a316350f7da57bde4a30c25`) from
+[PR #4416](https://github.com/CrocSwap/integer-mult-bounds/pull/4416) at head
+`e9058860b5c850760fdf970e796a96aefcdb1d98`. They are copied because that head is not reachable
+from canonical main; `verify.py` checks their SHA256 values. 1337isnot1337's work with OpenAI
+Codex assistance, building on zxv's #4359; Apache-2.0, as that package states.