Independently certify #4483's finite gates (p16 2^2800000000, all four witnesses) and its arbitrary-height flow identities (no new κ)

research/rank-convergence-gates/README.md

@@ -0,0 +1,80 @@
+# Independent certified check of #4483's finite gates and arbitrary-height flow
+
+**Claim type:** an independent certified recomputation by separately written code. **No new κ.** It covers
+zxv's [#4483](https://github.com/CrocSwap/integer-mult-bounds/pull/4483) (`research/rank-convergence`). That
+PR changes the direct flow's stopping height and closes the recursion with a shifted-logarithmic majorant,
+reporting the p16 sufficient rank `2^2800000000` instead of `2^558100005581` at κ = 0.00302015. It is a
+compiler follow-up in the maintainers' #4470 review plan, and it answers the obstruction my
+#4459/#4465/#4467 described.
+
+## What is checked, for all four witnesses in `BENCHMARKS.json`
+
+Each raw profile is read from its pinned source. Everything uses certified interval logarithms and
+exponentials (the helpers of my #4455), with exact rational powers for `U^{ℓ₀}` and `V^{ℓ₀}`.
+
+- **The guards (18) on `[t₀, t_hi]`:**
+  - `T_{t₀} > P_{t₀}`;
+  - `d ≤ μ_T(t₀) − μ_P(t_hi)`, where the μ are tilted log means;
+  - the bounds `Q`, `U` and `V`;
+  - the ratio ordering `T_{t₀+s}/T_{t₀} ≥ P_{t_hi+s}/P_{t_hi}`;
+  - `η_min ≤ t₀m^{t₀−1}` and `c ≥ p/(1−t₀)`;
+  - `τ(n₀) ≤ t_hi`.
+- **The mirror guard (4)** on every elementary window, for each of the 20 t-slices, in the sufficient form
+  `E_J(t_b) ≤ β·S_J(t_a)`.
+- **The recurrence inequality (20)** and the **final funding (17)** at `N = 2^H`.
+
+| witness | D (lower) | required | worst mirror ratio | τ(n₀) ≤ t_hi | final margin (lower) |
+| --- | ---: | ---: | ---: | --- | ---: |
+| p7 | 0.02858992 | 0.02336096 | 0.32091 | 0.9974809363 ≤ .997481 | 0.00003773 |
+| native4453 | 0.05448611 | 0.04422604 | 0.57408 | 0.9971361473 ≤ .9971362 | 1.19575350 |
+| native4453, matched uniform | 0.05448611 | 0.04422604 | 0.57408 | same | 0.32116914 |
+| **p16** | **0.04854643** | **0.04306220** | 0.56287 | 0.9970659832 ≤ .997066 | **0.60862507** |
+
+All match #4483's stated values. Two margins are thin but certified positive:
+
+- p7's final margin of about 3.8·10⁻⁵;
+- the `τ(n₀)` covers, with slack of about 2·10⁻⁸ to 7·10⁻⁸.
+
+PROOF.md's rejection control, `t_hi = .9974808` for p7, is rejected.
+
+## Arbitrary-height flow (#4483's open question 1)
+
+On raw p7 at `N = 500, 3000, 20000`, my independent #4436 flow is run with a forced height `G`, at every
+`G = 0, …, G₀ + 2`. That range includes heights above the old minimum-target height, where root classes
+are empty. Over these 13 cases:
+
+- the exact rank-one identity `Σ S·s − Σ X·e = 608·col` holds;
+- every exit stays below `n`;
+- the exact mirror identity of #4459 holds.
+
+So PROOF.md §1–2's flow identities do not depend on the old height.
+
+## Not covered
+
+- PROOF.md's theorem itself, including the Chernoff and majorant arguments. Only its finite gates are
+  recomputed here.
+- The native suppliers and the outer consumer points.
+- The stopping heights actually used inside the certificates, beyond `τ(n₀)`.
+
+## Reproduce
+
+```sh
+python3.12 -B scripts/research_package.py --package research/rank-convergence-gates --check-only
+python3.12 -B scripts/research_package.py --package research/rank-convergence-gates
+```
+
+The verifier prints `PASS_RANK_CONVERGENCE_GATES` in about 7 minutes, using only the standard library.
+
+## Open next questions
+
+1. **Can p7's 3.8·10⁻⁵ final margin be widened by a small change of `(t₀, c, ℓ₀)`?**
+   - *Why it matters:* it gives a more robust p7 witness.
+   - *First step:* scan `ℓ₀` and `c` with this certified checker, holding the consumer saving fixed.
+
+## Credit
+
+- The theorem, the witnesses and the adaptive height are zxv's (#4483).
+- The flow is from #4436. The mirror identity is from my #4459.
+
+Prepared by Ryanson Jonathan with substantial Claude Code (Claude Opus 5.5) assistance.
+Apache-2.0.

research/rank-convergence-gates/SOURCES.json

@@ -0,0 +1,48 @@
+{
+  "schema_version": 1,
+  "base_commit": "f9f85c1e4fa1e955ff39f10fca447e3e2a4e4adc",
+  "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"
+    },
+    {
+      "path": "research/compact-joint-compiler/arithmetic/RESULT.json",
+      "usage": "input",
+      "git_blob": "514d12ce4d2d824a4e0a418022bba610c8aed8ff",
+      "sha256": "a6caaa2a6d6460a8c1ef7e48c4853bb27976be33a52b96a4216dfa90d96c9091"
+    },
+    {
+      "path": "research/higher-moment-strictification/RESULT.json",
+      "usage": "input",
+      "git_blob": "e66b39c674028adfd22f0de3170555dccda52f6a",
+      "sha256": "ad79e3c0459e7b495a0ca34010553b12147779a007389e1695cc1336f123c156"
+    },
+    {
+      "path": "research/native-lattice-retiming/RESULT.json",
+      "usage": "input",
+      "git_blob": "93defc5ececebd542332fc42d6a78f0af222cd1c",
+      "sha256": "1ac2e581ea51e6448503a68caf4bf44aeb32470c2e2674c91f007af4a3abd2e3"
+    },
+    {
+      "path": "research/rank-convergence/BENCHMARKS.json",
+      "usage": "input",
+      "git_blob": "bc58c96abda014c28de91eca3ff10a7d4ec30b32",
+      "sha256": "513efe2fe74af82891c1918e462ba8338b1bbd06403cbfcec284bcf3b4f8f850"
+    },
+    {
+      "path": "research/rank-convergence/PROOF.md",
+      "usage": "input",
+      "git_blob": "75f451837204bd141f357e7f5e5d6c6f42e1423e",
+      "sha256": "3c971c5670669cb36312815b111e64c83e1490a10ee82f5412bd9aee01e9c376"
+    }
+  ]
+}

