LM006: source-bound replay for one-dimensional coefficient certificate

.github/workflows/lm006-oned-coefficient.yml

@@ -0,0 +1,60 @@
+name: LM006 one-dimensional coefficient replay
+
+'on':
+  pull_request:
+    paths:
+      - 'coefficients/lm006_wrong_sign_oned_20261006_a62c/**'
+      - 'coefficients/lm006_wrong_sign_20261006_r20/enclose.py'
+      - 'reviews/lm006_wrong_sign_asymptotic_20261006/NOTE.md'
+      - 'tools/lm006_oned_coefficient_replay.py'
+      - 'tests/test_lm006_oned_coefficient_replay.py'
+      - '.github/workflows/lm006-oned-coefficient.yml'
+  push:
+    branches: [main]
+    paths:
+      - 'coefficients/lm006_wrong_sign_oned_20261006_a62c/**'
+      - 'coefficients/lm006_wrong_sign_20261006_r20/enclose.py'
+      - 'reviews/lm006_wrong_sign_asymptotic_20261006/NOTE.md'
+      - 'tools/lm006_oned_coefficient_replay.py'
+      - 'tests/test_lm006_oned_coefficient_replay.py'
+      - '.github/workflows/lm006-oned-coefficient.yml'
+  workflow_dispatch:
+
+permissions:
+  contents: read
+
+jobs:
+  numerical-replay:
+    runs-on: ubuntu-latest
+    timeout-minutes: 30
+    strategy:
+      fail-fast: false
+      matrix:
+        mode: [normal, optimized]
+    name: lm006-oned-coefficient (${{ matrix.mode }})
+    steps:
+      - uses: actions/checkout@11d5960a326750d5838078e36cf38b85af677262
+        with:
+          persist-credentials: false
+          fetch-depth: 1
+      - uses: actions/setup-python@a26af69be951a213d495a4c3e4e4022e16d87065
+        with:
+          python-version: '3.13.5'
+      - name: Replay controls and frozen 1024-panel certificate
+        shell: bash
+        run: |
+          set -euo pipefail
+          mkdir -p "$RUNNER_TEMP/lm006-oned-protocol"
+          FLAGS="-B -S"
+          if [ "${{ matrix.mode }}" = optimized ]; then FLAGS="-B -O -S"; fi
+          python $FLAGS -m unittest discover -s tests -p 'test_lm006_oned_coefficient_replay.py' -v 2>&1 | tee "$RUNNER_TEMP/lm006-oned-protocol/${{ matrix.mode }}.log"
+          python -B -S tools/lm006_oned_coefficient_replay.py --mode "${{ matrix.mode }}" --output "$RUNNER_TEMP/lm006-oned-${{ matrix.mode }}-${{ github.run_attempt }}"
+      - name: Preserve success or failure evidence
+        if: always()
+        uses: actions/upload-artifact@ea165f8d65b6e75b540449e92b4886f43607fa02
+        with:
+          name: lm006-oned-${{ matrix.mode }}-${{ github.run_id }}-${{ github.run_attempt }}
+          path: |
+            ${{ runner.temp }}/lm006-oned-${{ matrix.mode }}-${{ github.run_attempt }}/
+            ${{ runner.temp }}/lm006-oned-protocol/
+          if-no-files-found: error

coefficients/lm006_wrong_sign_oned_20261006_a62c/PRIOR_WORK.md

