Small-prime check of #4612's outer-reserve threshold: displayed H fails at p=2 for moderate C; corrected H' = max(H, 4096 C log2(4096 C)) (no κ change)

research/pr4612-small-prime-threshold/README.md

@@ -0,0 +1,58 @@
+# Small-prime check of #4612's outer-reserve threshold
+
+**Task:** independent-moment (scoped correction). **Base:** canonical main `f626db5c`. **No κ or exponent change.**
+
+## The claim
+
+Matarener's #4612 (head `7e362114`) audits #4359's BIT row stock. Its "Threshold" paragraph and `outer_reserve()` check concern the bound q0(h, p) ≤ C(log₂h + h^δL³ + 1), with L = log₂p and δ ∈ {0.003, 0.004}. They state that the displayed threshold
+
+```text
+H(p) = [1024 C L³]^(1/(1−δ))
+```
+
+"already suffices" **for every C ≥ 1**, and that "C(log₂h + 2) ≤ h/1024 there as well". From this, #4612 concludes q0 + O(1) ≤ h/64 and R(h) ≤ 3h/128 + q0 ≤ h/16. Its finite grid uses only L ∈ {8, 64, 1024, 2²⁰, 2⁴⁰}, that is, p ≥ 256.
+
+## Findings
+
+These are scoped, wording-level findings.
+
+- **The intermediate claim fails at p = 2.** At L = 1, C(log₂h + 2) ≤ h/1024 fails at h = H for every tested C, from 1 to 2¹⁰⁰⁰.
+- **q0 ≤ h/64 fails at p = 2 for #4612's own constant.** With the width constant C = 232,960, the q0 bound is about 0.0276·h > h/64 at h = H(2).
+- **The conclusion R ≤ h/16 can fail at p = 2.** For C = 2⁴⁰, 2¹⁰⁰ and 2¹⁰⁰⁰, R(h) ≤ h/16 fails at h = H(2) for both atoms. Only when log₂C is so large that the factor (1024C)^(δ/(1−δ)) dominates (2¹⁰⁰⁰⁰, say) is the displayed threshold enough again.
+- **Why #4612's grid missed this.** The grid uses L ≥ 8, and the verifier confirms that every point in it passes.
+
+## Correction
+
+```text
+H′(p) = max( [1024 C L³]^(1/(1−δ)),  4096 C log₂(4096 C) ).
+```
+
+**Proof.**
+
+1. Put a = 1024C ≥ 1024. At h = 4a log₂(4a), we have a(log₂h + 2) ≤ h, because log₂log₂(4a) + 2 ≤ 3 log₂(4a).
+2. h − a log₂h is increasing for h > a/ln 2, so the inequality persists above that point.
+3. Above H we also have C h^δ L³ ≤ h/1024.
+4. Hence q0 ≤ h/512 ≤ h/64 and R ≤ h/16. ∎
+
+The added term does not depend on p, so the threshold remains polylogarithmic in p. #4612's conclusions survive with H′. Only the claims "no extra multiple is needed" and "for every C ≥ 1" need the amendment.
+
+The verifier checks the corrected threshold on a grid that includes L = 1 and the small primes 3, 5 and 7, with log₂C from 0 to 10,000.
+
+## Verify
+
+```text
+python3 -B research/pr4612-small-prime-threshold/verify.py
+```
+
+The check runs in under 1 s and uses the standard library only. It uses log-domain floats, with margins of at least 10⁻³ in log₂ units at every failure.
+
+## Limitations
+
+- **C is unbound.** The actual constant C is still unknown; binding it is #4612's open question 1. With the illustrative log₂C ≈ 2 log₂N + 64 ≈ 1.3·10¹⁰, the displayed H already suffices, because the δ-factor is enormous.
+- **No other checks redone.** This package does not re-check #4612's other statements.
+
+## Open next questions
+
+- **Bind C to the #4470 template.** Then state the exact threshold. First step: see #4612's open question 1.
+
+Credit: Matarener (Mark) for #4612, and zxv, Cinna Davis and the #4359/#4470 lineage. Prepared by Ryanson Jonathan with substantial Claude Code (Claude Opus 5.5) assistance.

