Sharp adaptive tail gate with prescribed interior mass

research/interior-mass-tail-gate/README.md

@@ -0,0 +1,69 @@
+# Sharp adaptive tail gate with prescribed interior mass
+
+This scoped theorem strengthens the range-and-mean tail screen with a specified amount of interior mass. It gives a sharp worst-case adaptive decision, an attaining law, and an integer histogram that the old screen cannot certify. It answers the released [Discussion #5335](https://github.com/CrocSwap/integer-mult-bounds/discussions/5335). Mirror and recurrence funding are separate. The complete kappa calculation is unchanged.
+
+**Contract.** Use the normalization in Nick Petalas's cited proof: q=T(t)/P(t)>=1, Z=(log k-A)/(B-A), p=E Z, x=(mu_P-A)/(B-A), and h=lambda(B-A). The scalar tail criterion is q E exp[-h(Z-x)]<1 for some h>0. The source's equivalence from this strict criterion to the three compiler gates is a cited premise, not audited here.
+
+Fix 0<rho<=1 and 0<ell<=u<1. Consider the class of probability laws supported in [0,1], with mean p and mass exactly rho in [ell,u]. It is nonempty precisely when rho ell<=p<=1-rho+rho u. The same worst-case result holds if the interior mass is at least rho. The class permits zero endpoint weights; requiring positive weights at both endpoints is a smaller class and can change attainment at boundary statistics. No arbitrary law is claimed to have an integer native realization.
+
+**Two-law envelope.** Set
+
+    L=max(ell,(p-1+rho)/rho),   U=min(u,p/rho).
+
+For y in [L,U], let Q_y have masses
+
+    at 0:   1-rho-p+rho y,
+    at ell: rho (u-y)/(u-ell),
+    at u:   rho (y-ell)/(u-ell),
+    at 1:   p-rho y.
+
+When ell=u, replace the two interior rows by mass rho at ell. Then L=U=ell. Zero weights can be omitted. Define
+
+    E(h)=max(E_(Q_L) exp[-h(Z-x)], E_(Q_U) exp[-h(Z-x)]).
+
+For each h>0, E(h) is the exact largest transform over the stated class. To prove this, split exactly rho of the interior mass from the law. Replace this part by its mean-preserving chord on ell,u; replace the remainder by its chord on 0,1. Convexity increases the transform. The interior mean y lies in [L,U], and the new transform is affine in y. Its maximum is at L or U. These endpoint laws belong to the exact-mass class, which proves attainment and also proves the at-least-rho claim.
+
+**Sharp adaptive decision.** Every law in the class has a strict passing h if and only if
+
+    q inf_(h>0) E(h) < 1.                              (1)
+
+Thus there is no gap between choosing h after the law is known and this robust envelope test. Here is an explicit complete boundary rule. Let z0 be the smallest point with positive mass in either Q_L or Q_U. Let eta be the larger mass assigned to z0 by those two laws.
+
+- If x>=p, all laws fail, by Jensen and q>=1.
+- If x<z0, E(h) tends to zero, so all laws pass.
+- If x=z0<p, E(h) decreases strictly to eta. Passing is equivalent to q eta<1. Equality fails, since every finite value of a law with mass eta at z0 is larger than eta.
+- If z0<x<p, E is strictly convex, its right derivative at zero is x-p<0, and E(h) tends to infinity. It has a unique positive minimum h*. Use (1) with that attained minimum; equality fails.
+
+In the last case this is a one-variable, two-function decision, not a search over laws. At h*, either one active function has zero derivative or the active derivatives straddle zero. Choose a convex combination of the active Q laws whose transform derivative is zero there. Call it Q*. Its transform is convex, so h* is its global minimum, equal to E(h*). Q* is feasible and fails whenever qE(h*)>=1. This proves necessity and the equality case without interchanging an unjustified supremum and infimum. Sufficiency follows directly from the envelope. The same proof applies when L=U. To locate h*, it suffices to check stationary points of the two transforms and their crossing points, retaining only points where the active derivatives contain zero. The theorem supplies this exact characterization; no general transcendental root solver is included.
+
+**A literal integer discriminator.** Take W4=1, W16=1, W256=32, P16=8 and t=1/2. Then T(t)=518, P(t)=32, x=1/3 and rho=4/518 at the known interior atom ell=u=1/3. With y=4^lambda, the unnormalized transform is
+
+    2y+4+512/y^2.
+
+Its exact minimum is 28 at y=8, lambda=3/2. The sharp condition for the same target and P16=c is c>7; equality at c=7 fails. In contrast, the endpoint law with the same total weight and mean has weights 14/3 and 1540/3. Its minimum cubed is (27/4)(14/3)^2(1540/3)=75460, which exceeds 32^3. Thus the older range-and-mean guarantee fails for c=8 while the new screen passes.
+
+The original compiler gates pass with a=1, b=31, M=2^132, s=1/2 and lambda=3/2. Direct substitution gives
+
+    u_tail = 2^-66 (4106/259) 4^31 = 2053/2072 < 1,
+    v_tail = 2^198 (7/512)^32 = 7^32/2^90 < 1,
+    T(1)/T(1/2) = 4106/259 > 4 = P(1)/P(1/2).
+
+All comparisons are exact integers or rationals. The exit interval (1/16,1/4] still has no inner-source coverage: the only nonempty inner interval is (1/256,1/16]. The added rank16 atom makes no interval. This fixture therefore fails mirror coverage. It is a tail/ordering improvement only.
+
+**Evidence and limits.** The checker verifies 150 rational statistic fixtures, 1,050 envelope comparisons and attaining cases, 77 chord comparisons, the three original gate inequalities, and seven invalid-input/boundary/old-screen/mirror controls. The general proof covers arbitrary probability laws in the stated class; these finite rational checks corroborate it. Histogram realization, all mirror and recurrence predicates, source preparation, native execution, complete stock and analytic recovery remain open.
+
+Credit Nick Petalas's [PR #5254](https://github.com/CrocSwap/integer-mult-bounds/pull/5254) supplies the normalized criterion, sharp endpoint screen and explicit interior-mass question in its [proof](https://github.com/CrocSwap/integer-mult-bounds/blob/f7c2625f5488b09e6d19b4bed7efe8b4e89a6782/research/adaptive-tail-entropy/PROOF.md). That proof records Dillon Amburgey's [PR #4532](https://github.com/CrocSwap/integer-mult-bounds/pull/4532) scalar-to-gate equivalence, and the compiler lineage of zxv, Jacob Alan Sussman and Ryanson Jonathan. Those are retained premises and credits. Convex chord bounds and extremal moment methods are classical; the contribution is the sharp interior-mass adaptive boundary and the source-gate discriminator.
+
+Prepared by Ali Romman with substantial OpenAI Codex assistance; Apache-2.0.
+
+## Reproduce
+
+```sh
+python3 -B scripts/research_package.py --package research/interior-mass-tail-gate
+```
+
+Use Python 3.12 with the standard library. The normal and optimized commands must print `PASS_INTERIOR_MASS_TAIL_GATE`. The launcher must print `PASS_REGISTERED_RESEARCH_PACKAGE`. The checker has no external runtime inputs.
+
+## Open next questions
+
+Apply the interior-mass screen to a source-bound histogram that also passes every mirror and recurrence predicate. The source binding and physical cost model are not supplied by this package. See `TASK.json` for the structured scope.

research/interior-mass-tail-gate/SOURCES.json

@@ -0,0 +1,18 @@
+{
+  "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"
+    }
+  ]
+}

