Independently check #4270's conservative κ = 1/580 exponent chain: every link holds (no new κ)

research/pr4270-outer-exponent-check/README.md

@@ -0,0 +1,80 @@
+# Independent check of #4270's conservative exponent chain
+
+**Claim type: an independent exact check of a written arithmetic chain,
+including a certified moment enclosure. No new κ.** This does not accept
+#4270. It checks no physical, hosting or analytic premise.
+
+## Object
+
+[PR #4270](https://github.com/CrocSwap/integer-mult-bounds/pull/4270)
+(Ross Richardson, head `a929a3fa36301bdfcffe82afd37434dd9e3c4887`) claims a
+conditional `κ = 1/580`, above the selected `0.001672660197076918`.
+
+Its conservative argument in `OUTER-JOIN.md` §1 and §5 rests on a chain of
+explicit inequalities. Before this package, the only outside check was
+thu-nmrc's comment on the PR, which replayed the registered commands under
+Python 3.11 and matched the source hashes. No independent recomputation of
+the chain existed.
+
+## Results
+
+Every link holds. Each is computed here with exact rationals from the
+vendored text and the pooled fill's result file.
+
+| Link | Margin |
+| --- | --- |
+| Pooled moment `Σ n_r (r/73)^(1−a)/322560` at `a = C`, against 1. The certified upper bound is `1 − 7.4158·10⁻²⁵`, and the moment exceeds 1 at the bracket's upper end `C + 10⁻²⁴`. Because it straddles 1, the bracket pins `m = 73` and `W = 322560` for #4181's profile. | `7.4·10⁻²⁵` |
+| `σ* = 0.99826995 > 1 − C` (so the moment at `σ*` is below 1) | `9.3·10⁻⁷` |
+| `τ = 332353/332929 < σ*` | `4.9·10⁻⁸` |
+| Stopped-tree leaf exponent `σ* + θ(1−σ*) < α_layer = 0.99827`. The internal exponent and the root reservation `.998` are lower still. | `4.8·10⁻⁸` |
+| `Φ = 1 − (997/1000)(1 − α_layer) = 0.99827519` exactly; full-support router `β = 41544341/41616125 < Φ` | `9.8·10⁻⁸` |
+| The other cost powers stay below `Φ`: `.997`, `.9981`, `3/5`, `.997τ` (the support's second term) and `.997` (the CRT `D·Tp` term) | at least `1.75·10⁻⁴` (from `.9981`) |
+| `1 − Φ > 1/580` | `6.7·10⁻⁷` |
+| `1/580 >` selected `κ` | `5.1·10⁻⁵` |
+
+**Control.** The old physical Fourier rate `.00172380303` falls short of
+`1/580`, as `OUTER-JOIN.md` itself says. So the changed layer exponent is
+load-bearing.
+
+**Reading the margins.** The tightest links are `σ* − τ`, `α_layer −` leaf
+and `Φ − β`, all at about `5–10·10⁻⁸`. They pass, but any upstream change to
+`τ` or `β` at that scale would need this chain rechecked.
+
+## Not covered
+
+This package does not cover:
+
+- the pooled native/hosting identities, the stopped-tree proof itself, the
+  support and Gaussian constructions, or the analytic prime and Gaussian
+  theorems — all of which #4270 states as premises;
+- the derivation of `τ`, `β` or `Φ`'s form from their sources (only the
+  arithmetic on them is checked);
+- the cost table's row structure (only its listed powers are checked);
+- any production run, or any proof-kernel check.
+
+## Reproduce
+
+```sh
+python3 scripts/research_package.py --package research/pr4270-outer-exponent-check --check-only
+python3.12 -B research/pr4270-outer-exponent-check/verify.py
+```
+
+It prints `PASS_PR4270_OUTER_EXPONENT_CHAIN` in under a second, using only
+the standard library.
+
+## Open next questions
+
+1. **Bind `τ` and `β` to their sources.**
+   - *Why it matters:* the chain's tightest margins (about `5·10⁻⁸`) sit on
+     these two constants.
+   - *First step:* recompute `τ = 332353/332929` from PR3599's encoded
+     coupling, and `β` from the full-support router's invoice.
+   - *Blocked by:* nothing.
+
+## Credit
+
+The audited chain is #4270's (Ross Richardson with OpenAI Codex assistance).
+The pooled fill is Rohan Arun's (PR #4181). The chain cites, among others,
+Jose Manuel's physical constructions and Tekalign's CRT converter. Prepared
+by Ryanson Jonathan with substantial Claude Code (Claude Opus 5.5)
+assistance. Apache-2.0.

research/pr4270-outer-exponent-check/SOURCES.json

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

research/pr4270-outer-exponent-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 recompute #4270's conservative kappa = 1/580 exponent chain (OUTER-JOIN.md sections 1 and 5) with exact rationals, including a certified enclosure of the pooled moment at its stated root bracket.",
+  "scope_change_reason": "The card asks for independent source-bound coverage of a new paid-profile or ceiling claim; #4270 is the newest such claim above the selected kappa and had only a replay audit.",
+  "bottleneck_link": "#4270 proposes a conditional kappa above the selected record; its exponent chain must hold before its premises are worth reviewing.",
+  "budget_minutes": 30,
+  "stop_rule": "Stop once every link of the written chain is recomputed exactly or a link fails.",
+  "outcome": "completed",
+  "evidence": "verify.py: pooled moment straddles 1 across #4181's 1e-24 root bracket (upper 1 - 7.4e-25 at 1-C); sigma*-(1-C)=9.3e-7; sigma*-tau=4.9e-8; alpha-leaf=4.8e-8; Phi exact, Phi-beta=9.8e-8; other powers below Phi; (1-Phi)-1/580=6.7e-7; 1/580 above selected by 5.1e-5; old Fourier rate control falls short.",
+  "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": "Bind tau and beta to their sources.",
+      "why_it_matters": "The chain's tightest margins (about 5e-8) sit on these two constants.",
+      "first_step": "Recompute tau from PR3599's encoded coupling and beta from the full-support router invoice.",
+      "blocked_by": "None."
+    }
+  ]
+}