research/pr4612-small-prime-threshold/SOURCES.json

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

research/pr4612-small-prime-threshold/TASK.json

@@ -0,0 +1,100 @@
+{
+  "schema_version": 1,
+  "task_id": "independent-moment",
+  "priority_revision": 7,
+  "base_commit": "f626db5c3a3d781d8f7695038776c621651f75e1",
+  "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": "unchanged",
+  "actual_scope": "Does a new paid-profile or mixture-ceiling claim have independent source-bound coverage of its actual changed ledger?",
+  "scope_change_reason": null,
+  "bottleneck_link": "Correctness of the outer-reserve threshold statement in the newest stock audit (#4612).",
+  "budget_minutes": 30,
+  "stop_rule": "Stop at the small-prime counterexamples and corrected threshold.",
+  "outcome": "completed",
+  "evidence": "At p=2 the displayed H fails C(log2 h+2)<=h/1024 for all tested C; with C=232960 q0>h/64 at H(2); for C=2^40,2^100,2^1000 R<=h/16 fails at H(2); #4612's L>=8 grid passes; corrected H'=max(H,4096 C log2(4096 C)) proved and grid-checked including small primes.",
+  "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": "Bind C to the #4470 template.",
+      "why_it_matters": "Exact threshold.",
+      "first_step": "#4612 open question 1.",
+      "blocked_by": "None."
+    }
+  ]
+}

research/pr4612-small-prime-threshold/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": "Small-prime failures of the displayed threshold; #4612 grid passes; corrected threshold grid incl. small primes; lemma."
+    }
+  ]
+}

research/pr4612-small-prime-threshold/verify.py