research/interior-mass-tail-gate/TASK.json

@@ -0,0 +1,106 @@
+{
+  "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": "This scoped theorem gives the sharp worst-case adaptive tail criterion with a prescribed mean and interior mass. Two explicit endpoint laws determine the envelope, and an attaining mixture proves the strict boundary. An integer three-rank fixture passes the original tail/ordering gates where the earlier range-and-mean guarantee fails; its mirror coverage still fails.",
+  "scope_change_reason": "This is a scoped interface theorem. It does not complete the original supplier or uniform-transfer task.",
+  "bottleneck_link": "Apply the interior-mass screen to a source-bound histogram that also passes every mirror and recurrence predicate.",
+  "budget_minutes": 60,
+  "stop_rule": "Stop after the scoped proof, exact controls and bounded registered replay; do not expand to physical lowering.",
+  "outcome": "completed",
+  "evidence": "150 rational statistic fixtures, 1,050 envelope comparisons and attaining cases, 77 chord checks, three original gate inequalities and seven controls",
+  "author": "Ali Romman",
+  "ai_assistance": "Substantial OpenAI Codex assistance; no independent human or proof-kernel acceptance is claimed.",
+  "open_questions": [
+    {
+      "question": "Apply the interior-mass screen to a source-bound histogram that also passes every mirror and recurrence predicate.",
+      "why_it_matters": "The abstract result needs an actual caller and a complete cost model.",
+      "first_step": "Apply the interior-mass screen to a source-bound histogram that also passes every mirror and recurrence predicate.",
+      "blocked_by": "No production caller or physical cost model is supplied."
+    }
+  ],
+  "upstream_checkpoint": {
+    "commit": "ff3cc58e370d0f678e529246f8c73e8094e18fcf",
+    "priority_revision": 7,
+    "checked_at": "2026-10-23T18:00:18.680728+00:00"
+  },
+  "claim": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19151510"
+}

research/interior-mass-tail-gate/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": "150 rational statistic fixtures, 1,050 envelope comparisons and attaining cases, 77 chord checks, three original gate inequalities and seven controls"
+    },
+    {
+      "argv": [
+        "{python}",
+        "-I",
+        "-W",
+        "error",
+        "-O",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 120,
+      "checks": "150 rational statistic fixtures, 1,050 envelope comparisons and attaining cases, 77 chord checks, three original gate inequalities and seven controls"
+    }
+  ]
+}

research/interior-mass-tail-gate/verify.py

