Independently check #4416's paid-completion tensor bound at kappa 0.00268647: proof steps and arithmetic hold; gamma margin 8e-6; least v 5745 (no new κ)

research/pr4416-padding-check/README.md

@@ -0,0 +1,82 @@
+# Independent check of #4416's paid-completion tensor bound
+
+**Claim type:** a written proof check plus certified exact arithmetic. **No new κ.** #4416 is not
+accepted, and the native p7 audit and the outer premises are not re-checked. The object is
+1337isnot1337's [#4416](https://github.com/CrocSwap/integer-mult-bounds/pull/4416) at head
+`e9058860`, with `TENSOR.md` SHA256 prefix `b2eba86c` and `ENDPOINT.md` prefix `e7056020`. It
+proposes conditional κ = 0.00268647 from zxv's p7 controller. The p7 controller is tensored
+`v = 6240` times, small targets are completed to `11^v`, and paid jobs are split at `10^v`.
+
+## Proof check (`TENSOR.md` §1–3, §5)
+
+- **Product moments multiply.**
+  - Copy `j` of `U` runs at column `h_j`.
+  - Each paid position `l` of `U` makes one call to `V` at column `r_l`, whose role `j` delivers
+    rank `r_l h_j`.
+  - So the targets are `k_i h_j`, the paid ranks are `r_l s_a`, `T_τ(UV) = T_τ(U)T_τ(V)` and
+    `P_τ(UV) = P_τ(U)P_τ(V)`.
+- **Completion.** Completing to rank `L` on disjoint axes is the canonical rank-`L` endpoint.
+  By concavity it loses moment, since `L^τ − K^τ < D^τ`. What it buys is the separation
+  `paid ≤ 10^v < 11^v ≤ target`. The bound conservatively keeps `T_τ^v` as the target moment.
+- **Split tails.** `qJ^τ + r^τ ≤ RJ^{−C} + J^τ ≤ 2RJ^{−C}` holds for `R > J`. For completions,
+  `charge(D) ≤ (D + J)J^{−C} < 2L/J^C`. Together these give `α^v + 2γ^v + 2δ^v`.
+- **Rank formula.**
+  - `r_max m^h < 2^{(111/26)v}` follows from `10 < 2⁴` and `121 < 2⁷`.
+  - `−log₂η < 1 + 7v(1−z0)` follows from `z0 > 1/2`.
+  - `θ < 25/26` follows from `10^26 < 11^25`.
+  - `H0 ≥ 7v` covers the base range `n < 121^v`.
+
+I found no gap in these steps.
+
+## Certified arithmetic
+
+| Quantity | This check | #4416 |
+| --- | --- | --- |
+| fields, paid calls, rank-one masses | 7,688; 55,998; 131,723 / 131,115 | same |
+| `α = P_τ/T_τ` at `C = 0.00268648` | `< 0.999999984404` | `< 1 − 10⁻⁸` |
+| `γ = P₁/(10^C T_τ)` | `< 0.99819171` | `< 4991/5000 = 0.9982` |
+| `δ = 7688·11/(10^C T_τ)` | `< 0.64382471` | `< 2/3` |
+| p7 mixed root | `(0.0026864890486, 0.0026864890492)` | above 0.00268648 |
+| `α^v + 2γ^v + 2δ^v < 1` at `v = 6240` | holds (Bernoulli and direct) | holds |
+| least `v` (direct certified route, `b = 11`, `c = 10`) | **5,745** | 6,240 used |
+| `H0`, `H1` | 4,307,773,805,920 and 16,201,843,136,005,340,321 | same |
+
+The tight margin is `γ`: its bound sits only `8·10⁻⁶` below 4991/5000. The tested saving
+0.00268648 is `9·10⁻⁹` below the p7 root.
+
+**A tighter rank from the same induction.** Using certified `−log₂η` and the exact
+`log₂(r_max m^h)`, together with the best `θ̄ = 145/151` (from `10^151 < 11^145`, so
+`h = 6/151`), gives `H1 = 15,370,312,178,898,752,926`. That is 5.4% below #4416's value. It is a
+minor gain: the binding factor is `δ_gap = 1/1,400,000,000`, which is set by the choice of κ.
+
+## Not covered
+
+- The native p7 audit: contacts, phases, helpers and the all-column contract.
+- The analytic, precision, tape and outer premises.
+- The 209-profile screen in `FOLLOWUP.md`.
+- Optimality of `(v, b, c)`.
+
+## Reproduce
+
+```sh
+python3.12 -B scripts/research_package.py --package research/pr4416-padding-check --check-only
+python3.12 -B scripts/research_package.py --package research/pr4416-padding-check
+```
+
+The verifier prints `PASS_PR4416_PADDING_ARITHMETIC` in about 10 seconds, using only the
+standard library.
+
+## Open next questions
+
+1. **Which `(b, c)` minimizes `v`?**
+   - *Why it matters:* the least `v` with `(11, 10)` is 5,745.
+   - *First step:* scan `c < b < 121` with the direct certified route.
+
+## Credit
+
+- The construction and invoice are 1337isnot1337's (#4416, #4414, #4412).
+- The native controller is 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/pr4416-padding-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-padding-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 #4416's paid-completion tensor bound and arithmetic at kappa 0.00268647.",
+  "scope_change_reason": "The card asks for independent coverage of a new paid-profile claim; #4416 is the largest open conditional claim and had no review.",
+  "bottleneck_link": "#4416's kappa rests on the p7 moment, the completion/split tails and the compiler rank.",
+  "budget_minutes": 30,
+  "stop_rule": "Stop at the tensor bound and arithmetic; do not audit the native p7 word.",
+  "outcome": "completed",
+  "evidence": "verify.py: alpha < 0.999999984404, gamma < 0.99819171 (margin 8e-6 to 4991/5000), delta < 0.6438; p7 root (0.0026864890486, 0.0026864890492); v=6240 inequality holds, least v 5745; #4416 H0/H1 reproduced; tighter H1 15370312178898752926.",
+  "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": "Which (b, c) minimizes the tensor power v?",
+      "why_it_matters": "The least v with (11,10) is 5745.",
+      "first_step": "Scan c<b<121 with the direct certified route.",
+      "blocked_by": "None."
+    }
+  ]
+}

research/pr4416-padding-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": 300,
+      "checks": "p7 invoice totals; certified alpha, gamma, delta at C=0.00268648; p7 mixed root bracket; v=6240 inequality by Bernoulli and direct certified powers; least v; #4416 H0/H1 reproduced; tighter sufficient rank."
+    }
+  ]
+}