@@ -0,0 +1,82 @@
+#!/usr/bin/env python3
+"""Small-prime check of PR #4612's outer-reserve threshold (Matarener, head 7e362114).
+
+#4612 states (README, "Threshold"; verify.py outer_reserve) that for q0(h,p) <= C(log2 h + h^d L^3 + 1), L = log2 p,
+d in {0.003, 0.004}, the displayed threshold H(p) = [1024 C L^3]^(1/(1-d)) "already suffices" for every C >= 1:
+"C(log2 h + 2) <= h/1024 there as well", hence q0 + O(1) <= h/64 and R(h) <= 3h/128 + q0 <= h/16. Its grid uses
+L in {8, 64, 1024, 2^20, 2^40} only (p >= 256).
+
+Findings (log-domain float arithmetic with explicit margins >= 1e-3 in log2 units; scoped, no kappa change):
+  * at p = 2 (L = 1) the intermediate claim C(log2 h + 2) <= h/1024 fails at h = H for every tested C (1 .. 2^1000);
+  * with #4612's own width constant C = 232960, q0's bound exceeds h/64 at h = H(2) (q0/h ~ 0.0276 > 0.0156);
+  * for C = 2^40, 2^100 and 2^1000 the conclusion R(h) <= h/16 itself fails at h = H(2) for both atoms
+    (it is rescued only when log2 C is so large that the factor (1024 C)^(d/(1-d)) dominates, e.g. 2^10000);
+  * correction: H'(p) = max(H(p), 4096 C log2(4096 C)). With a = 1024 C >= 1024 and h >= 4a log2(4a):
+    a(log2 h + 2) <= h at h = 4a log2(4a) because log2 log2(4a) + 2 <= 3 log2(4a), and h - a log2 h increases for
+    h > a/ln 2. Above H also C h^d L^3 <= h/1024. Hence q0 <= h/512 <= h/64 and R <= h/16; the threshold stays
+    polylogarithmic in p (the new term does not depend on p). Checked on a grid that includes L = 1 and small primes.
+The constant C itself remains unbound (#4612's open question 1); the conclusion R <= h/16 survives with H'.
+Ryanson Jonathan with Claude Code (Claude Opus 5.5) assistance. Apache-2.0.
+"""
+import json
+import math
+import sys
+
+DELTAS = (0.003, 0.004)
+
+
+def need(condition, message):
+    if not condition:
+        raise AssertionError(message)
+
+
+def log2_threshold(log_c, l, d):
+    return (10 + log_c + 3 * math.log2(l)) / (1 - d)
+
+
+def ratios(log_c, l, d, lh):
+    """(log2 of C(log2 h + 2) / h, q0_bound / h) at log2 h = lh."""
+    inter = log_c + math.log2(lh + 2) - lh
+    q0 = 2 ** (log_c - lh) * (lh + 1) + 2 ** (log_c + d * lh + 3 * math.log2(l) - lh)
+    return inter, q0
+
+
+def main():
+    out = {"intermediate_fails_at_p2": [], "h64_fails": [], "R_fails": []}
+    for d in DELTAS:
+        for log_c in (0, math.log2(232960), 40, 100, 1000):
+            inter, q0 = ratios(log_c, 1, d, log2_threshold(log_c, 1, d))
+            need(inter > -10 + 1e-3, "C(log2 h + 2) > h/1024 at h = H(2)")
+            out["intermediate_fails_at_p2"].append([d, round(log_c, 3)])
+            if q0 > 1 / 64:
+                out["h64_fails"].append([d, round(log_c, 3), round(q0, 5)])
+            if q0 > 5 / 128:
+                out["R_fails"].append([d, round(log_c, 3), round(q0, 5)])
+        _, q_big = ratios(10000, 1, d, log2_threshold(10000, 1, d))
+        need(q_big <= 5 / 128, "very large C is rescued by the (1024 C)^(d/(1-d)) factor")
+    need(any(abs(c - math.log2(232960)) < 1e-2 for _, c, _ in out["h64_fails"]), "C = 232960: q0 > h/64 at H(2)")
+    need({c for _, c, _ in out["R_fails"]} == {40, 100, 1000}, "R <= h/16 fails at H(2) for C = 2^40, 2^100, 2^1000")
+    # #4612's own grid (L >= 8) does pass, which is why it did not see the failure
+    for d in DELTAS:
+        for log_c in (0, 20, 1000):
+            for l in (8, 64, 1024):
+                lh = log2_threshold(log_c, l, d)
+                need(ratios(log_c, l, d, lh)[1] <= 1 / 64, "#4612 grid passes")
+    # corrected threshold H' = max(H, 4096 C log2(4096 C)): q0 <= h/512 on a grid including small primes
+    for d in DELTAS:
+        for log_c in (0, 5, math.log2(232960), 40, 100, 1000, 10000):
+            for l in (1, math.log2(3), math.log2(5), math.log2(7), 8, 64, 1024, 2 ** 20):
+                lh0 = max(log2_threshold(log_c, l, d), 12 + log_c + math.log2(12 + log_c))
+                for s in (0, 0.5, 1, 10, 100, 1e4):
+                    inter, q0 = ratios(log_c, l, d, lh0 + s)
+                    need(inter <= -10 + 1e-9 and q0 <= 1 / 512 + 1e-12, "corrected threshold suffices")
+    need(all(math.log2(math.log2(4 * a)) + 2 <= 3 * math.log2(4 * a) for a in (1024, 2 ** 20, 2 ** 100)),
+         "lemma: log2 log2(4a) + 2 <= 3 log2(4a) for a >= 1024")
+    print(json.dumps({"status": "PASS_PR4612_SMALL_PRIME_THRESHOLD_CHECK", **out,
+                      "corrected_threshold": "H'(p) = max([1024 C L^3]^(1/(1-d)), 4096 C log2(4096 C))",
+                      "conclusion_R_le_h_over_16_with_corrected_threshold": True, "new_kappa_claimed": False},
+                     indent=1))
+
+
+if __name__ == "__main__":
+    sys.exit(main())