@@ -0,0 +1,90 @@
+"""Exact rational envelopes and original tail-gate discriminator.
+
+Prepared by Ali Romman with substantial OpenAI Codex assistance. Apache-2.0.
+"""
+from fractions import Fraction as F
+from itertools import product
+
+
+def need(ok, message):
+    if not ok: raise ValueError(message)
+
+
+def laws(p,rho,ell,u):
+    need(0<rho<=1 and 0<ell<=u<1,'interior parameters')
+    need(rho*ell<=p<=1-rho+rho*u,'feasible mean')
+    low=max(ell,(p-1+rho)/rho); high=min(u,p/rho)
+    out=[]
+    for y in (low,high):
+        if ell==u:
+            w={F(0):1-rho-p+rho*y,ell:rho,F(1):p-rho*y}
+        else:
+            w={F(0):1-rho-p+rho*y,ell:rho*(u-y)/(u-ell),u:rho*(y-ell)/(u-ell),F(1):p-rho*y}
+        need(all(v>=0 for v in w.values()),'nonnegative extremizer')
+        need(sum(w.values())==1 and sum(z*v for z,v in w.items())==p,'law statistics')
+        out.append(w)
+    return out
+
+
+def laplace(w,j,den):
+    return sum(v*F(2)**(-j*int(z*den)) for z,v in w.items())
+
+
+def main():
+    grids=0; comparisons=0; attained=0
+    den=6
+    for ell_i,u_i in [(1,2),(1,4),(2,4),(3,5),(2,2)]:
+        ell,u=F(ell_i,den),F(u_i,den)
+        for units in range(1,5):
+            rho=F(units,4)
+            for inside in range(units+1):
+                y=ell+(u-ell)*F(inside,units)
+                for ones in range(5-units):
+                    p=rho*y+F(ones,4)
+                    endpoints=laws(p,rho,ell,u); grids+=1
+                    # A literal feasible law has the same prescribed mass and mean.
+                    w={F(0):1-rho-F(ones,4),F(1):F(ones,4)}
+                    w[ell]=w.get(ell,0)+rho*F(units-inside,units)
+                    w[u]=w.get(u,0)+rho*F(inside,units)
+                    for j in range(1,8):
+                        bound=max(laplace(a,j,den) for a in endpoints)
+                        need(laplace(w,j,den)<=bound,'extreme envelope dominates')
+                        need(any(laplace(a,j,den)==bound for a in endpoints),'attaining law')
+                        comparisons+=1;attained+=1
+    # Splitting an interior atom at its interval endpoints increases the transform.
+    chord=0
+    for ell_i,u_i in [(1,5),(2,4),(1,3)]:
+        for z in range(ell_i,u_i+1):
+            a=F(u_i-z,u_i-ell_i);b=1-a
+            for j in range(1,8):
+                need(F(2)**(-j*z)<=a*F(2)**(-j*ell_i)+b*F(2)**(-j*u_i),'interior chord')
+                chord+=1
+    # All numbers below come from the original gates, not a sampled minimizer.
+    target_half=F(518); paid_half=F(32)
+    target_one=F(8212); target_minus_one=F(7,16)
+    tail_u=F(1,2**66)*(target_one/target_half)*4**31
+    tail_v=2**198*(target_minus_one/paid_half)**32
+    need(tail_u==F(2053,2072) and tail_u<1,'forward tail')
+    need(tail_v==F(7**32,2**90) and tail_v<1,'backward tail')
+    need(target_one/target_half>4,'ordering')
+    # Actual transform: 2y+4+512/y^2; exact minimum 28 at y=8.
+    need(2*8+4+F(512,64)==28 and F(28,32)<1,'sharp three-rank minimum')
+    # Endpoint chord with the SAME mean has weights 14/3 and 1540/3.
+    low,high=F(14,3),F(1540,3)
+    min_cube=F(27,4)*low**2*high
+    need(min_cube==75460 and min_cube>32**3,'old screen cannot pass')
+    # A distinct accepting point does not certify the equality boundary.
+    need(F(28,4*7)==1 and F(28,4*6)>1,'strict c=7 boundary')
+    # Interior target rank 16 adds no mirror interval for paid rank 16.
+    exits=[(F(1,16),F(1,k)) for k in (4,16,256) if k<16]
+    inner=[(F(1,k),F(1,16)) for k in (4,16,256) if k>16]
+    point=F(1,8)
+    need(any(a<point<=b for a,b in exits) and not any(a<point<=b for a,b in inner),'mirror failure retained')
+    rejected=0
+    for args in [(F(0),F(1,2),F(1,4),F(3,4)),(F(1),F(1,2),F(1,4),F(3,4)),(F(1,2),F(0),F(1,4),F(3,4)),(F(1,2),F(1,2),F(3,4),F(1,4))]:
+        try: laws(*args)
+        except ValueError: rejected+=1
+    need(rejected==4,'invalid statistics reject')
+    print('PASS_INTERIOR_MASS_TAIL_GATE',dict(statistic_fixtures=grids,envelope_comparisons=comparisons,attaining_checks=attained,chord_checks=chord,original_gates=3,controls=7))
+
+if __name__=='__main__':main()