Independently review #4411's logarithmic majorant: proof holds, arithmetic certified, least ranks slightly below stated, exact L(N) <= F(N) to N = 6000 (no new κ)

research/pr4411-majorant-review/README.md

@@ -0,0 +1,77 @@
+# Independent review of #4411's logarithmic majorant
+
+**Claim type:** a written proof check, certified exact arithmetic and an independent flow
+simulation. **No new κ.** It reviews zxv's
+[#4411](https://github.com/CrocSwap/integer-mult-bounds/pull/4411) at head `ec2c9505`, with README
+SHA256 prefix `3b74b9b2`, as that PR's open question asks. #4411 replaces #4359's power majorant
+with
+
+    L(n) = P_n/B_n ≤ F(n) = n^t (1 + log₂ n)^{1/q},
+
+and specifies ranks `2^465000` (complex) and `2^7100` (BIT) at κ = 0.0023. Those supersede my
+own #4413 ranks, `2^268300549` and `2^14664`. #4411 and #4413 were posted in parallel.
+
+## Proof check
+
+The induction is checked line by line, and it holds.
+
+- **Base, `n < m`.** For `2 ≤ n < m`, `n^{q(1−t)} < m^{q(1−t)} < 2 ≤ 1 + log₂ n`, using (4).
+- **Exit contraction (6).** Since `θ < θ̄` and `n ≥ m`, `log₂ E ≤ log₂ r_max + θ̄(log₂ n − log₂ m)`.
+  Then `1 + log₂ E ≤ θ̄(1 + log₂ n)` is equivalent to `2^{1−θ̄} r_max ≤ m^{θ̄}`, which is (2). So
+  `C(e) ≤ θ̄^{1/q}C(n)`, and (1) gives `Σ x_e F(e) ≤ θ̄^{1/q}C(n)Σ w_s s^t`.
+- **Complements (7).** `C` is increasing, so `F(n−s) ≤ (n−s)^t C(n)`, with `F(0) = 0`. With
+  `1 − (1−y)^t ≥ η y^t` on `(1/m, 1]`, this gives `F(n) − Σ w_s F(n−s) ≥ η C(n) Σ w_s s^t`.
+- **Induction.** Condition (3), `θ̄ < η^q`, makes (6) smaller than (7). Strong induction then
+  gives `L(n) ≤ F(n)` for all `n ≥ 1`, with constant 1.
+- **Final rank test.** `L(N) < N^z` holds iff `1 + H < 2^{q(z−t)H}`.
+
+## Certified arithmetic
+
+| | complex | BIT |
+| --- | --- | --- |
+| `θ < θ̄` | `5^10 < 6^9` | `7^16 < 8^15` |
+| (2) `2^{b−a} r_max^b ≤ m^a` | holds | holds |
+| (3) `η^q − θ̄` | 0.000646856868 (matches #4411) | 0.009533387925 (matches) |
+| (4) `m^{q(1−t)} < 2` | holds | holds |
+| stated / **least** `H`, original savings | 2,352,000 / **2,351,697** | 529,000 / **528,066** |
+| stated / **least** `H`, κ-preserving savings | 465,000 / **464,850** | 7,100 / **7,091** |
+
+Every stated `H` is certified. #4411's values are rounded up from the least `H` that passes the
+same sufficient test; that least value is computed here by bisection with certified logarithms.
+
+## Flow simulation
+
+The separate aggregated lockstep-flow simulator from my #4404 computes exact rational `L(N)` for
+every `N ≤ 6000` in both families. At every rank it checks the source range, the exit bound and
+the exact rank-one potential identity, and that `L(N) ≤ F(N)`. The largest ratio `L(N)/F(N)` is
+0.927 (complex) and 0.843 (BIT), so the majorant holds with room on all simulated ranks.
+
+## Not covered
+
+- #4411's retuned consumer point (`b = 0.0023004`, `a = 0.0023003`) and its 63 + 22 predicates.
+- Native closure, the delayed cover and outer transfer.
+- Ranks above 6000 in the simulation. The proof, not the simulation, covers all `n`.
+
+## Reproduce
+
+```sh
+python3.12 -B scripts/research_package.py --package research/pr4411-majorant-review --check-only
+python3.12 -B scripts/research_package.py --package research/pr4411-majorant-review
+```
+
+The verifier prints `PASS_PR4411_MAJORANT_REVIEW` in about 30 seconds, using only the standard
+library.
+
+## Open next questions
+
+1. **Can the `(1 + log₂ n)^{1/q}` factor be replaced by a smaller slowly varying factor?**
+   - *Why it matters:* the simulated ratio `L/F` is well below 1.
+   - *First step:* fit the simulated `L(N)/N^t` against `log N`.
+
+## Credit
+
+The majorant, ranks and consumer retuning are zxv's (#4411). The compiler is #4359's, and the
+lockstep flow is Jacob Alan Sussman's Theorem 1G (#4268).
+
+Prepared by Ryanson Jonathan with substantial Claude Code (Claude Opus 5.5) assistance.
+Apache-2.0.

research/pr4411-majorant-review/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/pr4411-majorant-review/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 review #4411's logarithmic majorant and explicit ranks: proof check, certified arithmetic, least ranks, exact flow simulation.",
+  "scope_change_reason": "#4411's own open question asks for independent review of the new majorant.",
+  "bottleneck_link": "#4359/#4411's finite uniform templates are specified by these ranks.",
+  "budget_minutes": 30,
+  "stop_rule": "Stop at the majorant and ranks; do not audit the consumer retuning or native premises.",
+  "outcome": "completed",
+  "evidence": "verify.py: conditions (2)-(4) certified, eta^q - theta_bar = 0.000646856868 / 0.009533387925; least certified H 2351697, 464850 (complex) and 528066, 7091 (BIT), each below the stated rounded value; exact L(N) <= F(N) for N <= 6000 with max ratio 0.927 / 0.843.",
+  "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": "Can the (1+log2 n)^(1/q) factor be replaced by a smaller slowly varying factor?",
+      "why_it_matters": "The simulated L/F ratio is well below 1.",
+      "first_step": "Fit simulated L(N)/N^t against log N.",
+      "blocked_by": "None."
+    }
+  ]
+}

research/pr4411-majorant-review/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": "Embedded invoices; certified theta<theta_bar, conditions (2)-(4), eta^q - theta_bar matching #4411; stated and least certified H for four configurations; exact lockstep-flow L(N) <= F(N) for N <= 6000 with source range, exit bound and potential identity."
+    }
+  ]
+}