research: #4436 boundary exits — exact mirror identity, rigorous share bound 0.321, and a correction (leaf exits dominate)

research/direct-flow-boundary-share/README.md

@@ -0,0 +1,98 @@
+# #4436's boundary exits: a mirror identity, a rigorous share bound, and a correction
+
+**Claim type:** an exact identity and a rigorous uniform bound for #4436's boundary exits, plus a
+**correction** to this package's first version and finite measurements of the true exit coefficient.
+**No new κ.** It concerns zxv's [#4436](https://github.com/CrocSwap/integer-mult-bounds/pull/4436)
+open direct-exponent gate.
+
+## Correction to the first version
+
+The first version (head `04da76eb`) claimed that the gate reduces to a uniform boundary-exit share
+bound. That claim is **wrong**.
+
+- **The flaw.** Its lemma assumed leaf exits have rank `E(n) = o(n)`, so that their term
+  `(mE/n)^δ` vanishes. In #4436's direct flow this is false. Leaf exits `rρ` with `ρ ∈ F[G]` reach
+  **0.397·N**, and they carry **85–92 %** of the source `t`-potential at every scanned rank.
+- **What stands.** The lemma is still valid as a conditional statement, but its leaf hypothesis
+  fails here.
+- **What controls the gate.** The total exit coefficient, measured below.
+
+## Mirror identity (exact)
+
+Use #4436's lockstep nodes. A *base* is a pair `(ρ, a)` with `ρ ∈ F[d]`, `|a| = G−d−1` and
+`0 ≤ d < G`, of weight `μ = cnt(ρ)·u(a)` and size `z = ρ·c(a)`. Write `I(x) = m z/N ∈ x` for the
+window condition. Then:
+
+    boundary exits = Σ_{r>k} P_r W_k · [base (ρ,a) with I(1/r, 1/k]] at rank r k z,
+    sources        = Σ_{k>r} P_r W_k · [base (ρ,a) with I(1/k, 1/r]] at rank r k z  +  top layer.
+
+An exit occurs where node `(ρ, a+e_k)` is present but `(ρr, a)` is absent. A source occurs where
+`(ρr, a)` is present but `(ρ, a+e_k)` is absent. So exits and inner sources are the same base measure
+seen through mirrored windows. `verify.py` checks both equalities exactly, as multisets, at
+`N = 1089, 3000, 20000` and `100000`.
+
+## Rigorous uniform bound on the boundary share
+
+Let `M(J) = Σ_{bases in J} μ z^t`. Split the windows into elementary intervals `J` cut at the
+points `1/r` and `1/k`. Then exits `= Σ_J E_J M(J)` and inner sources `= Σ_J S_J M(J)`, where
+`E_J` and `S_J` sum `P_r W_k (rk)^t` over the exit and source windows covering `J`. Every exit window
+lies inside `(1/48, 1/5]`, and each of its pieces is covered by source windows. Hence, for every `N`:
+
+    β(N) ≤ max_J E_J / S_J = 0.3208   (raw p7, t = 1 − 0.0026865).
+
+The measured maximum is 0.1545. Even the crude cover bound, which compares all exits against the
+source pairs `r ≤ 5`, `k ≥ 57` only, gives 0.753. So hypothesis (C) of the first version is now a
+theorem. It is no longer the bottleneck.
+
+## The exit coefficient, measured
+
+This is the quantity #4405's refined induction actually needs:
+
+    κ(N, z0) = Σ x_e e^{z0} / Σ w_s s^{z0},     with κ ≤ η = z0·m^{z0−1} required.
+
+At `t` the exit and source potentials balance (κ = 1.000000), and κ falls only slowly as `z0` rises.
+
+| saving `1−z0` | η | sup κ, N ≥ 10³ | N ≥ 10⁴ | N ≥ 10⁵ | N ≥ 3·10⁵ |
+| --- | --- | --- | --- | --- | --- |
+| 0.002 | 0.98847 | 0.99864 | 0.99826 | 0.99807 | 0.99798 |
+| 0.001 | 0.99422 | 0.99667 | 0.99573 | 0.99526 | 0.99504 |
+| 0.0008 | 0.99537 | 0.99628 | 0.99523 | 0.99470 | **0.99445** |
+
+Through `N ≤ 5·10⁵`, the refined-induction test with the direct flow passes at saving 0.0008 for
+`N ≥ 3·10⁵`, and fails at 0.001. That agrees with the effective saving of about 0.0008 that #4456
+measured near `N = 3·10⁴`. The slow downward drift of sup κ is finite evidence only.
+
+## Not covered
+
+- Any asymptotic statement about κ(N, z0).
+- An explicit-rank endpoint.
+- Native premises.
+
+## Reproduce
+
+```sh
+python3.12 -B scripts/research_package.py --package research/direct-flow-boundary-share --check-only
+python3.12 -B scripts/research_package.py --package research/direct-flow-boundary-share
+```
+
+The verifier prints `PASS_DIRECT_FLOW_BOUNDARY_SHARE` in about 35 seconds, using only the standard
+library.
+
+## Open next questions
+
+1. **Do the leaf exits admit a mirror-type comparison with the sources?**
+   - *Why it matters:* leaf exits are about 90 % of the exit potential, so they decide κ.
+   - *First step:* write leaf exits `rρ` (`ρ ∈ F[G]`) and last-layer sources over a common base, as
+     above.
+2. **Does sup κ(N, z0) converge, and to what?**
+   - *Why it matters:* it decides the direct saving.
+   - *First step:* a renewal-type analysis of the tilted base measure near `log(N/m)`.
+
+## Credit
+
+- The direct flow and the gate are zxv's (#4436).
+- The refined induction is 1337isnot1337's (#4405).
+- The lockstep construction is Jacob Alan Sussman's Theorem 1G.
+
+Prepared by Ryanson Jonathan with substantial Claude Code (Claude Opus 5.5) assistance.
+Apache-2.0.