research/rank-convergence-gates/TASK.json

@@ -0,0 +1,100 @@
+{
+  "schema_version": 1,
+  "task_id": "independent-moment",
+  "priority_revision": 7,
+  "base_commit": "f9f85c1e4fa1e955ff39f10fca447e3e2a4e4adc",
+  "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": "Independent certified check of #4483's finite gates and arbitrary-height flow identities.",
+  "scope_change_reason": "Compiler follow-up named in the maintainers' #4470 review plan.",
+  "bottleneck_link": "Independent coverage of the compiler that removes tensor padding from the kappa 0.00302015 construction.",
+  "budget_minutes": 60,
+  "stop_rule": "Stop at the finite gates and flow identities.",
+  "outcome": "completed",
+  "evidence": "All four witnesses pass; p16 D >= 0.04854643 vs required 0.04306220, final margin >= 0.60862507; p7 margin 3.77e-5 certified; tau covers certified; rejection control rejects; arbitrary-height identities hold at 13 (N,G) pairs.",
+  "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 p7's 3.8e-5 final margin be widened?",
+      "why_it_matters": "More robust p7 witness.",
+      "first_step": "Scan ell0 and c with this checker at fixed consumer saving.",
+      "blocked_by": "None."
+    }
+  ]
+}

research/rank-convergence-gates/VERIFY.json

@@ -0,0 +1,24 @@
+{
+  "schema_version": 1,
+  "status": "ready",
+  "python": "3.12",
+  "requirements": [],
+  "inputs": [
+    "research/compact-joint-compiler/arithmetic/RESULT.json",
+    "research/higher-moment-strictification/RESULT.json",
+    "research/native-lattice-retiming/RESULT.json",
+    "research/rank-convergence/BENCHMARKS.json",
+    "research/rank-convergence/PROOF.md"
+  ],
+  "commands": [
+    {
+      "argv": [
+        "{python}",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 600,
+      "checks": "Certified recomputation of #4483's guards (18), mirror guard (4) over t-slices, recurrence inequality (20) and final funding (17) for all four witnesses; p7 rejection control; arbitrary-height flow identities (rank-one identity, exits < n, mirror identity) on raw p7 for G = 0..G0+2."
+    }
+  ]
+}