@@ -0,0 +1,40 @@
+# Prior-work correction — read with NOTE section 1
+
+OpenAI / GPT-6 Astra Pro, `coefficient-dimension-reduction-20261006-1340-a62c`,
+for Dylan Roy. Scientific effect NONE. This additive correction qualifies the
+contribution wording in the initial five-file packet; it does not alter its
+mathematical formulas, numerical code, results or execution history.
+
+The analytic reduction itself was already published in
+[Math-#362 comment6016901181](https://github.com/d6g8k5htny-coder/Math-/pull/362#issuecomment-6016901181)
+at 2026-10-06T13:05:10Z by OpenAI / GPT-6 Astra Pro,
+`r23-sign-integral-reduction-20261006-1255`, under pickup6016657196.
+It precedes this continuation's pickup6017509107 at13:38:52Z. A broader
+source read after initial publication exposed that earlier note, which fell
+outside the recent-comment window used for the initial ownership check.
+This was an omission in prior-work discovery, not new independence credit.
+
+In the earlier note's notation, its h(x) and this NOTE's g_v satisfy exactly
+
+    g_v(u)=s^3 h(u/s), s=sqrt(v).
+
+Changing b=s*z/2 in this packet's integral gives the earlier standard-normal
+coordinate integral. Both its positive-integral and truncated-moment proofs
+therefore precede the repeated derivations retained here for a self-contained
+implementation. No first-discovery claim is made for those identities.
+The earlier note also supplies separate small-argument series and tail bounds;
+this continuation does not claim their tests as its own execution or review.
+
+The additional work in this packet is NOTE sections3–6: a uniform fourth-
+derivative bound, the explicit composite-Simpson error, directed normal-tail
+arithmetic on[0,13], the chosen support-aware tail and the completed numerical
+enclosure with its own tests and countercontrols. This remains a genuinely
+new numerical-certificate review scope, not a repeated review of the earlier
+analytic identity. Neither packet establishes a numerical finite-r remainder,
+radius or a new persistence theorem.
+
+The original five files at6a2abb7a9bd8facecebca52de0b32d371645bfa5 remain
+byte-identical. Their source-map hashes and test/output identities remain valid;
+this new file is separately bound by its Git blob and delivery inventory.
+No historical note or review is silently rewritten. Coordination correction:
+[Math-#380 comment6018089819](https://github.com/d6g8k5htny-coder/Math-/pull/380#issuecomment-6018089819).

coefficients/lm006_wrong_sign_oned_20261006_a62c/RESULTS.json

@@ -0,0 +1 @@
+{"coefficient": ["0.001321995248726", "0.001321995413271"], "evaluations": 1025, "gamma": ["0.021702757242874", "0.021702759944149"], "independently_reviewed": false, "method": "analytic D integration; composite Simpson with proved |f4|<=1100; rational outward arithmetic", "omitted_tail_gamma_upper": "0.00000000000007444285", "panels": 1024, "quadrature_error_gamma_upper": "0.00000000135059963214", "scientific_effect": "NONE", "scope": "leading coefficient only; d2 L24 b6/5 original axes and pins; no finite-r remainder or radius", "source_commit": "64c0a203b94105f0fccbe6f8116a94e13431f84e"}

coefficients/lm006_wrong_sign_oned_20261006_a62c/SOURCES.json

@@ -0,0 +1,60 @@
+{
+  "schema_version": 1,
+  "scientific_effect": "NONE",
+  "author": {
+    "provider": "OpenAI",
+    "model": "GPT-6 Astra Pro",
+    "session": "coefficient-dimension-reduction-20261006-1340-a62c"
+  },
+  "files": {
+    "NOTE.md": {
+      "bytes": 15802,
+      "sha256": "b23be8ca33767c0c3413c8e12055c382c295f693349f9f624acce6dccce91b26",
+      "git_blob": "db27645e62bf846835b1daeb6c51f1eb3b417f1e"
+    },
+    "oned.py": {
+      "bytes": 7893,
+      "sha256": "07ae30528ccc2274dbad6f9e1898a9a4505ff80c4e2a97fda0b408f6f8d89e37",
+      "git_blob": "5015dee3a660b67c42ccab13a976626e6e2d02cc"
+    },
+    "test_oned.py": {
+      "bytes": 9708,
+      "sha256": "8314058f9b629786be7e9b9ff1c2d1dd256673200e4e154312a273223d1e104f",
+      "git_blob": "62e54422726f1caffab62e2e3fe38d297013e52d"
+    },
+    "RESULTS.json": {
+      "bytes": 598,
+      "sha256": "bdaf0f52021d9609f5b394df7ac82c80670f8a18319f0c8e703ce7bb6d6b405b",
+      "git_blob": "506833403f2dee91553d1a8dfc6eef6ee5c8faf8"
+    }
+  },
+  "dependencies": [
+    {
+      "repository": "d6g8k5htny-coder/Math-",
+      "commit": "1f64b8f8ee450262e0f56e6bdf9dfb37931f48c6",
+      "path": "coefficients/lm006_wrong_sign_20261006_r20/enclose.py",
+      "git_blob": "e680ddb7aa0abd4b6aab2cac6a54c1ff28efc782",
+      "sha256": "157e02ee22699b4fa2efdde1894824b92b962900dbb8da9bd65acee41ae91e88",
+      "slice": "parameters, outward pi/sqrt/exp/density and decimal formatting; original 2048 rectangle algorithm not called"
+    },
+    {
+      "repository": "d6g8k5htny-coder/Math-",
+      "commit": "64c0a203b94105f0fccbe6f8116a94e13431f84e",
+      "path": "reviews/lm006_wrong_sign_asymptotic_20261006/NOTE.md",
+      "git_blob": "ea914c1b8e0b8180b645f3f626e2081ab87700b9",
+      "sha256": "00d57d987c28ef5f2e3f6467c9e343fb60ffb3ad5806d004f245fe16914fbb61",
+      "slice": "coefficient definition, Gaussian laws and clipped J; no reproof of the asymptotic theorem"
+    }
+  ],
+  "external_reference": [
+    {
+      "url": "https://dlmf.nist.gov/3.5#ii",
+      "consumed": "3.5.7 and 3.5.8 composite Simpson and C4 remainder, exact formulas inspected"
+    },
+    {
+      "url": "https://dlmf.nist.gov/7.6#i",
+      "consumed": "power-series context; signed truncation directions derived in NOTE"
+    }
+  ],
+  "scope": "new analytic reduction/numerical enclosure only; author candidate until a separate source-bound review"
+}

coefficients/lm006_wrong_sign_oned_20261006_a62c/oned.py

@@ -0,0 +1,223 @@
+#!/usr/bin/env python3
+"""One-dimensional outward enclosure of the pinned LM006 leading coefficient.
+
+Integer/Fraction arithmetic only. Conditional on the exact #358 coefficient;
+not a finite-radius probability or a Lean proof. Parent arithmetic is hash-bound.
+"""
+import argparse
+from fractions import Fraction as F
+from functools import lru_cache
+import hashlib
+import json
+import os
+from pathlib import Path
+import stat
+import sys
+import types
+
+PARENT_SHA='157e02ee22699b4fa2efdde1894824b92b962900dbb8da9bd65acee41ae91e88'
+SCALE=10**36
+SERIES_SCALE=10**100
+SERIES_LAST=331  # Odd partial sum lower; preceding even partial sum upper.
+
+
+def exact(x):
+    if type(x) not in (int,F):
+        raise TypeError('exact int or Fraction required')
+    return F(x)
+
+
+def ceildiv(a,b):
+    return -((-a)//b)
+
+
+def iv(lo,hi=None):
+    lo=exact(lo); hi=lo if hi is None else exact(hi)
+    if lo>hi: raise ValueError('interval endpoints reversed')
+    return (F(lo.numerator*SCALE//lo.denominator,SCALE),
+            F(ceildiv(hi.numerator*SCALE,hi.denominator),SCALE))
+
+
+def as_iv(x):
+    if isinstance(x,tuple) and len(x)==2: return iv(*x)
+    return iv(x)
+
+
+def add(x,y):
+    x,y=as_iv(x),as_iv(y); return iv(x[0]+y[0],x[1]+y[1])
+
+
+def sub(x,y):
+    x,y=as_iv(x),as_iv(y); return iv(x[0]-y[1],x[1]-y[0])
+
+
+def mul(x,y):
+    x,y=as_iv(x),as_iv(y); z=[a*b for a in x for b in y]
+    return iv(min(z),max(z))
+
+
+def div(x,y):
+    x,y=as_iv(x),as_iv(y)
+    if y[0]<=0<=y[1]: raise ValueError('interval denominator contains zero')
+    z=[a/b for a in x for b in y]
+    return iv(min(z),max(z))
+
+
+def authenticate(raw):
+    if len(raw)!=7215 or hashlib.sha256(raw).hexdigest()!=PARENT_SHA:
+        raise ValueError('parent source identity mismatch')
+    return raw
+
+
+def parent_bytes():
+    path=Path(__file__).resolve().parent.parent/'lm006_wrong_sign_20261006_r20'/'enclose.py'
+    fd=os.open(path,os.O_RDONLY|os.O_NOFOLLOW|os.O_NONBLOCK)
+    with os.fdopen(fd,'rb') as stream:
+        if not stat.S_ISREG(os.fstat(stream.fileno()).st_mode):
+            raise ValueError('parent must be a regular file')
+        raw=stream.read(7217)
+    return authenticate(raw)
+
+
+@lru_cache(maxsize=1)
+def parent():
+    raw=parent_bytes(); module=types.ModuleType('verified_lm006_parent')
+    exec(compile(raw,'<sha256:'+PARENT_SHA+'>','exec'),module.__dict__)
+    return module
+
+
+def sqrt_iv(x):
+    x=as_iv(x)
+    if x[0]<0: raise ValueError('nonnegative square-root interval required')
+    return iv(parent().sqrt_bounds(x[0])[0],parent().sqrt_bounds(x[1])[1])
+
+
+def phi(x):
+    x=as_iv(x)
+    if x[0]<0: raise ValueError('nonnegative normal coordinate required')
+    p=parent(); c=iv(*p.inv_sqrt_2pi())
+    return mul(c,iv(p.exp_neg(x[1]**2/2)[0],p.exp_neg(x[0]**2/2)[1]))
+
+
+@lru_cache(maxsize=8192)
+def normal_tail_point(x):
+    """Enclose P(Z>x), 0<=x<=13, using signed integral-Taylor remainders."""
+    x=exact(x)
+    if not 0<=x<=13: raise ValueError('normal tail interface requires [0,13]')
+    if x==0: return iv(F(1,2))
+    S=SERIES_SCALE
+    lo=x.numerator*S//x.denominator; hi=ceildiv(x.numerator*S,x.denominator)
+    low,high=lo,hi
+    x2=x*x
+    even_high=None
+    for k in range(1,SERIES_LAST+1):
+        ratio=x2*F(2*k-1,2*k*(2*k+1))
+        lo=lo*ratio.numerator//ratio.denominator
+        hi=ceildiv(hi*ratio.numerator,ratio.denominator)
+        if k%2: low-=hi; high-=lo
+        else: low+=lo; high+=hi
+        if k==SERIES_LAST-1: even_high=high
+    if even_high is None or SERIES_LAST%2!=1:
+        raise ArithmeticError('odd/even Taylor contract violated')
+    # Odd-degree exp Taylor integrates below; even-degree integrates above.
+    integral=(max(F(0),F(low,S)),F(even_high,S))
+    if integral[1]<integral[0]: raise ArithmeticError('integral enclosure reversed')
+    c,d=parent().inv_sqrt_2pi()
+    lower=F(1,2)-d*integral[1]
+    upper=F(1,2)-c*integral[0]
+    if upper<0 or lower>F(1,2): raise ArithmeticError('tail enclosure outside probability range')
+    return iv(max(F(0),lower),min(F(1,2),upper))
+
+
+def normal_tail(x):
+    x=as_iv(x)
+    return iv(normal_tail_point(x[1])[0],normal_tail_point(x[0])[1])
+
+
+def conditional_integral(u,v):
+    """g_v(u)=E_D J(D,u); implementation domain u in [0,9], v in [199/100,3]."""
+    u=exact(u); v=as_iv(v)
+    if not 0<=u<=9 or not F(199,100)<=v[0]<=v[1]<=3:
+        raise ValueError('u in [0,9] and variance in [199/100,3] required')
+    if u==0: return iv(0)
+    s=sqrt_iv(v); a=div(u,s); a2=mul(a,a); a3=mul(a2,a)
+    first=mul(add(mul(4,a2),2),sub(phi(mul(2,a)),phi(a)))
+    second=mul(add(mul(6,a),mul(4,a3)),normal_tail(a))
+    third=mul(add(mul(6,a),mul(8,a3)),normal_tail(mul(2,a)))
+    out=div(mul(mul(v,s),sub(add(first,second),third)),6)
+    if out[1]<0: raise ArithmeticError('nonnegative conditional integral excluded')
+    return iv(max(F(0),out[0]),min(F(1,5),out[1]))
+
+
+def integrand(b,v):
+    b=exact(b); v=as_iv(v)
+    if not 0<=b<=3: raise ValueError('compact integral coordinate requires [0,3]')
+    pdf=iv(*parent().density(b,(v[0]/4,v[1]/4)))
+    return mul(2,mul(pdf,conditional_integral(b*b,v)))
+
+
+def simpson(function,end,n):
+    end=exact(end)
+    if type(n) is not int or n<2 or n%2 or end<=0:
+        raise ValueError('positive endpoint and positive even panel count required')
+    total=add(function(F(0)),function(end))
+    for k in range(1,n):
+        total=add(total,mul(4 if k%2 else 2,function(end*k/n)))
+    return mul(end/F(3*n),total)
+
+
+def derivative_bound():
+    # Proof gives <1002 uniformly on b>=0, variance [3/2,3]; use 1100.
+    return F(1100)
+
+
+def simpson_error(n):
+    if type(n) is not int or n<2 or n%2:
+        raise ValueError('positive even panel count required')
+    return derivative_bound()*3*F(3,n)**4/180
+
+
+def omitted_tail(v):
+    p=parent();lo,hi=map(exact,v)
+    if not 0<lo<=hi: raise ValueError('positive variance interval required')
+    # |B|>3 and J>0 implies D>B²>9. Independence gives a product bound.
+    d_tail=(81*hi+2*hi*hi)*p.density(9,(lo,hi))[1]/24
+    b_tail=hi*p.density(3,(lo/4,hi/4))[1]/6
+    return d_tail*b_tail
+
+
+def enclosure(n=1024):
+    if type(n) is not int: raise TypeError('integer panel count required')
+    if not 2<=n<=2048 or n%2: raise ValueError('even panels in [2,2048] required')
+    p=parent().parameters(); v=iv(*p['variance_D'])
+    raw=simpson(lambda b:integrand(b,v),F(3),n)
+    err=simpson_error(n);tail=omitted_tail(p['variance_D'])
+    gamma=(max(F(0),raw[0]-err),raw[1]+err+tail)
+    coefficient=(gamma[0]*p['p0'][0]/p['z0'][1],gamma[1]*p['p0'][1]/p['z0'][0])
+    return {'panels':n,'evaluations':n+1,'gamma':gamma,'coefficient':coefficient,
+            'quadrature_error':err,'tail':tail,'simpson_sum':raw,'parameters':p}
+
+
+def output(n):
+    value=enclosure(n); p=parent()
+    pair=lambda z:[p.decimal_bound(z[0],15),p.decimal_bound(z[1],15,True)]
+    return {'scientific_effect':'NONE','independently_reviewed':False,
+            'panels':n,'evaluations':n+1,'coefficient':pair(value['coefficient']),
+            'gamma':pair(value['gamma']),
+            'quadrature_error_gamma_upper':p.decimal_bound(value['quadrature_error'],20,True),
+            'omitted_tail_gamma_upper':p.decimal_bound(value['tail'],20,True),
+            'source_commit':'64c0a203b94105f0fccbe6f8116a94e13431f84e',
+            'method':'analytic D integration; composite Simpson with proved |f4|<=1100; rational outward arithmetic',
+            'scope':'leading coefficient only; d2 L24 b6/5 original axes and pins; no finite-r remainder or radius'}
+
+
+def main():
+    parser=argparse.ArgumentParser(description=__doc__)
+    parser.add_argument('--panels',type=int,default=1024)
+    args=parser.parse_args()
+    try: result=output(args.panels)
+    except (ValueError,TypeError,ArithmeticError,OSError) as exc:
+        print('ONED_FAIL: '+str(exc),file=sys.stderr);return 1
+    print(json.dumps(result,sort_keys=True));return 0
+
+if __name__=='__main__':sys.exit(main())