diff --git a/research/adaptive-tail-entropy/PROOF.md b/research/adaptive-tail-entropy/PROOF.md
new file mode 100644
index 0000000000..c9b0e7cb83
--- /dev/null
+++ b/research/adaptive-tail-entropy/PROOF.md
@@ -0,0 +1,186 @@
+# A sharp range-and-mean screen for the two tail gates
+
+## Contract and cited premise
+
+Let finite nonempty target and paid histograms have positive coefficients,
+with target ranks `2<=k<=m` and paid ranks `1<=r<m`. Fix `0<t<1` and set
+
+```text
+T(t)=sum W_k k^t,       P(t)=sum P_r r^t,
+q=T(t)/P(t)>=1,
+mu_T=T'(t)/T(t),        mu_P=P'(t)/P(t).
+```
+
+The analytic bounds below also hold for positive real histogram weights.
+Gate implications apply to histograms covered by the cited contract.
+
+We use Dillon Amburgey's #4532, PROOF.md section 3, as a cited premise.
+The following three gates admit positive integers a,b, an integer M>1
+and positive rational s,lambda if and only if some real lambda>0 has
+`F(lambda)<1`:
+
+```text
+u=M^(-s) [T(t+s)/T(t)]^a [P(t+s)/P(t)]^b <1,
+v=M^lambda [T(t-lambda)/P(t)]^(a+b) <1,
+T(t+s)/T(t) >= P(t+s)/P(t),
+F(lambda)=T(t-lambda) exp(lambda mu_P)/P(t).
+```
+
+The source proves the integer-height and rational-parameter existence
+implication. It is not an audit target here. This note computes a new
+explicit screen for F and its equality case. Mirror capacity, recurrence
+funding and native implementation are outside that equivalence.
+
+## The theorem
+
+Give `X=log k` probability `W_k k^t/T(t)`. Write
+
+```text
+A=min log k, B=max log k, R=B-A,
+Z=(X-A)/R,   p=E[Z]=(mu_T-A)/R,   x=(mu_P-A)/R.
+```
+
+First suppose the target has at least two distinct ranks. Then R>0,
+`0<p<1`, and `F(lambda)=q E exp[-lambda R(Z-x)]`.
+
+1. If `mu_P<A`, the gates are feasible.
+2. If `mu_P=A`, they are feasible exactly when
+   `W_kmin kmin^t < P(t)`.
+3. If `A<mu_P<mu_T`, define
+   `D(x||p)=x log(x/p)+(1-x)log((1-x)/(1-p))`.
+   If `log q<D(x||p)`, the gates are feasible. They are also feasible at
+   equality if any target rank lies strictly between the two extremes.
+   For targets supported on the two extremes only, the exact condition is
+   `log q<D(x||p)`. Equality fails.
+4. If `mu_P>=mu_T`, the gates are infeasible.
+
+For a one-rank target `k0`, feasibility is exactly `mu_P<log k0`.
+No upper bound on q is needed in that case, except the assumed q>=1.
+
+The interior-regime sufficient bound is sharp among positive finite laws
+with the same range and target mean: the two-endpoint law attains its
+bound, so above or at that threshold these statistics alone cannot
+guarantee feasibility. At equality, knowing that interior mass exists
+does supply additional information. For integer histograms, this sharpness
+assertion applies whenever the corresponding endpoint statistics can be
+realized. The integer boundary example below provides one such realization.
+
+## Proof
+
+If `mu_P<A`, then
+`F(lambda)<=q exp[-lambda(A-mu_P)]`, which tends to zero. If `mu_P=A`,
+F decreases strictly to `q Pr(X=A)`, and every finite value is larger than
+that limit. This proves cases 1 and 2.
+
+For `0<x<p`, put h=lambda R. Strict convexity on `[0,1]` gives
+
+```text
+exp[-h(z-x)] <= (1-z) exp(hx)+z exp[-h(1-x)].
+```
+
+For h>0 equality holds exactly at z=0 or z=1. Taking expectations gives
+
+```text
+F(lambda) <= q [(1-p) exp(hx)+p exp(-h(1-x))].       (1)
+```
+
+Differentiate the bracket. Its unique minimizing positive h is
+
+```text
+h*=log[p(1-x)/(x(1-p))]>0.
+```
+
+Substitution gives the minimum
+
+```text
+(p/x)^x ((1-p)/(1-x))^(1-x) = exp[-D(x||p)].         (2)
+```
+
+If `q exp(-D)<1`, (1) evaluated at h* supplies a strict passing point.
+If this product equals one and some interior rank has positive mass,
+strict convexity makes (1) strict at that same point. The source's premise
+then supplies integer height and rational tail parameters. There is no
+claim that h*/R is rational; the passing inequality is open.
+
+For a two-endpoint law, (1) is an equality for every h, and (2) is its
+actual minimum. Thus strict inequality is necessary and sufficient.
+This also proves the stated sharpness from range and mean alone.
+
+Finally Jensen's inequality gives
+`F(lambda)>=q exp[lambda(mu_P-mu_T)]>=1` if `mu_P>=mu_T`.
+For a single target rank the exact expression is
+`F(lambda)=q exp[lambda(mu_P-log k0)]`, proving the final case.
+
+These arguments address real lambda. The cited equivalence supplies the
+required rational and integer compiler parameters wherever a strict
+passing point exists. QED.
+
+## Exact new histogram boundary
+
+Take `W_4=1, W_256=32, P_16=c` and t=1/2. For integers `1<=c<=128`,
+q=514/(4c)>=1. The normalized log ranks are 0 and 1 with p=512/514,
+and `x=(log16-log4)/(log256-log4)=1/3<p`.
+
+Writing `y=4^lambda>1`, the unnormalized scalar criterion is
+
+```text
+T(t-lambda) exp(lambda mu_P) = 2y+512/y^2.
+```
+
+Its derivative vanishes exactly at y=8; it decreases below 8 and
+increases above 8. The exact minimum is 24, at lambda=3/2.
+Equivalently the entropy calculation gives
+`q exp[-D(1/3||256/257)]=6/c`.
+The strict gate condition is therefore c>6, proving the claimed integer
+transition. All c<=6 fail, including the equality case c=6.
+
+For c=7 choose a=1,b=31,M=2^132,s=1/2,lambda=3/2. Since
+
+```text
+T(1)/T(1/2)=(4+32*256)/514=4098/257,
+P(1)/P(1/2)=16/4=4,
+T(-1)=1/4+32/256=3/8,
+```
+
+direct substitution in the original gates gives
+
+```text
+u=2^-66 (4098/257) 4^31=2049/2056<1,
+v=2^198 (3/224)^32=64*(6/7)^32<1.
+```
+
+The latter strict inequality is the exact integer inequality
+`64*6^32<7^32`, checked by the verifier. The forward ratio also strictly
+exceeds 4. This is a literal gate witness, not just a scalar sufficient test.
+
+For c=7 and every nonnegative exponent z, `32*256^z>7*16^z`.
+Thus T(z)>P(z), so this passing fixture has no nonnegative moment
+crossing. This observation does not imply full recurrence funding.
+
+## Mirror failure and claim correction
+
+The only exit window is `(1/16,1/4]`, supplied by the pair (16,4),
+with coefficient `8c`. The only inner-source window is `(1/256,1/16]`,
+from (16,256), with coefficient `2048c`. They are disjoint. On the
+exit window the source coefficient is zero, so no finite mirror factor
+covers it. The coefficient ratio 1/256 does not establish coverage.
+
+The advance CLAIM predicted mirror slack for this fixture. That
+prediction was wrong and was explicitly corrected in the permitted
+[progress update](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19147154).
+The delivered claim is tail/ordering feasibility only. The entropy theorem
+does not assume mirror coverage. No full compiler admission was obtained.
+
+## Scope and credit
+
+Native realizability, full mirror/recurrence funding, chronological
+batching, ownership/restoration, adapters, precision/tape costs, stock,
+analytic transfer and exact recovery remain open. No selected frontier
+or frozen predecessor is changed.
+
+The exact scalar equivalence is Dillon Amburgey's #4532 contribution.
+The compiler/gate lineage is zxv #4436/#4483, Jacob Alan Sussman and
+Ryanson Jonathan #4459, together with the native and outer contributors
+credited there. The entropy optimization is a classical method. The
+new scoped screen, strict boundary application and exact histogram
+transition were produced by Nick Petalas. Apache-2.0.
diff --git a/research/adaptive-tail-entropy/README.md b/research/adaptive-tail-entropy/README.md
new file mode 100644
index 0000000000..d56fce7e2b
--- /dev/null
+++ b/research/adaptive-tail-entropy/README.md
@@ -0,0 +1,130 @@
+# Sharp entropy threshold for adaptive compiler tail gates
+
+For two target ranks, the adaptive compiler's two-tail feasibility question
+has a closed form. For arbitrary finite target profiles, the same expression
+gives a sharp sufficient test from the rank range and tilted mean.
+This is a scoped written proof with exact finite corroboration. It does not
+give a native word, supplier admission, a multiplication theorem or a new κ.
+
+Let `q=T(t)/P(t)>=1`. Normalize target log ranks to `[0,1]`, with target
+tilted mean `p` and paid tilted mean `x`. When `0<x<p<1`, put
+
+```text
+D(x||p) = x log(x/p) + (1-x) log((1-x)/(1-p)).
+```
+
+The condition `log q < D(x||p)` guarantees both tail gates and their ordering
+guard. For a two-rank target it is necessary as well. At equality, a profile
+with a target rank strictly between its extremes still passes, whereas a
+two-rank target fails. The boundary cases, proof and exact hypotheses are in
+[PROOF.md](PROOF.md). The underlying exponential convexity and binary entropy
+calculation are classical. The contribution is their sharp application to
+this compiler gate contract, including its strict equality boundary.
+
+## Exact integer-histogram transition
+
+At exponent `t=1/2`, consider the abstract histograms
+
+```text
+W_4=1, W_256=32;   P_16=c,   1<=c<=128.
+```
+
+Here `T=514`, `P=4c`, `p=256/257`, and `x=1/3`. The exact minimum of
+`T(t-lambda) exp(lambda mu_P)` over positive `lambda` is 24, attained at
+`lambda=3/2`. The tail and ordering gates are therefore feasible exactly
+when c>=7. The boundary c=6 fails despite moment surplus and a positive
+mean gap.
+
+For c=7, one explicit witness is
+
+```text
+a=1, b=31, M=2^132, s=1/2, lambda=3/2,
+mixed tail u=2049/2056 < 1,
+root tail v=64*(6/7)^32 < 1,
+forward ratio T(t+s)/T(t)=4098/257 > 4=P(t+s)/P(t).
+```
+
+This c=7 profile has no nonnegative moment crossing. The source's crossing
+hypothesis is sufficient for its wider theorem, not necessary for these
+three gates. The proof gives the all-c transition. The verifier checks
+all 128 integers and this literal rational witness. These histograms
+are not asserted to be realizable native inventories.
+
+The advance CLAIM incorrectly predicted mirror slack for this fixture.
+Its source and exit windows are disjoint, so it fails mirror coverage.
+The [progress correction](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19147154)
+records the narrowed delivered scope. No full compiler admission follows.
+
+## Reproduce
+
+From the repository root, standard-library CPython 3.12:
+
+```sh
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/adaptive-tail-entropy/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -O -W error -B research/adaptive-tail-entropy/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/adaptive-tail-entropy
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/adaptive-tail-entropy --check-source-history
+```
+
+Any CPython 3.12 executable may replace the absolute local interpreter path.
+The direct verifier is read-only and Git-free. It prints a generated JSON
+receipt bound to every package file, followed by `PASS_ADAPTIVE_TAIL_ENTROPY`.
+It uses exact rational powers to compare the entropy threshold, a separate
+rational search for actual passing tail points, finite interior-support
+chord checks, symbolic derivative identities and rejecting controls.
+The universal conclusion rests on the written proof, not a finite census.
+
+The finite domain contains all 8,640 combinations of exponents
+`1<=low<high<=5`, paid exponent `0<=e<high`, and three multiplicities
+in `1..6`, with ranks powers of four at t=1/2. Of these, 8,439 satisfy
+q>=1. The classifiers agree on all of them; 5,444 have an explicitly
+checked rational passing point and 2,995 fail. The verifier also checks
+288 three-position laws, including 256 strict interior cases and 32
+endpoint equalities, and 14,975 literal failing-point controls.
+
+The verifier has no recursion, subprocesses, network or external inputs.
+Each witness search has at most 128 tail trials or 96 bisections. Every
+function has at most 23 physical lines. Python's managed allocation is a
+documented deviation from fixed storage: counters have fixed key sets,
+only one histogram is live, the source inventory has six files capped at
+128 KiB each, and all arithmetic domains and iteration counts are bounded.
+Warning-strict normal and optimized execution and an AST inspection are
+the available local diagnostics; no repository-wide static analysis is claimed.
+
+## Scope and credit
+
+Canonical base `ff3cc58e370d0f678e529246f8c73e8094e18fcf`, priority revision 7.
+The [advance claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19147083)
+records the change from `independent-moment` to an original algebraic gate
+question. [TASK.json](TASK.json) records the remaining obligations and
+[SOURCES.json](SOURCES.json) pins historical provenance. No predecessor code
+or receipt is imported, executed or recounted as this contribution.
+
+Credit Dillon Amburgey's [#4532](https://github.com/CrocSwap/integer-mult-bounds/pull/4532)
+for the exact scalar gate criterion used as a cited premise, zxv's
+[#4436](https://github.com/CrocSwap/integer-mult-bounds/pull/4436) and
+[#4483](https://github.com/CrocSwap/integer-mult-bounds/pull/4483) for the
+adaptive flow and gates, Jacob Alan Sussman's compiler, and Ryanson Jonathan's
+[#4459](https://github.com/CrocSwap/integer-mult-bounds/pull/4459) mirror method.
+Their retained native, helper, geometry and outer contributors keep their
+credit. This contribution was produced by Nick Petalas. Apache-2.0.
+Independent human and formal proof-kernel review are unclaimed. Global
+literature priority for entropy or exponential-moment bounds is unclaimed.
+
+The result screens only the two tail gates and their ordering guard.
+General-profile failure of the sufficient entropy test is inconclusive.
+Native realizability, full mirror/recurrence funding, chronological widths,
+owned restoration, adapters, precision, movement, stock and outer transfer
+remain separate obligations. No selected scientific replay, Lean or Docker
+run is claimed. The selected frontier is unchanged.
+
+## Open next questions
+
+1. Can an actual changed native profile use the entropy screen to obtain a
+   useful integer-height witness? Start with its exact target and paid
+   histograms and complete mirror cells. Native semantics, width, funding
+   and the physical bill remain blockers.
+2. Can one interior target moment give a quantitatively sharper screen above
+   the endpoint threshold? Start with a fixed positive mass separated from
+   both extremes and bound the strict chord deficit. This proof uses only
+   the presence of interior mass at equality, not a positive uniform margin.
diff --git a/research/adaptive-tail-entropy/SOURCES.json b/research/adaptive-tail-entropy/SOURCES.json
new file mode 100644
index 0000000000..5c48ac1e7d
--- /dev/null
+++ b/research/adaptive-tail-entropy/SOURCES.json
@@ -0,0 +1,36 @@
+{
+  "schema_version": 1,
+  "base_commit": "ff3cc58e370d0f678e529246f8c73e8094e18fcf",
+  "files": [
+    {
+      "path": "certificates/selected-result.json",
+      "usage": "provenance",
+      "git_blob": "c35482cd9035843b15a634cc8276a7e1e40e8395",
+      "sha256": "6fe0a099b89aa2aed796a13c3a21dafc63f3388ebf397464e44e0451893b9375"
+    },
+    {
+      "path": "docs/research/agent-task-catalog.json",
+      "usage": "provenance",
+      "git_blob": "f126dd2e2dad2b669e75d1d0d0bd05c600725602",
+      "sha256": "f7a48bfa2659b88378282a8eee7d9fe52cdf505594124c4d1686b58510fffd72"
+    },
+    {
+      "path": "research/adaptive-gate-existence/README.md",
+      "usage": "provenance",
+      "git_blob": "955d60830dc7d95316e2fd9c0ca5df1fbd1738ed",
+      "sha256": "02170ceba88fafac5a3f49f766b86c32972be71e071cad8be3ac1d9f17228b13"
+    },
+    {
+      "path": "research/adaptive-gate-existence/PROOF.md",
+      "usage": "provenance",
+      "git_blob": "bdf142f26d8b01164c9db1c021f7385a9f11a7d6",
+      "sha256": "340d637feef40f44a808c718207c0fede12cc483e2c979b86c56bb736b9c1ef5"
+    },
+    {
+      "path": "research/rank-convergence/PROOF.md",
+      "usage": "provenance",
+      "git_blob": "75f451837204bd141f357e7f5e5d6c6f42e1423e",
+      "sha256": "3c971c5670669cb36312815b111e64c83e1490a10ee82f5412bd9aee01e9c376"
+    }
+  ]
+}
diff --git a/research/adaptive-tail-entropy/TASK.json b/research/adaptive-tail-entropy/TASK.json
new file mode 100644
index 0000000000..5de31d0e43
--- /dev/null
+++ b/research/adaptive-tail-entropy/TASK.json
@@ -0,0 +1,161 @@
+{
+  "schema_version": 1,
+  "task_id": "independent-moment",
+  "priority_revision": 7,
+  "base_commit": "ff3cc58e370d0f678e529246f8c73e8094e18fcf",
+  "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": "changed",
+  "actual_scope": "Derive a sharp range-and-tilted-mean entropy screen for adaptive compiler two-tail gates, exact for two-rank target profiles, with the strict equality case and an exact integer-histogram transition.",
+  "scope_change_reason": "The donor requests original research, not predecessor verification. This changes the historical independent-moment audit card to a new analytic consequence of Dillon Amburgey #4532's scalar gate equivalence. Its source theorem is cited rather than replayed.",
+  "bottleneck_link": "A closed-form screen distinguishes profiles that can satisfy the existing two-tail/ordering gates from those requiring changed geometry. This is an algebraic compiler side result; it does not discharge mirror, native or physical obligations.",
+  "budget_minutes": 60,
+  "stop_rule": "Stop at the first proved entropy screen and its strict boundary fixture; package it without searching for a native supplier or extending to more moments.",
+  "outcome": "completed",
+  "evidence": "PROOF.md gives the universal analytic argument. The read-only exact verifier compares entropy and monomial classifiers, finds actual rational passing points, checks interior strictness, the 128-case c transition, the literal rational gate witness, mirror failure and eleven controls.",
+  "author": "Nick Petalas",
+  "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.",
+  "open_questions": [
+    {
+      "question": "Can an actual changed native profile use the entropy screen to obtain a useful integer-height witness?",
+      "why_it_matters": "Tail feasibility is one required compiler gate but does not establish implementation or full funding.",
+      "first_step": "Pin the complete target/paid histograms and mirror cells of one native word, then apply the screen.",
+      "blocked_by": "Native semantics, mirror coverage, chronological width, funding and the complete physical bill remain unresolved."
+    },
+    {
+      "question": "Can a specified interior target moment give a stronger screen above the endpoint threshold?",
+      "why_it_matters": "The present bound knows only the target range and mean, with a qualitative strictness improvement at equality.",
+      "first_step": "Fix positive mass separated from both endpoints and bound its strict exponential chord deficit.",
+      "blocked_by": "No quantitative uniform lower bound on the interior deficit is supplied."
+    }
+  ],
+  "claim_type": "scoped written proof with exact finite corroboration",
+  "claim_url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19147083",
+  "progress_url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19147154",
+  "claim_correction": "The advance claim predicted mirror slack from a coefficient ratio. The exit and inner-source windows are disjoint; the progress post explicitly corrects this prediction. Delivered scope is tail/ordering feasibility, and the fixture records mirror failure.",
+  "preserved_start": {
+    "branch": null,
+    "head": "ff3cc58e370d0f678e529246f8c73e8094e18fcf",
+    "status": "Clean detached HEAD; no earlier branch was checked out. Prior commits preserved."
+  },
+  "environment": {
+    "python": "3.12.15",
+    "dependencies": "standard library only"
+  },
+  "overlap": {
+    "checked_utc": "2026-10-23T14:08:38.061102+00:00",
+    "sources": "Live open PRs, latest handoffs and active Discussions, 162 same-account PRs since 2026-10-22, main README topic searches, merged relative-entropy/tail-gates/W_256 searches, cached original-card and topic searches, simultaneous local reservations.",
+    "limitations": "The sparse helper scan does not search every main package. Separate git grep searches cover committed README files only. Remote queries are not atomic; unpublished work and arbitrary diffs are outside coverage.",
+    "predecessors": [
+      4532,
+      4483,
+      4436,
+      4459
+    ],
+    "recent_same_account_rule": "No PR from this account in the last 24 hours was selected as the target or as an open-question/generalization source."
+  },
+  "verification": {
+    "unrun": [
+      "Independent human review",
+      "Proof-kernel formalization",
+      "Native/physical supplier replay",
+      "Full mirror/funded compiler construction",
+      "Selected scientific cold replay",
+      "Whole-repository static analysis"
+    ],
+    "scope": "The registered commands are bounded exact finite corroboration. The infinite-domain conclusion rests on PROOF.md and the cited scalar equivalence.",
+    "finite_coverage": {
+      "histograms": 8439,
+      "passing_rational_points": 5444,
+      "failing_histograms": 2995,
+      "failing_point_controls": 14975,
+      "interior_laws": 288,
+      "strict_interior_cases": 256,
+      "endpoint_equalities": 32,
+      "integer_fixture_cases": 128,
+      "rejection_controls": 11,
+      "rejected_disposable_mutations": 3
+    },
+    "local": "Warning-strict normal and optimized direct checks and both registered commands pass. Every registered command was timed locally and is below one second in the observed runs; this is budget evidence, not a performance guarantee.",
+    "diagnostics": "Warning-strict execution and AST parsing pass; functions are at most 23 physical lines. No standalone linter was available on PATH. Managed-runtime allocation is bounded and documented in README.md."
+  },
+  "upstream_refresh": {
+    "main_commit": "ff3cc58e370d0f678e529246f8c73e8094e18fcf",
+    "priority_revision": 7,
+    "status": "Canonical main and governing guidance unchanged at precommit fetch; live open PRs, merged entropy results and the latest 30 handoff posts were checked again."
+  }
+}
diff --git a/research/adaptive-tail-entropy/VERIFY.json b/research/adaptive-tail-entropy/VERIFY.json
new file mode 100644
index 0000000000..a280058a8e
--- /dev/null
+++ b/research/adaptive-tail-entropy/VERIFY.json
@@ -0,0 +1,34 @@
+{
+  "schema_version": 1,
+  "status": "ready",
+  "python": "3.12",
+  "requirements": [],
+  "inputs": [],
+  "commands": [
+    {
+      "argv": [
+        "{python}",
+        "-I",
+        "-W",
+        "error",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 120,
+      "checks": "Exact entropy/monomial classifications, rational passing points, interior strictness, all 128 integer fixture cases, literal two-tail witness, explicit mirror failure and eleven controls."
+    },
+    {
+      "argv": [
+        "{python}",
+        "-I",
+        "-O",
+        "-W",
+        "error",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 120,
+      "checks": "The same exact checks with Python assertions disabled; predicates use explicit exceptions."
+    }
+  ]
+}
diff --git a/research/adaptive-tail-entropy/verify.py b/research/adaptive-tail-entropy/verify.py
new file mode 100644
index 0000000000..33ad033023
--- /dev/null
+++ b/research/adaptive-tail-entropy/verify.py
@@ -0,0 +1,225 @@
+#!/usr/bin/env python3
+"""Read-only exact corroboration of the new tail entropy theorem.
+
+produced by Nick Petalas. Apache-2.0.
+The universal assertion is the written proof, not this finite census.
+"""
+
+from collections import Counter
+from fractions import Fraction as Q
+from hashlib import sha256
+import json
+from pathlib import Path
+
+
+def require(condition, message):
+    if not condition:
+        raise ValueError(message)
+
+
+def entropy_power(q, p, x):
+    """Return (q exp(-D(x||p)))**denominator(x), exactly."""
+    require(q >= 1 and 0 < x < p < 1, "invalid entropy regime")
+    n, j = x.denominator, x.numerator
+    require(n <= 64, "finite check denominator exceeds 64")
+    return q**n * (p / x)**j * ((1 - p) / (1 - x))**(n - j)
+
+
+def binary_gate(a, b, low, high, paid_mean, paid):
+    """Classify a two-target law in common logarithmic rank units."""
+    require(a > 0 and b > 0 and paid > 0, "nonpositive mass")
+    require(0 <= low < high <= 5, "invalid finite rank exponents")
+    require(a + b >= paid, "q>=1 is required")
+    if paid_mean < low:
+        return True
+    if paid_mean == low:
+        return a < paid
+    mean = (a * low + b * high) / (a + b)
+    if paid_mean >= mean:
+        return False
+    x = Q(paid_mean - low, high - low)
+    return entropy_power((a + b) / paid, b / (a + b), x) < 1
+
+
+def derivative_classifier(a, b, low, high, paid_mean, paid):
+    """Independent monomial critical-value comparison, without entropy."""
+    if paid_mean < low:
+        return True
+    if paid_mean == low:
+        return a < paid
+    if (paid_mean - low) * a >= (high - paid_mean) * b:
+        return False
+    d, j = high - low, paid_mean - low
+    critical = a**(d - j) * b**j * d**d
+    divisor = (d - j)**(d - j) * j**j
+    return critical < paid**d * divisor
+
+
+def scalar_value(z, a, b, low, high, paid_mean):
+    require(0 < z <= 1, "tail variable outside (0,1]")
+    return a * z**(low - paid_mean) + b * z**(high - paid_mean)
+
+
+def passing_point(a, b, low, high, paid_mean, paid):
+    """Find a rational z=4**(-lambda) with a literal strict scalar gate."""
+    if paid_mean <= low:
+        for j in range(1, 129):
+            z = Q(1, 2**j)
+            if scalar_value(z, a, b, low, high, paid_mean) < paid:
+                return z
+    else:
+        left, right = Q(0), Q(1)
+        critical = a * (paid_mean - low) / (b * (high - paid_mean))
+        require(0 < critical < 1, "critical point must lie in (0,1)")
+        for _ in range(96):
+            z = (left + right) / 2
+            if scalar_value(z, a, b, low, high, paid_mean) < paid:
+                return z
+            if z**(high - low) < critical:
+                left = z
+            else:
+                right = z
+    raise ValueError("bounded rational witness search exhausted")
+
+
+def histogram_census():
+    counts = Counter()
+    for low in range(1, 5):
+        for high in range(low + 1, 6):
+            for paid_mean in range(high):
+                for wa in range(1, 7):
+                    for wb in range(1, 7):
+                        for wc in range(1, 7):
+                            masses = (Q(wa * 2**low), Q(wb * 2**high))
+                            paid = Q(wc * 2**paid_mean)
+                            if sum(masses) < paid:
+                                counts["outside_q_domain"] += 1
+                                continue
+                            check_histogram(masses, low, high, paid_mean, paid, counts)
+    require(counts["passing"] > 0 and counts["failing"] > 0, "empty outcome class")
+    return dict(sorted(counts.items()))
+
+
+def check_histogram(masses, low, high, paid_mean, paid, counts):
+    a, b = masses
+    decision = binary_gate(a, b, low, high, paid_mean, paid)
+    separate = derivative_classifier(a, b, low, high, paid_mean, paid)
+    require(decision == separate, "entropy and monomial classifiers disagree")
+    counts["histograms"] += 1
+    if decision:
+        z = passing_point(a, b, low, high, paid_mean, paid)
+        require(scalar_value(z, a, b, low, high, paid_mean) < paid, "bad witness")
+        counts["passing"] += 1
+    else:
+        for z in (Q(1), Q(3, 4), Q(1, 2), Q(1, 4), Q(1, 8)):
+            require(scalar_value(z, a, b, low, high, paid_mean) >= paid,
+                    "failing classification has a passing sample")
+            counts["failing_point_controls"] += 1
+        counts["failing"] += 1
+
+
+def interior_census():
+    counts = Counter()
+    for endpoint_mass in range(1, 9):
+        for interior_mass in range(9):
+            total = 2 * endpoint_mass + interior_mass
+            weights = tuple(Q(m, total) for m in
+                            (endpoint_mass, interior_mass, endpoint_mass))
+            for denominator in range(2, 6):
+                z = Q(1, denominator**2)
+                x = z / (1 + z)
+                literal = weights[0] + weights[1] / denominator + weights[2] * z
+                chord = (1 + z) / 2
+                require(literal <= chord, "chord inequality failed")
+                require((literal == chord) == (interior_mass == 0), "strictness failed")
+                power = chord**x.denominator / z**x.numerator
+                require(power == entropy_power(Q(1), Q(1, 2), x), "entropy value failed")
+                require(0 < power < 1, "invalid minimized value")
+                counts["laws"] += 1
+                counts["strict" if interior_mass else "endpoint_equality"] += 1
+    return dict(sorted(counts.items()))
+
+
+def fixture_transition():
+    for c in range(1, 129):
+        q, p, x = Q(514, 4 * c), Q(256, 257), Q(1, 3)
+        require(entropy_power(q, p, x) == Q(6, c)**3, "fixture optimum failed")
+        require(binary_gate(Q(2), Q(512), 1, 4, 2, Q(4 * c)) == (c >= 7),
+                "incorrect strict c transition")
+    u = Q(1, 2**66) * Q(8196, 514) * 4**31
+    v = Q(2**198) * Q(3, 224)**32
+    require(u == Q(2049, 2056) and u < 1, "mixed tail witness failed")
+    require(v == 64 * Q(6, 7)**32 and v < 1, "root tail witness failed")
+    require(Q(8196, 514) > 4, "forward ordering failed")
+    require(Q(1, 4) + Q(32, 256) == Q(3, 8), "negative moment failed")
+    require(2 * 8 + Q(512, 8**2) == 24, "attained minimum failed")
+    for j in range(1, 65):
+        y = Q(j, 4)
+        left = y**3 * (2 - 1024 / y**3)
+        right = 2 * (y - 8) * (y**2 + 8 * y + 64)
+        require(left == right, "fixture derivative factorization failed")
+    return {"integer_cases": 128, "u": str(u), "v": str(v), "minimum": 24}
+
+
+def mirror_failure():
+    cells = ((Q(1, 256), Q(1, 16)), (Q(1, 16), Q(1, 4)))
+    values = []
+    for left, right in cells:
+        z = (left + right) / 2
+        source = 2048 if Q(1, 256) < z <= Q(1, 16) else 0
+        exits = 8 if Q(1, 16) < z <= Q(1, 4) else 0
+        values.append((source, exits))
+    require(values == [(2048, 0), (0, 8)], "mirror window boundary changed")
+    covered = not any(e > 0 and s == 0 for s, e in values)
+    require(not covered, "mirror failure disappeared")
+    return {"cells_at_c1": values, "covered": covered}
+
+
+def rejection_controls():
+    require(entropy_power(Q(5, 4), Q(4, 5), Q(1, 2)) == 1,
+            "two-point equality must fail strictly")
+    require(Q(5, 4) * 2 * (Q(1, 10) + Q(1, 5) / 2 + Q(7, 10) / 4)
+            == Q(15, 16), "interior mass must rescue equality")
+    require(not binary_gate(Q(2), Q(512), 1, 4, 2, Q(24)), "equality accepted")
+    require(not binary_gate(Q(2), Q(2), 1, 3, 2, Q(4)), "mean equality accepted")
+    require(not binary_gate(Q(2), Q(2), 1, 3, 3, Q(3)), "reversed mean accepted")
+    require(binary_gate(Q(2), Q(8), 2, 4, 1, Q(1)), "below-range gate rejected")
+    require(not binary_gate(Q(2), Q(8), 2, 4, 2, Q(2)), "lower-atom equality accepted")
+    require(binary_gate(Q(2), Q(8), 2, 4, 2, Q(3)), "lower-atom strict gate rejected")
+    invalid = ((Q(1, 2), Q(4, 5), Q(1, 2)), (Q(1), Q(1, 2), Q(3, 4)),
+               (Q(1), Q(1), Q(1, 2)))
+    for args in invalid:
+        try:
+            entropy_power(*args)
+        except ValueError:
+            continue
+        raise ValueError("invalid entropy input was accepted")
+    return 11
+
+
+def source_hashes():
+    directory = Path(__file__).resolve().parent
+    names = ("README.md", "PROOF.md", "TASK.json", "SOURCES.json", "VERIFY.json", "verify.py")
+    for name in names:
+        require((directory / name).stat().st_size <= 128 * 1024, "package file exceeds 128 KiB")
+    return {name: sha256((directory / name).read_bytes()).hexdigest() for name in names}
+
+
+def main():
+    receipt = {
+        "claim_type": "scoped written proof with exact finite corroboration",
+        "histogram_census": histogram_census(),
+        "interior_census": interior_census(),
+        "fixture": fixture_transition(),
+        "mirror": mirror_failure(),
+        "rejection_controls": rejection_controls(),
+        "source_sha256": source_hashes(),
+    }
+    canonical = json.dumps(receipt, sort_keys=True, separators=(",", ":"))
+    receipt["receipt_sha256"] = sha256(canonical.encode()).hexdigest()
+    print(json.dumps(receipt, indent=2, sort_keys=True))
+    print("PASS_ADAPTIVE_TAIL_ENTROPY no_new_kappa")
+
+
+if __name__ == "__main__":
+    main()