diff --git a/reviews/lm006_endpoint_extension_20261005/NOTE.md b/reviews/lm006_endpoint_extension_20261005/NOTE.md new file mode 100644 index 000000000..551aa5635 --- /dev/null +++ b/reviews/lm006_endpoint_extension_20261005/NOTE.md @@ -0,0 +1,305 @@ +# LM006 endpoint extension by explicit integral kernels + +Dylan Roy — delegated AI mathematical work. Actual author: **OpenAI / GPT-6 +Astra Pro**, session `cross-source-closure-round9-20261005`, 5 October 2026. +Author-side additive companion; scientific effect **NONE**; organizational +independence credit **0**. This note neither edits nor reclassifies the frozen +historical LM006 body. It is not an independent review or a Lean formalization. + +## 1. Question, target, and assumptions + +The target is the six **pin-adjusted endpoint variables** in §§2–3 and the +uniform eighth-moment input in §7 of P02-LM-006 / LCR-DER-019-v1.0 [S1]. The +historical body has 9,147 bytes and SHA256 +`239ed094f70aa4352021572ad8bdc0c6ac6404edab4e1d7e61addec0c6659150`. +Its later source-bound review [S2] is conditional, not an unconditional +exact-field acceptance. A nine-midpoint-jet moment is not by itself a moment +bound for the six endpoint variables considered here. + +We give a direct argument with the following explicit hypotheses. Work on one +unconditioned probability space and interpret differentiability in its real +Hilbert space H = L². For a centered real Gaussian field near the origin put + + F(x) = f(x,0), H_y(x) = f_y(x,0), Q(x) = f_yy(x,0). + +Assume F is C³ as an H-valued map, H_y is C², and Q is continuous, on a common +open interval around zero. The indicated derivatives are the field's actual +mean-square derivatives: F' = f_x, F'' = f_xx, F''' = f_xxx, +H_y' = f_xy, and H_y'' = f_xxy. The finite families in question are jointly +Gaussian; derivatives and the integrals below remain Gaussian as L² limits of +linear combinations. Also assume that the covariance G₀ of + + J = (f, f_x, f_y, f_xx, f_xy, f_xxx)(0) + +is positive definite. These are hypotheses, not facts inferred from an old +status label. The field-to-source identification and the verification of G₀ +are separate from this endpoint argument. Nondegeneracy of Q conditional on J +is **not needed** for the endpoint extension or eighth moment proved here; it +is needed by the separate strictly positive normalizer conclusion in [S1]. + +Fix b = 6/5. Write r > 0, h = r/2, M = (-h,0), S = (h,0), with r sufficiently +small that the interval used below lies in the domain. The raw pin vector is + + X_r = (F(-h), F'(-h), H_y(-h), F(h), F'(h), H_y(h)), + +conditioned to (b,0,0,b-r³/6,0,0). Conditioning means the canonical Gaussian +regression law of the finite targets given X_r; the positive-definite pin +covariance proved below makes this law well-defined for every prescribed pin +value. It is the endpoint marginal of the usual Gaussian conditional field. +There is no conditioning on a good-event truncation. + +**Result.** Under exactly these hypotheses, the conditional means and +covariances of the six adjusted endpoint variables extend continuously to +r = 0, with limiting law + + (-1, 1, -a/2, a/2, Q_L, Q_L), + +where (a,Q_L) is the conditional law of (f_xxy(0), f_yy(0)) given +J = (b,0,0,0,0,2). The six-dimensional limiting covariance is allowed to be +singular. All its conditional eighth moments are uniformly bounded for +sufficiently small r. Consequently the exact typed endpoint weight has +E[W_r²] ≤ C r⁴, and W_r/r² is uniformly integrable. The constants and the +sufficiently small radius are qualitative, not numerical certificates. + +## 2. An explicit equivalent pin frame + +Define P_r = (P₀,…,P₅) by + + P₀ = (F(-h)+F(h))/2, + P₁ = (F'(-h)+F'(h))/2, + P₂ = (H_y(-h)+H_y(h))/2, + P₃ = (F'(h)-F'(-h))/r, + P₄ = (H_y(h)-H_y(-h))/r, + P₅ = (12/r²) [ P₁ - (F(h)-F(-h))/r ]. (2.1) + +This is an invertible linear transform for every r > 0. Indeed its inverse is + + F(±h) = P₀ ± (r/2)P₁ ∓ (r³/24)P₅, + F'(±h) = P₁ ± (r/2)P₃, + H_y(±h) = P₂ ± (r/2)P₄. (2.2) + +Thus no pin is lost, duplicated, or replaced. This is an explicit alternative +frame; no row-by-row identity with an unspecified historical GP-DER-044 frame +is asserted. Conditioning on X_r equals conditioning on P_r at the transformed +value. For the actual prescribed pins this value is exactly + + d_r = (b-r³/12, 0, 0, 0, 0, 2), (2.3) + +and d_r → d₀ = (b,0,0,0,0,2). In particular the limiting cubic pin is **2**, not +an unproved inference from the signs of the two Hessians. + +## 3. Integral identities remove the singular quotients + +All integrals in this section run over I = [-1/2,1/2] and are Bochner integrals +in H. The Hilbert-space fundamental theorem of calculus gives + + P₃ = ∫_I F''(ru) du, + P₄ = ∫_I H_y'(ru) du, + P₅ = 6 ∫_I (1/4-u²) F'''(ru) du. (3.1) + +For the last identity, put g(u) = F'(ru). Integration by parts twice gives + + ∫_I (1/4-u²) g''(u) du + = g(1/2)+g(-1/2) - 2∫_I g(u)du. + +Since g''(u) = r²F'''(ru), substitution into (2.1) proves (3.1). The kernel +6(1/4-u²) is nonnegative and has integral 1. In particular P₅ converges in L² +to F'''(0), with no unjustified division of an unconditioned derivative by r. + +Define the same adjusted endpoint variables as [S1]: + + A_± = (F''(±h)-P₃)/r, + B_± = (H_y'(±h)-P₄)/r, + C_± = Q(±h). (3.2) + +Applying the fundamental theorem once more and changing the order of +integration over the finite triangle gives the exact identities + + A_- = -∫_I (1/2-u) F'''(ru) du, + A_+ = ∫_I (u+1/2) F'''(ru) du, + B_- = -∫_I (1/2-u) H_y''(ru) du, + B_+ = ∫_I (u+1/2) H_y''(ru) du. (3.3) + +The two signed kernel masses are -1/2 and +1/2; each absolute kernel mass is +1/2. The identities are unconditioned linear-functional identities, before +imposing the pins. On the actual pin subspace P₃=P₄=0, so they become exactly +f_xx(M)/r, f_xx(S)/r, f_xy(M)/r, f_xy(S)/r. This order matters: for F(x)=x², +F''/r=2/r diverges but both adjusted A variables are identically zero. + +For any continuous H-valued map U, set + + ω_U(r) = sup_{|x|≤r/2} ||U(x)-U(0)||_H → 0. + +Then ∥∫_I k(u)[U(ru)-U(0)]du∥_H ≤ ∥k∥₁ ω_U(r). Thus (3.1)–(3.3) prove +joint L² convergence, on the original unconditioned probability space, + + (P_r, V_r) → (J,T), + V_r = (A_-,A_+,B_-,B_+,C_-,C_+), + T = (-F'''(0)/2, F'''(0)/2, + -H_y''(0)/2, H_y''(0)/2, Q(0), Q(0)). (3.4) + +Finite-dimensional joint convergence here follows by summing the squared +component L² errors. Cauchy–Schwarz then gives convergence of all covariance +entries, including pin–target cross-covariances. The same formulas show +continuity for positive r and extension at zero. No samplewise Taylor bound +under a changing conditional law is being assumed. + +## 4. Conditional means as well as covariances + +Write the unconditioned covariance blocks as + + G_r = Cov(P_r), K_r = Cov(V_r,P_r), B_r = Cov(V_r). + +All three extend continuously at zero by (3.4). Let λ₀ be the smallest +eigenvalue of G₀, positive by hypothesis. For sufficiently small r, +∥G_r-G₀∥op ≤ λ₀/2, hence G_r ≥ (λ₀/2)Id and ∥G_r⁻¹∥op ≤ 2/λ₀. This proves +that both P_r and its invertible raw-pin transform are nondegenerate. The +canonical conditional Gaussian law is N(m_r,Σ_r), with + + m_r = K_r G_r⁻¹ d_r, + Σ_r = B_r - K_r G_r⁻¹ K_rᵀ. (4.1) + +For completeness, subtract K_r G_r⁻¹P_r from V_r. The resulting Gaussian +residual has zero covariance with P_r, so their joint Gaussian characteristic +function factors. They are independent, proving (4.1) for every pin value. + +Because K_r, G_r⁻¹, and d_r all converge, m_r converges and is bounded. This +step is indispensable: a Loewner bound on the conditional covariance alone +does not control a conditional mean. The covariance Σ_r also converges and +is positive semidefinite, including at zero; it need not be invertible. +Equation (4.1) at r=0 is the conditional law of T given J=d₀. Its first two +coordinates are (-1,1), and the remaining coordinates have precisely the +(a,Q_L) description in §1. Convergence of Gaussian characteristic functions +now gives weak convergence of these conditional laws. No common samplewise +coupling of the original conditioned fields is claimed or needed. + +## 5. The genuine endpoint eighth moment and the exact weight + +Choose a sufficiently small r₁ ≤ 1. From §4 there are finite M and Λ such that +∥m_r∥≤M and ∥Σ_r∥op≤Λ for 0≤r≤r₁. For each individual marginal law one may +represent V_r in distribution as m_r+Σ_r^(1/2)Z, where Z is standard Gaussian +in R⁶. This is a statement about its moments, not a claim about the physical +sample paths under all the conditional laws. Therefore + + E||V_r||⁸ ≤ 2⁷ (M⁸ + Λ⁴ E||Z||⁸) + = 2⁷ (M⁸ + 5760 Λ⁴) =: C₈ < ∞. (5.1) + +The identity E||Z||⁸ = 6·8·10·12 = 5760 follows by differentiating four times +the chi-square moment generating function (1-2t)^(-3) at zero. The scalar +normal eighth moment 105 is not the six-dimensional norm moment. + +On the pins the exact physical Hessians are + + H_M = [[rA_-, rB_-], [rB_-, C_-]], + H_S = [[rA_+, rB_+], [rB_+, C_+]]. + +Writing Δ_±=A_±C_±-rB_±² gives det H_{M/S}=rΔ_-/+. For 00, +E[(W_r/r²) 1{W_r/r²>t}] ≤ C₈/t uniformly in r. This is the full exact-field +endpoint weight, not a quartic Taylor weight or a good-event-renormalized +weight. No numerical value of M, Λ, C₈, or r₁ has been established. + +## 6. Sufficient spectral regularity; separate application checks + +Here is a sufficient condition for the regularity portion of §1, not an +assertion that a named source satisfies it. Suppose the centered stationary +real field has an actual covariance representation + + C(z) = Σ_{k∈Z²} p_k exp(iν k·z), + p_k≥0, p_-k=p_k, ν>0, + Σ_k p_k (1+|νk|⁶) < ∞. (6.1) + +In its spectral Hilbert representation, a derivative of order |α|≤3 has +symbol (iνk)^α exp(iν k·x). Difference quotients converge in the weighted +L²(p) norm by dominated convergence, using |exp(it)-1|≤|t| and the sixth +spectral moment. Translations of the highest derivatives are continuous by +the bound |exp(it)-1|≤2 and the same summable envelope. Lower orders use the +corresponding lower moments, implied by (6.1). This gives the H-valued +regularity and joint Gaussian derivative family used in §§1–3. No analytic +covariance kernel, density for V₀, or pathwise derivative supremum is needed. + +Condition (6.1) alone does **not** prove G₀ positive definite: a spectrum +supported on too few frequencies can be degenerate. The separate seven-node +witness [S3] is one route under its additional positive-weight hypotheses. Its +field-to-symbol identification and review are separate tasks. In particular +this note does not import a mutable review label as a mathematical premise. +The canonical target remains the fixed side-24, d=2, b=6/5 six-pin law. A +change of field, frame direction, birth height or height-gap scaling needs its +own matching; no uniformity over those changes is claimed here. + +## 7. Verification scope and reproducibility + +The standard-library checker compares direct endpoint formulas with exact +polynomial integrals using `fractions.Fraction`. It tests 14 monomials on six +radii, 120 arbitrary-pin inversions, 18 prescribed-pin transformations, the +subtraction control, kernel masses, and Gaussian norm-moment arithmetic. The +unit suite additionally checks general rational polynomials and invalid +inputs. These tests support the algebra; the Hilbert-space and Gaussian +arguments in §§3–5 are the proof, not a consequence of finite tests. + +From the repository root: + +```sh +python3 -B -S -m unittest discover -s reviews/lm006_endpoint_extension_20261005 -p 'test_*.py' -v +python3 -B -O -S -m unittest discover -s reviews/lm006_endpoint_extension_20261005 -p 'test_*.py' -v +python3 -B -S reviews/lm006_endpoint_extension_20261005/endpoint_check.py +python3 -B -O -S reviews/lm006_endpoint_extension_20261005/endpoint_check.py +``` + +The explicit mutants M1–M5 replace 12 by 6 in the cubic pin row, flip the +negative-endpoint kernel sign, omit pin subtraction, reverse the prescribed +height gap, or replace the six-dimensional norm moment with the scalar one. +`--mutant M1` (and each of M2–M5) must exit 1 with `ENDPOINT_CHECK_FAIL`; +`--mutant BAD` must exit 2. Runtime checks do not depend on Python `assert`. +These commands do not fetch sources, access the network, run Lean, or change +any repository status. Existing hosted workflows are not claimed to execute +this new standalone checker automatically. + +## 8. Sources, coordination, and exclusions + +[S1] P02-LM-006 / LCR-DER-019-v1.0, frozen body named in §1. Public repository +`d6g8k5htny-coder/main`, commit `7caac254cbba5f513b2dc0afb56b78a598bc0c93`, full +file blob `e8d2e822eb49b2fcf3459a58868ce911e6d4ff80`. Exact path, body extraction +rule and consumed sections are in `SOURCES.json`. The original is unchanged. + +[S2] Native source-bound conditional review, main#229 comment +[6002603423](https://github.com/d6g8k5htny-coder/main/issues/229#issuecomment-6002603423), +xAI/Grok 4.7, Cursor session `bc-ac2ce04c-f30f-4443-8f02-f0943bde635d`. +This is a review of S1, **not of this new note**. New companion review is +separate; old semantic or execution approval is not transferred. + +[S3] Author-side explicit Gram witness, main#229 comment +[6002756269](https://github.com/d6g8k5htny-coder/main/issues/229#issuecomment-6002756269). +The witness's reviewer retains that separate scope. GP-DER-044 source/frame +reconciliation is separately claimed at comment6002782190. This note does +not duplicate that source audit or silently choose between colliding IDs. +Our endpoint claim is comment6002912204. + +External reconnaissance: Louis Gass and Michele Stecconi, *The number of +critical points of a Gaussian field: finiteness of moments*, Probability +Theory and Related Fields **190**, 1167–1197 (2024), DOI +`10.1007/s00440-024-01273-5`; author preprint +[arXiv:2305.17586v2](https://arxiv.org/abs/2305.17586v2), §§1.2 and 2.1. +Located via Consensus and checked against the primary author text and +publisher metadata. Its interpolation treatment is methodological context. +A critical-point **count** moment theorem is not the endpoint-vector moment +premise proved here; no theorem from that paper is used as a substitute for +our pin identities or Gaussian conditioning calculation. + +This companion proves an explicit endpoint extension and moment implication +under §1, with a separate sufficient regularity criterion in §6. It does not +by itself certify the covariance/pin identification for the concrete model, +remove the conditional status of S2, prove a Palm event tail, exact capture, +P0.1/P0.2, an all-marks/higher-dimensional assertion, numerical constants, or +full formal-package alignment. No original proof, status/register/prize/flag, +workflow, or prior review disposition is changed. Authoring this companion +is not nonauthor review, integration is not acceptance, and no Lean run is +claimed. diff --git a/reviews/lm006_endpoint_extension_20261005/SOURCES.json b/reviews/lm006_endpoint_extension_20261005/SOURCES.json new file mode 100644 index 000000000..1642f3516 --- /dev/null +++ b/reviews/lm006_endpoint_extension_20261005/SOURCES.json @@ -0,0 +1,55 @@ +{ + "schema_version": 1, + "scientific_effect": "NONE", + "purpose": "Sources and consumed scopes, not a scientific status register", + "author": { + "provider": "OpenAI", + "model": "GPT-6 Astra Pro", + "session": "cross-source-closure-round9-20261005" + }, + "sources": [ + { + "id": "S1", + "repository": "d6g8k5htny-coder/main", + "commit": "7caac254cbba5f513b2dc0afb56b78a598bc0c93", + "path": "drive/mirrors/02_RESEARCH_CARRY_FORWARD_CANON/00 — PRIORITY OPEN MATHEMATICAL TARGETS/P0.1 — UNIFORM ADJACENCY POSITIVITY/04_REVIEW_AND_FALSIFIERS/57_P02_LM006_EXACT_NORMALIZER_REVIEW/LCR-DER-019-v1.0 — P02-LM-006 Exact Full-Field Normalizer r2 Asymptotic.export.txt", + "git_blob": "e8d2e822eb49b2fcf3459a58868ce911e6d4ff80", + "frozen_body_bytes": 9147, + "frozen_body_sha256": "239ed094f70aa4352021572ad8bdc0c6ac6404edab4e1d7e61addec0c6659150", + "extraction": "Text after LF ending literal BEGIN_FROZEN_LEMMA_BODY line, before subsequent END_FROZEN_LEMMA_BODY line; CRLF/CR to LF; strip trailing LFs; append exactly one LF; UTF-8 without BOM. No blank-run halving.", + "consumed_sections": [ + "1 exact law and six pins", + "2 adjusted endpoint definitions", + "3 target conditional limit", + "4 exact determinant factorization", + "7 target endpoint eighth-moment premise" + ], + "review_transfer": false + }, + { + "id": "S2", + "url": "https://github.com/d6g8k5htny-coder/main/issues/229#issuecomment-6002603423", + "role": "historical-body conditional review; not a review of new note" + }, + { + "id": "S3", + "url": "https://github.com/d6g8k5htny-coder/main/issues/229#issuecomment-6002756269", + "role": "separate conditional Gram witness; application and review remain separately scoped" + }, + { + "id": "EXT1", + "authors": [ + "Louis Gass", + "Michele Stecconi" + ], + "title": "The number of critical points of a Gaussian field: finiteness of moments", + "doi": "10.1007/s00440-024-01273-5", + "journal_year": 2024, + "preprint": "https://arxiv.org/abs/2305.17586v2", + "preprint_year": 2023, + "consensus_id": "c85c28354f825e53a6abcf2c1f8cb049", + "role": "external methodological context only; not a consumed theorem premise" + } + ], + "claim": "https://github.com/d6g8k5htny-coder/main/issues/229#issuecomment-6002912204" +} diff --git a/reviews/lm006_endpoint_extension_20261005/endpoint_check.py b/reviews/lm006_endpoint_extension_20261005/endpoint_check.py new file mode 100644 index 000000000..ab721f4d8 --- /dev/null +++ b/reviews/lm006_endpoint_extension_20261005/endpoint_check.py @@ -0,0 +1,171 @@ +#!/usr/bin/env python3 +"""Exact rational controls for NOTE.md. Not an analytic or Lean proof. + +Run with Python's standard library only. M1--M5 intentionally alter a named +factor, sign, subtraction, prescribed gap, or Gaussian dimension. +""" +import argparse +from collections import Counter +from fractions import Fraction as Q +import json +import sys + + +def rational(x): + if isinstance(x, bool) or not isinstance(x, (int, Q)): + raise TypeError('exact int or Fraction required') + return Q(x) + + +def radius(r): + r = rational(r) + if r <= 0: + raise ValueError('r must be positive') + return r + + +def six(values): + values = tuple(rational(v) for v in values) + if len(values) != 6: + raise ValueError('exactly six coordinates required') + return values + + +def frame(raw, r, mutant=None): + r = radius(r) + fm, dxm, hym, fp, dxp, hyp = six(raw) + p0, p1, p2 = (fm+fp)/2, (dxm+dxp)/2, (hym+hyp)/2 + factor = 6 if mutant == 'M1' else 12 + return (p0, p1, p2, (dxp-dxm)/r, (hyp-hym)/r, + factor/r**2*(p1-(fp-fm)/r)) + + +def unframe(values, r): + r = radius(r) + p0, p1, p2, p3, p4, p5 = six(values) + shift = r*p1/2-r**3*p5/24 + return (p0-shift, p1-r*p3/2, p2-r*p4/2, + p0+shift, p1+r*p3/2, p2+r*p4/2) + + +def prescribed_pins(b, r, mutant=None): + b, r = rational(b), radius(r) + sign = 1 if mutant == 'M4' else -1 + return (b, Q(0), Q(0), b+sign*r**3/6, Q(0), Q(0)) + + +def poly(p): + p = tuple(rational(c) for c in p) + if not p: + raise ValueError('nonempty polynomial required') + return p + + +def value(p, x): + out = Q(0) + for coefficient in reversed(p): + out = out*x+coefficient + return out + + +def diff(p, n=1): + p = poly(p) + for _ in range(n): + p = tuple(j*p[j] for j in range(1,len(p))) or (Q(0),) + return p + + +def weighted_integral(p, r, kernel): + # Integrate kernel(u)*p(r*u) on [-1/2,1/2] exactly. + terms = Q(0) + for j, coefficient in enumerate(poly(p)): + for k, weight in enumerate(poly(kernel)): + power = j+k+1 + terms += coefficient*r**j*weight*(Q(1,2)**power-Q(-1,2)**power)/power + return terms + + +def direct(f, h, r, mutant=None): + r = radius(r) + f, h = poly(f), poly(h) + df, d2f, dh = diff(f), diff(f,2), diff(h) + m, p = -r/2, r/2 + raw = (value(f,m),value(df,m),value(h,m),value(f,p),value(df,p),value(h,p)) + _, _, _, p3, p4, p5 = frame(raw,r,mutant) + subtract3, subtract4 = (0,0) if mutant == 'M3' else (p3,p4) + return {'P3':p3, 'P4':p4, 'P5':p5, + 'Aminus':(value(d2f,m)-subtract3)/r, + 'Aplus':(value(d2f,p)-subtract3)/r, + 'Bminus':(value(dh,m)-subtract4)/r, + 'Bplus':(value(dh,p)-subtract4)/r} + + +def kernels(f, h, r, mutant=None): + r = radius(r) + minus = (Q(1,2),Q(-1)) if mutant == 'M2' else (Q(-1,2),Q(1)) + plus = (Q(1,2),Q(1)) + d3f, d2h = diff(f,3),diff(h,2) + return {'P3':weighted_integral(diff(f,2),r,(1,)), + 'P4':weighted_integral(diff(h),r,(1,)), + 'P5':weighted_integral(d3f,r,(Q(3,2),0,-6)), + 'Aminus':weighted_integral(d3f,r,minus), + 'Aplus':weighted_integral(d3f,r,plus), + 'Bminus':weighted_integral(d2h,r,minus), + 'Bplus':weighted_integral(d2h,r,plus)} + + +def gaussian_norm8(d, mutant=None): + if isinstance(d,bool) or not isinstance(d,int): + raise TypeError('dimension must be an integer') + if d <= 0: + raise ValueError('dimension must be positive') + if mutant == 'M5': + return 105 # invalid substitution of the scalar normal eighth moment + return d*(d+2)*(d+4)*(d+6) + + +def run_checks(mutant=None): + counts = Counter() + def check(group, actual, expected): + if actual != expected: + raise ValueError(f'{group}: {actual!r} != {expected!r}') + counts[group] += 1 + radii = (Q(1,128),Q(1,50),Q(1,7),Q(1,2),Q(1),Q(5,2)) + for r in radii: + for j in range(1,21): + raw = tuple(Q((-1)**i*(j+i),i+1) for i in range(6)) + check('frame_inversion',unframe(frame(raw,r,mutant),r),raw) + for b in (Q(6,5),Q(-3),Q(0)): + check('conditioned_frame',frame(prescribed_pins(b,r,mutant),r,mutant), + (b-r**3/12,Q(0),Q(0),Q(0),Q(0),Q(2))) + for j in range(14): + p = (Q(0),)*j+(Q(1),) + lhs,rhs = direct(p,p,r,mutant),kernels(p,p,r,mutant) + for key in lhs: + check('kernel_identity',lhs[key],rhs[key]) + v = direct((0,0,1),(0,),r,mutant) + check('subtraction_control',(v['Aminus'],v['Aplus']),(0,0)) + for d, expected in ((1,105),(2,384),(6,5760)): + check('normal_eighth_moment',gaussian_norm8(d,mutant),expected) + for k, mass in (((Q(3,2),0,-6),Q(1)),((Q(-1,2),1),Q(-1,2)),((Q(1,2),1),Q(1,2))): + check('kernel_mass',weighted_integral((1,),Q(1),k),mass) + return {'passed':True,'counts':dict(sorted(counts.items())), + 'total':sum(counts.values()),'arithmetic':'fractions.Fraction', + 'scope':'finite exact algebra controls; no field acceptance or Lean execution'} + + +def main(argv=None): + parser=argparse.ArgumentParser(description=__doc__) + parser.add_argument('--mutant',choices=['M1','M2','M3','M4','M5']) + args=parser.parse_args(argv) + try: + result=run_checks(args.mutant) + except (ValueError,TypeError) as exc: + print('ENDPOINT_CHECK_FAIL: '+str(exc),file=sys.stderr) + return 1 + print(json.dumps(result,sort_keys=True,indent=2)) + return 0 + + +if __name__=='__main__': + sys.exit(main()) diff --git a/reviews/lm006_endpoint_extension_20261005/test_endpoint_check.py b/reviews/lm006_endpoint_extension_20261005/test_endpoint_check.py new file mode 100644 index 000000000..1999a5fb3 --- /dev/null +++ b/reviews/lm006_endpoint_extension_20261005/test_endpoint_check.py @@ -0,0 +1,142 @@ +"""Exact algebra controls; these are not a Gaussian-field or Lean proof.""" +from fractions import Fraction as Q +import importlib.util +import json +from pathlib import Path +import random +import subprocess +import sys +import unittest + +HERE = Path(__file__).resolve().parent +SOURCE = HERE / 'endpoint_check.py' + + +def eval_poly(p, x): + return sum((a * x**j for j, a in enumerate(p)), Q(0)) + + +def derivative(p, order=1): + for _ in range(order): + p = [j * a for j, a in enumerate(p)][1:] + return p or [Q(0)] + + +def integrate(p, lo=Q(-1, 2), hi=Q(1, 2)): + return sum((a * (hi**(j+1) - lo**(j+1)) / (j+1) + for j, a in enumerate(p)), Q(0)) + + +class EndpointTests(unittest.TestCase): + def setUp(self): + self.assertTrue(SOURCE.is_file(), 'endpoint implementation is missing') + spec = importlib.util.spec_from_file_location('endpoint_check_under_test', SOURCE) + self.m = importlib.util.module_from_spec(spec) + spec.loader.exec_module(self.m) + + def test_frame_is_invertible_on_arbitrary_rational_pins(self): + rng = random.Random(1005) + for r in (Q(1,128), Q(1,7), Q(2), Q(5,2)): + for _ in range(30): + raw = tuple(Q(rng.randint(-20,20), rng.randint(1,9)) for _ in range(6)) + p = self.m.frame(raw, r) + self.assertEqual(self.m.unframe(p, r), raw) + + def test_prescribed_pins_have_bounded_transformed_values(self): + for r in (Q(1,128), Q(1,3), Q(2)): + for b in (Q(6,5), Q(-3), Q(0)): + raw = (b, Q(0), Q(0), b-r**3/6, Q(0), Q(0)) + self.assertEqual(self.m.frame(raw, r), (b-r**3/12, Q(0), Q(0), Q(0), Q(0), Q(2))) + self.assertEqual(self.m.prescribed_pins(b,r), raw) + + def test_cubic_frame_kernel_on_monomials(self): + for r in (Q(1,64), Q(1,3), Q(1), Q(5,2)): + for j in range(14): + f = [Q(0)]*j+[Q(1)] + d = derivative(f) + raw = (eval_poly(f,-r/2), eval_poly(d,-r/2), Q(0), + eval_poly(f,r/2), eval_poly(d,r/2), Q(0)) + lhs = self.m.frame(raw,r)[5] + self.assertEqual(lhs, self.m.kernels(f,[Q(0)],r)['P5']) + + def test_endpoint_kernels_on_general_polynomials(self): + rng = random.Random(1105) + for r in (Q(1,50), Q(1,2), Q(7,3)): + for _ in range(30): + f = [Q(rng.randint(-5,5)) for _ in range(10)] + h = [Q(rng.randint(-5,5)) for _ in range(8)] + direct = self.m.direct(f,h,r) + kernels = self.m.kernels(f,h,r) + for key in ('P3','P4','P5','Aminus','Aplus','Bminus','Bplus'): + self.assertEqual(direct[key],kernels[key],key) + + def test_kernel_masses_and_lower_degree_annihilation(self): + self.assertEqual(integrate([Q(3,2),Q(0),Q(-6)]),1) + self.assertEqual(integrate([Q(-1,2),Q(1)]),Q(-1,2)) + self.assertEqual(integrate([Q(1,2),Q(1)]),Q(1,2)) + for j in range(3): + f = [Q(0)]*j+[Q(1)] + values = self.m.kernels(f,[Q(0)],Q(1,2)) + self.assertEqual(values['P5'],0) + self.assertEqual(values['Aminus'],0) + self.assertEqual(values['Aplus'],0) + + def test_exact_cubic_and_transverse_limits(self): + # F'''=2, H''=a=4. No finite-r approximation is used. + for r in (Q(1,1000),Q(1,2),Q(3)): + v = self.m.direct([Q(6,5),0,0,Q(1,3)],[0,0,Q(2)],r) + self.assertEqual((v['Aminus'],v['Aplus'],v['Bminus'],v['Bplus']),(-1,1,-2,2)) + self.assertEqual(v['P5'],2) + + def test_subtraction_is_load_bearing(self): + # F=x^2: raw F''/r diverges, whereas the adjusted endpoint is zero. + for r in (Q(1,2),Q(1,8),Q(1,128)): + v=self.m.direct([0,0,Q(1)],[0],r) + self.assertEqual((v['Aminus'],v['Aplus']),(0,0)) + self.assertGreater(Q(2)/r,0) + + def test_full_dimension_gaussian_eighth_moment(self): + self.assertEqual(self.m.gaussian_norm8(6),5760) + self.assertEqual(self.m.gaussian_norm8(1),105) + self.assertEqual(self.m.gaussian_norm8(2),384) + + def test_bad_radius_and_shape_rejected(self): + for r in (Q(0),Q(-1),0.5,True): + with self.assertRaises((ValueError,TypeError)): + self.m.frame((Q(0),)*6,r) + with self.assertRaises(ValueError): + self.m.frame((Q(0),)*5,Q(1)) + for d in (0,-1,2.5,True): + with self.assertRaises((ValueError,TypeError)): + self.m.gaussian_norm8(d) + + def test_baseline_checks_and_normal_optimized_cli(self): + outputs=[] + for mode in ([],['-O']): + p=subprocess.run([sys.executable,'-B',*mode,'-S',str(SOURCE)],capture_output=True,check=False) + self.assertEqual(p.returncode,0,p.stderr) + self.assertEqual(p.stderr,b'') + result=json.loads(p.stdout) + self.assertTrue(result['passed']) + self.assertGreater(result['total'],500) + outputs.append(p.stdout) + self.assertEqual(*outputs) + + def test_mutants_fail_in_both_modes(self): + for mode in ([],['-O']): + for mutation in ('M1','M2','M3','M4','M5'): + p=subprocess.run([sys.executable,'-B',*mode,'-S',str(SOURCE),'--mutant',mutation],capture_output=True,check=False) + self.assertEqual(p.returncode,1,(mutation,p.stdout,p.stderr)) + self.assertIn(b'ENDPOINT_CHECK_FAIL',p.stderr) + self.assertEqual(p.stdout,b'') + + def test_invalid_cli_arguments(self): + for mode in ([],['-O']): + for args in (['--mutant','BAD'],['--unknown'],['--mutant']): + p=subprocess.run([sys.executable,'-B',*mode,'-S',str(SOURCE),*args],capture_output=True,check=False) + self.assertEqual(p.returncode,2,p.stderr) + self.assertEqual(p.stdout,b'') + + +if __name__=='__main__': + unittest.main()