research/pr4270-outer-exponent-check/VERIFY.json

@@ -0,0 +1,20 @@
+{
+  "schema_version": 1,
+  "status": "ready",
+  "python": "3.12",
+  "requirements": [],
+  "inputs": [
+    "certificates/selected-result.json"
+  ],
+  "commands": [
+    {
+      "argv": [
+        "{python}",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 120,
+      "checks": "Vendored #4270 OUTER-JOIN.md and #4181 RESULT.json hashes and 13 phrases; certified pooled moment enclosure across the root bracket; every link of the conservative exponent chain; old-rate control."
+    }
+  ]
+}

research/pr4270-outer-exponent-check/vendor/NOTICE.md

@@ -0,0 +1,16 @@
+# Vendored files
+
+These are byte-identical copies from
+[PR #4270](https://github.com/CrocSwap/integer-mult-bounds/pull/4270) at head
+`a929a3fa36301bdfcffe82afd37434dd9e3c4887`.
+
+| Vendored file | Source path in #4270 | Git blob |
+| --- | --- | --- |
+| `OUTER-JOIN.md` | `research/complex-pooled-full-admission/OUTER-JOIN.md` | `50cf3eefd5a4198f011bf378c5d6ddd2319feb0a` |
+| `pr4181-RESULT.json` | `research/complex-pooled-full-admission/frozen/pr4181/RESULT.json` | `5a0ba7aeeb39f849e09ab15cc65afb79028a20e2` |
+
+They are copied, not pinned, because that PR head is not reachable from canonical main.
+`verify.py` checks their SHA256 values before using them.
+
+`OUTER-JOIN.md` was prepared for Ross Richardson with OpenAI Codex assistance. The pooled
+fill result is Rohan Arun's (PR #4181). Both are Apache-2.0, as their packages state.