research/direct-flow-boundary-share/SOURCES.json

@@ -0,0 +1,18 @@
+{
+  "schema_version": 1,
+  "base_commit": "2a13eb1827784206202db90e5dc8327cf8a250db",
+  "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/direct-flow-boundary-share/TASK.json

@@ -0,0 +1,100 @@
+{
+  "schema_version": 1,
+  "task_id": "independent-moment",
+  "priority_revision": 7,
+  "base_commit": "2a13eb1827784206202db90e5dc8327cf8a250db",
+  "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": "#4436's boundary exits: exact mirror identity, rigorous uniform share bound 0.3208, and a correction (leaf exits dominate) with the measured exit coefficient vs eta.",
+  "scope_change_reason": "Follow-up to #4456; #4436 left the direct exponent gate open.",
+  "bottleneck_link": "A direct-flow exponent would remove the tensor/padding step behind the kappa ~0.0027-0.0030 claims.",
+  "budget_minutes": 30,
+  "stop_rule": "Stop at the conditional lemma and measurements.",
+  "outcome": "completed",
+  "evidence": "Mirror identity exact at 4 ranks; beta <= 0.3208 for all N (measured max 0.1545). Correction: leaf exits reach 0.397N with 85-92% of the t-potential, so the first version's reduction fails. Refined-induction test passes at saving 0.0008 and fails at 0.001 through N<=5e5.",
+  "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": "Do leaf exits admit a mirror-type comparison with sources?",
+      "why_it_matters": "They carry ~90% of the exit potential and decide kappa.",
+      "first_step": "Write leaf exits and last-layer sources over a common base.",
+      "blocked_by": "None."
+    }
+  ]
+}

research/direct-flow-boundary-share/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": "Independent #4436 direct flow on raw p7 at 3,394 ranks: exit rank bound, exact potential identity, exact mirror identity (boundary exits/sources as mirrored windows of one base measure) at 4 ranks, boundary share below the rigorous mirror bound 0.3208, leaf exits dominate (correction), exit coefficient vs eta table."
+    }
+  ]
+}