From 6a2abb7a9bd8facecebca52de0b32d371645bfa5 Mon Sep 17 00:00:00 2001 From: Dylan Roy <249851642+d6g8k5htny-coder@users.noreply.github.com> Date: Tue, 6 Oct 2026 07:05:22 -0700 Subject: [PATCH 1/6] LM006 coefficient: analytic Gaussian reduction and certified Simpson enclosure MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Five additive numerical/proof/test files; hash-bound existing parent arithmetic. No prior proof, numerical result, workflow, Lean or status change. Dylan Roy — delegated AI work; actual OpenAI / GPT-6 Astra Pro, coefficient-dimension-reduction-20261006-1340-a62c. Scientific effect NONE; new nonauthor review pending. --- .../NOTE.md | 310 ++++++++++++++++++ .../RESULTS.json | 1 + .../SOURCES.json | 60 ++++ .../oned.py | 223 +++++++++++++ .../test_oned.py | 189 +++++++++++ 5 files changed, 783 insertions(+) create mode 100644 coefficients/lm006_wrong_sign_oned_20261006_a62c/NOTE.md create mode 100644 coefficients/lm006_wrong_sign_oned_20261006_a62c/RESULTS.json create mode 100644 coefficients/lm006_wrong_sign_oned_20261006_a62c/SOURCES.json create mode 100644 coefficients/lm006_wrong_sign_oned_20261006_a62c/oned.py create mode 100644 coefficients/lm006_wrong_sign_oned_20261006_a62c/test_oned.py diff --git a/coefficients/lm006_wrong_sign_oned_20261006_a62c/NOTE.md b/coefficients/lm006_wrong_sign_oned_20261006_a62c/NOTE.md new file mode 100644 index 000000000..db27645e6 --- /dev/null +++ b/coefficients/lm006_wrong_sign_oned_20261006_a62c/NOTE.md @@ -0,0 +1,310 @@ +# LM006 coefficient: analytic dimension reduction and a certified one-dimensional enclosure + +Dylan Roy — delegated AI mathematical/numerical work. Actual author OpenAI / +GPT-6 Astra Pro, `coefficient-dimension-reduction-20261006-1340-a62c`, claim +Math-362/6017509107. Scientific effect NONE; organizational-independence credit0. +This is a new additive numerical candidate requiring its own source review. +No historical proof, numerical result, review disposition or Lean target changes. + +## 1. Exact object and relation to existing work + +Consume #358's coefficient definition at commit +`64c0a203b94105f0fccbe6f8116a94e13431f84e`, NOTE blob +`ea914c1b8e0b8180b645f3f626e2081ab87700b9`, in +`reviews/lm006_wrong_sign_asymptotic_20261006/`. For the fixed original-axis +periodized field d=2,L=24,b=6/5 with its six pins and gap r^3/6, it states + + C = p0 Gamma/z0, Gamma=E[J(D,B^2)], + D~N(0,v), B~N(0,v/4) independently, + Q~N(-m2*b,delta), z0=E(Q_-)^2, p0=density_Q(0), + delta=m4-m2^2, v=m2*delta, + J(d,u)=int_0^{d_+}(d-u-t)_+(u-t)_+ dt, u>=0. (1) + +These are UNTILTED Gaussian inputs defining a coefficient of the determinant- +tilted sign probability. Independence after tilting is not asserted. This note +neither re-proves #358's limit theorem nor turns C*r^3 into a finite-r bound. +There is no numerical asymptotic remainder, radius, arbitrary orientation/mark +extension, or capture/elder/persistence conclusion. + +#362's original packet `coefficients/lm006_wrong_sign_20261006_r20/` at +`1f64b8f8ee450262e0f56e6bdf9dfb37931f48c6` supplies reviewed interval arithmetic, +the actual periodic-moment enclosure and p0,z0 parameter bounds. Its five files +are unchanged on its actual landing `4fe1d6762db8faa13859c4eeda0167b3c65ac069`. +We load only its exact7215-byte enclose.py, blob +`e680ddb7aa0abd4b6aab2cac6a54c1ff28efc782`, SHA256 +`157e02ee22699b4fa2efdde1894824b92b962900dbb8da9bd65acee41ae91e88`. +The same bytes are authenticated then compiled, not checked and later reread. +The parent is trusted code, not made into a hostile-code sandbox by hashing. +Leaf symlinks/nonregular files reject; hostile ancestor resolution and external +future disk immutability are not claimed. The cached module retains the actual +verified in-memory code. + +#372 already refines the parent's two-dimensional rectangle sum by exact zero- +cell pruning. It has a reviewed4096 result and separately owned8192 execution. +Neither that source nor its outputs are changed, imported or re-executed here. +The present contribution integrates D out analytically, proves a uniform fourth- +derivative bound for the remaining smooth integrand, and uses Simpson's rule +with an explicit error, not agreement between grids. Gaussian truncated moments +and Simpson integration are classical methods; no general novelty is claimed. + +## 2. Analytic integration over D + +Write s=sqrt(v), phi for the standard normal density and T=1-Phi. For u>=0, +Tonelli gives + + g_v(u):=E_D J(D,u) + =int_0^u (u-t) E[(D-u-t)_+] dt + =int_u^{2u}(2u-a)[s phi(a/s)-a T(a/s)] da. (2) + +The first equality uses that the original positive parts restrict t to[0,u] +and D>u+t. In particular no factor involving B's density has entered yet. +For a=u/s, explicit integration yields + + g_v(u)=s^3/6 * { + (4a^2+2)[phi(2a)-phi(a)] + +(6a+4a^3)T(a) -(6a+8a^3)T(2a) }. (3) + +An independent derivation specifies every coefficient. On u=2u, J(d,u)=u^2 d/2-2u^3/3; elsewhere it is zero. +The truncated Gaussian moments at threshold t, x=t/s, are + + M0(t)=T(x), M1(t)=s phi(x), + M2(t)=s^2[x phi(x)+T(x)], + M3(t)=s^3[(x^2+2)phi(x)]. + +These follow by integration by parts from phi'=-x phi. Integrating the two +polynomials over[u,2u] and[2u,infinity) with these moments simplifies to(3). +At u=0 both expressions give0. Formula(3) extends analytically across u=0, +which supplies all right derivatives used below. The clipped polynomial J +itself need not have four continuous derivatives. + +By symmetry of B, retain BOTH its variance v/4 and the folding factor2: + + Gamma=int_0^infinity F_v(b) db, + F_v(b)=2 f_B(b) g_v(b^2), + f_B(b)=c exp(-alpha b^2), c=2/(s sqrt(2pi)), alpha=2/v. (4) + +This is an exact one-dimensional integral, not an approximation of the other +Gaussian integral by a fitted curve. + +## 3. A uniform fourth-derivative bound + +The following estimates hold on the COARSE range 3/2<=v<=3 and u>=0. +They apply in particular to every actual parameter in the narrower parent box. +Denote derivatives of g_v with respect to u by g',...,g''''. Then + + |g|<=1/5, |g'|<=3/16, |g''|<=3/4, + |g'''|<=9/4, |g''''|<=29/4. (5) + +Here is a proof, not a sampled derivative maximum. For d>0, J as a function of +u has maximum d^3/24 at u=d/2. Its first derivative has absolute value at most +d^2/8. It is C1 across its clipping thresholds, and that first derivative is +Lipschitz with constant d, since each piece has |J''|<=d. These bounds justify +differentiating the Gaussian expectation through order2 by dominated difference +quotients (or absolute continuity plus domination). Therefore + + |g|<=s^3/(12 sqrt(2pi)), |g'|<=v/16, + |g''|<=s/sqrt(2pi), + +which give the first three estimates in(5) for v<=3. Direct differentiation of +(3), remembering a=u/s, gives + + g'''(u)=4T(a)-8T(2a)-a phi(a), + g''''(u)=[16phi(2a)+(a^2-5)phi(a)]/s. (6) + +Because 0<=T(2a)<=T(a)<=1/2, the first two terms of g''' lie in[-2,2]. +Also max_{a>=0} a phi(a)=1/sqrt(2pi e)<1/4, using pi>3,e>8/3. For g'''', +max a^2 phi(a)=2phi(0)/e, and phi(0)/s<1/3 for v>=3/2. Thus its magnitude +is less than(21+3/4)/3=29/4. Degenerate clipping endpoints do not require +exceptional-point exclusions, since g has the analytic representation(3). + +The exact product/chain differentiation of(4) is + + F_v''''(b)=2c exp(-alpha b^2) * [ + (16alpha^4 b^4-48alpha^3 b^2+12alpha^2) g + +(144alpha^2 b^2-64alpha^3 b^4-24alpha) g' + +(96alpha^2 b^4-144alpha b^2+12) g'' + +(-64alpha b^4+48b^2) g''' +16b^4 g'''' ], (7) + +with all g derivatives evaluated at b^2. The exact rational polynomial tests +independently differentiate both(3) and exp(-alpha b^2)g(b^2), verifying every +coefficient in(6),(7). For 2/3<=alpha<=4/3, + + sup b^2 exp(-alpha b^2)<=1/(2alpha), + sup b^4 exp(-alpha b^2)<=1/alpha^2, c<=2/3. + +These use e>2. Taking absolute values separately in(7), the bracket multiplied +by its exponential is bounded by + + 52alpha^2 G0 +160alpha G1+180G2+88G3/alpha+16G4/alpha^2, + +where G_j are the five constants in(5). Consequently + + sup_{b>=0,3/2<=v<=3}|F_v''''(b)| + <=(4/3)[832/45+40+135+297+261]<1002<1100. (8) + +The deliberately rounded constant1100 is uniform on the WHOLE stated variance +range, not only at v=2. Neither this bound nor the leading coefficient is claimed +optimal. The code uses1100 without attempting a numerical derivative maximum. + +## 4. Compact quadrature and a smaller support-aware tail + +On[0,3] use the classical composite Simpson rule with EVEN panel count n, +spacing h=3/n. NIST DLMF3.5.7–3.5.8 gives, for F in C4, + absolute error <=(3/180)h^4 sup|F''''|. +The assumptions were proved above. Thus + + E_n=1485/n^4 (9) + +is a valid uniform quadrature error for every permitted v. Every evaluated +node is enclosed by rational intervals. Simpson's coefficients are positive, +so the lower and upper weighted sums enclose the exact Simpson sum, without +assuming monotonicity in v. Subtract E_n from the lower endpoint and add it to +the upper endpoint. No agreement between resolutions enters this proof. + +For the omitted part |B|>3, the support condition J(D,B^2)>0 forces D>B^2>9. +Since J<=D_+^3/24 and D,B are independent BEFORE tilting, + + Gamma_tail <= (1/24) E[D^3;D>9] P(|B|>3). (10) + +Gaussian integration by parts and the two-sided Mills bound give + E[D^3;D>9]=(81v+2v^2)f_D(9), + P(|B|>3)<= (v/6) f_B(3). + +For a parameter interval [v_-,v_+], evaluate the polynomial factors at v_+ and +use valid upper density bounds from the parent. Their product is the tail tau. +This is not a bound obtained by dropping the D>B^2 support condition. The +rectangle D in[12,13], B in[3,13/4] also has strictly positive integrand and +positive density lower bounds, proving that the omitted integral is not zero. +The tests verify its explicit lower bound is below the proposed upper tail. +The tail is ADDED ONLY to the upper Gamma endpoint. + +For this parameter box, the outward decimal upper tail is + + tau <= 0.00000000000007444285. + +A fixed b cutoff therefore imposes a tail floor on eventual accuracy; increasing +n alone would not establish an arbitrarily accurate enclosure. + +## 5. Exact intervals and stable treatment of the normal tail + +The parent proves for epsilon=10^-24 the actual image-corrected bounds + m2 in[1-epsilon,1], m4 in[3,3+epsilon]. Its actual parameter code computes + delta and v=m2 delta outward, together with positive p0,z0 intervals. We use +THOSE intervals, not the nonperiodic values m2=1,m4=3. In particular v's lower +endpoint is slightly below2; claiming v>=2 would be wrong. The interval lies +inside[199/100,3], a subset of the coarse derivative domain[3/2,3]. + +The parent Machin/pi, nonnegative exponential, density and square-root bounds +are hash-bound prerequisites already derived/reviewed there. This note does +not transfer its predecessor's verdict to new code. New interval add/subtract/ +multiply/divide operations take all appropriate endpoint extrema and round +outward at scale10^36, using integer floor/ceiling. Denominators containing0 +reject. Fraction operations have no binary64 conversion on the production path. + +The parent normal CDF interface only handles arguments in[0,1]. It is NOT used +outside that domain. We introduce a normal upper-tail enclosure for 0<=x<=13. +Taylor's integral remainder for exp(-y), y>=0, shows that its odd partial +polynomial is below exp(-y) and its even partial polynomial is above it for +all y>=0. This fact does NOT require that the early alternating terms decrease. +Integrating at y=t^2/2 from0 to x gives + + I_331(x) <= I(x):=int_0^x exp(-t^2/2)dt <= I_330(x), + I_N(x)=sum_{k=0}^N (-1)^k x^(2k+1)/(2^k k!(2k+1)). (11) + +The positive term magnitudes satisfy + t0=x, t_k/t_{k-1}=x^2(2k-1)/[2k(2k+1)]. +The implementation encloses each magnitude at internal scale10^100 and adds +with alternating signs and outward endpoints. All recurrence multipliers are +nonnegative, so induction bounds every term and signed partial sum. It retains +the LOWER endpoint of the final odd sum and the UPPER endpoint of the preceding +even sum. Known I>=0 permits clipping the lower side at0. From the parent +interval for c0=1/sqrt(2pi), form + + T(x) in[1/2-c0_upper*I_upper, 1/2-c0_lower*I_lower], + +intersect with the known[0,1/2], then round outward. Evaluating T on an interval +uses its monotonicity with opposite endpoints. Formula(11) and tracked rounding, +not a floating erfc call or cancellation estimate, are the certificate. Large +intermediate terms can cancel without losing enclosure because integer/Fraction +arithmetic and directed bounds are used. Extremely small tails may have lower +endpoint0; this is legitimate and not replaced by a signed negative probability. + +The implementation only requires u in[0,9] and v in[199/100,3], so the largest +argument 2u/s is below13. It enforces those domains. The formula for g is evaluated +with signed interval arithmetic; intersecting with the independently proved +0<=g<=1/5 is valid and improves cancellation at small values. A cache contains +only already computed exact argument enclosures. Parent authentication uses the +same byte buffer for hashing and compilation; it provides identity, not a general +source sandbox or a guarantee against mutable ancestor directories. + +## 6. Result, test history and precise exclusions + +For n=1024, the two completed author commands produce the inclusive enclosure + + 0.001321995248726 <= C_(24,6/5) <= 0.001321995413271. (12) + +The final assembly is + Gamma in[max(0,S_lower-E_n), S_upper+E_n+tau], + C in[Gamma_lower*p0_lower/z0_upper, + Gamma_upper*p0_upper/z0_lower]. + +The Gamma interval is[0.021702757242874,0.021702759944149]. The quadrature +error upper is0.00000000135059963214. These displayed decimals themselves +are rounded outward, not nearest. RESULTS.json retains independently_reviewed=false +as immutable author-execution history. It is not changed automatically by a +later technical review or CI pass. + +There are1025 interval-valued node evaluations, each using analytic Gaussian +moments and bounded series, rather than millions of two-dimensional cells. +This is an algorithmic count, NOT a controlled wallclock benchmark against the +other implementations or hardware. Bounds nest within the prior2048/4096/8192 +records as a corroboration; such nesting is not the proof of(12). No source or +execution of #372 is claimed by this packet. + +Reproduction from this directory, with the unchanged parent at its repository path: + + python -B -S test_oned.py + python -B -O -S test_oned.py + python -B -S oned.py --panels 1024 + python -B -O -S oned.py --panels 1024 + +The initial12 methods produced12 intended missing-implementation assertions in +each mode and zero errors. After implementation those12 passed; additional +independent coefficient/assembly and truncated-moment controls make15 final +methods. Tests include independent unrounded335/334 integral-series enclosures, +exact symbolic third/fourth derivatives and all12 product-derivative coefficients, +exact rational Simpson identities, signed outward operations and B scaling, +the nonzero tail and opposite-normalizer attachment. A few math.erfc and midpoint +comparisons are explicitly binary64 SANITY checks in tests only, not premises of +the certificate. Tests neither numerically maximize the fourth derivative nor +replace the written proof by a grid. + +Eight isolated source variants each fail the same complete15-method suite in +normal and optimized modes, with intended assertion sets and zero errors: +missing symmetry, wrong B variance, halved integrated kernel, wrong Simpson +weights, omitted upper tail, wrong normalizer endpoint, inward interval rounding, +and wrong lower-error sign. These check the implemented proof contract; an +omitted tiny tail can leave a decimal interval containing the answer by accident, +which would not make that proof-contract change sound. No result is learned from +the variant under test. The combined campaign's outer60-second tool deadline +occurred after15 completed records; its final optimized variant was completed +separately. Original streams and the interruption remain retained, not labeled +as an uninterrupted16-process run. + +Existing general CI does NOT automatically run these standalone files. No new +workflow, Lean target, full local checkout, full historical-archive replay, or +formal independent alignment is claimed. Direct local GitHub access was unavailable; +the recovered parent was authenticated to native source identities. A new +nonauthor numerical/source read must check this reduction, bounds, signed series, +exact code, domains and actual executions. #362's source review does not cover +this successor. General publication CI, if successful, remains separate. + +Classical references checked: NIST DLMF3.5(ii), equations3.5.7–3.5.8 +(https://dlmf.nist.gov/3.5#ii) for composite Simpson and its C4 remainder; +DLMF7.6(i) (https://dlmf.nist.gov/7.6#i) for error-function power-series context. +The signed finite truncation directions needed here were proved directly above. +No new general quadrature/stability principle, complete literature review, +finite-r probability or numerical radius, non-axial product decomposition, or +full-field capture/elder/persistence theorem is asserted. diff --git a/coefficients/lm006_wrong_sign_oned_20261006_a62c/RESULTS.json b/coefficients/lm006_wrong_sign_oned_20261006_a62c/RESULTS.json new file mode 100644 index 000000000..506833403 --- /dev/null +++ b/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"} diff --git a/coefficients/lm006_wrong_sign_oned_20261006_a62c/SOURCES.json b/coefficients/lm006_wrong_sign_oned_20261006_a62c/SOURCES.json new file mode 100644 index 000000000..a6de8d411 --- /dev/null +++ b/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" +} diff --git a/coefficients/lm006_wrong_sign_oned_20261006_a62c/oned.py b/coefficients/lm006_wrong_sign_oned_20261006_a62c/oned.py new file mode 100644 index 000000000..5015dee3a --- /dev/null +++ b/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,'','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]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 03 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()) diff --git a/coefficients/lm006_wrong_sign_oned_20261006_a62c/test_oned.py b/coefficients/lm006_wrong_sign_oned_20261006_a62c/test_oned.py new file mode 100644 index 000000000..62e544227 --- /dev/null +++ b/coefficients/lm006_wrong_sign_oned_20261006_a62c/test_oned.py @@ -0,0 +1,189 @@ +"""Exact/algebraic and numerical sanity controls; not a Lean or field proof.""" +from fractions import Fraction as F +from pathlib import Path +import hashlib, importlib.util, math, subprocess, sys, unittest + +P = Path(__file__).with_name('oned.py') + +class OneDimensionalTests(unittest.TestCase): + def setUp(self): + self.assertTrue(P.is_file(), 'one-dimensional implementation not supplied') + spec=importlib.util.spec_from_file_location('oned',P) + self.m=importlib.util.module_from_spec(spec); spec.loader.exec_module(self.m) + + def test_interval_arithmetic(self): + m=self.m + for a,b,c,d in [(-2,1,3,4),(-3,-1,-4,-2),(0,2,1,3)]: + x,y=m.iv(a,b),m.iv(c,d) + for u in (F(a),F(a+b,2),F(b)): + for v in (F(c),F(c+d,2),F(d)): + for z,val in [(m.add(x,y),u+v),(m.sub(x,y),u-v),(m.mul(x,y),u*v)]: + self.assertLessEqual(z[0],val); self.assertLessEqual(val,z[1]) + for v in (F(1,7),F(-1,7),F(2,3),F(-13,17)): + z=m.iv(v) + self.assertLessEqual(z[0],v); self.assertLessEqual(v,z[1]) + self.assertLessEqual(z[1]-z[0],F(1,m.SCALE)) + with self.assertRaises(ValueError): m.div(m.iv(1),m.iv(-1,1)) + with self.assertRaises(TypeError): m.iv(True) + + def test_parent_authentication(self): + raw=self.m.parent_bytes() + self.assertEqual(len(raw),7215) + self.assertEqual(hashlib.sha256(raw).hexdigest(),self.m.PARENT_SHA) + with self.assertRaises(ValueError): self.m.authenticate(raw+b'\n') + self.assertEqual(self.m.parent().j(3,1),F(5,6)) + + def test_tail_exact_series(self): + # Independently sum unrounded terms. These narrower exact partial sums + # must fit inside the wider fixed-point implementation enclosure. + m=self.m + c=m.parent().inv_sqrt_2pi() + for x in (F(0),F(1,2),F(1),F(4),F(8),F(13)): + term=total=x + for k in range(1,336): + term *= -x*x*F(2*k-1,2*k*(2*k+1)); total += term + lower=F(1,2)-c[1]*(total-term) + upper=F(1,2)-c[0]*total + got=m.normal_tail_point(x) + self.assertLessEqual(got[0],max(0,lower)) + self.assertGreaterEqual(got[1],min(F(1,2),upper)) + self.assertLessEqual(got[1]-got[0],F(1,10**28)) + + def test_tail_sanity_and_domain(self): + for x in (0,F(1,4),1,2,4,8,13): + lo,hi=self.m.normal_tail_point(F(x)); expected=math.erfc(float(x)/math.sqrt(2))/2 + self.assertLessEqual(float(lo)-1e-15,expected) + self.assertLessEqual(expected,float(hi)+1e-15) + for x in (-1,14): + with self.assertRaises(ValueError): self.m.normal_tail_point(F(x)) + + def test_exact_fourth_derivative_algebra(self): + # Polynomial coefficient maps for h(a), in basis phi(a),phi(2a),T(a),T(2a). + def trim(p): return {k:v for k,v in p.items() if v} + def add(p,q): + r=dict(p) + for k,v in q.items(): r[k]=r.get(k,F(0))+v + return trim(r) + def scale(p,s,shift=0): return trim({k+shift:v*s for k,v in p.items()}) + def derivative(p): return {k-1:k*v for k,v in p.items() if k} + h=[{0:-F(1,3),2:-F(2,3)},{0:F(1,3),2:F(2,3)}, + {1:F(1),3:F(2,3)},{1:-F(1),3:-F(4,3)}] + def step(a): + out=[derivative(p) for p in a] + out[0]=add(add(out[0],scale(a[0],-1,1)),scale(a[2],-1)) + out[1]=add(add(out[1],scale(a[1],-4,1)),scale(a[3],-2)) + return out + for _ in range(3): h=step(h) + self.assertEqual(h,[{1:F(-1)}, {}, {0:F(4)}, {0:F(-8)}]) + h=step(h) + self.assertEqual(h,[{0:F(-5),2:F(1)},{0:F(16)}, {}, {}]) + self.assertEqual(self.m.derivative_bound(),F(1100)) + self.assertLess(F(4,3)*(F(832,45)+40+135+297+261),1100) + + def test_conditional_formula_against_positive_integral(self): + # Binary64 midpoint integration is a SANITY SCREEN, not certification. + m=self.m + for u in (F(1,8),F(1,2),1,2,4,8): + got=m.conditional_integral(F(u),m.iv(2)) + s=math.sqrt(2); n=4000; dx=float(u)/n + h=lambda a:s*math.exp(-a*a/4)/math.sqrt(2*math.pi)-a*math.erfc(a/2)/2 + approx=sum((float(u)-((i+0.5)*dx))*h(float(u)+(i+0.5)*dx) for i in range(n))*dx + self.assertLessEqual(abs((float(got[0])+float(got[1]))/2-approx),1e-8) + self.assertEqual(m.conditional_integral(F(0),m.iv(2)),m.iv(0)) + + def test_reduction_from_truncated_moments(self): + # Independent expression: integrate the two polynomial branches of J + # against moments M0..M3 on [u,2u] and [2u,infinity). + m=self.m;v=m.iv(2);sd=m.sqrt_iv(v) + def moments(t): + x=m.div(t,sd);ph=m.phi(x);tail=m.normal_tail(x) + return [tail,m.mul(sd,ph),m.mul(v,m.add(m.mul(x,ph),tail)), + m.mul(m.mul(v,sd),m.mul(m.add(m.mul(x,x),2),ph))] + for u in (F(1,4),F(1),F(2),F(4),F(8)): + a,b=moments(u),moments(2*u);d=[m.sub(x,y) for x,y in zip(a,b)] + first=m.div(m.add(m.sub(m.mul(6*u,d[2]),d[3]), + m.sub(m.mul(4*u**3,d[0]),m.mul(9*u*u,d[1]))),6) + second=m.sub(m.mul(u*u/2,b[1]),m.mul(2*u**3/3,b[0])) + separate=m.add(first,second);direct=m.conditional_integral(u,v) + self.assertLessEqual(max(separate[0],direct[0]),min(separate[1],direct[1])) + + def test_simpson_weights_and_error(self): + m=self.m + for n in (2,4,8,16): + for degree in range(4): + z=m.simpson(lambda x:m.iv(x**degree),F(3),n) + target=F(3**(degree+1),degree+1) + self.assertLessEqual(z[0],target);self.assertLessEqual(target,z[1]) + z=m.simpson(lambda x:m.iv(x**4),F(3),n) + error=abs(z[1]-F(3**5,5)) + self.assertLessEqual(error,24*3*F(3,n)**4/180+F(1,10**30)) + self.assertEqual(m.simpson_error(n),F(1485,n**4)) + + def test_tail_is_present_and_small(self): + p=self.m.parent().parameters();tail=self.m.omitted_tail(p['variance_D']) + self.assertGreater(tail,0); self.assertLess(tail,F(1,10**12)) + # It is stricter than ignoring the support condition D>B^2. + v=p['variance_D'][1]; pdfD=self.m.parent().density(9,p['variance_D'])[1] + pdfB=self.m.parent().density(3,(p['variance_D'][0]/4,v/4))[1] + self.assertEqual(tail,(81*v+2*v*v)*pdfD/24 *v*pdfB/6) + + def test_nonzero_integrand_and_scaling(self): + m=self.m + for b in (F(1,4),F(1,2),1,F(3,2)): + z=m.integrand(b,m.iv(2)); self.assertGreater(z[0],0) + density=m.iv(*m.parent().density(b,(F(1,2),F(1,2)))) + expected=m.mul(2,m.mul(density,m.conditional_integral(b*b,m.iv(2)))) + self.assertEqual(z,expected) + self.assertEqual(m.integrand(0,m.iv(2)),m.iv(0)) + self.assertGreater(m.conditional_integral(F(1),m.iv(2))[0],F(1,100)) + + def test_low_resolution_is_genuine_enclosure(self): + m=self.m;result=m.enclosure(32) + self.assertLessEqual(result['coefficient'][0],F(1322,10**6)) + self.assertGreaterEqual(result['coefficient'][1],F(1322,10**6)) + self.assertGreater(result['quadrature_error'],0) + self.assertLessEqual(result['gamma'][0],result['gamma'][1]) + + def test_error_tail_and_quotient_attachment(self): + m=self.m; r=m.enclosure(8);p=r['parameters'] + self.assertEqual(r['gamma'][0],max(F(0),r['simpson_sum'][0]-r['quadrature_error'])) + self.assertEqual(r['gamma'][1],r['simpson_sum'][1]+r['quadrature_error']+r['tail']) + self.assertEqual(r['coefficient'],(r['gamma'][0]*p['p0'][0]/p['z0'][1],r['gamma'][1]*p['p0'][1]/p['z0'][0])) + lower_j=m.parent().cell_bounds(12,13,9,F(169,16))[0] + lower_tail=F(1,2)*lower_j*m.parent().density(13,p['variance_D'])[0]*m.parent().density(F(13,4),(p['variance_D'][0]/4,p['variance_D'][1]/4))[0] + self.assertGreater(lower_tail,0);self.assertLess(lower_tail,r['tail']) + for u,v in [(10,m.iv(2)),(1,m.iv(F(3,2))),(1,m.iv(4))]: + with self.assertRaises(ValueError):m.conditional_integral(u,v) + + def test_product_derivative_identity(self): + # d/db(exp(-alpha*b²) * g(b²)); symbolic polynomial coefficients. + terms={(0,0,0):F(1)} + for _ in range(4): + new={} + def acc(key,value):new[key]=new.get(key,F(0))+value + for (k,a,j),c in terms.items(): + if k:acc((k-1,a,j),k*c) + acc((k+1,a,j+1),2*c) + acc((k+1,a+1,j),-2*c) + terms={k:v for k,v in new.items() if v} + expected={(4,4,0):16,(2,3,0):-48,(0,2,0):12, + (2,2,1):144,(4,3,1):-64,(0,1,1):-24, + (4,2,2):96,(2,1,2):-144,(0,0,2):12, + (4,1,3):-64,(2,0,3):48,(4,0,4):16} + self.assertEqual(terms,expected) + + def test_invalid_resolution(self): + for n in (True,0,1,3,5000): + with self.assertRaises((TypeError,ValueError)): self.m.enclosure(n) + + def test_cli(self): + for flags in (['-B','-S'],['-B','-O','-S']): + p=subprocess.run([sys.executable,*flags,str(P),'--panels','16'],capture_output=True,timeout=40) + self.assertEqual(p.returncode,0,p.stderr); self.assertEqual(p.stderr,b'') + for args in (['--panels','3'],['--bogus']): + p=subprocess.run([sys.executable,'-B','-S',str(P),*args],capture_output=True,timeout=20) + self.assertEqual(p.returncode,1 if args[0]=='--panels' else 2) + if args[0]=='--panels': + self.assertEqual(p.stderr,b'ONED_FAIL: even panels in [2,2048] required\n') + +if __name__=='__main__':unittest.main() From 8fe14358a1ee5d7ef7d7e20520391f62f432fe04 Mon Sep 17 00:00:00 2001 From: Dylan Roy <249851642+d6g8k5htny-coder@users.noreply.github.com> Date: Tue, 6 Oct 2026 07:10:57 -0700 Subject: [PATCH 2/6] Credit prior one-dimensional identity; preserve the frozen numerical packet Add PRIOR_WORK.md only. The original five proof/code/result/source files, assumptions and executions are unchanged. New contribution is the derivative and Simpson-error certificate plus actual narrower enclosure, not first publication of the reduction identity. Scientific effect NONE. --- .../PRIOR_WORK.md | 40 +++++++++++++++++++ 1 file changed, 40 insertions(+) create mode 100644 coefficients/lm006_wrong_sign_oned_20261006_a62c/PRIOR_WORK.md diff --git a/coefficients/lm006_wrong_sign_oned_20261006_a62c/PRIOR_WORK.md b/coefficients/lm006_wrong_sign_oned_20261006_a62c/PRIOR_WORK.md new file mode 100644 index 000000000..1fb9afde1 --- /dev/null +++ b/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). From 268156ab71fa6bbada01b1e2c21c5c0f51b7d94b Mon Sep 17 00:00:00 2001 From: Dylan Roy <249851642+d6g8k5htny-coder@users.noreply.github.com> Date: Tue, 6 Oct 2026 09:18:10 -0700 Subject: [PATCH 3/6] LM006: add source-bound one-dimensional coefficient replay Three engineering files only: replay driver, focused controls and dedicated workflow for the frozen PR380 1024-panel certificate. No proof, result, scientific register, Lean source or parent packet changes. Scientific effect NONE. --- .github/workflows/lm006-oned-coefficient.yml | 60 +++++++++ tests/test_lm006_oned_coefficient_replay.py | 130 +++++++++++++++++++ tools/lm006_oned_coefficient_replay.py | 127 ++++++++++++++++++ 3 files changed, 317 insertions(+) create mode 100644 .github/workflows/lm006-oned-coefficient.yml create mode 100644 tests/test_lm006_oned_coefficient_replay.py create mode 100644 tools/lm006_oned_coefficient_replay.py diff --git a/.github/workflows/lm006-oned-coefficient.yml b/.github/workflows/lm006-oned-coefficient.yml new file mode 100644 index 000000000..2f0fa91e6 --- /dev/null +++ b/.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 diff --git a/tests/test_lm006_oned_coefficient_replay.py b/tests/test_lm006_oned_coefficient_replay.py new file mode 100644 index 000000000..98c1b52bf --- /dev/null +++ b/tests/test_lm006_oned_coefficient_replay.py @@ -0,0 +1,130 @@ +"""Execution/custody controls for the frozen PR380 one-dimensional coefficient.""" +import importlib.util, json, os, subprocess, sys, tempfile, time, unittest +from pathlib import Path + +DRIVER=Path(__file__).resolve().parents[1]/'tools/lm006_oned_coefficient_replay.py' + +class ReplayTests(unittest.TestCase): + def setUp(self): + self.assertTrue(DRIVER.is_file(),'replay implementation missing') + spec=importlib.util.spec_from_file_location('oned_replay',DRIVER) + self.m=importlib.util.module_from_spec(spec);spec.loader.exec_module(self.m) + self.tmp=tempfile.TemporaryDirectory();self.addCleanup(self.tmp.cleanup) + self.root=Path(self.tmp.name)/'repo';self.root.mkdir();self.logs=Path(self.tmp.name)/'logs';self.logs.mkdir() + + def fixture(self): + pins={} + for name in self.m.PINS: + p=self.root/name;p.parent.mkdir(parents=True,exist_ok=True);p.write_bytes(('fixture:'+name+'\n').encode()) + pins[name]=self.m.git_blob(p.read_bytes()) + return pins + + def child(self, code, expected=b'ok\n', timeout=3, name='child'): + return self.m.run_step([sys.executable,'-B','-S','-c',code],self.root,self.logs,name,expected,'exact',timeout) + + def test_snapshot_and_exact_packet_membership(self): + pins=self.fixture();ids=self.m.validate_snapshot(self.root,pins) + self.assertEqual(set(ids),set(pins)) + extra=self.root/self.m.PACKET/'extra';extra.write_text('x') + with self.assertRaisesRegex(self.m.ReplayError,'packet_membership'): self.m.validate_snapshot(self.root,pins) + + def test_changed_missing_and_symlink_sources_rejected(self): + pins=self.fixture();name=next(iter(pins));p=self.root/name;old=p.read_bytes() + p.write_bytes(old+b'x') + with self.assertRaisesRegex(self.m.ReplayError,'source_identity'): self.m.validate_snapshot(self.root,pins) + p.unlink() + with self.assertRaisesRegex(self.m.ReplayError,'source_missing'): self.m.validate_snapshot(self.root,pins) + p.write_bytes(old); outside=Path(self.tmp.name)/'outside';outside.write_bytes(old);p.unlink();p.symlink_to(outside) + with self.assertRaisesRegex(self.m.ReplayError,'source_symlink'): self.m.validate_snapshot(self.root,pins) + + def test_path_validation(self): + for name in ('../x','/x','a/../b','a//b','a\\b','a/./b',''): + with self.assertRaises(self.m.ReplayError): self.m.source_file(self.root,name) + + def test_success_process_record(self): + row=self.child("print('ok')");self.assertEqual(row['status'],'PASS');self.assertFalse(row['timed_out']) + self.assertEqual((self.logs/'child.stdout').read_bytes(),b'ok\n') + + def test_wrong_exit_output_and_stderr_rejected(self): + cases=[("raise RuntimeError('x')",'unexpected_exit'),('pass','stdout_mismatch'),("print('bad')",'stdout_mismatch'),("import sys;print('ok');print('w',file=sys.stderr)",'unexpected_stderr')] + for i,(code,reason) in enumerate(cases): + with self.assertRaisesRegex(self.m.ReplayError,reason): self.child(code,name='bad'+str(i)) + + def test_timeout_retains_partial_evidence(self): + with self.assertRaisesRegex(self.m.ReplayError,'timeout'): + self.child("import sys,time;print('s',flush=True);print('e',file=sys.stderr,flush=True);time.sleep(10)",timeout=.2) + row=json.loads((self.logs/'child.process.json').read_text());self.assertTrue(row['timed_out']);self.assertEqual(row['failure'],'timeout') + + def test_existing_evidence_not_overwritten(self): + self.child("print('ok')");before={p.name:p.read_bytes() for p in self.logs.iterdir()} + with self.assertRaisesRegex(self.m.ReplayError,'step_evidence_exists'): self.child("print('changed')") + self.assertEqual(before,{p.name:p.read_bytes() for p in self.logs.iterdir()}) + + def test_test_report_contract_requires_all_named_passes(self): + good=('\n'.join(n+' (test_oned.OneDimensionalTests.'+n+') ... ok' for n in self.m.TEST_NAMES)+'\n\n'+'-'*70+'\nRan 15 tests in 0.001s\n\nOK\n').encode() + self.m.check_output(b'',good,None,'tests') + for bad in (good.replace(b' ... ok',b' ... FAIL',1),good+b'noise',good.replace(b'Ran 15',b'Ran 0')): + with self.assertRaisesRegex(self.m.ReplayError,'test_report_mismatch'): self.m.check_output(b'',bad,None,'tests') + + def test_exact_output_contract_is_byte_exact(self): + want=b'{"panels":1024,"independently_reviewed":false}\n';self.m.check_output(want,b'',want,'exact') + for bad in (b'',want+b'\n',want.replace(b'false',b'true')): + with self.assertRaisesRegex(self.m.ReplayError,'stdout_mismatch'): self.m.check_output(bad,b'',want,'exact') + + def test_host_identity(self): + h='1'*40;env={'GITHUB_ACTIONS':'true','GITHUB_REPOSITORY':self.m.REPOSITORY,'GITHUB_SHA':h,'GITHUB_RUN_ID':'1','GITHUB_RUN_ATTEMPT':'2'} + self.m.host_identity(h,env) + env['GITHUB_SHA']='2'*40 + with self.assertRaisesRegex(self.m.ReplayError,'host_identity'): self.m.host_identity(h,env) + + def test_invalid_cli(self): + for args in ([],['--mode','bad','--output','x'],['--mode','normal','--output','x','--panels','2048']): + p=subprocess.run([sys.executable,'-B','-S',str(DRIVER),*args],capture_output=True);self.assertEqual(p.returncode,2) + + def test_workflow_contract(self): + wf=DRIVER.parents[1]/'.github/workflows/lm006-oned-coefficient.yml';self.assertTrue(wf.is_file(),'workflow missing') + text=wf.read_text() + for phrase in ('permissions:\n contents: read','fail-fast: false','mode: [normal, optimized]','if: always()',"python-version: '3.13.5'",'persist-credentials: false','if-no-files-found: error'): + self.assertIn(phrase,text) + self.assertNotIn('continue-on-error:',text);self.assertNotIn('pull_request_target:',text) + + + def synthetic_project(self, bad_test=False, output='synthetic', mutate=False): + import shutil + previous=os.environ.get('GITHUB_ACTIONS') + self.addCleanup(lambda: os.environ.pop('GITHUB_ACTIONS',None) if previous is None else os.environ.__setitem__('GITHUB_ACTIONS',previous)) + os.environ['GITHUB_ACTIONS']='false' + pins=self.fixture(); packet=self.root/self.m.PACKET + (packet/'RESULTS.json').write_text('synthetic\n') + methods='\n'.join(' def '+n+'(self): self.assertTrue('+('False' if bad_test and i==0 else 'True')+')' for i,n in enumerate(self.m.TEST_NAMES)) + (packet/'test_oned.py').write_text('import unittest\nclass OneDimensionalTests(unittest.TestCase):\n'+methods+'\n') + suffix="\nfrom pathlib import Path;Path('NOTE.md').write_text('changed')" if mutate else '' + (packet/'oned.py').write_text("import sys\nassert sys.argv[1:]==['--panels','1024']\nprint("+repr(output)+")"+suffix+'\n') + for name in self.m.EXECUTION_FILES: + d=self.root/name;d.parent.mkdir(parents=True,exist_ok=True);shutil.copyfile(DRIVER.parents[1]/name,d) + subprocess.run(['git','init','-q'],cwd=self.root,check=True);subprocess.run(['git','add','.'],cwd=self.root,check=True) + subprocess.run(['git','-c','user.name=Fixture','-c','user.email=f@example.invalid','-c','commit.gpgsign=false','commit','-qm','fixture'],cwd=self.root,check=True) + spec=importlib.util.spec_from_file_location('fixture_driver',self.root/self.m.EXECUTION_FILES[0]);mod=importlib.util.module_from_spec(spec);spec.loader.exec_module(mod) + mod.PINS={n:mod.git_blob((self.root/n).read_bytes()) for n in pins} + return mod + + def test_complete_orchestration_real_subprocesses(self): + mod=self.synthetic_project();out=Path(self.tmp.name)/'ok';receipt=mod.execute(self.root,out,'optimized') + self.assertEqual(receipt['status'],'PASS');self.assertEqual(set(receipt['steps']),{'tests','coefficient'});self.assertEqual((out/'coefficient.stdout').read_bytes(),b'synthetic\n') + + def test_failed_tests_stop_before_coefficient(self): + mod=self.synthetic_project(bad_test=True);out=Path(self.tmp.name)/'badtests' + with self.assertRaisesRegex(mod.ReplayError,'unexpected_exit'): mod.execute(self.root,out,'normal') + self.assertFalse((out/'coefficient.stdout').exists());self.assertEqual(json.loads((out/'receipt.json').read_text())['status'],'FAIL') + + def test_wrong_output_cannot_pass(self): + mod=self.synthetic_project(output='wrong');out=Path(self.tmp.name)/'wrong' + with self.assertRaisesRegex(mod.ReplayError,'stdout_mismatch'): mod.execute(self.root,out,'normal') + row=json.loads((out/'receipt.json').read_text());self.assertEqual(row['steps']['tests']['record']['status'],'PASS');self.assertEqual(row['steps']['coefficient']['record']['status'],'FAIL') + + def test_postflight_source_drift_rejected(self): + mod=self.synthetic_project(mutate=True);out=Path(self.tmp.name)/'drift' + with self.assertRaisesRegex(mod.ReplayError,'source_identity'): mod.execute(self.root,out,'normal') + self.assertEqual(json.loads((out/'receipt.json').read_text())['status'],'FAIL') + +if __name__=='__main__': unittest.main() diff --git a/tools/lm006_oned_coefficient_replay.py b/tools/lm006_oned_coefficient_replay.py new file mode 100644 index 000000000..8715ffa31 --- /dev/null +++ b/tools/lm006_oned_coefficient_replay.py @@ -0,0 +1,127 @@ +#!/usr/bin/env python3 +"""Replay the frozen PR380 one-dimensional LM006 coefficient certificate. + +Standard library / POSIX only. Execution/custody interlock, not theorem acceptance. +""" +import argparse, hashlib, json, os, re, signal, subprocess, sys, time +from pathlib import Path, PurePosixPath + +REPOSITORY='d6g8k5htny-coder/Math-' +SOURCE_COMMIT='8fe14358a1ee5d7ef7d7e20520391f62f432fe04' +PACKET='coefficients/lm006_wrong_sign_oned_20261006_a62c' +EXECUTION_FILES=('tools/lm006_oned_coefficient_replay.py','tests/test_lm006_oned_coefficient_replay.py','.github/workflows/lm006-oned-coefficient.yml') +PINS={ + PACKET+'/NOTE.md':'db27645e62bf846835b1daeb6c51f1eb3b417f1e', + PACKET+'/oned.py':'5015dee3a660b67c42ccab13a976626e6e2d02cc', + PACKET+'/test_oned.py':'62e54422726f1caffab62e2e3fe38d297013e52d', + PACKET+'/RESULTS.json':'506833403f2dee91553d1a8dfc6eef6ee5c8faf8', + PACKET+'/SOURCES.json':'a6de8d4113cedf548b17c750da406f8aa6705eb4', + PACKET+'/PRIOR_WORK.md':'1fb9afde1490b8e86c3b1d453f1c16a45b35a352', + 'coefficients/lm006_wrong_sign_20261006_r20/enclose.py':'e680ddb7aa0abd4b6aab2cac6a54c1ff28efc782', + 'reviews/lm006_wrong_sign_asymptotic_20261006/NOTE.md':'ea914c1b8e0b8180b645f3f626e2081ab87700b9'} +DEPENDENCIES=('coefficients/lm006_wrong_sign_20261006_r20/enclose.py','reviews/lm006_wrong_sign_asymptotic_20261006/NOTE.md') +TEST_NAMES=('test_cli', 'test_conditional_formula_against_positive_integral', 'test_error_tail_and_quotient_attachment', 'test_exact_fourth_derivative_algebra', 'test_interval_arithmetic', 'test_invalid_resolution', 'test_low_resolution_is_genuine_enclosure', 'test_nonzero_integrand_and_scaling', 'test_parent_authentication', 'test_product_derivative_identity', 'test_reduction_from_truncated_moments', 'test_simpson_weights_and_error', 'test_tail_exact_series', 'test_tail_is_present_and_small', 'test_tail_sanity_and_domain') +MAX_STREAM_BYTES=4*1024*1024 + +class ReplayError(ValueError): pass + +def require(ok,reason): + if not ok: raise ReplayError(reason) +def sha256(raw): return hashlib.sha256(raw).hexdigest() +def git_blob(raw): return hashlib.sha1(b'blob %d\0'%len(raw)+raw).hexdigest() + +def source_file(root,relative): + require(type(relative) is str and relative and '\\' not in relative and not relative.startswith('/') and all(x not in ('','.','..') for x in relative.split('/')),'unsafe_path') + p=Path(root) + for part in PurePosixPath(relative).parts: + p=p/part; require(not p.is_symlink(),'source_symlink') + require(p.is_file(),'source_missing'); return p + +def validate_snapshot(root,pins=None): + pins=PINS if pins is None else pins; result={} + for name,expected in pins.items(): + raw=source_file(root,name).read_bytes(); actual=git_blob(raw) + require(actual==expected,'source_identity: '+name) + result[name]={'bytes':len(raw),'sha256':sha256(raw),'git_blob':actual} + names=sorted(Path(n).name for n in pins if n.startswith(PACKET+'/')) + require(sorted(p.name for p in (Path(root)/PACKET).iterdir())==names,'packet_membership') + return result + +def check_output(stdout,stderr,expected,kind): + if kind=='tests': + prefix='\n'.join(n+' (test_oned.OneDimensionalTests.'+n+') ... ok' for n in TEST_NAMES).encode() + pattern=re.escape(prefix+b'\n\n'+b'-'*70)+rb'\nRan 15 tests in [0-9]+(?:\.[0-9]+)?s\n\nOK\n' + require(stdout==b'' and re.fullmatch(pattern,stderr) is not None,'test_report_mismatch'); return + require(kind=='exact','unknown_contract'); require(stderr==b'','unexpected_stderr'); require(stdout==expected,'stdout_mismatch') + +def write_json(path,value): + with Path(path).open('x',encoding='utf-8',newline='\n') as f: json.dump(value,f,sort_keys=True,indent=2,allow_nan=False);f.write('\n') + +def run_step(argv,cwd,logs,name,expected,kind,timeout=900): + require(os.name=='posix','posix_required');require(re.fullmatch(r'[a-z][a-z0-9_-]*',name) is not None,'unsafe_step_name') + logs=Path(logs); out=logs/(name+'.stdout');err=logs/(name+'.stderr');proc=logs/(name+'.process.json') + require(not any(p.exists() or p.is_symlink() for p in (out,err,proc)),'step_evidence_exists') + start=time.monotonic_ns();record={'command':list(map(str,argv)),'returncode':None,'timed_out':False,'status':'FAIL','timeout_seconds':timeout};failure=None + with out.open('xb') as so,err.open('xb') as se: + try: + child=subprocess.Popen(argv,cwd=cwd,stdout=so,stderr=se,start_new_session=True,env={**os.environ,'PYTHONDONTWRITEBYTECODE':'1'}) + try: record['returncode']=child.wait(timeout=timeout) + except subprocess.TimeoutExpired: + record['timed_out']=True;failure='timeout' + try: os.killpg(child.pid,signal.SIGKILL) + except ProcessLookupError: pass + record['returncode']=child.wait(timeout=5) + except OSError as exc: failure='spawn_error';record['detail']=type(exc).__name__+': '+str(exc) + record['elapsed_ns']=time.monotonic_ns()-start;sizes=(out.stat().st_size,err.stat().st_size) + if max(sizes)>MAX_STREAM_BYTES: failure=failure or 'output_too_large';record.update(stdout_bytes=sizes[0],stderr_bytes=sizes[1]) + else: + a,b=out.read_bytes(),err.read_bytes();record.update(stdout_bytes=len(a),stderr_bytes=len(b),stdout_sha256=sha256(a),stderr_sha256=sha256(b)) + if failure is None: + try: require(record['returncode']==0,'unexpected_exit');check_output(a,b,expected,kind) + except ReplayError as exc: failure=str(exc) + if failure is None: record['status']='PASS' + else: record['failure']=failure + write_json(proc,record) + if failure is not None: raise ReplayError(failure) + return record + +def git(root,*args): + p=subprocess.run(['git',*args],cwd=root,capture_output=True,timeout=30);require(p.returncode==0,'git_command_failed');return p.stdout.decode('ascii').strip() +def git_head(root): + h=git(root,'rev-parse','HEAD');require(re.fullmatch('[0-9a-f]{40}',h) is not None,'invalid_git_head');return h + +def execution_sources(root,head): + result={} + for name in EXECUTION_FILES: + raw=source_file(root,name).read_bytes();committed=git(root,'rev-parse',head+':'+name);require(committed==git_blob(raw),'execution_source_drift');result[name]={'git_blob':committed,'sha256':sha256(raw),'bytes':len(raw)} + return result + +def host_identity(head,env): + if env.get('GITHUB_ACTIONS')=='true': + require(env.get('GITHUB_REPOSITORY')==REPOSITORY and env.get('GITHUB_SHA')==head,'host_identity') + for k in ('GITHUB_RUN_ID','GITHUB_RUN_ATTEMPT'): require(re.fullmatch('[1-9][0-9]*',env.get(k,'')) is not None,'host_identity') + +def execute(root,output,mode): + root,output=Path(root).resolve(),Path(output).resolve();require(mode in ('normal','optimized'),'invalid_mode');require(not output.is_relative_to(root),'evidence_inside_source');require(not output.exists(),'evidence_exists');output.mkdir(parents=True) + receipt={'schema_version':1,'object':'LM006-ONED-COEFFICIENT-REPLAY','repository':REPOSITORY,'source_commit':SOURCE_COMMIT,'mode':mode,'scientific_acceptance':False,'formal_verification':False,'status':'FAIL','steps':{},'run_id':os.environ.get('GITHUB_RUN_ID'),'run_attempt':os.environ.get('GITHUB_RUN_ATTEMPT'),'event':os.environ.get('GITHUB_EVENT_NAME')} + try: + before=validate_snapshot(root);head=git_head(root);receipt['tested_commit']=head;host_identity(head,os.environ);receipt['execution_sources']=execution_sources(root,head);receipt['sources']=before + require(Path(__file__).resolve()==root/EXECUTION_FILES[0],'driver_location');require(git(root,'status','--porcelain','--untracked-files=no')=='','tracked_source_dirty') + packet=root/PACKET;flags=['-B']+(['-O'] if mode=='optimized' else [])+['-S'] + specs=[('tests',['-m','unittest','test_oned','-v'],None,'tests'),('coefficient',['oned.py','--panels','1024'],(packet/'RESULTS.json').read_bytes(),'exact')] + for name,args,expected,kind in specs: + try: run_step([sys.executable,*flags,*args],packet,output,name,expected,kind) + finally: + p=output/(name+'.process.json') + if p.is_file(): receipt['steps'][name]={'process_sha256':sha256(p.read_bytes()),'record':json.loads(p.read_bytes())} + require(validate_snapshot(root)==before,'source_changed_during_execution');require(execution_sources(root,head)==receipt['execution_sources'],'execution_source_drift');require(git_head(root)==head,'head_changed_during_execution');require(git(root,'status','--porcelain','--untracked-files=no')=='','tracked_source_dirty');receipt['status']='PASS' + except Exception as exc: receipt['failure']=type(exc).__name__+': '+str(exc);raise + finally: write_json(output/'receipt.json',receipt) + return receipt + +def main(): + p=argparse.ArgumentParser(description=__doc__);p.add_argument('--root',type=Path,default=Path('.'));p.add_argument('--output',type=Path,required=True);p.add_argument('--mode',choices=('normal','optimized'),required=True);a=p.parse_args() + try: result=execute(a.root,a.output,a.mode) + except Exception as exc: print('LM006_ONED_REPLAY_FAIL: '+type(exc).__name__+': '+str(exc),file=sys.stderr);return 1 + print(json.dumps(result,sort_keys=True,indent=2,allow_nan=False));return 0 +if __name__=='__main__': raise SystemExit(main()) From 6a5aa322d9fdfa3faf5e4699e62f70a38cc162ba Mon Sep 17 00:00:00 2001 From: Dylan Roy <249851642+d6g8k5htny-coder@users.noreply.github.com> Date: Tue, 6 Oct 2026 09:27:43 -0700 Subject: [PATCH 4/6] LM006 replay: retain evidence when post-kill wait also times out Handle the secondary TimeoutExpired after SIGKILL and add a deterministic regression ensuring FAIL process evidence and stream digests are still written. No numerical, proof, workflow or scientific-status change. --- tests/test_lm006_oned_coefficient_replay.py | 169 ++++++++++++++++++++ tools/lm006_oned_coefficient_replay.py | 3 +- 2 files changed, 171 insertions(+), 1 deletion(-) diff --git a/tests/test_lm006_oned_coefficient_replay.py b/tests/test_lm006_oned_coefficient_replay.py index 98c1b52bf..b7eaabb85 100644 --- a/tests/test_lm006_oned_coefficient_replay.py +++ b/tests/test_lm006_oned_coefficient_replay.py @@ -1,5 +1,6 @@ """Execution/custody controls for the frozen PR380 one-dimensional coefficient.""" import importlib.util, json, os, subprocess, sys, tempfile, time, unittest +from unittest import mock from pathlib import Path DRIVER=Path(__file__).resolve().parents[1]/'tools/lm006_oned_coefficient_replay.py' @@ -55,6 +56,174 @@ def test_timeout_retains_partial_evidence(self): self.child("import sys,time;print('s',flush=True);print('e',file=sys.stderr,flush=True);time.sleep(10)",timeout=.2) row=json.loads((self.logs/'child.process.json').read_text());self.assertTrue(row['timed_out']);self.assertEqual(row['failure'],'timeout') + + def test_secondary_timeout_still_writes_process_record(self): + class Stuck: + pid=424242 + def __init__(self,*args,**kwargs): + kwargs['stdout'].write(b'started\\n');kwargs['stdout'].flush() + kwargs['stderr'].write(b'partial\\n');kwargs['stderr'].flush() + self.calls=0 + def wait(self,timeout=None): + self.calls+=1 + raise subprocess.TimeoutExpired(['fake'],timeout) + with mock.patch.object(self.m.subprocess,'Popen',Stuck), mock.patch.object(self.m.os,'killpg') as kill: + with self.assertRaisesRegex(self.m.ReplayError,'timeout'): + self.m.run_step(['fake'],self.root,self.logs,'stuck',b'','exact',.1) + kill.assert_called_once_with(424242,self.m.signal.SIGKILL) + row=json.loads((self.logs/'stuck.process.json').read_text()) + self.assertEqual((row['status'],row['failure'],row['timed_out'],row['returncode']),('FAIL','timeout',True,None)) + self.assertIn('did not finish',row['detail']) + self.assertEqual((self.logs/'stuck.stdout').read_bytes(),b'started\\n') + self.assertEqual((self.logs/'stuck.stderr').read_bytes(),b'partial\\n') + self.assertRegex(row['stdout_sha256'],'^[0-9a-f]{64} self.child("print('ok')");before={p.name:p.read_bytes() for p in self.logs.iterdir()} + with self.assertRaisesRegex(self.m.ReplayError,'step_evidence_exists'): self.child("print('changed')") + self.assertEqual(before,{p.name:p.read_bytes() for p in self.logs.iterdir()}) + + def test_test_report_contract_requires_all_named_passes(self): + good=('\n'.join(n+' (test_oned.OneDimensionalTests.'+n+') ... ok' for n in self.m.TEST_NAMES)+'\n\n'+'-'*70+'\nRan 15 tests in 0.001s\n\nOK\n').encode() + self.m.check_output(b'',good,None,'tests') + for bad in (good.replace(b' ... ok',b' ... FAIL',1),good+b'noise',good.replace(b'Ran 15',b'Ran 0')): + with self.assertRaisesRegex(self.m.ReplayError,'test_report_mismatch'): self.m.check_output(b'',bad,None,'tests') + + def test_exact_output_contract_is_byte_exact(self): + want=b'{"panels":1024,"independently_reviewed":false}\n';self.m.check_output(want,b'',want,'exact') + for bad in (b'',want+b'\n',want.replace(b'false',b'true')): + with self.assertRaisesRegex(self.m.ReplayError,'stdout_mismatch'): self.m.check_output(bad,b'',want,'exact') + + def test_host_identity(self): + h='1'*40;env={'GITHUB_ACTIONS':'true','GITHUB_REPOSITORY':self.m.REPOSITORY,'GITHUB_SHA':h,'GITHUB_RUN_ID':'1','GITHUB_RUN_ATTEMPT':'2'} + self.m.host_identity(h,env) + env['GITHUB_SHA']='2'*40 + with self.assertRaisesRegex(self.m.ReplayError,'host_identity'): self.m.host_identity(h,env) + + def test_invalid_cli(self): + for args in ([],['--mode','bad','--output','x'],['--mode','normal','--output','x','--panels','2048']): + p=subprocess.run([sys.executable,'-B','-S',str(DRIVER),*args],capture_output=True);self.assertEqual(p.returncode,2) + + def test_workflow_contract(self): + wf=DRIVER.parents[1]/'.github/workflows/lm006-oned-coefficient.yml';self.assertTrue(wf.is_file(),'workflow missing') + text=wf.read_text() + for phrase in ('permissions:\n contents: read','fail-fast: false','mode: [normal, optimized]','if: always()',"python-version: '3.13.5'",'persist-credentials: false','if-no-files-found: error'): + self.assertIn(phrase,text) + self.assertNotIn('continue-on-error:',text);self.assertNotIn('pull_request_target:',text) + + + def synthetic_project(self, bad_test=False, output='synthetic', mutate=False): + import shutil + previous=os.environ.get('GITHUB_ACTIONS') + self.addCleanup(lambda: os.environ.pop('GITHUB_ACTIONS',None) if previous is None else os.environ.__setitem__('GITHUB_ACTIONS',previous)) + os.environ['GITHUB_ACTIONS']='false' + pins=self.fixture(); packet=self.root/self.m.PACKET + (packet/'RESULTS.json').write_text('synthetic\n') + methods='\n'.join(' def '+n+'(self): self.assertTrue('+('False' if bad_test and i==0 else 'True')+')' for i,n in enumerate(self.m.TEST_NAMES)) + (packet/'test_oned.py').write_text('import unittest\nclass OneDimensionalTests(unittest.TestCase):\n'+methods+'\n') + suffix="\nfrom pathlib import Path;Path('NOTE.md').write_text('changed')" if mutate else '' + (packet/'oned.py').write_text("import sys\nassert sys.argv[1:]==['--panels','1024']\nprint("+repr(output)+")"+suffix+'\n') + for name in self.m.EXECUTION_FILES: + d=self.root/name;d.parent.mkdir(parents=True,exist_ok=True);shutil.copyfile(DRIVER.parents[1]/name,d) + subprocess.run(['git','init','-q'],cwd=self.root,check=True);subprocess.run(['git','add','.'],cwd=self.root,check=True) + subprocess.run(['git','-c','user.name=Fixture','-c','user.email=f@example.invalid','-c','commit.gpgsign=false','commit','-qm','fixture'],cwd=self.root,check=True) + spec=importlib.util.spec_from_file_location('fixture_driver',self.root/self.m.EXECUTION_FILES[0]);mod=importlib.util.module_from_spec(spec);spec.loader.exec_module(mod) + mod.PINS={n:mod.git_blob((self.root/n).read_bytes()) for n in pins} + return mod + + def test_complete_orchestration_real_subprocesses(self): + mod=self.synthetic_project();out=Path(self.tmp.name)/'ok';receipt=mod.execute(self.root,out,'optimized') + self.assertEqual(receipt['status'],'PASS');self.assertEqual(set(receipt['steps']),{'tests','coefficient'});self.assertEqual((out/'coefficient.stdout').read_bytes(),b'synthetic\n') + + def test_failed_tests_stop_before_coefficient(self): + mod=self.synthetic_project(bad_test=True);out=Path(self.tmp.name)/'badtests' + with self.assertRaisesRegex(mod.ReplayError,'unexpected_exit'): mod.execute(self.root,out,'normal') + self.assertFalse((out/'coefficient.stdout').exists());self.assertEqual(json.loads((out/'receipt.json').read_text())['status'],'FAIL') + + def test_wrong_output_cannot_pass(self): + mod=self.synthetic_project(output='wrong');out=Path(self.tmp.name)/'wrong' + with self.assertRaisesRegex(mod.ReplayError,'stdout_mismatch'): mod.execute(self.root,out,'normal') + row=json.loads((out/'receipt.json').read_text());self.assertEqual(row['steps']['tests']['record']['status'],'PASS');self.assertEqual(row['steps']['coefficient']['record']['status'],'FAIL') + + def test_postflight_source_drift_rejected(self): + mod=self.synthetic_project(mutate=True);out=Path(self.tmp.name)/'drift' + with self.assertRaisesRegex(mod.ReplayError,'source_identity'): mod.execute(self.root,out,'normal') + self.assertEqual(json.loads((out/'receipt.json').read_text())['status'],'FAIL') + +if __name__=='__main__': unittest.main() +) + self.assertRegex(row['stderr_sha256'],'^[0-9a-f]{64} self.child("print('ok')");before={p.name:p.read_bytes() for p in self.logs.iterdir()} + with self.assertRaisesRegex(self.m.ReplayError,'step_evidence_exists'): self.child("print('changed')") + self.assertEqual(before,{p.name:p.read_bytes() for p in self.logs.iterdir()}) + + def test_test_report_contract_requires_all_named_passes(self): + good=('\n'.join(n+' (test_oned.OneDimensionalTests.'+n+') ... ok' for n in self.m.TEST_NAMES)+'\n\n'+'-'*70+'\nRan 15 tests in 0.001s\n\nOK\n').encode() + self.m.check_output(b'',good,None,'tests') + for bad in (good.replace(b' ... ok',b' ... FAIL',1),good+b'noise',good.replace(b'Ran 15',b'Ran 0')): + with self.assertRaisesRegex(self.m.ReplayError,'test_report_mismatch'): self.m.check_output(b'',bad,None,'tests') + + def test_exact_output_contract_is_byte_exact(self): + want=b'{"panels":1024,"independently_reviewed":false}\n';self.m.check_output(want,b'',want,'exact') + for bad in (b'',want+b'\n',want.replace(b'false',b'true')): + with self.assertRaisesRegex(self.m.ReplayError,'stdout_mismatch'): self.m.check_output(bad,b'',want,'exact') + + def test_host_identity(self): + h='1'*40;env={'GITHUB_ACTIONS':'true','GITHUB_REPOSITORY':self.m.REPOSITORY,'GITHUB_SHA':h,'GITHUB_RUN_ID':'1','GITHUB_RUN_ATTEMPT':'2'} + self.m.host_identity(h,env) + env['GITHUB_SHA']='2'*40 + with self.assertRaisesRegex(self.m.ReplayError,'host_identity'): self.m.host_identity(h,env) + + def test_invalid_cli(self): + for args in ([],['--mode','bad','--output','x'],['--mode','normal','--output','x','--panels','2048']): + p=subprocess.run([sys.executable,'-B','-S',str(DRIVER),*args],capture_output=True);self.assertEqual(p.returncode,2) + + def test_workflow_contract(self): + wf=DRIVER.parents[1]/'.github/workflows/lm006-oned-coefficient.yml';self.assertTrue(wf.is_file(),'workflow missing') + text=wf.read_text() + for phrase in ('permissions:\n contents: read','fail-fast: false','mode: [normal, optimized]','if: always()',"python-version: '3.13.5'",'persist-credentials: false','if-no-files-found: error'): + self.assertIn(phrase,text) + self.assertNotIn('continue-on-error:',text);self.assertNotIn('pull_request_target:',text) + + + def synthetic_project(self, bad_test=False, output='synthetic', mutate=False): + import shutil + previous=os.environ.get('GITHUB_ACTIONS') + self.addCleanup(lambda: os.environ.pop('GITHUB_ACTIONS',None) if previous is None else os.environ.__setitem__('GITHUB_ACTIONS',previous)) + os.environ['GITHUB_ACTIONS']='false' + pins=self.fixture(); packet=self.root/self.m.PACKET + (packet/'RESULTS.json').write_text('synthetic\n') + methods='\n'.join(' def '+n+'(self): self.assertTrue('+('False' if bad_test and i==0 else 'True')+')' for i,n in enumerate(self.m.TEST_NAMES)) + (packet/'test_oned.py').write_text('import unittest\nclass OneDimensionalTests(unittest.TestCase):\n'+methods+'\n') + suffix="\nfrom pathlib import Path;Path('NOTE.md').write_text('changed')" if mutate else '' + (packet/'oned.py').write_text("import sys\nassert sys.argv[1:]==['--panels','1024']\nprint("+repr(output)+")"+suffix+'\n') + for name in self.m.EXECUTION_FILES: + d=self.root/name;d.parent.mkdir(parents=True,exist_ok=True);shutil.copyfile(DRIVER.parents[1]/name,d) + subprocess.run(['git','init','-q'],cwd=self.root,check=True);subprocess.run(['git','add','.'],cwd=self.root,check=True) + subprocess.run(['git','-c','user.name=Fixture','-c','user.email=f@example.invalid','-c','commit.gpgsign=false','commit','-qm','fixture'],cwd=self.root,check=True) + spec=importlib.util.spec_from_file_location('fixture_driver',self.root/self.m.EXECUTION_FILES[0]);mod=importlib.util.module_from_spec(spec);spec.loader.exec_module(mod) + mod.PINS={n:mod.git_blob((self.root/n).read_bytes()) for n in pins} + return mod + + def test_complete_orchestration_real_subprocesses(self): + mod=self.synthetic_project();out=Path(self.tmp.name)/'ok';receipt=mod.execute(self.root,out,'optimized') + self.assertEqual(receipt['status'],'PASS');self.assertEqual(set(receipt['steps']),{'tests','coefficient'});self.assertEqual((out/'coefficient.stdout').read_bytes(),b'synthetic\n') + + def test_failed_tests_stop_before_coefficient(self): + mod=self.synthetic_project(bad_test=True);out=Path(self.tmp.name)/'badtests' + with self.assertRaisesRegex(mod.ReplayError,'unexpected_exit'): mod.execute(self.root,out,'normal') + self.assertFalse((out/'coefficient.stdout').exists());self.assertEqual(json.loads((out/'receipt.json').read_text())['status'],'FAIL') + + def test_wrong_output_cannot_pass(self): + mod=self.synthetic_project(output='wrong');out=Path(self.tmp.name)/'wrong' + with self.assertRaisesRegex(mod.ReplayError,'stdout_mismatch'): mod.execute(self.root,out,'normal') + row=json.loads((out/'receipt.json').read_text());self.assertEqual(row['steps']['tests']['record']['status'],'PASS');self.assertEqual(row['steps']['coefficient']['record']['status'],'FAIL') + + def test_postflight_source_drift_rejected(self): + mod=self.synthetic_project(mutate=True);out=Path(self.tmp.name)/'drift' + with self.assertRaisesRegex(mod.ReplayError,'source_identity'): mod.execute(self.root,out,'normal') + self.assertEqual(json.loads((out/'receipt.json').read_text())['status'],'FAIL') + +if __name__=='__main__': unittest.main() +) + + def test_existing_evidence_not_overwritten(self): self.child("print('ok')");before={p.name:p.read_bytes() for p in self.logs.iterdir()} with self.assertRaisesRegex(self.m.ReplayError,'step_evidence_exists'): self.child("print('changed')") diff --git a/tools/lm006_oned_coefficient_replay.py b/tools/lm006_oned_coefficient_replay.py index 8715ffa31..04bcf9344 100644 --- a/tools/lm006_oned_coefficient_replay.py +++ b/tools/lm006_oned_coefficient_replay.py @@ -70,7 +70,8 @@ def run_step(argv,cwd,logs,name,expected,kind,timeout=900): record['timed_out']=True;failure='timeout' try: os.killpg(child.pid,signal.SIGKILL) except ProcessLookupError: pass - record['returncode']=child.wait(timeout=5) + try: record['returncode']=child.wait(timeout=5) + except subprocess.TimeoutExpired: record['detail']='process-group termination did not finish in 5 seconds' except OSError as exc: failure='spawn_error';record['detail']=type(exc).__name__+': '+str(exc) record['elapsed_ns']=time.monotonic_ns()-start;sizes=(out.stat().st_size,err.stat().st_size) if max(sizes)>MAX_STREAM_BYTES: failure=failure or 'output_too_large';record.update(stdout_bytes=sizes[0],stderr_bytes=sizes[1]) From ed58c25c70777570a9048936656b3d41d5e59568 Mon Sep 17 00:00:00 2001 From: Dylan Roy <249851642+d6g8k5htny-coder@users.noreply.github.com> Date: Tue, 6 Oct 2026 09:29:30 -0700 Subject: [PATCH 5/6] LM006 replay: repair cleanup regression syntax Restore the existing evidence-nonoverwrite test and complete both digest assertions in the new secondary-timeout regression. No driver/workflow/numerical change. --- tests/test_lm006_oned_coefficient_replay.py | 8 +++++--- 1 file changed, 5 insertions(+), 3 deletions(-) diff --git a/tests/test_lm006_oned_coefficient_replay.py b/tests/test_lm006_oned_coefficient_replay.py index b7eaabb85..f26e02b39 100644 --- a/tests/test_lm006_oned_coefficient_replay.py +++ b/tests/test_lm006_oned_coefficient_replay.py @@ -63,9 +63,7 @@ class Stuck: def __init__(self,*args,**kwargs): kwargs['stdout'].write(b'started\\n');kwargs['stdout'].flush() kwargs['stderr'].write(b'partial\\n');kwargs['stderr'].flush() - self.calls=0 def wait(self,timeout=None): - self.calls+=1 raise subprocess.TimeoutExpired(['fake'],timeout) with mock.patch.object(self.m.subprocess,'Popen',Stuck), mock.patch.object(self.m.os,'killpg') as kill: with self.assertRaisesRegex(self.m.ReplayError,'timeout'): @@ -76,7 +74,11 @@ def wait(self,timeout=None): self.assertIn('did not finish',row['detail']) self.assertEqual((self.logs/'stuck.stdout').read_bytes(),b'started\\n') self.assertEqual((self.logs/'stuck.stderr').read_bytes(),b'partial\\n') - self.assertRegex(row['stdout_sha256'],'^[0-9a-f]{64} self.child("print('ok')");before={p.name:p.read_bytes() for p in self.logs.iterdir()} + self.assertRegex(row['stdout_sha256'],r'^[0-9a-f]{64}$') + self.assertRegex(row['stderr_sha256'],r'^[0-9a-f]{64}$') + + def test_existing_evidence_not_overwritten(self): + self.child("print('ok')");before={p.name:p.read_bytes() for p in self.logs.iterdir()} with self.assertRaisesRegex(self.m.ReplayError,'step_evidence_exists'): self.child("print('changed')") self.assertEqual(before,{p.name:p.read_bytes() for p in self.logs.iterdir()}) From 089d87ace030e755511a04735c42c1f91911d4c1 Mon Sep 17 00:00:00 2001 From: Dylan Roy <249851642+d6g8k5htny-coder@users.noreply.github.com> Date: Tue, 6 Oct 2026 09:32:20 -0700 Subject: [PATCH 6/6] LM006 replay: restore clean focused suite with cleanup regression Rebuild from the last green 16-test source and add exactly one deterministic secondary-timeout evidence test. No driver, workflow, or numerical change. --- tests/test_lm006_oned_coefficient_replay.py | 16 ++++++---------- 1 file changed, 6 insertions(+), 10 deletions(-) diff --git a/tests/test_lm006_oned_coefficient_replay.py b/tests/test_lm006_oned_coefficient_replay.py index f26e02b39..ecafafc03 100644 --- a/tests/test_lm006_oned_coefficient_replay.py +++ b/tests/test_lm006_oned_coefficient_replay.py @@ -56,13 +56,14 @@ def test_timeout_retains_partial_evidence(self): self.child("import sys,time;print('s',flush=True);print('e',file=sys.stderr,flush=True);time.sleep(10)",timeout=.2) row=json.loads((self.logs/'child.process.json').read_text());self.assertTrue(row['timed_out']);self.assertEqual(row['failure'],'timeout') - def test_secondary_timeout_still_writes_process_record(self): class Stuck: pid=424242 def __init__(self,*args,**kwargs): - kwargs['stdout'].write(b'started\\n');kwargs['stdout'].flush() - kwargs['stderr'].write(b'partial\\n');kwargs['stderr'].flush() + kwargs['stdout'].write(b'started\\n') + kwargs['stdout'].flush() + kwargs['stderr'].write(b'partial\\n') + kwargs['stderr'].flush() def wait(self,timeout=None): raise subprocess.TimeoutExpired(['fake'],timeout) with mock.patch.object(self.m.subprocess,'Popen',Stuck), mock.patch.object(self.m.os,'killpg') as kill: @@ -74,11 +75,7 @@ def wait(self,timeout=None): self.assertIn('did not finish',row['detail']) self.assertEqual((self.logs/'stuck.stdout').read_bytes(),b'started\\n') self.assertEqual((self.logs/'stuck.stderr').read_bytes(),b'partial\\n') - self.assertRegex(row['stdout_sha256'],r'^[0-9a-f]{64}$') - self.assertRegex(row['stderr_sha256'],r'^[0-9a-f]{64}$') - - def test_existing_evidence_not_overwritten(self): - self.child("print('ok')");before={p.name:p.read_bytes() for p in self.logs.iterdir()} + self.assertRegex(row['stdout_sha256'],r'^[0-9a-f]{64} self.child("print('ok')");before={p.name:p.read_bytes() for p in self.logs.iterdir()} with self.assertRaisesRegex(self.m.ReplayError,'step_evidence_exists'): self.child("print('changed')") self.assertEqual(before,{p.name:p.read_bytes() for p in self.logs.iterdir()}) @@ -151,7 +148,7 @@ def test_postflight_source_drift_rejected(self): if __name__=='__main__': unittest.main() ) - self.assertRegex(row['stderr_sha256'],'^[0-9a-f]{64} self.child("print('ok')");before={p.name:p.read_bytes() for p in self.logs.iterdir()} + self.assertRegex(row['stderr_sha256'],r'^[0-9a-f]{64} self.child("print('ok')");before={p.name:p.read_bytes() for p in self.logs.iterdir()} with self.assertRaisesRegex(self.m.ReplayError,'step_evidence_exists'): self.child("print('changed')") self.assertEqual(before,{p.name:p.read_bytes() for p in self.logs.iterdir()}) @@ -225,7 +222,6 @@ def test_postflight_source_drift_rejected(self): if __name__=='__main__': unittest.main() ) - def test_existing_evidence_not_overwritten(self): self.child("print('ok')");before={p.name:p.read_bytes() for p in self.logs.iterdir()} with self.assertRaisesRegex(self.m.ReplayError,'step_evidence_exists'): self.child("print('changed')")