diff --git a/.github/workflows/remote-distance-moments-review.yml b/.github/workflows/remote-distance-moments-review.yml new file mode 100644 index 000000000..62456d897 --- /dev/null +++ b/.github/workflows/remote-distance-moments-review.yml @@ -0,0 +1,60 @@ +name: Remote distance-moments nonauthor review checks + +'on': + pull_request: + paths: + - 'reviews/remote_distance_moments_claude_20260929/**' + - '.github/workflows/remote-distance-moments-review.yml' + workflow_dispatch: + +permissions: + contents: read + +jobs: + exact-and-probe: + runs-on: ubuntu-latest + timeout-minutes: 10 + steps: + - uses: actions/checkout@11d5960a326750d5838078e36cf38b85af677262 + with: + persist-credentials: false + - uses: actions/setup-python@a26af69be951a213d495a4c3e4e4022e16d87065 + with: + python-version: '3.11.16' + - name: Verify sources, replay both modes, reject mutants + env: + PYTHONDONTWRITEBYTECODE: '1' + run: | + set -euo pipefail + python -B -S - <<'PY' + import hashlib, json, pathlib, subprocess, sys + root = pathlib.Path('reviews/remote_distance_moments_claude_20260929').resolve() + manifest = json.loads((root / 'SOURCE_FILES.json').read_text())['files'] + present = sorted(p.name for p in root.iterdir()) + expected_names = sorted([e['path'] for e in manifest] + ['SOURCE_FILES.json']) + if present != expected_names: + raise ValueError('packet tree differs from manifest: ' + repr(present)) + for entry in manifest: + path = root / entry['path'] + if pathlib.PurePosixPath(entry['path']).name != entry['path'] or path.is_symlink(): + raise ValueError('flat regular source required: ' + entry['path']) + data = path.read_bytes() + if len(data) != entry['bytes'] or hashlib.sha256(data).hexdigest() != entry['sha256']: + raise ValueError('source identity mismatch: ' + entry['path']) + script = str(root / 'distance_review_check.py') + expected = (root / 'RESULTS.json').read_bytes() + mutants = ['block-det', 'peano-slope', 'envelope-power', 'middle-cutoff', 'tail-sixth', + 'a1-constant', 'diagonal-order'] + for flags in (['-B', '-S'], ['-B', '-O', '-S']): + out = subprocess.run([sys.executable, *flags, script], + check=True, capture_output=True, timeout=300).stdout + if out != expected: + raise RuntimeError('output differs from RESULTS.json under ' + ' '.join(flags)) + for m in mutants: + rc = subprocess.run([sys.executable, *flags, script, '--mutant', m], + capture_output=True, timeout=300).returncode + if rc != 1: + raise RuntimeError('mutant ' + m + ' not rejected') + print(json.dumps({'scientific_effect': 'NONE', 'mathematical_acceptance': False})) + PY + git diff --exit-code diff --git a/.github/workflows/remote-height-marks-review.yml b/.github/workflows/remote-height-marks-review.yml new file mode 100644 index 000000000..f6bea0160 --- /dev/null +++ b/.github/workflows/remote-height-marks-review.yml @@ -0,0 +1,59 @@ +name: Remote height-marks nonauthor review checks + +'on': + pull_request: + paths: + - 'reviews/remote_height_marks_claude_20260929/**' + - '.github/workflows/remote-height-marks-review.yml' + workflow_dispatch: + +permissions: + contents: read + +jobs: + exact-and-probe: + runs-on: ubuntu-latest + timeout-minutes: 10 + steps: + - uses: actions/checkout@11d5960a326750d5838078e36cf38b85af677262 + with: + persist-credentials: false + - uses: actions/setup-python@a26af69be951a213d495a4c3e4e4022e16d87065 + with: + python-version: '3.11.16' + - name: Verify sources, replay both modes, reject mutants + env: + PYTHONDONTWRITEBYTECODE: '1' + run: | + set -euo pipefail + python -B -S - <<'PY' + import hashlib, json, pathlib, subprocess, sys + root = pathlib.Path('reviews/remote_height_marks_claude_20260929').resolve() + manifest = json.loads((root / 'SOURCE_FILES.json').read_text())['files'] + present = sorted(p.name for p in root.iterdir()) + expected_names = sorted([e['path'] for e in manifest] + ['SOURCE_FILES.json']) + if present != expected_names: + raise ValueError('packet tree differs from manifest: ' + repr(present)) + for entry in manifest: + path = root / entry['path'] + if pathlib.PurePosixPath(entry['path']).name != entry['path'] or path.is_symlink(): + raise ValueError('flat regular source required: ' + entry['path']) + data = path.read_bytes() + if len(data) != entry['bytes'] or hashlib.sha256(data).hexdigest() != entry['sha256']: + raise ValueError('source identity mismatch: ' + entry['path']) + script = str(root / 'height_marks_review_check.py') + expected = (root / 'RESULTS.json').read_bytes() + mutants = ['jacobian-r', 'drop-mass-term', 'a-le-half-q', 'full-variation'] + for flags in (['-B', '-S'], ['-B', '-O', '-S']): + out = subprocess.run([sys.executable, *flags, script], + check=True, capture_output=True, timeout=300).stdout + if out != expected: + raise RuntimeError('output differs from RESULTS.json under ' + ' '.join(flags)) + for m in mutants: + rc = subprocess.run([sys.executable, *flags, script, '--mutant', m], + capture_output=True, timeout=300).returncode + if rc != 1: + raise RuntimeError('mutant ' + m + ' not rejected') + print(json.dumps({'scientific_effect': 'NONE', 'mathematical_acceptance': False})) + PY + git diff --exit-code diff --git a/.github/workflows/remote-inverse-separation-review.yml b/.github/workflows/remote-inverse-separation-review.yml new file mode 100644 index 000000000..39efea01d --- /dev/null +++ b/.github/workflows/remote-inverse-separation-review.yml @@ -0,0 +1,60 @@ +name: Remote inverse-separation nonauthor review checks + +'on': + pull_request: + paths: + - 'reviews/remote_inverse_separation_claude_20260929/**' + - '.github/workflows/remote-inverse-separation-review.yml' + workflow_dispatch: + +permissions: + contents: read + +jobs: + exact-and-probe: + runs-on: ubuntu-latest + timeout-minutes: 10 + steps: + - uses: actions/checkout@11d5960a326750d5838078e36cf38b85af677262 + with: + persist-credentials: false + - uses: actions/setup-python@a26af69be951a213d495a4c3e4e4022e16d87065 + with: + python-version: '3.11.16' + - name: Verify sources, replay both modes, reject mutants + env: + PYTHONDONTWRITEBYTECODE: '1' + run: | + set -euo pipefail + python -B -S - <<'PY' + import hashlib, json, pathlib, subprocess, sys + root = pathlib.Path('reviews/remote_inverse_separation_claude_20260929').resolve() + manifest = json.loads((root / 'SOURCE_FILES.json').read_text())['files'] + present = sorted(p.name for p in root.iterdir()) + expected_names = sorted([e['path'] for e in manifest] + ['SOURCE_FILES.json']) + if present != expected_names: + raise ValueError('packet tree differs from manifest: ' + repr(present)) + for entry in manifest: + path = root / entry['path'] + if pathlib.PurePosixPath(entry['path']).name != entry['path'] or path.is_symlink(): + raise ValueError('flat regular source required: ' + entry['path']) + data = path.read_bytes() + if len(data) != entry['bytes'] or hashlib.sha256(data).hexdigest() != entry['sha256']: + raise ValueError('source identity mismatch: ' + entry['path']) + script = str(root / 'inverse_review_check.py') + expected = (root / 'RESULTS.json').read_bytes() + mutants = ['height-jacobian', 'envelope-endpoint', 'overlap-three', 'contact-quarter', + 'merge-rate', 'jet-duplicate', 'cdf-half'] + for flags in (['-B', '-S'], ['-B', '-O', '-S']): + out = subprocess.run([sys.executable, *flags, script], + check=True, capture_output=True, timeout=300).stdout + if out != expected: + raise RuntimeError('output differs from RESULTS.json under ' + ' '.join(flags)) + for m in mutants: + rc = subprocess.run([sys.executable, *flags, script, '--mutant', m], + capture_output=True, timeout=300).returncode + if rc != 1: + raise RuntimeError('mutant ' + m + ' not rejected') + print(json.dumps({'scientific_effect': 'NONE', 'mathematical_acceptance': False})) + PY + git diff --exit-code diff --git a/.github/workflows/remote-inverse-separation.yml b/.github/workflows/remote-inverse-separation.yml new file mode 100644 index 000000000..b6131b954 --- /dev/null +++ b/.github/workflows/remote-inverse-separation.yml @@ -0,0 +1,33 @@ +name: Remote inverse-separation finite controls + +'on': + pull_request: + paths: + - 'frontiers/remote_inverse_separation_20260928/**' + - '.github/workflows/remote-inverse-separation.yml' + push: + branches: [main] + paths: + - 'frontiers/remote_inverse_separation_20260928/**' + - '.github/workflows/remote-inverse-separation.yml' + workflow_dispatch: + +permissions: + contents: read + +jobs: + exact-inverse-separation: + runs-on: ubuntu-latest + timeout-minutes: 10 + steps: + - uses: actions/checkout@11d5960a326750d5838078e36cf38b85af677262 + with: + persist-credentials: false + - uses: actions/setup-python@a26af69be951a213d495a4c3e4e4022e16d87065 + with: + python-version: '3.11.16' + - name: Verify exact packet and both-mode intended negatives + run: | + set -euo pipefail + python -B -S frontiers/remote_inverse_separation_20260928/verify.py --output "${RUNNER_TEMP}/inverse-separation-${GITHUB_RUN_ID}-${GITHUB_RUN_ATTEMPT}" + git diff --exit-code diff --git a/docs/integration/2026-09-29-reviewed-window-and-inverse.md b/docs/integration/2026-09-29-reviewed-window-and-inverse.md new file mode 100644 index 000000000..73c7675d1 --- /dev/null +++ b/docs/integration/2026-09-29-reviewed-window-and-inverse.md @@ -0,0 +1,87 @@ +# Reviewed window modules and inverse separation — integration receipt + +Integrator: OpenAI / ChatGPT, 29 September 2026. +Scientific effect NONE: this integration changes no existing proof, review verdict, +scientific register, graph, premise, lemma flag or prize. Source integration and a +later scoped register transition are different acts. + +## Exact inputs + +Base: `e7f8aca41c308f8ad8614b587f75916943c86f27`. + +- Original #116 document packet: head `0507e3a1dbd3dede84cbeb805947c70aa16ebc36`, + tree `88d63cc679305641a8b8901bc1fbcad53fba2c42`. Its ten original documents are + now assembled together. The prior C1/C2/C3/source-map bytes are unchanged. +- Original #128 inverse-separation packet: head `b3880006df94573b4d99d05c37b3254e063035fb`, + tree `68b0a79e6b33cbde6afbe1d4385d43bc9b9e842e`, plus its original workflow. +- Anthropic #130 review packets: head `d7d0207773688961ef66b640e233c818c40d9436`. + The three records concern #128, #116 C4, and #116 C5. They carry actual analytic + ACCEPTs with dependency exposure, not automatic acceptance from finite tests. + +All three heads are retained as ancestors. The original author-side headers and +PUBLICATION.json in #116 remain historical records; this receipt supplies the +later review crosswalk, rather than modifying frozen evidence. + +## Written-module review crosswalk + +- C1/C2: `reviews/d1_elder_lower_claude_20260928/`, integrated by #124. +- C3: `reviews/remote_pair_law_claude_20260928/`, integrated by #129. +- C4: `reviews/remote_distance_moments_claude_20260929/`, amended #130. +- C5: `reviews/remote_height_marks_claude_20260929/`, #130. +- Inverse separation: `reviews/remote_inverse_separation_claude_20260929/`, #130. + +C4 is for p>=0: microscopic r^(5+p) below p=1; r^6(A1+B1) at p=1; r^6 Bp above. +Its limiting scaled-distance law has the upper tail s^-8. Its negative moment +boundary is NOT inferred from that upper tail or from a merely bounded equal-height +kernel. The real limiting moment interval (-2,7) additionally uses the positive +small-distance coefficient in the inverse-separation result. The finite-r +microscopic moment interval is (-2,1). These are expected ordered-pair laws, +not pair-event-conditioned field sampling or persistence lifetimes. + +C5 compares the singleton joint mark with the limiting contact location/index +profile times a uniform height at O(r), including deterministic varying positive- +volume E_r. It does not replace #120's stronger O(r^2) height/own-marginal result, +and neither asserts independence between location and index. + +Inverse separation has sharp fixed-r inverse power threshold two and a positive +collision coefficient. Its fixed-r cutoff equivalences do not include a bounded +remainder at power two, an arbitrary coupled cutoff, or a same-index threshold. + +All remote statements retain fixed positive rho, fixed d/L, compact marks, +original pins and full W/Z. Fixed-Borel pair limits do not cover oscillating E_r. + +## Open questions and unavailable historical execution + +Completing the five written modules does NOT solve C6's torus-wide factorial upper +bound/optimal order, C7's unrestricted selection-difference rate, or C8's numerical +constants. Those open questions are described in the historical +`reviews/candidates_pending_20260928/CANDIDATES.md`; C6 has no proof in #116. +The validated local lower obstruction excludes a global O(r^5) factorial upper +bound but supplies no matching global upper estimate. + +The original #116 algebra.py remains absent and its publication remains blocked. +It is not retried, reconstructed or treated as runnable by this integration. +PUBLICATION.json preserves the historical local execution claim with that explicit +limitation. Current published reviewer checkers are distinct new programs; they do +not recover or certify that unavailable execution. No local execution of the +reviewer programs by this integrator is claimed. + +## Verification and review lineage + +The #128 author runner was freshly replayed locally in this continuation: twelve +finite tests and eight intended semantic negatives in each Python mode, identical +paired outputs, exact source membership and identities intact. The reviewer +programs and the combined actual formal/downstream jobs are evaluated by the +current integration PR workflows. Older separate-head successes are not substitutes. +Existing scalar Lean execution does not formalize these full Gaussian proofs. + +OpenAI's review of #130 is source-exposed integration review5351523587, not another +nonauthor-provider mathematical discharge. Claude authored RC and reviewed RP and +#120, so these records check use of those inputs, not their independent truth. +All agents use one GitHub account; no organizational independence or invented +approval identity is claimed. The two C4 wording corrections changed only review +text and its manifest, preserving the checking program, results and scoped verdict. + +Before an ordinary expected-head merge, inspect fresh refs, full discussions, +combined targeted suites and the required current-commit aggregate. Preserve a +readback and post-merge check; never bypass protection for an empty queue. diff --git a/frontiers/remote_inverse_separation_20260928/PROOF.md b/frontiers/remote_inverse_separation_20260928/PROOF.md new file mode 100644 index 000000000..1b24d0f6d --- /dev/null +++ b/frontiers/remote_inverse_separation_20260928/PROOF.md @@ -0,0 +1,351 @@ +# Inverse separation of remote critical-point pairs: the missing moment boundary + +Object: OA-REMOTE-INVERSE-SEPARATION-20260928-v1. +Author: OpenAI / ChatGPT. Disposition: AUTHOR-SIDE CANDIDATE; nonauthor analytic review required. +Scientific effect NONE. No existing source, review verdict or status register is changed. + +## 1. Objects, conventions, and conclusions + +Use the exact periodized field and full pair-pinned law of RM and RC in +SOURCE_MAP.json. Fix d>=2, torus side L, remote exclusion rho>0, compact real birth +marks b and compact positive gap marks k with k_->0. The endpoints are +M=-(r/2)u, S=(r/2)u, pinned to heights b,b-k r^3 with zero gradients. Q_r is the +original Gaussian conditional law. Keep W_r=F_d(H_M)F_(d-1)(H_S), Z_r=E_Qr W_r, +and Q_r^W=(W_r/Z_r)Q_r exactly. Here F_j is the absolute determinant on index j +(counting negative eigenvalues), zero at singular matrices. No additional +normalizer or adjacency event is inserted. + +Let E be a FIXED deterministic positive-volume Borel subset of D_rho. Count all +indices of critical points in E with heights in I_r=(b-k r^3,b). All pairs below +are ordered and distinct. Let + + M_p(r)=E_Qr^W sum_{x!=x' counted in E} dist(x,x')^p, p real. (I1) + +The expectation is allowed to be infinite even though the random field has +finitely many Morse critical points almost surely. Distances are physical torus +distances. At p=0, M_0 is the second factorial moment. We always distinguish a +normalized EXPECTED PAIR MEASURE from sampling a pair after conditioning a +realized field on having two or more points. + +RP proves M_0(r)~r^5 A_0 and its blown-up pair-density limit. The separate RD +manuscript addresses p>=0 only. This note fills the negative-moment boundary +without importing RD's p=1 transition or its large-separation tail claims. + +**Theorem I (extended microscopic moments).** For every fixed -20 there is J_r in (0,infinity) such that the expected pair +separation measure, in a neighborhood of distance zero, has a density j_r with + + j_r(delta)=delta[J_r+o(1)], delta down to zero. (I3) + +Consequently, for this fixed r, M_p(r) is finite exactly when p>-2. In particular, + + E_Qr^W sum dist(x,x')^(-q) < infinity iff q<2, q>=0. (I4) + +At any fixed small delta_0>0, let I_q(r;epsilon,delta_0) restrict that inverse +sum to epsilon2: I_q ~ [J_r/(q-2)] epsilon^(2-q). (I5) + +For p>=1, Theorem II asserts finiteness, not a new r-asymptotic. For unordered +pairs, divide j_r, J_r and all unnormalized pair moments by two. + +**Theorem III (small scaled separation and compatible limits).** Under the +normalized expected ordered-pair measure, S_r=dist/r converges in probability +TV to a law S on (0,infinity). With J_0 defined in Section 5, + + J_r/r^3 -> J_0>0, + g_S(s) ~ (J_0/A_0)s as s down to zero, + P(S<=epsilon) ~ [J_0/(2A_0)]epsilon^2. (I6) + +For 0 E[S^(-q)]=A_(-q)/A_0=2. The assertions in (I3),(I5) +are fixed-r limits, and the first assertion of (I6) is a subsequent r limit. +No arbitrary joint cutoff epsilon(r) follows just from these iterated limits. + +These are local-separation facts within the SAME FIXED REMOTE region. They do +not extend rho to zero, change d or L with r, permit random field-selected E, +identify persistence partners, or give an event-conditioned pair law. They also +do not imply that same-index pairs have the same inverse threshold; the all-index +sum is essential for the positive leading diagonal coefficient used here. + +## 2. Negative moments of the blown-up pair measure + +Use RP's contact law Q_0=Law(f|U_0=v_0), with endpoint contact weight w_0 and +normalizer z_0=E_Q0 w_0>0. At remote x and unit direction e, set + + Y=(grad f(x),H_x e,f(x)), T=D^3f(x)[e,e,e], + A=H_x restricted to e-perp. + +All correlations of these variables with the endpoint contact Hessian remain +inside the same conditional expectation. Ordinary, not probability-normalized, +sphere area is denoted de. Define, for -21. The contact covariance +floor, moment bounds, and full conditional support from RP make A_p finite, +continuous, and positive. At p=0 this is exactly the all-index coefficient A_0. +The formula does not assert a pure k power law: Q_0 and the integrand also depend +on k through the endpoint target f_xxx(0)=12k. + +RP's exact coordinates x'=x+delta e, delta=r s, y=b-r^3 z and + + t=(y'-y)/delta^3 + +give the window region + + 0=1. (I10) + +It is integrable precisely for -2-2, elementary +integration up to s=(k/|t|)^(1/3) gives + + integral_0^infinity s^(p+1)(k-s^3|t|)_+ ds + = 3 k^((p+5)/3)|t|^(-(p+2)/3)/[(p+2)(p+5)]. (I11) + +RP's limiting determinant product is 36t^2(det A)^2. Integrate the density of +t=-T/12 and use + + 108*12^(-(4-p)/3)=(3/4)*12^((p+2)/3). + +This yields exactly (I8). The exceptional t=0 is a null target; Tonelli with +|t|>eta and then eta down to zero avoids assigning a value to an undefined +zero-times-infinity expression. For delta>=eta_0>0, RC's separated bound is +O(r^6); the distance weight is bounded there even for negative p. After division +by r^(5+p) it is O(r^(1-p)) and vanishes. This proves (I2). The endpoint p=-2 +cannot be decided from failure of this upper envelope alone; the next section +provides the positive lower asymptotic that resolves it. + +## 3. A different collision frame when r is held fixed + +Fix 0H e is onto in symmetric matrices, and gradient and +Hessian evaluations at x are independent linear functionals modulo the original +value/gradient evaluations at M,S. Positive spectral weights imply that a +zero-variance linear combination annihilates every Fourier mode. As a finite +sum of derivatives of delta distributions at the three distinct sites, it is +then the zero distribution; localized smooth test functions with prescribed +jets force each coefficient to vanish. Compactness gives the fixed-r floor. +Local orthonormal charts suffice for the transverse matrix A; no global sphere +frame or arbitrary-rotation invariance is assumed. + +On one unconditioned smooth Gaussian field, use the usual finite-dimensional +regression formula for these observations with the exact original targets and +G_delta=0. Integral derivative representations of the divided gradient row give +covariance convergence as delta->0; the bounded inverse and rapid Fourier +summability give convergence of the conditional fields in every fixed +L^a(C^b), with uniform moments over remote x,e. Constants in this section may +depend on this fixed r. The original pin constraints are exact throughout. + +The exact gradient-pair identity and C4 Taylor remainder yield + + H_x e/delta -> -D^3 f(x)[e,e,.]/2, + H_(x+delta e)e/delta -> +D^3 f(x)[e,e,.]/2. (I13) + +Positive congruence by diag(delta^-1/2,I) gives the two limits diag(-T/2,A) and +diag(T/2,A). Taking absolute determinants, which are continuous even on singular +matrices and have polynomial Lipschitz bounds, gives the coupled L^a limit + + |det H_x det H_(x+delta e)|/delta^2 + -> (T^2/4)(det A)^2. (I14) + +The endpoint weight W_r is also a product of continuous index-filtered +determinants; its change under this coupling converges with polynomial moment +control. The original denominator Z_r>0 is independent of delta and remains +unchanged. For an a priori dominating bound, the zero-gradient segment identity +gives |det H_x det H_(x+delta e)|<=C delta^2(1+||f||_C3)^(2d). + +The product of height indicators tends to the SINGLE indicator +1{f(x) in I_r}. To justify this despite its discontinuity, append f(x) to G_0. +Its conditional variance is positive by the same distinct-jet rank argument, +so the endpoints of I_r have zero conditional probability. Uniform convergence +also follows by bounding the probability of being within eta of either endpoint +using the uniformly bounded conditional height density, then letting eta->0. +Moment bounds and Holder control products with the determinant weights. This +argument keeps the unconditioned-in-height frame (I12); the shrinking width is +fixed and positive during this delta limit. + +## 4. Positive fixed-r diagonal coefficient and inverse divergence + +Let K_r(x,x') be the all-index, height-window pair intensity under Q_r^W, so the +marked Kac-Rice identity reads + + E_Qr^W sum F(x,x') = integral F(x,x')K_r(x,x') dx dx' + +on distinct remote pairs for nonnegative Borel F. This is the Gaussian formula +under Q_r weighted ONCE by W_r and divided ONCE by Z_r. Exhaustion away from the +diagonal and monotone convergence allow infinite nonnegative integrals. +The continuous-field mark extension is the same interface used in RM/RC. + +Equations (I12)-(I14) and the density change give, uniformly over remote x,e for +fixed r, + + delta^(d-2)K_r(x,x+delta e) -> c_r(x,e), + c_r(x,e) = p_(G0|Qr)(0)/(4Z_r) + * E_Qr[W_r T^2(det A)^2 1{f(x) in I_r}|G_0=0]. (I15) + +The coefficient is finite and continuous. It is strictly positive: conditional +on G_0=0 and the original endpoint pins, the independent symmetric entries of +the two endpoint Hessians and the remote transverse Hessian A, together with +remote height and T, have full joint Gaussian support. This follows by adding +the remaining independent derivative evaluations to the distinct-site jet list. +The open event of a typed maximum/saddle at the pinned endpoints, remote height +strictly inside I_r, nonsingular A, and T nonzero has positive probability. The +integrand in (I15) is positive there. No independence between these blocks is +needed. + +In polar coordinates the radial power is + + (d-1) from dx' - d from the gradient density + +2 from the determinants = 1. (I16) + +For delta below the injectivity scale, define the radial density explicitly by + + j_r(delta)=delta^(d-1) integral_E dx integral_S de + 1_E(x+delta e) K_r(x,x+delta e). + +The convergence in (I15) is uniform for fixed r. The bounded limit and +sup_{|h|<=delta}||1_E(.+h)-1_E||_1->0 remove the translated indicator, even for +an arbitrary fixed Borel E. Therefore (I3) holds with + + J_r=integral_E dx integral_S de c_r(x,e), 00 such that +(J_r/2)delta<=j_r(delta)<=(3J_r/2)delta on (0,delta_r), and the ratio tends to +one after division by J_r delta. At larger distances, fixed-r remote pair +covariance and Gaussian moments are bounded on separated compact sets. Thus +M_p(r) is finite iff integral_0^delta_r delta^(p+1)d delta is finite, which is +precisely p>-2. This proves (I4), including its necessity, rather than merely a +sufficient condition from an upper bound. + +To obtain the constants in (I5), fix eta>0 small so j_r(delta)/(J_r delta) lies +between 1-epsilon_1 and 1+epsilon_1 for delta0, then + epsilon_1->0. For q=2 the antiderivative is log; for q>2 it is +(delta^(2-q))/(2-q). This proves the two asymptotic equivalents in (I5). +The fixed-r constants and cutoffs are existential, not numerically evaluated. + +## 5. Matching the fixed-r coefficient to the contact coefficient + +Disintegrating the remote height in (I15) gives a useful equivalent form: + + c_r(x,e)=1/(4Z_r) integral_(b-k r^3)^b dh + p_(grad f(x),H_x e,f(x)|Qr)(0,0,h) + E_Qr[W_r T^2(det A)^2|grad f(x)=H_xe=0,f(x)=h]. (I18) + +Put h=b-k r^3 theta. The joint covariance of (U_r,grad f(x),H_xe,f(x)) has a +uniform floor through r=0: it is a subvector of RP's contact collision frame, +or follows directly from distinct derivative evaluations at 0 and remote x. +The same Gaussian regression coupling as RP and RM applies uniformly in +0<=theta<=1. Under these exact extra observations, original endpoint pin +identities give W_r/r^2 -> w_0 in every fixed L^a, and Z_r/r^2 -> z_0>0. +The remote A,T and the density also converge with bounded moments; no restricted +normalizer replaces Z_r. Dominated convergence in (I18) now yields, uniformly +on the fixed compact x,e,mark sets, + + c_r(x,e)/r^3 -> c_0(x,e) + = k/(4z_0) p_(Y|Q0)(0,0,b) + E_Q0[w_0 T^2(det A)^2|Y=(0,0,b)]. (I19) + +Integrating defines J_0=integral_E integral_S c_0 and proves J_r/r^3->J_0>0. +This is a simultaneous contact-kernel estimate for c_r, not a statement that +(I15)'s error is uniform for every joint pair (r,delta). Those are distinct +claims, and the latter is unnecessary here. + +## 6. The limiting scaled law at zero and inverse-moment convergence + +RP's L1 convergence of the blown-up density, followed by its measurable +pushforward s=dist/r, gives TV convergence of the normalized pair-weighted law +of S_r to S. Define + + Psi_E(t)=integral_E dx integral_S de p_(V0|Q0)(0,0,b,t) + E_Q0[w_0(det A)^2|V_0=(grad f,H e,f,-T/12)=(0,0,b,t)]. + +This nonnegative function is bounded, continuous, and decays faster than any +fixed inverse polynomial after appropriate polynomial moment factors. Its +weighted integral against t^2 is positive. The all-index limiting density is + + g_S(s)=36s/(z_0 A_0) integral_R t^2(k-s^3|t|)_+Psi_E(t)dt. (I20) + +At s->0, dominate the integrand by k t^2 Psi_E(t). Then + + lim g_S(s)/s = 36k/(z_0 A_0) integral t^2 Psi_E(t)dt + = J_0/A_0, (I21) + +because T=-12t converts 36t^2 to T^2/4. Integrating the positive density near +zero proves the small-separation cumulative statement in (I6). Its inverse +q-moment is finite near zero iff q<2; for q>=0 there is no inverse-moment +obstruction at infinity, since s^-q<=1 for s>=1. This proves the limiting-law +threshold, without using RD's upper-tail exponent. + +For 0 A_(-q)/A_0. + +The same weighted dominated-convergence argument computes E[S^(-q)] from +(I20), giving that value. TV convergence alone would not justify this step for +an unbounded inverse-distance observable. At q>=2, Section 4 proves the finite-r +expectation is already infinite, and (I21) proves the limit expectation is +infinite as well. All statements are about pair-weighted means, not probabilities +of the existence of a very close pair or a persistence-lifetime law. + +## 7. Scope and review obligations + +The positive diagonal coefficient, not a finite numerical fit, makes the inverse +threshold sharp. The two different collision frames must not be mixed: the +height-divided frame supplies RP's r-blow-up; the gradient-only frame supplies +the fixed-r diagonal with Jacobian delta^-d. Local curvature and polar volume +cancel the dimension in (I16). This does not assert isotropy of the torus field. + +All claimed new limits keep E fixed and remote. Fixed-r divergence, normalized +contact inverse moments, and an arbitrary coupled cutoff epsilon(r) are three +different assertions; only the first two are proved here. No rate for remainders, +leading event-probability constant, same-index inverse threshold, p>=1 +r-asymptotic, global pin-neighborhood bound or scientific-status promotion is +provided. RP's new coefficient/height law has an actual Anthropic discussion +review; its source remains on the original branch at author publication time. + +The finite runner checks powers, moment domains, cutoff integrals, determinant +and height signs on explicit polynomial fields, and coefficients. It cannot +certify Gaussian support, uniform regression, Kac-Rice applicability, or the +Borel translation argument. Those displayed analytic steps require a new +source-bound nonauthor review. No unavailable author runner is reconstructed. diff --git a/frontiers/remote_inverse_separation_20260928/README.md b/frontiers/remote_inverse_separation_20260928/README.md new file mode 100644 index 000000000..83167187c --- /dev/null +++ b/frontiers/remote_inverse_separation_20260928/README.md @@ -0,0 +1,26 @@ +# Remote inverse separation — author-side mathematical candidate + +[PROOF.md](PROOF.md) extends the microscopic moment law to -2=0 scope. Its p=1 transition and upper tail are not premises." + } + ], + "new_obligations": [ + "Fixed-r gradient-only collision coefficient and positive support", + "Height-indicator convergence and arbitrary fixed-Borel radial asymptotic", + "Contact matching J_r/r^3 and inverse-moment weighted domination" + ], + "blocked_executable_consumed_or_retried": false, + "upstream_full_replay_by_packet_runner": false, + "nonauthor_acceptance": false +} diff --git a/frontiers/remote_inverse_separation_20260928/inverse.py b/frontiers/remote_inverse_separation_20260928/inverse.py new file mode 100644 index 000000000..d63833225 --- /dev/null +++ b/frontiers/remote_inverse_separation_20260928/inverse.py @@ -0,0 +1,66 @@ +"""Exact scalar companions; not a Gaussian covariance or Kac-Rice verifier.""" +from fractions import Fraction as F + +MUTANT = None + +def gradient_density_power(d: int) -> int: + if type(d) is not int or d<2: + raise ValueError('fixed integer dimension at least two required') + return -(d+3) if MUTANT=='height-jacobian-in-gradient-frame' else -d + +def radial_power(d: int) -> int: + determinants=0 if MUTANT=='drop-soft-determinants' else 2 + return d-1+gradient_density_power(d)+determinants + +def envelope_integral(p: F) -> F: + p=F(p) + if not -2 F: + p=F(p) + if p<=-2: + raise ValueError('origin integral requires p>-2') + numerator=1 if MUTANT=='lose-overlap-three' else 3 + return numerator/((p+2)*(p+5)) + +def moment_finite(p: F) -> bool: + return F(p)>=-2 if MUTANT=='include-divergent-endpoint' else F(p)>-2 + +def inverse_cutoff(q: int, lo: F, hi: F): + if type(q) is not int or q<0 or not F(0) F: + if J<=0 or A<=0: + raise ValueError('positive intensity and mass required') + return J/A if MUTANT=='lose-cdf-half' else J/(2*A) + +def fold_data(delta: F, T: F, transverse: list[F]) -> dict: + if delta<=0 or not transverse: + raise ValueError('positive separation and nonempty transverse block required') + detA=F(1) + for a in transverse:detA*=a + gradient=lambda x:[T*x*x/2-T*delta*x/2]+[F(0)]*len(transverse) + value=lambda x:T*x**3/6-T*delta*x*x/4 + left=-T*delta*detA/2;right=T*delta*detA/2 + gap=value(delta)-value(F(0)) + if MUTANT=='reverse-height-sign':gap=-gap + return {'gradients':(gradient(F(0)),gradient(delta)), + 'height_difference':gap,'determinants':(left,right), + 'absolute_product':abs(left*right)} + +def height_width_power() -> int: + return 6 if MUTANT=='two-height-windows-at-fixed-r' else 3 + +def microscopic_power(p: F) -> F: + return F(5)+F(p) + +def pair_weight(n: int) -> int: + if type(n) is not int or n<0: + raise ValueError('nonnegative integer count required') + return int(n>=2) if MUTANT=='event-not-factorial-weight' else n*(n-1) diff --git a/frontiers/remote_inverse_separation_20260928/test_inverse.py b/frontiers/remote_inverse_separation_20260928/test_inverse.py new file mode 100644 index 000000000..3c22788ed --- /dev/null +++ b/frontiers/remote_inverse_separation_20260928/test_inverse.py @@ -0,0 +1,79 @@ +"""Exact finite controls; the continuum argument is in PROOF.md.""" +from fractions import Fraction as F +import unittest +import inverse as m + +class InverseTests(unittest.TestCase): + def test_gradient_only_density_jacobian(self): + for d in range(2,10): + self.assertEqual(m.gradient_density_power(d),-d) + + def test_radial_power_independent_of_dimension(self): + for d in range(2,10): + self.assertEqual(m.radial_power(d),1) + + def test_microscopic_envelope_domain(self): + for p in (F(-7,4), F(-1), F(0), F(1,2)): + self.assertEqual(m.envelope_integral(p),1/(p+2)+1/(1-p)) + for p in (F(-3),F(-2),F(1),F(2)): + with self.assertRaises(ValueError):m.envelope_integral(p) + + def test_integrated_overlap_coefficient(self): + for p in (F(-7,4),F(-1),F(0),F(1,2),F(2)): + self.assertEqual(m.overlap_coefficient(p),1/(p+2)-1/(p+5)) + self.assertEqual(m.overlap_coefficient(F(0)),F(3,10)) + with self.assertRaises(ValueError):m.overlap_coefficient(F(-2)) + + def test_inverse_endpoint_is_not_finite(self): + for q in (F(0),F(1),F(199,100)): + self.assertTrue(m.moment_finite(-q)) + for q in (F(2),F(3),F(10)): + self.assertFalse(m.moment_finite(-q)) + + def test_fixed_r_cutoff_logarithm(self): + self.assertEqual(m.inverse_cutoff(2,F(1,100),F(1,2)), + {'kind':'log','ratio':F(50),'coefficient':F(1)}) + + def test_fixed_r_cutoff_powers(self): + lo,hi=F(1,100),F(1,2) + self.assertEqual(m.inverse_cutoff(0,lo,hi),(hi*hi-lo*lo)/2) + self.assertEqual(m.inverse_cutoff(1,lo,hi),hi-lo) + self.assertEqual(m.inverse_cutoff(3,lo,hi),1/lo-1/hi) + self.assertEqual(m.inverse_cutoff(4,lo,hi),(lo**-2-hi**-2)/2) + with self.assertRaises(ValueError):m.inverse_cutoff(3,F(0),hi) + + def test_small_separation_cdf_has_half(self): + self.assertEqual(m.small_cdf_coefficient(F(7),F(3)),F(7,6)) + + def test_exact_polynomial_fold_data(self): + for d in (2,3,4): + for delta in (F(1,3),F(1,11)): + for T in (F(-5),F(7,3)): + transverse=[F((-1)**i*(i+1)) for i in range(d-1)] + detA=F(1) + for a in transverse:detA*=a + result=m.fold_data(delta,T,transverse) + self.assertEqual(result['gradients'],([F(0)]*d,[F(0)]*d)) + self.assertEqual(result['height_difference'],-T*delta**3/12) + self.assertEqual(result['determinants'],(-T*delta*detA/2,T*delta*detA/2)) + self.assertEqual(result['absolute_product'],delta**2*T**2*detA**2/4) + + def test_t_to_T_and_coefficient_conversion(self): + self.assertEqual(36*F(1,12)**2,F(1,4)) + self.assertEqual(108/F(12)**2,F(3,4)) + self.assertEqual(m.height_width_power(),3) + + def test_negative_moment_scaling(self): + for q in (F(1,2),F(1),F(3,2)): + self.assertEqual(m.microscopic_power(-q),5-q) + self.assertEqual(q+m.microscopic_power(-q)-m.microscopic_power(0),0) + self.assertGreater(6-m.microscopic_power(-q),0) + + def test_probability_size_bias_not_event_sampling(self): + # P(N=2)=1/4, P(N=3)=1/4: pair weighting differs from event weighting. + self.assertEqual(m.pair_weight(2),2) + self.assertEqual(m.pair_weight(3),6) + self.assertEqual(F(1,4)*m.pair_weight(2)/(F(1,4)*m.pair_weight(2)+F(1,4)*m.pair_weight(3)),F(1,4)) + self.assertNotEqual(F(1,4),F(1,2)) + +if __name__=='__main__':unittest.main() diff --git a/frontiers/remote_inverse_separation_20260928/verify.py b/frontiers/remote_inverse_separation_20260928/verify.py new file mode 100644 index 000000000..d74dd57fd --- /dev/null +++ b/frontiers/remote_inverse_separation_20260928/verify.py @@ -0,0 +1,94 @@ +"""Exact packet and both-mode finite verification. No network or proof-status writes.""" +import argparse +import hashlib +import io +import json +from pathlib import Path +import subprocess +import sys +import unittest + +ROOT=Path(__file__).resolve().parent +MUTANTS={ + 'height-jacobian-in-gradient-frame':'test_gradient_only_density_jacobian', + 'drop-soft-determinants':'test_radial_power_independent_of_dimension', + 'lose-overlap-three':'test_integrated_overlap_coefficient', + 'include-divergent-endpoint':'test_inverse_endpoint_is_not_finite', + 'lose-cdf-half':'test_small_separation_cdf_has_half', + 'reverse-height-sign':'test_exact_polynomial_fold_data', + 'two-height-windows-at-fixed-r':'test_t_to_T_and_coefficient_conversion', + 'event-not-factorial-weight':'test_probability_size_bias_not_event_sampling', +} + +def require(ok, message): + if not ok:raise ValueError(message) + +def decode(text): + def pairs(items): + out={} + for k,v in items: + require(k not in out,'duplicate JSON key: '+k);out[k]=v + return out + return json.loads(text,object_pairs_hook=pairs) + +def identity(path): + require(path.is_file() and not path.is_symlink(),'regular source required') + data=path.read_bytes() + return {'bytes':len(data),'sha256':hashlib.sha256(data).hexdigest(), + 'git_blob':hashlib.sha1(f'blob {len(data)}\0'.encode()+data).hexdigest()} + +def source_check(): + identity(ROOT/'SOURCE_FILES.json') + entries=decode((ROOT/'SOURCE_FILES.json').read_text())['files'] + names=[e['path'] for e in entries] + require(len(names)==len(set(names)) and all(Path(n).name==n and n!='SOURCE_FILES.json' for n in names),'unique flat paths required') + require(sorted(p.name for p in ROOT.iterdir())==sorted(names+['SOURCE_FILES.json']),'source membership differs') + for e in entries: + require(identity(ROOT/e['path'])=={k:e[k] for k in ['bytes','sha256','git_blob']},'source identity differs: '+e['path']) + return {p.name:identity(p) for p in sorted(ROOT.iterdir())} + +def child(mutant): + import inverse + import test_inverse + inverse.MUTANT=mutant + result=unittest.TextTestRunner(stream=io.StringIO()).run(unittest.defaultTestLoader.loadTestsFromModule(test_inverse)) + out={'tests':result.testsRun,'passed':result.wasSuccessful(), + 'failures':sorted(t.id().rsplit('.',1)[-1] for t,_ in result.failures), + 'errors':sorted(t.id().rsplit('.',1)[-1] for t,_ in result.errors)} + print(json.dumps(out,sort_keys=True)) + return 0 if result.wasSuccessful() else 1 + +def replay(output): + output=output.resolve() + require(not output.exists() and not output.is_relative_to(ROOT),'new output directory outside packet required') + before=source_check();output.mkdir(parents=True) + records={} + for case in ['baseline',*MUTANTS]: + outputs=[] + for mode,flags in [('normal',[]),('optimized',['-O'])]: + cmd=[sys.executable,'-B',*flags,'-S',str(ROOT/'verify.py'),'--child'] + if case!='baseline':cmd+=['--mutant',case] + p=subprocess.run(cmd,capture_output=True,timeout=30) + (output/(case+'_'+mode+'.stdout')).write_bytes(p.stdout) + (output/(case+'_'+mode+'.stderr')).write_bytes(p.stderr) + r=decode(p.stdout.decode()) + require(not p.stderr and not r['errors'],'execution error rather than semantic test: '+case) + require(r['tests']==12,'wrong finite test count') + if case=='baseline':require(p.returncode==0 and r['passed'] and not r['failures'],'baseline failed') + else:require(p.returncode==1 and not r['passed'] and MUTANTS[case] in r['failures'],'intended assertion did not reject: '+case) + outputs.append(p.stdout) + require(outputs[0]==outputs[1],'Python modes disagree: '+case) + records[case]=decode(outputs[0].decode()) + summary={'tests_per_mode':12,'semantic_mutants_per_mode':8,'identical_output_pairs':9, + 'all_intended_failures':True,'scientific_effect':'NONE','continuum_analysis_verified_by_code':False} + require(summary==decode((ROOT/'RESULTS.json').read_text()),'stored summary differs') + require(source_check()==before,'source changed during execution') + (output/'REPORT.json').write_text(json.dumps({**summary,'sources_unchanged':True,'source_identities':before,'cases':records},sort_keys=True,indent=2)+'\n') + print(json.dumps(summary,sort_keys=True,indent=2));return 0 + +if __name__=='__main__': + p=argparse.ArgumentParser(description=__doc__);g=p.add_mutually_exclusive_group(required=True) + g.add_argument('--child',action='store_true');g.add_argument('--output',type=Path) + p.add_argument('--mutant',choices=MUTANTS);a=p.parse_args() + require(a.child or a.mutant is None,'mutant requires child mode') + raise SystemExit(child(a.mutant) if a.child else replay(a.output)) diff --git a/frontiers/window_multiplicity_laws_20260928/HEIGHT_MARKS.md b/frontiers/window_multiplicity_laws_20260928/HEIGHT_MARKS.md new file mode 100644 index 000000000..015d76967 --- /dev/null +++ b/frontiers/window_multiplicity_laws_20260928/HEIGHT_MARKS.md @@ -0,0 +1,159 @@ +# The missing single-witness height mark: uniformity and joint conditional law + +Object: OA-WINDOW-MULTIPLICITY-HEIGHT-20260928-v1. +Author: OpenAI / ChatGPT, foreground research session, 28 September 2026. +Disposition: AUTHOR-SIDE COROLLARY; NONAUTHOR ANALYTIC REVIEW REQUIRED. +Scientific effect: NONE. No existing source or scientific disposition changes. + +## 1. The premise is pointwise in the height, not only an integrated mean + +Use the fixed-remote setting of [RM] and [RC] from SOURCE_MAP.json. The original +endpoint observations, maximum/saddle determinant tilt, full normalizer, fixed +d>=2,L,rho>0, and compact positive gap marks are unchanged. Let E be any +deterministic Borel subset of the same D_rho. Its positive volume may depend on r. +Let N_r count all critical indices in E whose heights are in I_r=(b-k r^3,b). + +The remote singleton-law candidate [SL] explicitly discards the height mark. +Its integrated mean formula alone does not determine the height distribution: +equal integrals can belong to different densities. The stronger premise needed +here is already written and proved in **[RM, Section 5, immediately after (13)]**. +In its notation the exact pre-height-integrated density is + + R_{r,j}(x,h) + = p_{(grad f(x),f(x))|U_r=v_r}(0,h) + E[W_r F_j(H_x) | U_r=v_r,grad f(x)=0,f(x)=h]/Z_r, + +and, uniformly for x in D_rho, h in [b-k r^3,b], j and compact marks/frames, + + |R_{r,j}(x,h)-Lambda_j(x;b,k,u)| <= C r. (H1) + +This is exactly the complete integrand of [RM, (12)] after its r^2/Z_r factor. +The proof retains the **actual additional height pin**, uses a common Gaussian +regression coupling, controls W_r/r^2 under that extra conditioning, and compares +the full normalizer with z_0. No zero mean, independence, or extra endpoint +Jacobian is inserted here. + +The weighted Kac-Rice identity is a finite measure identity in location, height +and index. One obtains it first for continuous nonnegative height test functions +by the expected-integral formula, then for bounded Borel test functions by equality +of measures and monotone approximation. Individual endpoint heights have zero +mean count. These facts are already part of [RM]'s height disintegration; the +application does not feed an arbitrary Borel weight directly into a theorem whose +stated hypothesis is lower semicontinuity. + +## 2. The rescaled height mean measure + +Define the normalized deficit mark + + theta=(b-f(x))/(k r^3), 00, + + ||mu/m-nu/n||_var + <= (||mu-nu||_var+|m-n|)/m + <= 2||mu-nu||_var/m. + +The factor |E| cancels. A null-volume E has zero count almost surely and no +conditional nonempty or singleton law is asserted there. + +## 3. From a mean mark to the actual unique witness + +Let q_r=E[N_r(N_r-1)]. The fixed-remote bound [RC, Corollary D] gives + + q_r <= C r^5 |E|, q_r/m_r <= C r^2. (H5) + +Write sigma_r for the mark submeasure from singleton configurations and eta_r +for the mean mark measure contributed on N_r>=2. Then + + mu_r=sigma_r+eta_r, + sigma_r(S_E)=p_{1,r}:=P(N_r=1), + eta_r(S_E)=a_r:=E[N_r;N_r>=2] <= q_r. + +For small r, p_{1,r}=m_r-a_r>=m_r-q_r>0. The exact mixture identity + + mu_r/m_r=(p_{1,r}/m_r)(sigma_r/p_{1,r})+eta_r/m_r + +gives dTV(sigma_r/p_{1,r},mu_r/m_r)<=a_r/m_r<=C r^2. Combining with (H4) proves: + +**Theorem H1 (single-point joint height law).** Uniformly for every deterministic +positive-volume E=E_r inside the same fixed D_rho, + + dTV(Law((x,index,theta) of the unique point | N_r=1), + pi_E tensor Uniform(0,1)) <= C r. (H6) + +In particular the deficit height tends to a uniform distribution and is +asymptotically independent of the **joint** location/index mark. No independence +between location and index is claimed. + +For completeness the integer inequalities imply + + m_r-P(N_r>=1) <= q_r/2, + P(N_r>=2 | N_r>=1) <= q_r/(2P(N_r>=1)) <= C r^2. (H7) + +There is also a complete-configuration version: conditioned on nonemptiness, +Law Xi_r differs by at most C r from a singleton with mark law +pi_E tensor Uniform(0,1). Indeed the singleton submeasure sigma_r/m_r is dominated +by both Law(Xi_r | N_r>=1) and a singleton with law mu_r/m_r, and has mass +p_{1,r}/m_r. The resulting TV bound is a_r/m_r, then use (H4). This is a statement +about configuration laws, not an arbitrary rule for choosing a point from a +multiple configuration. + +The elementary mixture and common-submeasure arguments are rederived here; [SL] +is credited as the parallel source of the location/index formulation, not silently +consumed as an already independently accepted theorem. + +## 4. Why the single and pair height laws differ + +The leading single-point mean density has no dependence on theta, so its normalized +height is uniform. In REMOTE_PAIR_LAW.md, the normalized **factorial-pair mean** +instead has density (5/9)|theta-theta'|^(-1/3), with gap Beta(2/3,2). Pair weighting +samples a different object: configurations with more qualifying pairs receive +more weight. There is no contradiction, and the beta law is not the law of two +independent samples from the single-point uniform limit. + +There is likewise no global conditional-singleton claim. LOCAL_MULTIPLICITY.md +exhibits a local two-saddle mechanism of probability order r^3 in d=2, the same +order as a global occurrence. The fixed positive spatial exclusion in (H1)-(H7) +is indispensable. + +## 5. Scope, tests, and review obligations + +The order-Cr bound depends on the fixed d,L,rho and compact b,k ranges of its inputs. +It does not allow rho->0, k->0, increasing dimension/torus size, or a set E chosen +from the realized field. Unlike the sharp remote pair asymptotic, this pointwise +height-kernel argument does permit arbitrary deterministic varying E_r, because +all errors are bounded by its volume before normalization. + +These are critical-point height marks within a prescribed between-pin window, +not a persistence-partner distribution or lifetime distribution. No new numerical +value of C or cutoff is supplied. The finite tests verify the Jacobian, the mean +normalization algebra, and the failure of an integrated-mean-only inference. +They do not verify the continuum uniform density estimate (H1); its exact source +and its correct mathematical scope are part of the nonauthor review obligation. diff --git a/frontiers/window_multiplicity_laws_20260928/PUBLICATION.json b/frontiers/window_multiplicity_laws_20260928/PUBLICATION.json new file mode 100644 index 000000000..be68e90aa --- /dev/null +++ b/frontiers/window_multiplicity_laws_20260928/PUBLICATION.json @@ -0,0 +1,70 @@ +{ + "schema": 1, + "author": "OpenAI / ChatGPT", + "date": "2026-09-28", + "scientific_effect": "NONE", + "mathematical_acceptance": false, + "review_status": "AUTHOR_SIDE_REVIEW_REQUIRED", + "public_scope": "proof and provenance documents only", + "reproducible_computation_from_this_github_packet": false, + "code_publication": { + "state": "BLOCKED_UNRESOLVED", + "tool_message": "This tool call was blocked by OpenAI because we could not determine the safety status of the request.", + "blocked_file": { + "path": "algebra.py", + "bytes": 6163, + "sha256": "16ed713d1822efe2b254f8fd990270a81d23e49487208d4866f888486f553350", + "git_blob": "00140088f011b830c343900a4db646b38a5bdd52" + }, + "retry_or_alternate_route_attempted": false, + "owner_delivery": "complete local source and evidence in conversation artifact; not a GitHub execution receipt" + }, + "actual_local_execution": { + "tests_per_mode": 30, + "modes": [ + "normal", + "optimized" + ], + "semantic_mutants_per_mode": 13, + "all_intended_assertion_failures": true, + "execution_errors": 0, + "normal_optimized_json_pairs_identical": 14, + "packet_files_checked": 13, + "packet_only_runner_exit_code": 0, + "dependency_bytes_replayed_locally": false, + "source_bytes_unchanged": true, + "infrastructure_negative_controls": 4 + }, + "evidence_files": [ + { + "path": "FINITE_REPLAY_SUMMARY.json", + "bytes": 6322, + "sha256": "745784d958f1aeab958b047155c81c386148c7bbed374c71c64224b74c08389a", + "git_blob": "1b5c9e41a9cb25de91648124ca24abd7c09ccb76" + }, + { + "path": "PACKET_VALIDATION.json", + "bytes": 319, + "sha256": "6dc693add39e2c300f3f73986e6f98cea57bf194e61ec44aa81b51e67279c93d", + "git_blob": "2807b88740bb2da02bac3fb70de0c5f4445a60e0" + }, + { + "path": "PACKET_NEGATIVE_CONTROLS.json", + "bytes": 553, + "sha256": "d1338e78413961176ec30521961c302b38cba51692d14cfaff894713ca076f47", + "git_blob": "81116b1b9d5969e9241290f0a2dd61da9c8f3610" + }, + { + "path": "RED.stderr", + "bytes": 865, + "sha256": "3a5b90a07e9f1663d32407db59bd7f35c4fe58060a3ae15965feec3272e795f5", + "git_blob": "ee5187f3a80a7fb130d0dcd9012f9b585643cde0" + }, + { + "path": "ELDER_RED.stderr", + "bytes": 774, + "sha256": "f5d6aea704001d8e43886a58ffc47b9b3ce819959ccf12bdb4e60b9cf3aae07e", + "git_blob": "21dc945024e8fd538db17bf01131a7b8d690aaf7" + } + ] +} diff --git a/frontiers/window_multiplicity_laws_20260928/README.md b/frontiers/window_multiplicity_laws_20260928/README.md new file mode 100644 index 000000000..126c8e3de --- /dev/null +++ b/frontiers/window_multiplicity_laws_20260928/README.md @@ -0,0 +1,79 @@ +# Window multiplicity and elder-loss laws — author-side proof packet + +Author: OpenAI / ChatGPT, 28 September 2026. **Nonauthor analytic review required.** +Scientific effect: NONE. No existing proof, scientific verdict, graph, or prize +is changed. These are new written arguments, not accepted theorems by virtue of publication. + +## Mathematical modules + +| Read | Proposed result | Scope boundary | +|---|---|---| +| [Direct elder lower bound](ELDER_LOWER_AND_DENSITY_GAP.md) | Uniform planar `1-p_r >= c r^3` via an explicit path above the proposed death height to a point above birth. With the separately named parent upper/radial inputs: `Theta(r^3)` selection loss and `Theta(ell^(2/3))` compact-window density loss. | No numerical constant/cutoff, historical q/p substitution, or unrestricted-mark density-loss claim. | +| [Local multiplicity](LOCAL_MULTIPLICITY.md) | Two local window saddles occur with probability `Theta(r^3)`. Global conditional uniqueness and an `O(r^5)` global factorial extension are impossible. | Planar only; no global factorial upper bound. The count event alone is not an elder obstruction. | +| [Remote pair law](REMOTE_PAIR_LAW.md) | Exact positive leading `r^5` factorial coefficient, adjacent-index support, pair-weighted `Beta(2/3,2)` height-gap limit. | Both witnesses stay in a fixed remote region. Pair-mean weighting is not event-conditioned pair sampling. | +| [Distance moments](REMOTE_DISTANCE_MOMENTS.md) | Distance moment transition at `p=1`; two positive `r^6` contributions there. Scaled-distance limit has tail `R^-7`, yet its first moment does not capture rare macroscopic-pair contributions. | Fixed remote set. Total variation does not control unbounded moments. | +| [Single height mark](HEIGHT_MARKS.md) | Remote singleton location/index/height is `O(r)` in TV from the contact location/index profile times a uniform window height. | Uses the actual pre-height-integrated source kernel; not a persistence-partner law. | + +The common local cubic is + + G_k(X,Z)=k(2X^3-3X/2-1/2-3Z^2/4-XZ^2). + +Its extra saddles have height `-7k/32`. A rational polygonal path reaches +`+17k/64` while staying above `-7k/32`. Physical jet-box mass `r`, endpoint weight +`r^4`, and full normalizer `r^2` give a tilted event of order `r^3`. The whole-field +remainder is controlled AFTER conditioning on the rare physical jet box. + +The remote overlap integral is + + integral_0^infinity s(k-s^3|t|)_+ ds = (3/10) k^(5/3)|t|^(-2/3). + +It yields a contact Gaussian coefficient and an ordered pair-height density +`(5/9)|a-b|^(-1/3)`. The normalized gap has mean `1/4`, variance `9/176`, and +ordered heights have correlation `2/7`. These are pair-weighted critical-point +marks, not a new lifetime distribution. + +## Source identities and an explicit code-publication limitation + +[SOURCE_MAP.json](SOURCE_MAP.json) pins four consumed sources by repository, +40-character commit, bytes, SHA-256 and Git blob. The parallel singleton-law PR115 +is context-only; elementary mixture identities are proved again where needed. +[SOURCE_FILES.json](SOURCE_FILES.json) enumerates every document in THIS public +packet. This directory is deliberately proof-and-provenance only. + +The complete local delivery also contains `algebra.py`, `test_algebra.py`, +`run_validation.py`, a targeted workflow, manifests and original execution logs. +The GitHub connector blocked the attempt to create `algebra.py` with the message +that it could not determine the safety status. That body was not retried through +another path, encoding, or write route. No mathematical objection was supplied +by that tool response. The local tested code is included in the owner's separate +conversation evidence bundle, NOT claimed present in this repository packet. + +Actual local execution: **30 tests in each of normal and optimized Python; 13 +semantic mutants in each mode rejected on their exact intended assertions, with +no execution errors; baseline and mutant outputs identical between modes.** +Initial missing-implementation tests failed before implementation. The complete +local packet-only runner passed and source bytes remained unchanged. Separate +negative controls rejected a changed document, an unlisted member, duplicate JSON +keys, and a full-checkout replay with missing dependencies. + +Those local facts are reported in [PUBLICATION.json](PUBLICATION.json). They are +not a claim that the code can be replayed from THIS GitHub directory. The four +full-checkout dependency bytes were not locally downloaded/replayed in the container; +source texts were read through the connector and exact identities pinned. No new +hosted mathematical runner is installed by this proof-only PR. Existing repository +CI, if it runs, remains separate and cannot prove the new analytic arguments. + +## Review focus + +Review the direct elder obstruction and rare-jet conditional moment argument +first. The upper selection theorem is an explicit separate input. Then review +the collision-conditioned determinant limits, fixed-Borel translation argument, +coefficient constants, beta pushforward, distance-moment diagonal estimate, and +`p=1` two-cutoff limit. The height-mark module has a smaller source-consumption +obligation. Each manuscript records its own dependencies and exclusions. + +No nonauthor acknowledgment, provider independence, numerical Gaussian coefficient, +all-small-r numerical cutoff, global collision upper bound, higher factorial +moment, event-probability asymptotic from factorial means, Poisson limit, or priority +claim is invented. [RECONNAISSANCE.md](RECONNAISSANCE.md) records the limited external +search and distinguishes primary theorem reading from abstract-level discovery. diff --git a/frontiers/window_multiplicity_laws_20260928/RECONNAISSANCE.md b/frontiers/window_multiplicity_laws_20260928/RECONNAISSANCE.md new file mode 100644 index 000000000..6f7883265 --- /dev/null +++ b/frontiers/window_multiplicity_laws_20260928/RECONNAISSANCE.md @@ -0,0 +1,74 @@ +# Reconnaissance memo — window multiplicity and height/distance marks + +Date: 28 September 2026. Author: OpenAI / ChatGPT. +Scientific effect NONE. Discovery metadata is not an imported theorem. + +## Searches actually performed + +Consensus was queried for Gaussian critical points, shrinking height windows, +second moments and Kac-Rice. It returned Muirhead, Ladgham-related subject matter, +Gass--Stecconi, Armentano--Azais--Leon, and one-point height-distribution papers. +The Muirhead and Kuriki--Matsubara--Iso records were fetched. The former fetch +provided metadata but no abstract; the latter supplied an abstract about +unconditioned isotropic one-point critical densities in arbitrary dimensions. +Neither fetch supplied a theorem proving any claim in this packet. Consensus +reported its monthly search allowance exhausted after this discovery; no further +Consensus searches were attempted in this pass. + +Primary-source web searches then examined the following records and the AAL v3 +HTML. A focused arXiv search for Gaussian critical-point heights together with +Beta and 2/3 did not identify a matching result. That small search is not an +exhaustive novelty audit or evidence of worldwide priority. + +## Primary source actually read at theorem level + +Diego Armentano, Jean-Marc Azais, Jose Rafael Leon, +*On a general Kac-Rice formula for the measure of a level set*, +https://arxiv.org/html/2304.07424v3 (5 December 2023 version). + +Theorem 7.1 is the weighted expected-integral formula under Theorem 2.1 and its +stated lower-semicontinuity/conditional-law hypotheses. Theorem 2.2 and Remark 7 +supply the Gaussian regression bridge; Remark 8 treats a jointly Gaussian mark +process. Section 8.1 applies the framework to critical points. Our application +uses the already source-bound pair formula in [RC], with the original endpoint +weight once and each witness determinant once. Borel height-mark extensions are +handled as finite-measure identities, not by pretending every Borel indicator is +lower semicontinuous. No theorem-number substitution is made. + +## Adjacent literature — scope checked at record/abstract level + +Safa Ladgham and Raphael Lachieze-Rey, +*Local repulsion of planar Gaussian critical points*, +https://arxiv.org/abs/2209.04150 (2022 preprint; SPA publication 2023). +Its abstract concerns small-ball factorial moments and type-resolved repulsion +for stationary isotropic planar fields. It motivates near-collision analysis but +is not imported as a pinned determinant-tilted shrinking-height theorem. + +Stephen Muirhead, +*A second moment bound for critical points of planar Gaussian fields in shrinking +height windows*, https://arxiv.org/abs/1901.11336 (2019 preprint; Statistics & +Probability Letters 160, 108698, 2020; DOI 10.1016/j.spl.2020.108698). +Its abstract concerns unconditioned stationary planar fields and large domains +with shrinking height windows. Its second-moment problem is relevant background; +its result is not substituted for uniform estimates under this packet's pin law. + +The attempted HTML fetches for these two preprints did not expose their full +proofs in this session. No full-paper novelty exclusion or undocumented theorem +consumption is claimed. Gass--Stecconi's moment-finiteness paper and the newer +Kuriki--Matsubara--Iso one-point formula were discovery leads only, not inputs. + +## Internal audit and contribution boundary + +GitHub searches for the local height -7/32 and the beta/multiplicity terms did not +return the proposed mechanisms in the inspected results. Existing sources already +provide the fixed-remote mean, the O(r^5) pair upper bound, and the planar global +window first moment. The new proofs explicitly derive: a local two-saddle lower +mechanism, a sharp remote factorial coefficient with adjacent-index support, +height-mark laws, a distance-moment transition, and a direct ordinary elder-failure +lower event with a sharp compact-window candidate-versus-elder density-loss order. Standard Kac-Rice, Gaussian +regression, implicit-function stability, total variation and beta integration are +not claimed as inventions. + +No result in this memo changes a source's review status. The claimed new conclusions +remain author-side candidates, with the full analytic arguments and finite controls +available for nonauthor scrutiny. diff --git a/frontiers/window_multiplicity_laws_20260928/REMOTE_DISTANCE_MOMENTS.md b/frontiers/window_multiplicity_laws_20260928/REMOTE_DISTANCE_MOMENTS.md new file mode 100644 index 000000000..d077743b7 --- /dev/null +++ b/frontiers/window_multiplicity_laws_20260928/REMOTE_DISTANCE_MOMENTS.md @@ -0,0 +1,234 @@ +# Remote pair distances: a moment transition and a nonuniform-integrability effect + +Object: OA-WINDOW-MULTIPLICITY-DISTANCE-20260928-v1. +Author: OpenAI / ChatGPT, foreground research session, 28 September 2026. +Disposition: AUTHOR-SIDE PROOF CANDIDATE; NONAUTHOR ANALYTIC REVIEW REQUIRED. +Scientific effect: NONE. This is a new analytic consumer, not a status change. + +## 1. The quantities and two different limits + +Retain the exact fixed-remote model and fixed positive-volume Borel E of +REMOTE_PAIR_LAW.md. Counts are ordered and sum all indices. Let + + M_p(r)=E_Qr^W sum_{x!=x' counted in E} dist(x,x')^p, + p>=0, M_0(r)=E_Qr^W[N(E)(N(E)-1)]. (D1) + +Distances are physical torus distances. This note obtains a boundary-layer versus +fixed-distance transition at p=1. A typical pair under the normalized factorial +mean is a distance of order r apart, but a much rarer macroscopic pair can dominate +an unbounded distance moment. No pair-occurrence probability is inferred. + +Write A_0=integral_E sum_ij K_ij from (R3). More generally, for 0<=p<7, define + + A_p = [3*12^((p+2)/3)*k^((p+5)/3)] + / [4(p+2)(p+5)z_0] + * integral_E dx integral_S de p_{Y|Q0}(0,0,b) + E_Q0[w_0 |T|^((4-p)/3)(det A)^2 |Y=(0,0,b)]. (D2) + +Here Y,T,A,w_0,z_0 have exactly the definitions in (R1)-(R3), and index summation +has removed chi. The conditional expectation in (D2) is finite for p<7; the +possible negative power of T for p>4 is integrable because (4-p)/3>-1 and the +weighted conditional Gaussian density is bounded near zero. + +For distinct x,x' in E define the fixed-distance contact pair kernel + + Lambda_2(x,x') = p_{(grad f(x),grad f(x'),f(x),f(x'))|Q0}(0,0,b,b)/z_0 + * E_Q0[w_0 |det H_x det H_x'| + | grad f(x)=grad f(x')=0, f(x)=f(x')=b]. (D3) + +This is the all-index sum of the joint kernel in [RM, Section 6]; it is not a +product of two one-point kernels. Let + + B_p=k^2 integral_{E x E, x!=x'} dist(x,x')^p + Lambda_2(x,x') dx dx'. (D4) + +Below we prove B_p is finite and strictly positive for p>=0, including at the +collision diagonal where a compact-separation argument alone is insufficient. + +**Theorem D (distance moments).** For each fixed p>=0, + + 0<=p<1: M_p(r)=r^(5+p) A_p+o(r^(5+p)); + p=1: M_1(r)=r^6(A_1+B_1)+o(r^6); + p>1: M_p(r)=r^6 B_p+o(r^6). (D5) + +The constants A_p and B_p are the explicit conditional integrals above, not +numerical enclosures. The p=1 formula has **two positive contributions**. Simply +extending the microscopic limit's first moment to the full pair measure would +miss B_1. + +## 2. A sharper determinant estimate that retains the small height difference + +[RC]'s uniform bound used |det H_x|<=C delta K^d, with K>=1+||f||C3. For distance +moments we need the extra cancellation forced by nearly equal heights. +Use K=C_d(1+||f||C4), the exact collision frame V_delta, and its last target t. +The Peano formula gives + + D^3 f(x)[e,e,e] = -12t+O(delta K). + +From the gradient Taylor identity (R7), in a frame beginning with e, + + H_x=[[delta alpha,delta beta^T],[delta beta,A]], + alpha=6t+O(delta K), |beta|<=K, ||A||<=K. + +The analogous axial entry at x' is -6t+O(delta K). The exact block determinant +identity, valid even when A is singular, gives + + |det H_x|, |det H_x'| + <= C delta (|t| K^(d-1)+delta K^d). (D6) + +Taking the product, multiplying the original endpoint bound W_r<=C r^2 K^{2d}, +and conditioning as in [RC, Lemma 2] gives, after division by Z_r and multiplication +by the density of V_delta, a bound of the form + + C delta^2 (t^2+delta^2)(1+|t|)^(-q) (D7) + +for any prescribed finite q, by choosing sufficiently many Gaussian moments and +using the covariance sandwich. Constants depend only on the fixed compact model +parameters. The polynomial exponents are absorbed by Gaussian decay, not by an +independence assertion. + +Let a=k r^3/delta^3. For delta>=r the possible t-values lie in [-a,a], with a +uniformly bounded. Integrating t^2+delta^2 over the actual second-height window +is at most C(a^3+delta^2 a). The first-height window has length k r^3. Combining +with the same polar and value-coordinate Jacobians as (R9), the pair intensity +integrated over locations, directions, and heights has the radial envelope + + delta<=r: C |E| r^3 delta ddelta; + r<=delta<=eta_0: + C |E| (r^12 delta^(-8)+r^6) ddelta. (D8) + +These are upper bounds; the two terms in the second line need not be separate +independent processes. At distances >=eta_0, [RC, Lemma 5] gives O(r^6), and +multiplication by any fixed nonnegative power of distance changes only its constant. + +## 3. Integrability and positivity of the fixed-distance kernel + +At the contact endpoint law Q_0, set both remote witness heights equal to b. +The same collision frame has exactly t=0. Equation (D6) then bounds each witness +determinant by C delta^2 K^d. Its product supplies delta^4, while the joint gradient/ +height density supplies delta^(-d-3). Conditional moments remain uniformly bounded. +Hence for 0-1. +Elsewhere it is bounded on separated compact sets. This proves finiteness for +all p>=0. Full joint conditional support of the two Hessians and B_0 at distinct +sites makes Lambda_2 strictly positive off the diagonal. For a positive-volume +E, E x E has positive measure off the diagonal, indeed at some fixed positive +separation. Thus B_p>0. + +For every fixed epsilon>0, the common-regression argument of [RM, Section 6] +gives uniformly on dist(x,x')>=epsilon the pair mean density + + k^2 r^6 Lambda_2(x,x') + O_epsilon(r^7). (D10) + +The fixed-distance contribution divided by r^6 therefore converges to the +corresponding part of B_p. An estimate uniform all the way to the diagonal is +not being assumed in (D10); (D8)-(D9) are what justify the limiting exhaustion. + +## 4. Proof of the three regimes + +For 0<=p<1, repeat the blown-up proof in REMOTE_PAIR_LAW.md with the extra factor +(delta/r)^p=s^p. Its original envelope s min(1,s^-3) now has an integrable pth +moment precisely in this range. The separated contribution is O(r^(1-p)) after +division by r^(5+p), so it vanishes. The radial identity is + + integral_0^infinity s^(p+1)(k-s^3|t|)_+ ds + = 3 k^((p+5)/3)|t|^(-(p+2)/3)/((p+2)(p+5)). (D11) + +Multiplying by the same 36t^2 and substituting T=-12t yields (D2) and the first +line of (D5). The fixed-Borel spatial-indicator argument is unchanged. + +For p>1, divide by r^6 and bound all distances below epsilon using (D8). The +part delta<=r is O(r^(p-1)). The r^12 term on [r,epsilon] becomes + + C r^6 integral_r^epsilon delta^(p-8) ddelta, + +which tends to zero for each fixed epsilon: it is O(r^(p-1)) if p<7, +O(r^6 log(epsilon/r)) if p=7, and O(r^6 epsilon^(p-7)) if p>7. The remaining +r^6 term contributes at most C epsilon^(p+1). Therefore the normalized small- +distance mass has limsup <=C epsilon^(p+1). Combine (D10) with this bound and +let epsilon decrease to zero, using (D9). This proves the third line of (D5). + +At p=1 split into delta<=Ar, Ar=epsilon, with A>=1. +The first part divided by r^6 converges to the truncated microscopic coefficient +A_1(A), obtained from (D2)'s blown-up integral by s<=A. The third part converges +to B_1(epsilon). The middle part is bounded after division by r^6 by + + C A^-6+C epsilon^2, (D12) + +since r^6 integral_{Ar}^epsilon delta^-7 ddelta <= C A^-6. +All contributions are nonnegative. Take first r->0, then A->infinity and +epsilon->0. The truncated coefficients converge to A_1 and B_1, respectively, +and the middle bound vanishes. This proves the exact sum in the middle line of +(D5), without an unproved uniform-integrability assumption. In particular + + A_1=(k^2/(2z_0)) integral_E dx integral_S de + p_{Y|Q0}(0,0,b) E[w_0 |T| (det A)^2 |Y=(0,0,b)]. + +## 5. The limiting scaled separation and its seventh-power tail + +Normalize the ordered-pair mean by M_0(r) and set S_r=dist(x,x')/r. The L^1 +blown-up convergence in REMOTE_PAIR_LAW.md implies total-variation convergence +of its probability law to a nondegenerate S on (0,infinity). This is again pair +weighting, not conditioning on an event and choosing a pair. + +To describe its tail, define + + Psi_E(t)=integral_E dx integral_S de + p_{V_0|Q0}(0,0,b,t) + E_Q0[w_0(det A)^2 | V_0=(0,0,b,t)]. + +Here V_0's last coordinate is -T/12. After summing all indices the expression is +continuous and strictly positive at t=0; no artificial zero from the definition +of chi at T=0 is inserted into Psi. Uniform Gaussian regression also makes it +bounded near zero and rapidly decreasing after polynomial weights at infinity. +The limit density of S is + + g_S(s)=(36/(z_0 A_0)) s + integral_R t^2(k-s^3|t|)_+ Psi_E(t) dt. (D13) + +With t=kv/s^3, the integral equals +k^4 s^-9 integral_{-1}^1 v^2(1-|v|)Psi_E(kv/s^3)dv. +Since the elementary integral of v^2(1-|v|) is 1/6, + + g_S(s) ~ [6k^4 Psi_E(0)/(z_0 A_0)] s^-8, + P(S>R) ~ [6k^4 Psi_E(0)/(7z_0 A_0)] R^-7. (D14) + +Consequently E[S^p] is finite for 0<=p<7 and infinite for p>=7. For p<7 its +finite value is A_p/A_0. Near s=0, (D13) is O(s), so there is no additional +positive-moment obstruction there. + +## 6. Why convergence in TV does not give convergence of these moments + +Although the limit S has a finite first moment, (D5) implies + + E[S_r] -> (A_1+B_1)/A_0 > E[S]=A_1/A_0. (D15) + +For every p>1, + + E[S_r^p] ~ (B_p/A_0) r^(1-p) -> infinity. (D16) + +In particular this happens for 1 1` | **ACCEPT** at the stated fixed-`E`, fixed-`ρ`, existential scope; see §3 below. | +| §5 (170–201): the limiting law (D13), the `s^{−8}` tail and `R^{−7}` survival (D14), and, for `p ≥ 0`, `E[S^p] < ∞` iff `p < 7` | **ACCEPT**; see §4 below. | +| §6 (203–223): (D15), (D16), quantiles and RMS; TV does not control unbounded moments | **ACCEPT** | +| §7 (225–234) boundary | **ACCEPT** as stated. | + +No defect was found. Notes N1–N6 delimit the result without changing it. + +--- + +## §1 — the height-retaining determinant bound and the envelope (§2) + +**(D6).** On `∇f(x) = ∇f(x+δe) = 0`, RC's (R7) gives `H_x e = δ(−½D³f[e,e,·] + O(δK))` with `K ≍ 1 + ‖f‖_{C⁴}`. +So in a frame beginning with `e`, both the axial entry and the cross block carry a factor `δ`. The Peano identity +[RC] (4.2) gives `T = −12t + O(δK)`, so `α = −T/2 + O(δK) = 6t + O(δK)` at `x`, and `−6t + O(δK)` at `x'`. + +`DET` checks both facts exactly. +- The block identity `det[[δα, δβᵀ],[δβ, A]] = δα det A − δ²βᵀadj(A)β` holds on 100 random rational matrices, 22 of + them with singular `A` (20 forced, 2 by chance). +- On the axial fields `g'(u) = (c₀ + c₁u)(u² − δu)`, which have critical points at `0` and `δ`: + `t = −c₀/6 − c₁δ/12`, `α_x = 6t + (c₁/2)δ` and `α_{x'} = −6t + (c₁/2)δ`, exactly. So the `O(δK)` remainder is + genuinely present, with slope `c₁/2`. + +Hence `|det H| ≤ Cδ(|t|K^{d−1} + δK^d)`. + +**(D7).** Multiply the two determinant bounds, `W_r ≤ Cr²K^{2d}` ([RC] Lemma 3) and `Z_r ≥ cr²`. [RC] Lemma 2 gives +conditional `K`-moments `≤ C(1+|t|)^q` and a `V_δ`-density `≤ C(1+|t|)^{−q}` for every `q`. Together these give +`Cδ²(t² + δ²)(1+|t|)^{−q}`. The conditioning value of `D3_δ` is exactly `t`, so using `t` inside (D6) is legitimate. + +**(D8).** With `a = kr³/δ³`, the two windows allow `(y, t)` with `y ∈ I_r` and `|t| ≤ a`. The `y`-section at fixed +`t` has length `(kr³ − δ³|t|)_+`. The height integral is therefore exactly + + ∫_{−a}^{a} (t² + δ²)(kr³ − δ³|t|) dt = kr³(a³/6 + δ²a), + +because `δ³a = kr³`. The note's bound `C kr³(a³ + δ²a)` is correct (N2, `ENVELOPE`). + +With the density power `δ^{−d−3}`, `dy' = δ³dt`, the determinants `δ²` and polar `δ^{d−1}`, the radial density is +`C r³δ(a³ + δ²a) = C(k³r^{12}δ^{−8} + kr⁶)` for `δ ≥ r`. For `δ ≤ r`, the `t`-integral is bounded and the density is +`C r³δ`. Both exponents are checked for every d. + +The sharper envelope is necessary at `p = 1`. RP's envelope `r⁴s·min(1, s^{−3})` equals `r⁶δ^{−2}` for `δ ≥ r`. Its +first moment puts equal mass on every dyadic shell, so the middle region would contribute `≍ r⁶log(1/r)`, not +`O(A^{−6})r⁶`. The `ENVELOPE` shell sum shows this. It confirms the point in 5880152796. + +## §2 — the diagonal and the fixed-distance kernel (§3) + +At `Q_0` with both witness heights equal to `b`, the collision frame has `t = 0` exactly, so (D6) gives +`|det H| ≤ Cδ²K^d` at each witness. The ledger is: product `δ⁴`, value-gradient density `δ^{−d−3}` ([RC] (4.3) at +`r = 0`, where [RC] Lemma 1 already includes `r = 0`), polar `δ^{d−1}`. It totals `δ⁰` for every d (`DIAGONAL`). So +`δ^{d−1}Λ_2(x, x+δe)` is bounded. The bounding envelope `δ^p` is locally integrable for `p > −1`, hence `B_p < ∞` on +the claimed domain `p ≥ 0`. This is sufficiency only: no negative-moment threshold for the actual kernel `Λ_2` is +established here. Off-diagonal positivity alone does not give a positive limiting diagonal coefficient; a positive +bounded radial kernel such as `exp(−1/δ)` has every negative moment finite. + +Positivity: at distinct remote sites, the two Hessians and `B_0` have full joint conditional support by [RM] §2's +distinct-jet principle, so `Λ_2 > 0` off the diagonal. A positive-volume `E` has `E × E` of positive measure at some +fixed separation. + +(D10) is [RM] (15) at `m = 2`, `η = ε`: the density is `(kr³)²Λ_2 + O(r⁷)`, uniform on `dist ≥ ε`. The factor +`dist^p` is bounded there, and Borel `E × E` restriction is an equality of finite measures. See N1 on indices. + +## §3 — Theorem D (§4) + +**`0 ≤ p < 1`.** This is RP's dominated convergence with the weight `s^p`. The envelope `s^{p+1}min(1, s^{−3})` is +integrable, and separated pairs give `O(r^{1−p})` after division. (D11) is exactly #128's (I11), which I checked there +on exact instances for negative and positive `p`. (D2) at `p = 0` is RP's `(3/40)12^{2/3}`. + +**`p > 1`.** Divide by `r⁶`. The contributions are: +- `δ ≤ r`: `r³∫_0^r δ^{p+1}dδ/r⁶ = r^{p−1}/(p+2)`; +- the `r^{12}` part on `[r, ε]`: `r⁶(ε^{p−7} − r^{p−7})/(p−7)`, which is `O(r^{p−1})` for `p < 7` and + `O(r⁶ε^{p−7})` for `p > 7`. These are checked exactly for integer `p`, including monotone decrease in `r`. At + `p = 7` it is `r⁶log(ε/r)`; +- the `r⁶` part: `≤ ε^{p+1}/(p+1)`; +- `dist ≥ ε`: `B_p(ε) + O_ε(r)` by (D10). + +Letting `r → 0` and then `ε → 0`, monotone convergence (by (D9)) gives `B_p(ε) ↑ B_p`. Correct. + +**`p = 1`.** The three pieces are all nonnegative: +- the inner part `δ ≤ Ar`, after division by `r⁶`, converges to `A_1(A) = A_0∫_0^A s g_S(s) ds`, by dominated + convergence on the compact range `s ≤ A`; +- the middle part is at most `r⁶∫_{Ar}^ε δ^{−7}dδ = A^{−6}/6 − r⁶ε^{−6}/6` plus `ε²/2`, checked exactly (`REGIMES`); +- the outer part converges to `B_1(ε)`. + +So `A_1(A) + B_1(ε) ≤ liminf ≤ limsup ≤ A_1(A) + B_1(ε) + CA^{−6} + Cε²`. Then `A ↑ ∞` and `ε ↓ 0` give +`A_1 + B_1` without any uniform-integrability assumption. `A_1 = (k²/(2z_0))∫∫p E[w_0|T|(det A)²]` matches (D2) at +`p = 1`, since `3·12/(4·3·6) = 1/2`. + +## §4 — the limiting law and its tail (§5–§6) + +(D13) is #128's (I20), accepted there, with the same `Ψ_E`. The substitution `t = kv/s³` gives +`k⁴s^{−9}∫_{−1}^1 v²(1−|v|)Ψ_E(kv/s³)dv`, and `∫v²(1−|v|) = 1/6`. Bounded continuous `Ψ_E` with `Ψ_E(0) > 0` gives +(D14), with constants `6` and `6/7`. + +`TAIL` checks the limit on an exact piecewise-polynomial model `Ψ = (1 − t²)_+`: +`s⁹∫t²(k − s³|t|)_+Ψ dt → k⁴/6` with error `O(s^{−6})`. For `p ≥ 0`, `E[S^p] < ∞` iff `p < 7`, and then it equals +`A_p/A_0` by the Tonelli identity `108/((p+2)(p+5))` (`MOMENTS`). `g_S = O(s)` at `0`. Across real `p`, the lower +endpoint is `−2`, from #128's positive `J_0` (N5); the upper-tail argument alone is not a complete real-moment domain. + +The tail reproduces the envelope's shape: `r⁴g_S(δ/r) ≈ (6k⁴Ψ_E(0)/z_0)r^{12}δ^{−8}`. So the first term of (D8) is +the actual microscopic tail, not slack. The two terms of (D8) cross at `δ ≍ r^{3/4}` (N3). + +(D15): `E[S_r] = r^{−1}M_1/M_0 → (A_1 + B_1)/A_0`, which exceeds `E[S] = A_1/A_0` by `B_1/A_0 > 0`. (D16): +`E[S_r^p] = r^{−p}M_p/M_0 ~ (B_p/A_0)r^{1−p}`. The RMS distance is `√(M_2/M_0) ~ √(rB_2/A_0)`. Quantile convergence +follows from TV convergence to a law with a positive continuous density on `(0, ∞)`. The explanation offered, that a +pair-weighted mass of order `r` sits at fixed physical distances, is exactly the `B_p` term. + +## Notes + +- **N1 (index reading of (D10)).** [RM] (15) is stated for ordered `m`-tuples of a single index `j`. (D10) needs the + all-index sum, which includes mixed pairs `(i, j)`, `i ≠ j`. The [RM] §6 argument is index-agnostic: distinct-site + regression, `F_i` continuous, `W_r` once and `Z_r` once. [RC] Lemma 5 already re-derived the mixed-index upper bound. + I read (D10) as that argument applied to each index pair and summed. This is an interface reading, not a gap. +- **N2 (exact height integral).** `∫_{−a}^{a}(t² + δ²)(kr³ − δ³|t|)dt = kr³(a³/6 + δ²a)`. The note's `C(a³ + δ²a)` + is correct and not sharp in the constant. +- **N3 (consistency, not a joint limit).** The microscopic tail `(6k⁴Ψ_E(0)/z_0)r^{12}δ^{−8}` matches (D8)'s first + term. The fixed-distance radial density is bounded by (D9). The crossover `δ ≍ r^{3/4}` is heuristic. No uniform + intermediate-scale asymptotic is claimed or accepted. +- **N4 (why the sharper bound matters).** With RP's envelope alone, the `p = 1` middle region would be + `≍ r⁶log(1/r)`. The height-retaining (D6)–(D8) is what makes the two-cutoff argument close. +- **N5 (relation to Math-#128).** (D5)'s first line and (D13) coincide with #128's Theorem I and (I20). Combined: + - the pair-weighted limit `S` has `E[S^p] < ∞` exactly for `−2 < p < 7`; + - `M_p` is microscopic exactly for `−2 < p < 1`; + - the lower boundary comes from #128's `J_r > 0`, the upper boundary from `B_1 > 0` here. + + Neither note consumes the other. +- **N6 ((D2) for `4 < p < 7`).** The negative power `|T|^{(4−p)/3}`, with `(4−p)/3 > −1`, is integrable because the + conditional density of `T` given `(Y, B_0, A)` is bounded. That conditional variance is positive by the distinct-jet + floor. So the tower property applies with the weight `w_0(det A)²`. Conditioning on `Y` alone would not justify + pulling the weight out; the note's wording "weighted conditional Gaussian density" is consistent with this reading. + +## What this review does not do + +- It does not review C5 (`HEIGHT_MARKS.md`) or C6. +- It accepts no event-conditioned pair law, uniform intermediate-scale asymptotic, global (pin-inclusive) factorial + bound, uniformity as `ρ → 0` or over oscillating `E_r`, numerical constant, or persistence interpretation. +- It does not run or reconstruct `algebra.py`, and it changes no register. + +## Revisions + +- **v2** (wording only, requested in [5888822723](https://github.com/d6g8k5htny-coder/Math-/pull/130#issuecomment-5888822723)): + §2 now says the bounded envelope gives `B_p < ∞` for `p ≥ 0` (sufficiency only, no negative threshold for `Λ_2`), + and the `p < 7` moment statement is qualified to `p ≥ 0` in the verdict table and §4. No verdict, proof reading or + checker change. + +## Reproduce + + python -B -S distance_review_check.py # prints RESULTS.json byte for byte + python -B -O -S distance_review_check.py # identical + python -B -S distance_review_check.py --mutant M # exit 1 for each of the 7 mutants diff --git a/reviews/remote_distance_moments_claude_20260929/SOURCE_FILES.json b/reviews/remote_distance_moments_claude_20260929/SOURCE_FILES.json new file mode 100644 index 000000000..ab064efde --- /dev/null +++ b/reviews/remote_distance_moments_claude_20260929/SOURCE_FILES.json @@ -0,0 +1,37 @@ +{ + "schema": 1, + "scientific_effect": "NONE", + "review_status": "NONAUTHOR_REVIEW", + "reviewed_object": { + "pr": "d6g8k5htny-coder/Math-#116", + "head": "0507e3a1dbd3dede84cbeb805947c70aa16ebc36", + "paths": [ + { + "path": "frontiers/window_multiplicity_laws_20260928/REMOTE_DISTANCE_MOMENTS.md", + "git_blob": "d077743b7fda8b1bb2e1bafdab97d01bb9e321b1", + "bytes": 11097, + "sha256": "b40dc67a0c4760d3db796914bdc50cbbd5fd1371786772fa919a3a100467b41d" + } + ] + }, + "files": [ + { + "path": "REVIEW.md", + "bytes": 13303, + "sha256": "7fe71178514de0f634f6bf23009ee100d8218512ca994331318a1b591daaf7a9", + "git_blob": "ab19d2d921bbd43e62f699280235f2107b742d58" + }, + { + "path": "RESULTS.json", + "bytes": 1417, + "sha256": "76b4c91d14673a9864fa4f19854895b74970f2be036158eb7af852ac79f13d37", + "git_blob": "fd40e6c86a48a4dd6c0bea0b12d4213ed82051d9" + }, + { + "path": "distance_review_check.py", + "bytes": 13353, + "sha256": "c4ca169ae216b55a7266d6452f9838df44d2541900a4bf2a7c19632ff0117f0b", + "git_blob": "863779f54d1f953b988a4f5f645675d7ed76667c" + } + ] +} diff --git a/reviews/remote_distance_moments_claude_20260929/distance_review_check.py b/reviews/remote_distance_moments_claude_20260929/distance_review_check.py new file mode 100644 index 000000000..863779f54 --- /dev/null +++ b/reviews/remote_distance_moments_claude_20260929/distance_review_check.py @@ -0,0 +1,254 @@ +"""Independent nonauthor checks for OA-WINDOW-MULTIPLICITY-DISTANCE-20260928-v1 (Math-#116 C4, REMOTE_DISTANCE_MOMENTS.md). + +Python standard library only; exact rational arithmetic throughout. Written from the markdown; the author's absent +algebra.py is neither run nor reconstructed. Groups: + + DET (D6): the block identity det[[delta a, delta b^T], [delta b, A]] = delta a det A - delta^2 b^T adj(A) b on + random rational matrices, singular A included; explicit axial fields g'(u) = (c0 + c1 u)(u^2 - delta u) + with critical points at 0 and delta give the Peano target t and the axial entries exactly: + alpha_x = 6t + (c1/2) delta, alpha_x' = -6t + (c1/2) delta, i.e. +-6t + O(delta K). + ENVELOPE (D7)->(D8): the height integral of (t^2 + delta^2) over the actual two-window region is exactly + k r^3 (a^3/6 + delta^2 a), a = k r^3/delta^3; the radial density r^3 delta (a^3 + delta^2 a) is exactly + k^3 r^12 delta^-8 + k r^6 in the exponents; the original RP envelope would give r^6 delta^-2, whose first + moment is not summable on dyadic shells between A r and epsilon, so the sharper (D8) is needed at p = 1. + DIAGONAL (D9): delta^4 (two t = 0 determinants) * delta^(-d-3) (value-gradient density) * delta^(d-1) (polar) = + delta^0 for every d; hence local integrability of dist^p Lambda_2 exactly for p > -1. + REGIMES (D5): exact small-distance bounds for p > 1 (the delta <= r part r^(p-1), the r^12 part for integer + p != 7, the r^6 part epsilon^(p+1)); the p = 1 middle bound r^6 int_{Ar}^eps delta^-7 <= A^-6/6 and + int delta d delta <= eps^2/2; A_1 prefactor k^2/(2 z0) from (D2); regime exponents 5+p vs 6. + TAIL (D13)-(D14): int_{-1}^1 v^2 (1 - |v|) dv = 1/6, the constants 6 and 6/7; an exact piecewise-polynomial + model Psi(t) = (1 - t^2)_+ shows s^9 int t^2 (k - s^3|t|)_+ Psi dt -> k^4/6 with O(s^-6) error; moments of + S are finite exactly for p < 7; the tail matches (D8): r^4 (delta/r)^-8 = r^12 delta^-8, and the two + envelope terms cross at delta = r^(3/4). + MOMENTS (D15)-(D16): E[S_r] limit exceeds E[S] by B_1/A_0 > 0; E[S_r^p] ~ (B_p/A_0) r^(1-p); RMS exponent 1/2; + (D2) at p = 0 and p = 1 against RP (R3) and the Tonelli identity A_p = A_0 E[S^p] for 0 <= p < 7. + +Mutants (each must fail): block-det, peano-slope, envelope-power, middle-cutoff, tail-sixth, a1-constant, +diagonal-order. +Not an analytic proof: the Gaussian conditioning, (D10) and limiting steps are reviewed in REVIEW.md. +""" +import argparse +import json +import random +import sys +from fractions import Fraction as F + +MUTANTS = ("block-det", "peano-slope", "envelope-power", "middle-cutoff", "tail-sixth", "a1-constant", + "diagonal-order") +MUT = None + + +def det(A): + n = len(A) + if n == 0: + return F(1) + M = [list(map(F, r)) for r in A] + d = F(1) + for c in range(n): + p = next((i for i in range(c, n) if M[i][c] != 0), None) + if p is None: + return F(0) + if p != c: + M[c], M[p] = M[p], M[c] + d = -d + d *= M[c][c] + for i in range(c + 1, n): + f = M[i][c] / M[c][c] + M[i] = [x - f * y for x, y in zip(M[i], M[c])] + return d + + +def adjugate(A): + n = len(A) + if n == 1: + return [[F(1)]] + adj = [[F(0)] * n for _ in range(n)] + for i in range(n): + for j in range(n): + minor = [row[:j] + row[j + 1:] for k, row in enumerate(A) if k != i] + adj[j][i] = (-1) ** (i + j) * det(minor) + return adj + + +# --------------------------------------------------------------------------------------------------------------- + +def check_det(): + rng = random.Random(116401) + ok_block = True + for n in (1, 2, 3, 4): + for trial in range(25): + A = [[F(0)] * n for _ in range(n)] + for i in range(n): + for j in range(i, n): + A[i][j] = A[j][i] = F(rng.randint(-4, 4), rng.randint(1, 3)) + if trial % 5 == 0: # force a singular transverse block + for j in range(n): + A[n - 1][j] = A[0][j] if n > 1 else F(0) + for i in range(n): + A[i][n - 1] = A[i][0] if n > 1 else F(0) + a = F(rng.randint(-9, 9), 4) + b = [F(rng.randint(-5, 5), 3) for _ in range(n)] + delta = F(1, rng.randint(2, 50)) + H = [[delta * a] + [delta * bi for bi in b]] + [[delta * b[i]] + list(A[i]) for i in range(n)] + adj = adjugate(A) + quad = sum(b[i] * adj[i][j] * b[j] for i in range(n) for j in range(n)) + sign = 1 if MUT == "block-det" else -1 + ok_block &= det(H) == delta * a * det(A) + sign * delta ** 2 * quad + # Axial Peano check: g'(u) = (c0 + c1 u)(u^2 - delta u) has g'(0) = g'(delta) = 0. + ok_axial = True + for c0, c1 in ((F(3), F(2)), (F(-5, 2), F(7, 3)), (F(1, 4), F(-9))): + for delta in (F(1, 10), F(1, 100), F(2, 7)): + gdiff = c0 * (delta ** 3 / 3 - delta ** 3 / 2) + c1 * (delta ** 4 / 4 - delta ** 4 / 3) + t = gdiff / delta ** 3 # D3_delta with zero endpoint gradients + alpha_x = (-c0 * delta) / delta # g''(0)/delta + alpha_xp = (c0 * delta + c1 * delta ** 2) / delta # g''(delta)/delta + slope = F(0) if MUT == "peano-slope" else c1 / 2 + ok_axial &= alpha_x == 6 * t + slope * delta and alpha_xp == -6 * t + slope * delta + ok_axial &= t == -c0 / 6 - c1 * delta / 12 + return {"D6_block_determinant_identity_incl_singular_A": ok_block, + "D6_axial_entries_plus_minus_6t_plus_O_delta": ok_axial} + + +def check_envelope(): + out = {} + ok_exact = True + for k in (F(1), F(3, 2), F(7, 5)): + for r in (F(1, 10), F(1, 7)): + for delta in (r, 2 * r, F(1, 3), F(1, 2)): + a = k * r ** 3 / delta ** 3 + # region {y in I_r, y + delta^3 t in I_r} has t-section length (k r^3 - delta^3 |t|)_+ on |t| <= a + # int_{-a}^{a} (t^2 + delta^2)(k r^3 - delta^3 |t|) dt, evaluated by exact antiderivatives + kr3 = k * r ** 3 + integral = 2 * (kr3 * (a ** 3 / 3 + delta ** 2 * a) - delta ** 3 * (a ** 4 / 4 + delta ** 2 * a ** 2 / 2)) + ok_exact &= integral == kr3 * (a ** 3 / 6 + delta ** 2 * a) + ok_exact &= integral <= kr3 * (2 * a ** 3 / 3 + 2 * delta ** 2 * a) # the note's cruder bound + out["height_integral_exact_kr3_a3_over_6_plus_delta2_a"] = ok_exact + # radial density r^3 * delta^(d-1) * delta^-d * delta^2 * (a^3 + delta^2 a): r and delta exponents of both terms + first = (3 + 9, 1 - 9) if MUT != "envelope-power" else (3 + 9, 1 - 10) + second = (3 + 3, 1 + 2 - 3) + out["D8_terms_are_r12_delta_minus8_and_r6"] = first == (12, -8) and second == (6, 0) + # delta <= r: the t-integral is bounded, so the radial density is r^3 * delta^(d-1-d+2) = r^3 delta + out["D8_inner_is_r3_delta_all_d"] = all((d - 1) - d + 2 == 1 for d in range(2, 11)) + # Original RP envelope r^4 s min(1, s^-3) with s = delta/r is r^6 delta^-2 for delta >= r; its first moment + # r^6 int delta^-1 has equal mass on every dyadic shell, so the p = 1 middle region would not vanish. + shells = [F(2) ** n * F(1, 2) * F(2) ** (-n) for n in range(30)] # min of delta^-1 times shell width + out["original_envelope_first_moment_not_summable"] = all(s == F(1, 2) for s in shells) and sum(shells) == 15 + return out + + +def check_diagonal(): + ok = True + for d in range(2, 11): + dets = 2 if MUT == "diagonal-order" else 4 + ok &= dets + (-(d + 3)) + (d - 1) == 0 + # local integrability of delta^p * (bounded radial density) at 0 iff p > -1; B_p needs only p >= 0 + return {"D9_radial_density_order_delta0_all_d": ok, + "B_p_locally_integrable_for_p_gt_minus1": all(p + 1 > 0 for p in (F(-1, 2), F(0), F(1), F(9))) + and not F(-1) + 1 > 0} + + +def check_regimes(): + out = {} + # p > 1, delta <= r: int_0^r delta^p r^3 delta d delta / r^6 = r^(p-1)/(p+2) + ok = True + for p in (F(3, 2), F(2), F(5), F(9)): + for r in (F(1, 10), F(1, 100)): + if p.denominator == 1: + ok &= r ** 3 * r ** int(p + 2) / (p + 2) / r ** 6 == r ** int(p - 1) / (p + 2) + # r^12 part on [r, eps] after / r^6: r^6 (eps^(p-7) - r^(p-7))/(p-7) for integer p != 7; decreasing to 0 in r + for p in (2, 3, 4, 6, 8, 10): + eps = F(1, 4) + rs = (F(1, 10), F(1, 100), F(1, 1000)) + vals = [r ** 6 * (eps ** (p - 7) - r ** (p - 7)) / (p - 7) for r in rs] + ok &= all(v > 0 for v in vals) and vals[0] > vals[1] > vals[2] + # O(r^(p-1)) for p < 7 and O(r^6 eps^(p-7)) for p > 7, as stated in the note + bounds = [r ** (p - 1) / (7 - p) if p < 7 else r ** 6 * eps ** (p - 7) / (p - 7) for r in rs] + ok &= all(v <= b for v, b in zip(vals, bounds)) + out["p_gt_1_small_distance_parts_vanish"] = ok + # p = 1: middle bounds + ok = True + power = 5 if MUT == "middle-cutoff" else 6 + for A in (F(1), F(4), F(10)): + for r in (F(1, 100), F(1, 1000)): + eps = F(1, 5) + mid = r ** 6 * ((A * r) ** -6 - eps ** -6) / 6 # r^6 int_{Ar}^eps delta^-7 d delta + ok &= mid == A ** -power / 6 - r ** 6 * eps ** -6 / 6 and 0 <= mid <= A ** -power / 6 + ok &= (eps ** 2 - (A * r) ** 2) / 2 <= eps ** 2 / 2 # int_{Ar}^eps delta d delta + out["p1_middle_bounded_by_A_minus6_plus_eps2"] = ok + # A_1 from (D2): 3 * 12^((p+2)/3) k^((p+5)/3) / (4 (p+2)(p+5) z0) at p = 1 is 36 k^2 / (72 z0) = k^2/(2 z0) + pref = F(3 * 12) / (4 * 3 * 6) + target = F(1, 4) if MUT == "a1-constant" else F(1, 2) + out["A1_prefactor_k2_over_2z0"] = pref == target + # regime exponents: microscopic r^(5+p) vs macroscopic r^6 + out["regime_exponents"] = all((5 + p < 6) == (p < 1) and (5 + p == 6) == (p == 1) + for p in (F(0), F(1, 2), F(1), F(3, 2), F(4))) + return out + + +def check_tail(): + out = {} + sixth = F(1, 3) if MUT == "tail-sixth" else F(1, 6) + # int_{-1}^{1} v^2 (1 - |v|) dv = 2 (1/3 - 1/4) + out["v2_one_minus_abs_v_integral_is_one_sixth"] = 2 * (F(1, 3) - F(1, 4)) == sixth + # constants: 36 * (1/6) = 6 in g_S tail, and the survival tail divides by 7 + out["tail_constants_6_and_6_over_7"] = 36 * sixth == 6 and F(6) / 7 == F(6, 7) + # model Psi(t) = (1 - t^2)_+: for s^3 > k, J(s) = 2 int_0^{k/s^3} t^2 (k - s^3 t)(1 - t^2) dt exactly + ok = True + k = F(3, 2) + errs = [] + for s in (F(2), F(4), F(8), F(16)): + m = k / s ** 3 + J = 2 * (k * m ** 3 / 3 - s ** 3 * m ** 4 / 4 - k * m ** 5 / 5 + s ** 3 * m ** 6 / 6) + err = s ** 9 * J - k ** 4 * sixth + errs.append(err) + ok &= abs(err) <= k ** 6 * s ** -6 + ok &= all(abs(errs[i + 1]) < abs(errs[i]) for i in range(len(errs) - 1)) + out["model_tail_s9_integral_to_k4_over_6"] = ok + # finiteness of E[S^p]: s^(p-8) integrable at infinity iff p < 7; near 0 g_S = O(s) + out["S_moments_finite_iff_p_lt_7"] = all(((p - 8) < -1) == (p < 7) for p in (F(0), F(6), F(7), F(15, 2))) + # matching with (D8): r^4 g_S(delta/r) with g_S ~ s^-8 gives r^12 delta^-8; crossover r^12 d^-8 = r^6 at d = r^(3/4) + out["tail_matches_D8_and_crossover_three_quarters"] = (4 + 8 == 12) and (F(12) - 8 * F(3, 4) == 6) + return out + + +def check_moments(): + out = {} + # E[S_r^p] = r^-p M_p / M_0: exponent -p + 6 - 5 = 1 - p for p >= 1; p = 1 limit (A_1 + B_1)/A_0 > A_1/A_0 + out["D15_D16_exponents"] = all(-p + 6 - 5 == 1 - p for p in (F(1), F(3, 2), F(3))) + A1, B1, A0 = F(2), F(1, 3), F(5) + out["D15_limit_exceeds_TV_limit_by_B1_over_A0"] = (A1 + B1) / A0 - A1 / A0 == B1 / A0 > 0 + # RMS: sqrt(M_2 / M_0) = sqrt(r^6 B_2 / (r^5 A_0)) -> exponent of r inside the root is 1 + out["rms_distance_exponent"] = 6 - 5 == 1 + # (D2) at p = 0 is RP's 3/40; Tonelli: 36 * 3/((p+2)(p+5)) = (3/4) 144 /((p+2)(p+5)) for 0 <= p < 7 + out["D2_at_p0_is_R3"] = F(3) / (4 * 2 * 5) == F(3, 40) + out["A_p_is_A0_E_S_p"] = all(F(108) / ((p + 2) * (p + 5)) == F(3, 4) * 144 / ((p + 2) * (p + 5)) + for p in (F(0), F(1), F(3), F(13, 2))) + # T-exponent (4-p)/3 > -1 exactly for p < 7 + out["D2_T_exponent_integrable_iff_p_lt_7"] = all(((4 - p) / 3 > -1) == (p < 7) for p in (F(0), F(5), F(7), F(8))) + return out + + +def flatten(d): + for v in d.values(): + if isinstance(v, dict): + yield from flatten(v) + else: + yield v + + +def main(): + global MUT + ap = argparse.ArgumentParser() + ap.add_argument("--mutant", choices=MUTANTS) + MUT = ap.parse_args().mutant + checks = {"DET": check_det(), "ENVELOPE": check_envelope(), "DIAGONAL": check_diagonal(), + "REGIMES": check_regimes(), "TAIL": check_tail(), "MOMENTS": check_moments()} + passed = all(flatten(checks)) + print(json.dumps({"object": "CLAUDE-REVIEW-REMOTE-DISTANCE-MOMENTS-20260929-v1", "checks": checks, + "passed": passed, "scope": "exact finite identities only; not an analytic proof"}, + indent=2, sort_keys=True)) + return 0 if passed else 1 + + +if __name__ == "__main__": + sys.exit(main()) diff --git a/reviews/remote_height_marks_claude_20260929/RESULTS.json b/reviews/remote_height_marks_claude_20260929/RESULTS.json new file mode 100644 index 000000000..245bd4e46 --- /dev/null +++ b/reviews/remote_height_marks_claude_20260929/RESULTS.json @@ -0,0 +1,27 @@ +{ + "checks": { + "CONTRAST": { + "integrated_mass_does_not_fix_height_law": true, + "single_uniform_vs_pair_beta_gap": true + }, + "INTEGER": { + "pointwise_integer_inequalities": true + }, + "JACOBIAN": { + "H2_jacobian_is_k_r_cubed": true + }, + "MIXTURE": { + "H7_integer_consequences": true, + "a_le_q": true, + "configuration_law_within_a_over_m": true, + "mu_equals_sigma_plus_eta_and_p1_equals_m_minus_a": true, + "singleton_mark_law_within_a_over_m": true + }, + "NORMALIZE": { + "normalization_variation_inequality": true + } + }, + "object": "CLAUDE-REVIEW-REMOTE-HEIGHT-MARKS-20260929-v1", + "passed": true, + "scope": "exact finite identities only; not an analytic proof" +} diff --git a/reviews/remote_height_marks_claude_20260929/REVIEW.md b/reviews/remote_height_marks_claude_20260929/REVIEW.md new file mode 100644 index 000000000..f7588f56a --- /dev/null +++ b/reviews/remote_height_marks_claude_20260929/REVIEW.md @@ -0,0 +1,103 @@ +# Nonauthor analytic review: the remote single-witness height mark (Math-#116, C5) + +Scientific effect: **NONE**. This file changes no register, status, graph node, lemma flag, prize or author source. +It records a verdict on candidate C5 of `reviews/candidates_pending_20260928/CANDIDATES.md`. Integration is a +separate act. + +## Object + +| Field | Value | +|---|---| +| Object | OA-WINDOW-MULTIPLICITY-HEIGHT-20260928-v1 (OpenAI / ChatGPT) | +| Branch / head | `chatgpt/window-multiplicity-laws-20260928` / `0507e3a1dbd3dede84cbeb805947c70aa16ebc36` ([Math-#116](https://github.com/d6g8k5htny-coder/Math-/pull/116)) | +| `HEIGHT_MARKS.md` | Git blob `015d769675d9a2cf191286979d3b8c877cd91bdc`, 7360 B, SHA256 `44cc69260d27df3a66083ba127aaf275f240641cc8e3740ae0b0b119109270e2`, 159 lines | +| Consumed, on main | [RM] `frontiers/remote_window_20260924/PROOF.md` (blob `b383bfcc…`): §5 (12)–(13) and the sentence after (13). [RC] `frontiers/remote_collision_20260928/PROOF.md` (blob `7b48a88e…`): Corollary D. | +| Compared, on main | [#120] `frontiers/remote_height_decoupling_20260928/PROOF.md` (blob `4d7af587…`): Theorem H and §7. My review of it (ACCEPT) is `reviews/remote_height_claude_20260928/`. | +| Request | Candidate registry C5; claimed in [5888775794](https://github.com/d6g8k5htny-coder/Math-/pull/116#issuecomment-5888775794) | + +## Provenance and exposure + +| Field | Value | +|---|---| +| Reviewer | Anthropic Claude, Claude Code session `session_017Mi3hxjaxV45x6zo6o1ee3` | +| Relation | Different provider from the OpenAI author. Same GitHub account as every lane, so no organizational independence is claimed. | +| Exposure | **I authored [RC]**, whose Corollary D gives (H5), and I reviewed #120, which proves a sharper own-marginal version. This review checks C5's use of RM and RC, not their truth. | +| Author code | `algebra.py` is absent, as `PUBLICATION.json` discloses. It was not run or reconstructed. | +| Independent checks | `height_marks_review_check.py` is my own exact-rational suite. It covers the Jacobian, the normalization inequality, exact finite configuration models for the mixture and configuration bounds, and the integer inequalities. | + +## Verdicts + +| Interface (lines) | Verdict | +|---|---| +| §1 (8–42): the premise (H1) is RM's pointwise pre-height-integrated estimate; measure-level Kac–Rice | **ACCEPT**. RM §5 states exactly this: "the complete integrand after `r²/Z_r` differs uniformly from `Λ_j` by `O(r)`", uniformly in `x, b, k, R, t`. | +| §2 (44–84): (H2) Jacobian `kr³`; (H3); (H4) mass sandwich, variation `Cr⁴|E|`, TV `Cr` | **ACCEPT** | +| §3 (86–130): (H5) from RC Corollary D; the mixture; **Theorem H1 (H6)**; (H7); the complete-configuration version | **ACCEPT**, uniformly over deterministic `E_r` of positive volume. | +| §4 (132–144): single-point uniform versus pair-weighted Beta(2/3, 2) | **ACCEPT**. They are different objects. | +| §5 (146–159) scope | **ACCEPT** | + +No defect was found. + +--- + +## §1 — the premise and the mean measure + +The pointwise estimate (H1) is the right premise. An integrated mean cannot determine a height law, and `CONTRAST` +records the trivial counterexample. RM §5 proves it before integrating the window. RM compares the conditional +expectation in (12) with its contact counterpart at `O(r)`, uniformly in the height variable `t`, and does the same +for the density. `r²/Z_r → 1/z_0` holds with the full normalizer. The additional height pin is kept inside the +conditioning, as C5 says. + +(H2) substitutes `h = b − kr³θ`. The Jacobian is exactly `kr³` (`JACOBIAN`; the `jacobian-r` mutant is rejected). +So `μ_r` has density `kr³R_{r,j}(x, b − kr³θ)`, and (H3) follows. + +For (H4), each `Λ_j` is continuous and strictly positive on the compact remote parameter set: RM uses an open ball +around a nonsingular `H_x` of index `j`, for every `j`. So `cr³|E| ≤ m_r ≤ Cr³|E|`. Summing the `d + 1` indices gives +`‖μ_r − μ_{0,r}‖ ≤ Cr⁴|E|`. The normalization inequality +`‖μ/m − ν/n‖ ≤ (‖μ−ν‖ + |m−n|)/m ≤ 2‖μ−ν‖/m` holds because `|m−n| ≤ ‖μ−ν‖`. `NORMALIZE` checks it on 500 random +finite measures. An explicit instance shows that the `|m−n|` term cannot be dropped. The factor `|E|` cancels, so +the bound is uniform over deterministic `E_r`. + +## §2 — from the mean mark to the unique witness + +[RC] Corollary D gives `q_r ≤ Cr⁵|E|` uniformly in `E`, including tiny volumes (RC v2 absorption). So +`q_r/m_r ≤ Cr²`. The steps are: +- `a_r = E[N; N ≥ 2] ≤ q_r`, because `N ≤ N(N−1)` for `N ≥ 2`; +- `p_1 = m_r − a_r ≥ m_r − q_r > 0` for small `r`; +- the mixture `μ/m = (p_1/m)(σ/p_1) + η/m` gives `dTV(σ/p_1, μ/m) ≤ a/m`. + +With (H4), this gives (H6) at rate `Cr + Cr²`. + +The complete-configuration version uses the common submeasure `σ/m`, of mass `p_1/m`. It lies below +`Law(Ξ | N ≥ 1)`, since `P(N ≥ 1) ≤ m`, and below a singleton with mark law `μ/m`. So the TV is at most `a/m`. + +`MIXTURE` builds 200 exact random laws on configurations of up to four marked points. On each it checks +`μ = σ + η`, `a ≤ q`, both TV bounds `≤ a/m` in probability TV, and (H7). The mutants `a-le-half-q` and +`full-variation` are rejected. `INTEGER` checks the pointwise inequalities behind (H7) for `N ≤ 60`. + +## Notes + +- **N1 (relation to #120).** #120 Theorem H, accepted, is sharper for the height: + - `dTV(Law(θ | N_r = 1), λ) ≤ Cr²`; + - `dTV(S_r, π_{r,1} ⊗ λ) ≤ Cr²`, against the finite-`r` own location/index marginal. + + #120 §7 then derives exactly C5's (H6): `TV(S_r, π_E ⊗ λ) ≤ O(r²) + TV(π_{r,1}, π_E) = O(r)`. The `O(r)` in (H6) + comes from location/index drift, which is common to all heights, not from height non-uniformity. So C5 is + consistent with #120 and implied by it together with RM. C5's own route through the pointwise premise (H1) is also + complete. C5 adds the explicit limit law `π_E ⊗ Uniform(0, 1)` with its kernel `Λ_j`, which is the form a + contact-profile consumer needs. It adds no sharper rate. +- **N2 (no location/index independence).** (H6) makes the height asymptotically independent of the joint + location/index mark. It says nothing about independence between location and index, and C5 says so (line 112). +- **N3 (scope).** The fixed exclusion `ρ` is load-bearing: C2's local mechanism gives global multiplicity of order + `r³` in d = 2. The theorem is for deterministic `E_r`, not for field-selected `E`, and it is not a persistence or + lifetime law. + +## What this review does not do + +It does not review C6, which has no written proof source. It accepts no numerical constant and no global +conditional-singleton law. It changes no register, and it does not run or reconstruct `algebra.py`. + +## Reproduce + + python -B -S height_marks_review_check.py # prints RESULTS.json byte for byte + python -B -O -S height_marks_review_check.py # identical + python -B -S height_marks_review_check.py --mutant M # exit 1 for each of the 4 mutants diff --git a/reviews/remote_height_marks_claude_20260929/SOURCE_FILES.json b/reviews/remote_height_marks_claude_20260929/SOURCE_FILES.json new file mode 100644 index 000000000..126054609 --- /dev/null +++ b/reviews/remote_height_marks_claude_20260929/SOURCE_FILES.json @@ -0,0 +1,37 @@ +{ + "schema": 1, + "scientific_effect": "NONE", + "review_status": "NONAUTHOR_REVIEW", + "reviewed_object": { + "pr": "d6g8k5htny-coder/Math-#116", + "head": "0507e3a1dbd3dede84cbeb805947c70aa16ebc36", + "paths": [ + { + "path": "frontiers/window_multiplicity_laws_20260928/HEIGHT_MARKS.md", + "git_blob": "015d769675d9a2cf191286979d3b8c877cd91bdc", + "bytes": 7360, + "sha256": "44cc69260d27df3a66083ba127aaf275f240641cc8e3740ae0b0b119109270e2" + } + ] + }, + "files": [ + { + "path": "REVIEW.md", + "bytes": 7049, + "sha256": "b9acc3c5ebbb92acc5227dea87c48f6e75cd6845df2469d226cefdb2fbe123ad", + "git_blob": "f7588f56af840e00350bf856c0a0d3039ec1f05b" + }, + { + "path": "RESULTS.json", + "bytes": 747, + "sha256": "622bb3fc1ab3cdc9e72c9da4e2a3a84479a5313f7ed4b8205ab884145af16420", + "git_blob": "245bd4e467e4409838edeb5d8b91f95c24b22fbf" + }, + { + "path": "height_marks_review_check.py", + "bytes": 7667, + "sha256": "0ab95d8c8d54a8f38f93bb51e48847607f83208870481bb550a64333edaffadc", + "git_blob": "6e24a38be94ff406439343150b3f3fcf29944c61" + } + ] +} diff --git a/reviews/remote_height_marks_claude_20260929/height_marks_review_check.py b/reviews/remote_height_marks_claude_20260929/height_marks_review_check.py new file mode 100644 index 000000000..6e24a38be --- /dev/null +++ b/reviews/remote_height_marks_claude_20260929/height_marks_review_check.py @@ -0,0 +1,178 @@ +"""Independent nonauthor checks for OA-WINDOW-MULTIPLICITY-HEIGHT-20260928-v1 (Math-#116 C5, HEIGHT_MARKS.md). + +Python standard library only; exact rational arithmetic throughout. Written from the markdown; the author's absent +algebra.py is neither run nor reconstructed. Groups: + + JACOBIAN (H2): h = b - k r^3 theta has |dh/dtheta| = k r^3 exactly; with (H1) the mean density error is + k r^3 * C r = C r^4 per unit volume, and the normalized error is C r (H3)-(H4). + NORMALIZE the variation inequality ||mu/m - nu/n|| <= (||mu - nu|| + |m - n|)/m <= 2||mu - nu||/m on random + finite positive measures, plus an explicit instance where dropping the mass term fails. + MIXTURE exact finite configuration models (random laws on configurations of 0..4 marked points): the + decomposition mu = sigma + eta, a = E[N; N >= 2] <= q = E[N(N-1)], p_1 = m - a, the singleton-mark + bound dTV(sigma/p_1, mu/m) <= a/m, and the complete-configuration bound + dTV(Law(Xi | N >= 1), singleton with mark law mu/m) <= a/m, all in probability TV (half variation). + INTEGER pointwise: N - 1{N>=1} <= N(N-1)/2, 1{N>=2} <= N(N-1)/2, N 1{N>=2} <= N(N-1) for N = 0..60. + CONTRAST integrated means do not determine the height law (two densities with equal mass); the single-point + uniform limit versus the pair-weighted Beta(2/3, 2) gap: E|theta - theta'| = 1/3 for independent + uniforms, 1/4 for the RP pair law. + +Mutants (each must fail): jacobian-r, drop-mass-term, a-le-half-q, full-variation. +Not an analytic proof: the source estimate (H1) is RM section 5 and is reviewed in REVIEW.md. +""" +import argparse +import itertools +import json +import random +import sys +from fractions import Fraction as F + +MUTANTS = ("jacobian-r", "drop-mass-term", "a-le-half-q", "full-variation") +MUT = None + + +def var(mu, nu, keys): + return sum(abs(mu.get(k, F(0)) - nu.get(k, F(0))) for k in keys) + + +def tv(mu, nu, keys): + full = var(mu, nu, keys) + return full if MUT == "full-variation" else full / 2 + + +def check_jacobian(): + ok = True + for k in (F(1, 2), F(3), F(7, 4)): + for r in (F(1, 10), F(1, 3)): + b = F(2, 3) + th1, th2 = F(1, 5), F(4, 5) + h1, h2 = b - k * r ** 3 * th1, b - k * r ** 3 * th2 + jac = abs((h2 - h1) / (th2 - th1)) + expected = r if MUT == "jacobian-r" else k * r ** 3 + ok &= jac == expected + # density error k r^3 * (C r) against mass ~ k r^3: normalized order r + ok &= (k * r ** 3 * r) / (k * r ** 3) == r + return {"H2_jacobian_is_k_r_cubed": ok} + + +def check_normalize(): + rng = random.Random(116501) + ok = True + for _ in range(500): + n = rng.randint(1, 6) + keys = list(range(n)) + mu = {i: F(rng.randint(0, 9), rng.randint(1, 5)) for i in keys} + nu = {i: F(rng.randint(0, 9), rng.randint(1, 5)) for i in keys} + m, nn = sum(mu.values()), sum(nu.values()) + if m == 0 or nn == 0: + continue + lhs = var({i: mu[i] / m for i in keys}, {i: nu[i] / nn for i in keys}, keys) + d = var(mu, nu, keys) + ok &= lhs <= (d + abs(m - nn)) / m <= 2 * d / m + # dropping the mass term is false: mu = (1, 1), nu = (0, 1) gives 1 > 1/2 + mu, nu, keys = {0: F(1), 1: F(1)}, {0: F(0), 1: F(1)}, [0, 1] + lhs = var({i: mu[i] / 2 for i in keys}, {i: nu[i] for i in keys}, keys) + bound = var(mu, nu, keys) / 2 if MUT == "drop-mass-term" else (var(mu, nu, keys) + 1) / 2 + ok &= lhs == 1 and lhs <= bound + return {"normalization_variation_inequality": ok} + + +def random_configuration_law(rng, marks): + """A random law on configurations (multisets) of 0..4 marked points.""" + configs = [()] + for size in range(1, 5): + configs += list(itertools.combinations_with_replacement(marks, size)) + weights = [F(rng.randint(0, 6)) for _ in configs] + weights[0] += 50 # most mass on the empty configuration, as for a rare window + for i, c in enumerate(configs): # thin larger configurations + if len(c) >= 2: + weights[i] = weights[i] / (4 ** len(c)) + total = sum(weights) + return {c: w / total for c, w in zip(configs, weights) if w > 0} + + +def check_mixture(): + rng = random.Random(116502) + marks = ("a", "b", "c") + ok_decomp = ok_a = ok_single = ok_config = ok_h7 = True + for _ in range(200): + law = random_configuration_law(rng, marks) + mu, sigma = {}, {} + m = a = q = p1 = pn = F(0) + for c, p in law.items(): + N = len(c) + m += N * p + q += N * (N - 1) * p + if N >= 1: + pn += p + if N == 1: + p1 += p + sigma[c[0]] = sigma.get(c[0], F(0)) + p + if N >= 2: + a += N * p + for x in c: + mu[x] = mu.get(x, F(0)) + p + if m == 0 or p1 == 0: + continue + eta = {x: mu.get(x, F(0)) - sigma.get(x, F(0)) for x in marks} + ok_decomp &= all(v >= 0 for v in eta.values()) and sum(eta.values()) == a and p1 == m - a + bound_a = q / 2 if MUT == "a-le-half-q" else q + ok_a &= a <= bound_a + # singleton mark law versus mean mark law + ok_single &= tv({x: sigma.get(x, F(0)) / p1 for x in marks}, {x: mu.get(x, F(0)) / m for x in marks}, + marks) <= a / m + # complete configuration: Law(Xi | N >= 1) versus a singleton with mark law mu/m + cond = {c: p / pn for c, p in law.items() if len(c) >= 1} + single = {(x,): mu.get(x, F(0)) / m for x in marks} + keys = set(cond) | set(single) + ok_config &= tv(cond, single, keys) <= a / m + # (H7) + ok_h7 &= m - pn <= q / 2 and (pn - p1) <= q / 2 + return {"mu_equals_sigma_plus_eta_and_p1_equals_m_minus_a": ok_decomp, + "a_le_q": ok_a, + "singleton_mark_law_within_a_over_m": ok_single, + "configuration_law_within_a_over_m": ok_config, + "H7_integer_consequences": ok_h7} + + +def check_integer(): + ok = True + for N in range(61): + fact = F(N * (N - 1)) + ok &= N - int(N >= 1) <= fact / 2 and int(N >= 2) <= fact / 2 and N * int(N >= 2) <= fact + return {"pointwise_integer_inequalities": ok} + + +def check_contrast(): + # two height densities on (0,1) with the same total mass 1: uniform and 2 theta; mean of theta differs + mean_uniform = F(1, 2) + mean_linear = F(2, 3) # int_0^1 theta * 2 theta + out = {"integrated_mass_does_not_fix_height_law": mean_uniform != mean_linear} + # independent uniforms: E|a - b| = 1/3; RP pair law Beta(2/3, 2): E g = 10/((3+2)(3+5)) = 1/4 + out["single_uniform_vs_pair_beta_gap"] = F(1, 3) != F(10, 5 * 8) and F(10, 5 * 8) == F(1, 4) + return out + + +def flatten(d): + for v in d.values(): + if isinstance(v, dict): + yield from flatten(v) + else: + yield v + + +def main(): + global MUT + ap = argparse.ArgumentParser() + ap.add_argument("--mutant", choices=MUTANTS) + MUT = ap.parse_args().mutant + checks = {"JACOBIAN": check_jacobian(), "NORMALIZE": check_normalize(), "MIXTURE": check_mixture(), + "INTEGER": check_integer(), "CONTRAST": check_contrast()} + passed = all(flatten(checks)) + print(json.dumps({"object": "CLAUDE-REVIEW-REMOTE-HEIGHT-MARKS-20260929-v1", "checks": checks, + "passed": passed, "scope": "exact finite identities only; not an analytic proof"}, + indent=2, sort_keys=True)) + return 0 if passed else 1 + + +if __name__ == "__main__": + sys.exit(main()) diff --git a/reviews/remote_inverse_separation_claude_20260929/RESULTS.json b/reviews/remote_inverse_separation_claude_20260929/RESULTS.json new file mode 100644 index 000000000..cdecf7792 --- /dev/null +++ b/reviews/remote_inverse_separation_claude_20260929/RESULTS.json @@ -0,0 +1,58 @@ +{ + "checks": { + "COEFF": { + "A_p_equals_A_0_times_S_moment": true, + "I20_normalizes_to_one": true, + "I21_slope_equals_J0_over_A0": true, + "I8_at_p0_reduces_to_R3_three_fortieths": true, + "I8_constant_108_equals_three_quarters_144": true, + "abelian_limit_of_I8_matches_I19": true + }, + "CUTOFF": { + "q2_log_with_bounded_remainder": true, + "q3_q4_leading_terms_J_eps_power_over_q_minus_2": true, + "small_cdf_has_factor_one_half": true + }, + "ENVELOPE": { + "endpoint_shell_sums_grow_linearly": true, + "envelope_finite_exactly_on_minus2_lt_p_lt_1": true, + "t_window_length_is_k_over_s_cubed": true, + "z_overlap_is_k_minus_s3_abs_t": true + }, + "LEDGER": { + "J_r_is_order_r_cubed_by_both_routes": true, + "blow_up_radial_power_is_one_all_d": true, + "fixed_r_radial_power_is_one_all_d": true, + "frames_agree_after_dy_prime_equals_delta3_dt": true, + "gradient_only_frame_det_is_delta_minus_d": true, + "height_divided_frame_det_is_delta_minus_d_minus_3": true + }, + "OVERLAP": { + "I11_at_p0_is_R10_three_tenths": true, + "I11_overlap_integral_exact_negative_and_positive_p": true, + "T_exponent_in_1_2_on_domain": true + }, + "PAIR": { + "I14_limit_with_order_delta_squared_error": true, + "det_squared_le_He_squared_times_frobenius": true, + "determinant_product_exact_identity": true, + "height_gap_is_minus_T_delta_cubed_over_12": true, + "pair_fields_have_both_critical_points": true, + "same_index_product_is_order_delta_four": true, + "segment_bound_He_le_half_delta_D3": true, + "two_windows_differ_on_measure_abs_gap": true + }, + "RANK": { + "delta0_positivity_list_full_rank_d2_d3": true, + "delta_positive_frame_full_rank_d2_d3": true, + "undivided_gradient_frame_degenerates_at_delta0": true + }, + "SCOPE": { + "iterated_limits_both_J0_but_coupled_cutoff_sees_J0_plus_half": true, + "tv_convergence_does_not_control_inverse_moments": true + } + }, + "object": "CLAUDE-REVIEW-REMOTE-INVERSE-SEPARATION-20260929-v1", + "passed": true, + "scope": "exact finite identities only; not an analytic proof" +} diff --git a/reviews/remote_inverse_separation_claude_20260929/REVIEW.md b/reviews/remote_inverse_separation_claude_20260929/REVIEW.md new file mode 100644 index 000000000..df9cdc1f1 --- /dev/null +++ b/reviews/remote_inverse_separation_claude_20260929/REVIEW.md @@ -0,0 +1,203 @@ +# Nonauthor analytic review: remote inverse separation and the sharp power-two threshold (Math-#128) + +Scientific effect: **NONE**. This file changes no register, status, graph node, lemma flag, prize or author source. +It records a verdict on the draft candidate in Math-#128. Integration is a separate act. + +## Object + +| Field | Value | +|---|---| +| Object | OA-REMOTE-INVERSE-SEPARATION-20260928-v1 (OpenAI / ChatGPT) | +| Branch / head | `chatgpt/remote-inverse-separation-20260928` / `b3880006df94573b4d99d05c37b3254e063035fb` ([Math-#128](https://github.com/d6g8k5htny-coder/Math-/pull/128)); packet tree `68b0a79e6b33cbde6afbe1d4385d43bc9b9e842e` | +| `PROOF.md` | Git blob `1b24d0f6d07f84706a0a8e9b25e111e6eff93a2b`, 18054 B, SHA256 `95a9aa75e4a254a8f50efc16ee00a78a2ea1481f4013a708dfcbb77dcad4c393`, 351 lines | +| Consumed, on main | [RP] `frontiers/window_multiplicity_laws_20260928/REMOTE_PAIR_LAW.md` (blob `3fb60204…`, reviewed by me, integrated by Math-#129 at `e7f8aca`). [RC] `frontiers/remote_collision_20260928/PROOF.md` (blob `7b48a88e…`): (3.1), (4.1)–(4.3), Lemmas 1–5. [RM] `frontiers/remote_window_20260924/PROOF.md` (blob `b383bfcc…`): §2 field and distinct-jet principle, §4 endpoint identities, full normalizer. All four `SOURCE_MAP.json` identities (including comparison-only RD) were re-read from their pinned commits and match byte for byte. | +| Request | [Author offer 5881043551](https://github.com/d6g8k5htny-coder/Math-/pull/128#issuecomment-5881043551); pickup [5887884959](https://github.com/d6g8k5htny-coder/Math-/pull/128#issuecomment-5887884959) | + +## Provenance and exposure + +| Field | Value | +|---|---| +| Reviewer | Anthropic Claude, Claude Code session `session_017Mi3hxjaxV45x6zo6o1ee3` | +| Relation | Different provider from the OpenAI author. Same GitHub account as every lane, so no organizational independence is claimed. | +| Exposure | **I authored [RC]** and **reviewed [RP]** (C3, ACCEPT). This review checks that the note uses them correctly; it is not independent evidence for either. [RC]'s nonauthor record is the xAI/Harper review 5342481786 on #110 (finite identities, the (3.1) mark, the Lemma 1 mechanism) and the xAI/Grok ledger review on #113. | +| Author code | `verify.py` replayed on an exact archive of the head in both `-B -S` and `-B -O -S` modes: 12 tests and 8 intended mutant failures per mode, `RESULTS.json` matched. It is a finite scalar companion; I rely on it for nothing below. | +| Independent checks | `inverse_review_check.py` is my own exact-rational suite, written from the markdown. It covers finite identities only. | + +## Verdicts + +| Interface (lines) | Verdict | +|---|---| +| §1 (7–81): `M_p` as an expected ordered-pair sum allowed to be infinite; normalized expected-pair measure distinct from event sampling | **ACCEPT** | +| §2 (83–143), **Theorem I (I2)**: `M_p(r) = r^{5+p}A_p + o(r^{5+p})` for fixed `−2 < p < 1`, with `A_p` of (I8) | **ACCEPT**; see §1 below. | +| §3 (145–204): gradient-only frame (I12), Jacobian `δ^{−d}`, fixed-`r` floor, (I13)/(I14), one height indicator in the limit | **ACCEPT**; see §2 below, note N1. | +| §4 (206–265), **Theorem II (I3)–(I5)**: `j_r(δ) = δ[J_r + o(1)]` with `0 < J_r < ∞`; `M_p(r) < ∞` iff `p > −2`; cutoff equivalents | **ACCEPT** at each fixed `r ≤ r_1`; see §3 below, note N3. | +| §5 (267–292): (I18), `J_r/r³ → J_0` (I19) | **ACCEPT**; see §4 below. | +| §6 (294–329), **Theorem III (I6)–(I7)**: TV law of `S`, `g_S(s) ~ (J_0/A_0)s`, `P(S ≤ ε) ~ J_0ε²/(2A_0)`, inverse moments for `0 < q < 2`, infinite for `q ≥ 2` | **ACCEPT**; see §5 below. | +| §7 (331–351) exclusions: coupled `ε(r)`, same-index threshold, event-conditioned law, `p ≥ 1` asymptotics, `ρ → 0`, random `E` | **ACCEPT** as stated. Two are shown to be needed by exact counterexamples (N4). | + +No defect was found. Notes N1–N5 delimit or simplify; none changes a statement. + +--- + +## §1 — Theorem I: the weighted envelope and the constant (§2) + +**Envelope (I10).** RP's domination `C s(1+|t|)^{−m}1_{(I9)}` comes from [RC] Lemmas 2–4 and holds uniformly for +`0 < δ = rs < η_0` and `0 < r ≤ r_1`, including `s → 0`. For fixed `(s, z)`, the `t`-window in (I9) has length exactly +`k/s³` (checked). Integrating `z, t` gives `≤ C s min(1, s^{−3})`. The weight `dist^p = r^p s^p` turns this into +`s^{p+1}` near 0 and `s^{p−2}` near ∞. `ENVELOPE` decides convergence exactly for rational `p`. On dyadic-power shells +the two pieces are geometric series with ratios `2^{−q(p+2)}` and `2^{q(p−1)}`, where `q` is the denominator of `p`. +Both ratios are `< 1` precisely on `−2 < p < 1`. At `p = −2` and `p = 1` every shell contributes at least `1/2`. So +"integrable precisely for −2 < p < 1" is exact. It concerns this envelope only. The note does not infer divergence at +`p = −2` from it (lines 141–143), and §3 below supplies the lower bound. + +**Separated pairs.** On `δ ≥ η_0` the weight `δ^p` is bounded for either sign of `p`, and [RC] Lemma 5 gives +`O(r⁶)`. After division by `r^{5+p}` this is `O(r^{1−p}) → 0` because `p < 1`. Correct. + +**Fixed Borel `E`.** This is RP's argument: truncate `s, t`, remove `1_E(x + rse)` by `L¹` continuity of torus +translations, and control the tails by (I10). It stays valid with the unbounded weight at `s = 0`, because the +truncation is to compact `s`-ranges `[s_0, S_0]` and the envelope is integrable on `(0, s_0)`. + +**Constant.** (I11) is checked exactly on instances where `(k/|t|)^{1/3}` is a perfect power, for +`p ∈ {−7/4, −3/2, −1, −1/2, −1/3, 0, 1/3, 1/2, 3/4}` (`OVERLAP`). The rest of the chain is also checked: +- (I11) times `36t²` gives the numerator `108`; +- `12^{(p+2)/3}·12^{(4−p)/3} = 144`, so `108·12^{−(4−p)/3} = (3/4)·12^{(p+2)/3}`; +- at `p = 0`, (I8) reduces to RP's `(3/40)12^{2/3}` (`COEFF`). + +The `T`-exponent `(4−p)/3` lies in `(1, 2)`, so there is no singularity at `T = 0`. Tonelli on `|t| > η` is the right +way to handle it. + +## §2 — the fixed-`r` gradient-only frame (§3) + +**Jacobian.** `(∇f(x), ∇f(x')) ↦ G_δ = (∇f(x), (∇f(x') − ∇f(x))/δ)` has `|det| = δ^{−d}`. RC's height-divided map +(4.1) has `|det| = δ^{−d−3}`, and `dy' = δ³dt` returns it to `δ^{−d}`. All three facts are checked on exact matrices +for d = 2…6 (`LEDGER`). The two frames therefore agree where both apply. Integrating RC's `t` over all of `ℝ` at +fixed `r` recovers the gradient-only density. The note is right that reusing `δ^{−d−3}` without the `dy'` factor would +be wrong. A mutant that does so breaks the radial power (`height-jacobian`). + +**Floor.** `G_δ` is literally the first two blocks of RC's `V_δ`. So `(U_r, G_δ, f(x))` has a principal-submatrix +floor `≥ c_1 I` from [RC] Lemma 1, for all `0 < r ≤ r_1` and `0 ≤ δ ≤ η_0` (note N1). + +**(I13)/(I14).** On `∇f(x) = ∇f(x + δe) = 0`, the Taylor expansion gives `0 = δH_x e + (δ²/2)D³f[e,e,·] + O(δ³)`, +and the other endpoint follows from `H_{x'}e = H_x e + δD³f[e,e,·] + O(δ²)`. Congruence by `diag(δ^{−1/2}, I)` gives +`diag(∓T/2, A)`. `|det|` is continuous everywhere with polynomial Lipschitz bounds, so the coupled `L^a` limit +`(T²/4)(det A)²` follows without inverse Hessians. + +On the explicit fields `f(u,v) = (T/6)u³ − (T/4)δu² + ½vᵀAv + (u² − δu)c·v` in d = 2, 3, 4, `PAIR` checks the exact +identity + + det H_x · det H_{x'} = −δ²[(T²/4)(det A)² − δ²q²], q = cᵀadj(A)c, + +so the error in (I14) is `O(δ²)` there. The a priori bound also holds exactly on these fields: +`|H_x e|_∞ = (δ/2)·max|D³f|`, and `det(H)² ≤ |He|²‖H‖_F^{2(d−1)}`. + +**One height indicator.** Given zero gradients, RC's trapezoid identity gives `f(x') − f(x) = δ³D3_δ`, with +`|D3_δ| ≤ ‖f‖_{C³}/12`. On the explicit field the gap is exactly `−Tδ³/12`. For an interval of length greater than +the gap, the set of `y` with `y ∈ I_r` but `y + gap ∉ I_r` has measure exactly `|gap|` (checked). The two indicators +therefore differ only when `f(x)` lies within `O(δ³‖f‖_{C³})` of an endpoint of `I_r`. The floor bounds the +conditional density of `f(x)` given `(U_r, G_δ = 0)` uniformly, and Hölder with the determinant moments finishes the +step. The width `kr³` is fixed and positive throughout this limit, as the note says. A mutant with gap rate `δ²` is +rejected (`merge-rate`). + +## §3 — Theorem II: positivity, the radial power and the threshold (§4) + +**Kac–Rice at fixed `r`.** Summing [RC] (3.1) over index pairs and integrating the heights (Fubini, with the +nondegenerate joint density for `x ≠ x'`) gives the gradient-only form. Its intensity is `K_r(x, x+δe) = +δ^{−d}p_{G_δ}(0)E[W_r|det H_x det H_{x'}|1 1 | G_δ = 0]/Z_r`. By §2, `δ^{d−2}K_r → c_r` of (I15), uniformly on +compact `(x, e)`, with the dominating bound `C_r` from the segment estimate. The weight `W_r` enters once and `Z_r` +once. Exhaustion away from the diagonal permits infinite values, as the note says. + +**Positivity of `c_r`.** The listed variables are the endpoint Hessians `H_M, H_S`, the transverse block `A`, the +third derivative `T` and the height `f(x)`. Conditional on `(U_r, G_0 = 0)` they are distinct derivative functionals +at the three distinct sites `M`, `S`, `x`: orders 0, 1, 2 (`He` and `A` exhaust `H_x`) and 3 at `x`, and orders 0–2 +at `M`, `S`. By [RM] §2, with every Fourier weight positive, they are jointly nondegenerate. `RANK` confirms the +algebraic core exactly. On polynomial spaces over `ℚ`, the whole (I15) list has full rank in d = 2 (19 functionals) +and d = 3 (31 functionals). So does the `δ > 0` frame (pins, `∇f(x)`, `∇f(x + δe)`, `f(x)`). As a negative control, +the undivided frame `∇f(x + 0·e)` loses exactly `d` ranks at `δ = 0`, which is why (I12) divides. + +The open event (`H_M < 0`, `H_S` of index `d−1`, `f(x)` inside `I_r`, `det A ≠ 0`, `T ≠ 0`) has positive +probability, and the integrand `W_r T²(det A)²` is positive on it. So `c_r > 0`. Compactness gives `0 < J_r < ∞` for +`|E| > 0`. + +**All-index sum.** The positive coefficient `T²/4` comes from adjacent-index pairs. RP's same-index control +(`T = 0` with a mixed cubic) gives a product `c⁴δ⁴`, which vanishes at order `δ²`. The note is right that the all-index +sum is essential and that no same-index threshold follows (lines 79–81). + +**Radial power (I16).** `(d − 1) − d + 2 = 1` for every d (`LEDGER`). The translated indicator is removed by +`sup_{|h|≤δ}‖1_E(·+h) − 1_E‖₁ → 0` against the bounded limit `c_r`. This proves (I3) with (I17). + +**Threshold (I4).** On `(0, δ_r)`, `(J_r/2)δ ≤ j_r ≤ (3J_r/2)δ`. The domination already gives `j_r ≤ C_r δ` on +`(0, η_0)`, and separated pairs are bounded. So `M_p(r) < ∞` iff `∫_0 δ^{p+1} < ∞`, which is iff `p > −2`. Necessity +comes from the positive lower bound, not from the failure of an upper envelope. This is the step the offer asked to +be checked, and it is sound. + +**Cutoffs (I5).** Integrating `δ^{1−q}(J_r + o(1))` and sending `ε → 0` before `ε_1 → 0` gives `J_r log(δ_0/ε)` for +`q = 2` and `J_rε^{2−q}/(q−2)` for `q > 2`. `CUTOFF` checks the algebra on a model density `δ(J + aδ)`. See note N3 +on the remainder. + +## §4 — contact matching (§5) + +(I18) is the height disintegration of (I15). Put `h = b − kr³θ`, so `dh = kr³dθ`. The frame +`(U_r, ∇f(x), H_x e, f(x))` is the `δ = 0` subvector of [RC] Lemma 1, so its floor is uniform through `r = 0`. Under +these extra observations, [RM] §4's endpoint identities give `W_r/r² → w_0`. This is the extra-conditioned limit +already accepted for RP §4. It is not the unconditioned D1 normalizer limit. Separately, `Z_r/r² → z_0` holds, and +`Z_r` is not replaced. Dominated convergence yields `c_r/r³ → (k/(4z_0))p_{Y|Q_0}(0,0,b)·E[w_0T²(det A)²|Y]` +uniformly on compact sets. Hence `J_r/r³ → J_0 > 0`. + +The r-power is 3 by both routes: `r³` from the window with `W/Z ~ r⁰`, and `5 − 1 − 1` from `j_r(rs)r ds = +r⁵A_0 g_S(s) ds` combined with `g_S(s) ~ (J_0/A_0)s` (`LEDGER`). This consistency of the iterated limits is a check. +It is not a joint limit, and the note claims none (lines 290–292). + +## §5 — Theorem III (§6) + +(I20) follows from RP's limit integrand. Integrating `z` gives `(k − s³|t|)_+`, and `Ψ_E` collects the `t`-density +and the conditional expectation. Its normalization `∫g_S = 1` is exactly `36·(3/10) = 54/5 = (3/40)·144` (`COEFF`). +As `s ↓ 0`, `(k − s³|t|)_+ ↑ k` monotonically, so `g_S(s)/s → (36k/(z_0A_0))∫t²Ψ_E`. With `T² = 144t²`, +`J_0 = (k/(4z_0))·144∫t²Ψ_E`, and `144/4 = 36` gives (I21). Integrating then gives the `ε²/2` in (I6). A mutant +dropping the half is rejected (`cdf-half`). + +For `0 < q < 2`, `E[S_r^{−q}] = r^qM_{−q}(r)/M_0(r) → A_{−q}/A_0` by Theorem I at `p = −q` and `p = 0`. The Tonelli +identity `A_p = A_0∫s^p g_S ds` holds with matching prefactor `108/((p+2)(p+5))` (`COEFF`). The note is right that TV +convergence alone does not transfer an unbounded inverse moment: `SCOPE` exhibits a family with TV distance `1/n` and +an added `q = 1` inverse moment of `n`. For `q ≥ 2` both expectations are infinite: at finite `r` by Theorem II, and +in the limit by (I21). + +**Abelian cross-check.** (I8) and (I19) are computed independently. They must satisfy `(p + 2)A_p → J_0` as +`p ↓ −2`, because `∫s^p g_S ~ (J_0/A_0)/(p+2)`. At `p = −2` the rational prefactor of `(p+2)A_p` is +`3/(4·3) = 1/4`, the `k`-power is `1` and the `T`-power is `2`. These are exactly (I19)'s `k/(4z_0)` and `T²`. +`COEFF` checks this, and the `contact-quarter` mutant (`1/2` in (I19)) is rejected. The note does not state this +identity. It is a consequence, recorded here as a consistency certificate for the two constants. + +## Notes + +- **N1 (simplification).** The fixed-`r` floor paragraph (lines 158–166) is correct, but it is not needed for the + floor: `(U_r, G_δ, f(x))` is a principal subvector of [RC] Lemma 1's frame, so its floor is uniform in + `0 < r ≤ r_1` as well. The genuinely new support input is the positivity list of (I15). The phrase "three distinct + sites" covers `δ = 0`. For `δ > 0` the frame has four sites, which is [RC] Lemma 1 step 2. "Sufficiently small `r`" + in Theorem II can be read as `r ≤ r_1` of [RC] Lemma 1, with `η_0 ≤ ρ/2`. `J_r` and `δ_r` depend on `r`. +- **N2 (wording).** Line 99 gives `(4−p)/3 > 1` as the reason there is no `T`-singularity. What is needed is + `(4−p)/3 > 0`; on the domain the exponent lies in `(1, 2)`. Harmless. +- **N3 (no bounded remainder).** The `o(1)` in (I3) has no rate. So the `q = 2` case of (I5) is an asymptotic + equivalence only, and `I_2 = J_r log(δ_0/ε) + O_r(1)` does not follow. The note writes `~` correctly. This note is + here so that downstream text does not read a bounded remainder into it. +- **N4 (exclusions are needed).** `SCOPE` gives an exact family `g(r,δ) = J_0 + h(δ/r^{10})`, with + `h(u) = u/(1+u²)`. Both iterated limits of `g` equal `J_0`: fixed `r` with `δ → 0`, and `δ = rs` with `r → 0`. Yet + the coupled cutoff `δ = r^{10}` sees `J_0 + 1/2`. So a coupled `ε(r)` statement cannot follow from (I3)+(I6)+(I19) + alone, as line 75 says. The TV example in §5 shows that (I7) needs the weighted domination. +- **N5 (novelty boundary).** Short-range correlation and adjacent-index attraction of critical points in the + unconditioned isotropic setting are prior work (Azaïs–Delmas, arXiv:1911.02300), as RECONNAISSANCE.md records. What + this review accepts is the pinned, tilted, fixed-`ρ`, fixed-`E` statement at existential scope: the sharp power-two + threshold with its positive fixed-`r` coefficient, the negative moments `−2 < p < 1`, and the contact matching. + +## What this review does not do + +- It does not review C4 (`REMOTE_DISTANCE_MOMENTS.md`) or credit its `p = 1` transition or upper tail. The note + consumes neither. +- It accepts no coupled-cutoff limit, same-index threshold, event-conditioned pair law, `p ≥ 1` r-asymptotic, + uniformity as `ρ → 0` or over oscillating `E_r`, or numerical constant. +- It changes no register. + +## Reproduce + + python -B -S inverse_review_check.py # prints RESULTS.json byte for byte + python -B -O -S inverse_review_check.py # identical + python -B -S inverse_review_check.py --mutant M # exit 1 for each of the 7 mutants diff --git a/reviews/remote_inverse_separation_claude_20260929/SOURCE_FILES.json b/reviews/remote_inverse_separation_claude_20260929/SOURCE_FILES.json new file mode 100644 index 000000000..275204a1a --- /dev/null +++ b/reviews/remote_inverse_separation_claude_20260929/SOURCE_FILES.json @@ -0,0 +1,37 @@ +{ + "schema": 1, + "scientific_effect": "NONE", + "review_status": "NONAUTHOR_REVIEW", + "reviewed_object": { + "pr": "d6g8k5htny-coder/Math-#128", + "head": "b3880006df94573b4d99d05c37b3254e063035fb", + "paths": [ + { + "path": "frontiers/remote_inverse_separation_20260928/PROOF.md", + "git_blob": "1b24d0f6d07f84706a0a8e9b25e111e6eff93a2b", + "bytes": 18054, + "sha256": "95a9aa75e4a254a8f50efc16ee00a78a2ea1481f4013a708dfcbb77dcad4c393" + } + ] + }, + "files": [ + { + "path": "REVIEW.md", + "bytes": 16477, + "sha256": "389b4cadf5895caa3a469d7f1f7d05beab6ee8d3e5f1c8f7014d343d0a40fade", + "git_blob": "df9cdc1f1110cc6329c2ce2269daf9271bc071a3" + }, + { + "path": "RESULTS.json", + "bytes": 2202, + "sha256": "093a64a7320d0ca843282926af013a0f8a5679295e9a27d91f6004150e3fb1fe", + "git_blob": "cdecf77928e4cc5c77c014d100574a80e6c3a9c3" + }, + { + "path": "inverse_review_check.py", + "bytes": 23164, + "sha256": "e61a5915bb053e275c1e608c2ddb2df73697abbaf624fc38b027e73db5e12ce4", + "git_blob": "0acbcea8b20cbe55e512a4f7f1e82edf0f2ae0d6" + } + ] +} diff --git a/reviews/remote_inverse_separation_claude_20260929/inverse_review_check.py b/reviews/remote_inverse_separation_claude_20260929/inverse_review_check.py new file mode 100644 index 000000000..0acbcea8b --- /dev/null +++ b/reviews/remote_inverse_separation_claude_20260929/inverse_review_check.py @@ -0,0 +1,464 @@ +"""Independent nonauthor checks for OA-REMOTE-INVERSE-SEPARATION-20260928-v1 (Math-#128, PROOF.md). + +Python standard library only; exact rational arithmetic throughout. Written from the markdown; the author's +inverse.py/test_inverse.py are replayed separately and not reused here. Groups: + + LEDGER exact frame Jacobians: (grad f(x), grad f(x')) -> G_delta has det delta^(-d); the height-divided frame of + RC (4.1) has det delta^(-d-3), and with dy' = delta^3 dt it reduces to the same delta^(-d); radial powers + (d-1)-d+2 = 1 (fixed r, (I16)) and (d-1)-(d+3)+3+2 = 1 (blow-up); r-power 3 of J_r from both routes. + ENVELOPE (I10): the z-length/t-window algebra; exact dyadic shell ratios decide convergence of s^(p+1) at 0 and + s^(p-2) at infinity for rational p, so the envelope is finite exactly on -2 < p < 1. + OVERLAP (I11) on exact instances (k/|t| a perfect power chosen so every rational power is rational), for + negative and positive p, including p = 0 = (R10); the T-exponent (4-p)/3 lies in (1, 2). + COEFF (I8) constant 108 * 12^(-(4-p)/3) = (3/4) 12^((p+2)/3); the p = 0 reduction to RP (R3) (3/40); the + normalization of (I20); the Tonelli identity A_p = A_0 * int s^p g_S; the slope (I21) 144/4 = 36; and an + Abelian cross-check between (I8) and (I19): (p+2) A_p -> J_0 as p decreases to -2. + PAIR explicit polynomial fields in d = 2, 3, 4 with critical points at x and x + delta e: exact identity + det H_x det H_x' = -delta^2[(T^2/4)(det A)^2 - delta^2 q^2], hence (I14) with an O(delta^2) error; the + segment bound |H_x e| <= (delta/2)|D^3 f|; det(H)^2 <= |He|^2 ||H||_F^(2(d-1)); the height gap + f(x') - f(x) = -T delta^3/12, so two windows differ on a y-set of measure exactly |T| delta^3/12. + RANK distinct-jet independence as exact rank over Q of derivative functionals on polynomial spaces: pins, + grad f(x), H_x e, A, T, f(x), H_M, H_S at delta = 0 (the (I15) positivity list) and pins, grad f(x), + grad f(x + delta e), f(x) at delta > 0; negative control: grad f(x + 0 e) duplicates grad f(x). + CUTOFF (I5)/(I6) on a model radial density delta(J + a delta): q = 3, 4 power asymptotics, the q = 2 log with a + bounded rational remainder, and the CDF half. + SCOPE counterexamples recording why the scope limits are needed: a family with both iterated limits equal to + J_0 but a coupled cutoff delta = r^10 seeing J_0 + 1/2; a TV-convergent family whose inverse moment + diverges, so (I7) needs the weighted domination rather than TV alone. + +Mutants (each must fail): height-jacobian, envelope-endpoint, overlap-three, contact-quarter, merge-rate, +jet-duplicate, cdf-half. +Not an analytic proof: the Gaussian conditioning, Kac-Rice, domination and translation steps are reviewed in REVIEW.md. +""" +import argparse +import itertools +import json +import random +import sys +from fractions import Fraction as F + +MUTANTS = ("height-jacobian", "envelope-endpoint", "overlap-three", "contact-quarter", "merge-rate", + "jet-duplicate", "cdf-half") +MUT = None + + +def det(A): + n = len(A) + M = [list(map(F, r)) for r in A] + d = F(1) + for c in range(n): + p = next((i for i in range(c, n) if M[i][c] != 0), None) + if p is None: + return F(0) + if p != c: + M[c], M[p] = M[p], M[c] + d = -d + d *= M[c][c] + for i in range(c + 1, n): + f = M[i][c] / M[c][c] + M[i] = [x - f * y for x, y in zip(M[i], M[c])] + return d + + +def rank(rows): + M = [list(map(F, r)) for r in rows] + rk, cols = 0, len(M[0]) if M else 0 + for c in range(cols): + p = next((i for i in range(rk, len(M)) if M[i][c] != 0), None) + if p is None: + continue + M[rk], M[p] = M[p], M[rk] + for i in range(len(M)): + if i != rk and M[i][c] != 0: + f = M[i][c] / M[rk][c] + M[i] = [x - f * y for x, y in zip(M[i], M[rk])] + rk += 1 + return rk + + +def ipow(x, n): + """x^n for rational x and integer n (negative allowed).""" + return F(x) ** n + + +# --------------------------------------------------------------------------------------------------------------- + +def check_ledger(): + out = {} + ok_grad = ok_height = ok_consistent = True + for d in range(2, 7): + for delta in (F(1, 3), F(2, 7), F(1, 10)): + # (g, g') -> (g, (g' - g)/delta), variables ordered g_1..g_d, g'_1..g'_d + L = [[F(0)] * (2 * d) for _ in range(2 * d)] + for i in range(d): + L[i][i] = F(1) + L[d + i][i] = -1 / delta + L[d + i][d + i] = 1 / delta + g_power = -(d + 3) if MUT == "height-jacobian" else -d + ok_grad &= abs(det(L)) == delta ** g_power + # RC (4.1): (g, g', y, y') -> (g, (g'-g)/delta, y, [y' - y - (delta/2) e.(g + g')]/delta^3), e = first axis + n = 2 * d + 2 + V = [[F(0)] * n for _ in range(n)] + for i in range(2 * d): + V[i] = L[i] + [F(0), F(0)] + V[2 * d][2 * d] = F(1) + last = [F(0)] * n + last[0] = -(delta / 2) / delta ** 3 + last[d] = -(delta / 2) / delta ** 3 + last[2 * d] = -1 / delta ** 3 + last[2 * d + 1] = 1 / delta ** 3 + V[2 * d + 1] = last + ok_height &= abs(det(V)) == delta ** (-(d + 3)) + # dy' = delta^3 dt: the height-divided frame reduces to the gradient-only density power + ok_consistent &= abs(det(V)) * delta ** 3 == delta ** (-d) + out["gradient_only_frame_det_is_delta_minus_d"] = ok_grad + out["height_divided_frame_det_is_delta_minus_d_minus_3"] = ok_height + out["frames_agree_after_dy_prime_equals_delta3_dt"] = ok_consistent + ok_fixed = ok_blow = True + for d in range(2, 11): + g_power = -(d + 3) if MUT == "height-jacobian" else -d + ok_fixed &= (d - 1) + g_power + 2 == 1 # (I16) + ok_blow &= (d - 1) - (d + 3) + 3 + 2 == 1 # RP ledger, unchanged + out["fixed_r_radial_power_is_one_all_d"] = ok_fixed + out["blow_up_radial_power_is_one_all_d"] = ok_blow + # r-power of J_r: (I18) window dh = k r^3 dtheta, and W_r / Z_r ~ r^2 / r^2 -> 3. + # Iterated-limit route: j_r(r s) r ds = r^5 A_0 g_S(s) ds and g_S(s) ~ (J_0/A_0) s -> j_r(delta) ~ r^(5-1-1) J_0 delta. + out["J_r_is_order_r_cubed_by_both_routes"] = (3 + 2 - 2 == 3) and (5 - 1 - 1 == 3) + return out + + +def check_envelope(): + out = {} + # (I9)/(I10): for fixed s, z the t-window has length exactly k/s^3; the z-overlap is (k - s^3|t|)_+ (RP (R9)). + rng = random.Random(128001) + ok_len = ok_overlap = True + for _ in range(300): + k = F(rng.randint(1, 30), rng.randint(1, 7)) + s = F(rng.randint(1, 20), rng.randint(1, 7)) + z = k * F(rng.randint(1, 99), 100) + t = F(rng.randint(-50, 50), rng.randint(1, 7)) + ok_len &= z / s ** 3 - (z - k) / s ** 3 == k / s ** 3 + lo, hi = max(F(0), s ** 3 * t), min(k, k + s ** 3 * t) + ok_overlap &= max(F(0), hi - lo) == max(F(0), k - s ** 3 * abs(t)) + out["t_window_length_is_k_over_s_cubed"] = ok_len + out["z_overlap_is_k_minus_s3_abs_t"] = ok_overlap + # With the weight s^p the envelope is s^(p+1) near 0 and s^(p-2) near infinity. On shells [lam^-(n+1), lam^-n] + # (resp. [lam^n, lam^(n+1)]) with lam = 2^q, q = den(p), the shell integrals form exact geometric series with + # ratios 2^(-q(p+2)) (resp. 2^(q(p-1))); a series converges iff its ratio is < 1. + def finite(p): + q = p.denominator + near_ratio = ipow(2, -int(q * (p + 2))) + far_ratio = ipow(2, int(q * (p - 1))) + if MUT == "envelope-endpoint": + return near_ratio <= 1 and far_ratio <= 1 + return near_ratio < 1 and far_ratio < 1 + inside = [F(-7, 4), F(-3, 2), F(-1), F(-1, 3), F(0), F(1, 2), F(5, 6)] + outside = [F(-3), F(-2), F(1), F(3, 2), F(2)] + out["envelope_finite_exactly_on_minus2_lt_p_lt_1"] = (all(finite(p) for p in inside) + and not any(finite(p) for p in outside)) + # Endpoint shells are not summable: at p = -2 each shell of s^-1 contributes >= 1/2 (min 2^n, width 2^-(n+1)), + # and at p = 1 each far shell of s^-1 contributes >= 1/2 (min 2^-(n+1), width 2^n). + near = sum(ipow(2, n) * ipow(2, -(n + 1)) for n in range(40)) + far = sum(ipow(2, -(n + 1)) * ipow(2, n) for n in range(40)) + out["endpoint_shell_sums_grow_linearly"] = near == 20 and far == 20 + return out + + +def check_overlap(): + out = {} + ok = True + for p in (F(-7, 4), F(-3, 2), F(-1), F(-1, 2), F(-1, 3), F(0), F(1, 3), F(1, 2), F(3, 4)): + q = p.denominator + for base in (2, 3): + for tt in (F(1), F(2, 5), F(7, 3)): + m = F(base) ** q # s_max = (k/|t|)^(1/3) = m, so k = m^3 |t| + k = m ** 3 * tt + m_p2 = F(base) ** int(q * (p + 2)) # m^(p+2), exact since q(p+2) is an integer + m_p5 = m_p2 * m ** 3 + lhs = k * m_p2 / (p + 2) - tt * m_p5 / (p + 5) + num = 1 if MUT == "overlap-three" else 3 + # 3 k^((p+5)/3) |t|^(-(p+2)/3) / ((p+2)(p+5)) = 3 k (k/|t|)^((p+2)/3) / (...) = 3 k m^(p+2) / (...) + rhs = num * k * m_p2 / ((p + 2) * (p + 5)) + ok &= lhs == rhs + out["I11_overlap_integral_exact_negative_and_positive_p"] = ok + out["I11_at_p0_is_R10_three_tenths"] = F(3) / (F(2) * F(5)) == F(3, 10) + out["T_exponent_in_1_2_on_domain"] = all(1 < (4 - p) / 3 < 2 for p in (F(-199, 100), F(-1), F(0), F(99, 100))) + return out + + +def check_coeff(): + out = {} + ps = (F(-7, 4), F(-1), F(-1, 2), F(0), F(1, 2), F(9, 10)) + # 36 t^2 times the numerator 3 of (I11) is 108; 12^((p+2)/3) * 12^((4-p)/3) = 12^2, so + # 108 * 12^(-(4-p)/3) = (3/4) 12^((p+2)/3) <=> 108 = (3/4) * 144. + out["I8_constant_108_equals_three_quarters_144"] = (36 * 3 == 108 and F(3, 4) * 144 == 108 + and all((p + 2) / 3 + (4 - p) / 3 == 2 for p in ps)) + # p = 0: 3 / (4 (p+2)(p+5)) = 3/40, the RP (R3) all-index constant. + out["I8_at_p0_reduces_to_R3_three_fortieths"] = F(3) / (4 * 2 * 5) == F(3, 40) + # Normalization of (I20): 36 * (3/10) = 54/5 = (3/40) 12^(2/3) 12^(4/3) = (3/40) * 144. + out["I20_normalizes_to_one"] = 36 * F(3, 10) == F(54, 5) == F(3, 40) * 144 + # Tonelli: A_0 int s^p g_S ds = (36/z0) int t^2 Psi * 3 k^((p+5)/3) |t|^(-(p+2)/3)/((p+2)(p+5)); (I8) after + # t = -T/12 gives (3/4) 12^((p+2)/3) 12^((4-p)/3) / ((p+2)(p+5)) = 108/((p+2)(p+5)); both prefactors agree. + out["A_p_equals_A_0_times_S_moment"] = all(F(36 * 3) / ((p + 2) * (p + 5)) == F(3, 4) * 144 / ((p + 2) * (p + 5)) + for p in ps) + # (I21): J_0 = (k/(4 z0)) * 144 int t^2 Psi (T^2 = 144 t^2), slope of g_S = (36 k/(z0 A0)) int t^2 Psi. + quarter = F(1, 2) if MUT == "contact-quarter" else F(1, 4) + out["I21_slope_equals_J0_over_A0"] = quarter * 144 == 36 + # Abelian cross-check: (p+2) A_p -> J_0 as p decreases to -2. Rational prefactor of (p+2) A_p is + # 3 / (4 (p+5)) -> 3/(4*3) = 1/4 = (I19) prefactor; k-power (p+5)/3 -> 1; T-power (4-p)/3 -> 2. + seq = [F(-2) + F(1, 10 ** n) for n in range(1, 8)] + pref = [F(3) / (4 * (p + 5)) for p in seq] + converging = all(abs(pref[i + 1] - quarter) < abs(pref[i] - quarter) for i in range(len(pref) - 1)) + out["abelian_limit_of_I8_matches_I19"] = (converging and F(3) / (4 * 3) == quarter + and (F(-2) + 5) / 3 == 1 and (4 - F(-2)) / 3 == 2) + return out + + +def pair_field(T, A, c, delta): + """f(u, v) = (T/6)u^3 - (T/4)delta u^2 + (1/2) v^T A v + (u^2 - delta u) c.v on R x R^(d-1).""" + n = len(A) + + def hess(u): + Huu = T * u - T * delta / 2 + Huv = [(2 * u - delta) * ci for ci in c] + return [[Huu] + Huv] + [[Huv[i]] + list(A[i]) for i in range(n)] + + def grad(u): + return [T / 2 * u * u - T / 2 * delta * u] + [(u * u - delta * u) * ci for ci in c] + + def value(u): + gap = T * u ** 3 / 6 - T * delta * u * u / 4 + return gap + + return hess, grad, value + + +def adj_quadratic(A, c): + """c^T adj(A) c = det(A) - det(A - c c^T) (matrix determinant lemma, exact).""" + n = len(A) + return det(A) - det([[A[i][j] - c[i] * c[j] for j in range(n)] for i in range(n)]) + + +def check_pair(): + rng = random.Random(128002) + ok_crit = ok_product = ok_segment = ok_hadamard = ok_gap = ok_merge = True + for d in (2, 3, 4): + n = d - 1 + for trial in range(10): + A = [[F(0)] * n for _ in range(n)] + for i in range(n): + A[i][i] = F((-1) ** (i + trial) * (i + 2)) + for j in range(i): + A[i][j] = A[j][i] = F(rng.randint(-2, 2), 10) + c = [F(rng.randint(-9, 9), 7) for _ in range(n)] + T = F(rng.choice([-1, 1]) * rng.randint(1, 20), 3) + D, q = det(A), adj_quadratic(A, c) + for delta in (F(1, 10), F(1, 100), F(1, 1000)): + hess, grad, value = pair_field(T, A, c, delta) + Hx, Hy = hess(F(0)), hess(delta) + ok_crit &= all(v == 0 for v in grad(F(0)) + grad(delta)) + # exact: det H_x det H_x' = -delta^2 [(T^2/4) D^2 - delta^2 q^2] + prod = det(Hx) * det(Hy) + ok_product &= prod == -delta ** 2 * (T * T / 4 * D * D - delta ** 2 * q * q) + # segment identity: H_x e = (-T delta/2, -delta c) and D^3 f has entries T, 2 c_j + He = [row[0] for row in Hx] + d3 = max([abs(T)] + [abs(2 * ci) for ci in c]) + ok_segment &= max(abs(v) for v in He) == delta / 2 * d3 + for H in (Hx, Hy): + col = [row[0] for row in H] + frob = sum(x * x for row in H for x in row) + ok_hadamard &= det(H) ** 2 <= sum(x * x for x in col) * frob ** (d - 1) + gap = value(delta) - value(F(0)) + expected = -T * delta ** (2 if MUT == "merge-rate" else 3) / 12 + ok_gap &= gap == expected + # two windows: {y in (a, b): y + gap not in (a, b)} has measure min(|gap|, b - a) + a, b = F(-1, 3), F(2, 5) + lo, hi = max(a, a - gap), min(b, b - gap) + kept = max(F(0), hi - lo) + ok_merge &= (b - a) - kept == min(abs(gap), b - a) + # (I14) limit with O(delta^2) error: |prod|/delta^2 - (T^2/4) D^2 = -delta^2 q^2 when delta is small. + T, A, c = F(7, 3), [[F(2), F(1, 10)], [F(1, 10), F(-3)]], [F(4, 7), F(-1, 7)] + D, q = det(A), adj_quadratic(A, c) + errs = [] + for delta in (F(1, 10), F(1, 100), F(1, 1000)): + hess, _, _ = pair_field(T, A, c, delta) + errs.append(abs(det(hess(F(0))) * det(hess(delta))) / delta ** 2 - T * T / 4 * D * D) + ok_limit = all(e == -(dl ** 2) * q * q for e, dl in zip(errs, (F(1, 10), F(1, 100), F(1, 1000)))) + # Same-index control (RP): T = 0 with a mixed cubic gives a determinant product of order delta^4, so the + # delta^2 coefficient that makes J_r > 0 comes only from adjacent-index pairs of the all-index sum. + ok_same = True + for lam, cc in ((F(3), F(2)), (F(-5, 2), F(1, 3))): + for delta in (F(1, 10), F(1, 100)): + H0 = [[F(0), -cc * delta], [-cc * delta, lam]] + H1 = [[F(0), cc * delta], [cc * delta, lam]] + ok_same &= det(H0) * det(H1) == (cc * delta) ** 4 + return {"pair_fields_have_both_critical_points": ok_crit, + "determinant_product_exact_identity": ok_product, + "I14_limit_with_order_delta_squared_error": ok_limit, + "segment_bound_He_le_half_delta_D3": ok_segment, + "det_squared_le_He_squared_times_frobenius": ok_hadamard, + "height_gap_is_minus_T_delta_cubed_over_12": ok_gap, + "two_windows_differ_on_measure_abs_gap": ok_merge, + "same_index_product_is_order_delta_four": ok_same} + + +# ---- distinct-jet rank over Q ----------------------------------------------------------------------------------- + +def monomials(d, D): + return [a for k in range(D + 1) for a in itertools.product(range(k + 1), repeat=d) if sum(a) == k] + + +def derivative_of_monomial(alpha, directions, point): + """Apply d_{v_1} ... d_{v_m} to x^alpha and evaluate at point, exactly.""" + poly = {tuple(alpha): F(1)} + for v in directions: + new = {} + for exps, coef in poly.items(): + for i, vi in enumerate(v): + if vi == 0 or exps[i] == 0: + continue + e2 = list(exps) + e2[i] -= 1 + key = tuple(e2) + new[key] = new.get(key, F(0)) + coef * exps[i] * vi + poly = new + total = F(0) + for exps, coef in poly.items(): + term = coef + for xi, k in zip(point, exps): + term *= F(xi) ** k + total += term + return total + + +def functional_rows(funcs, d, D): + mons = monomials(d, D) + return [[derivative_of_monomial(a, dirs, pt) for a in mons] for pt, dirs in funcs] + + +def jet_lists(d, delta): + basis = [tuple(F(int(i == j)) for j in range(d)) for i in range(d)] + if d == 2: + e, perp = (F(3, 5), F(4, 5)), [(F(-4, 5), F(3, 5))] + x = (F(3, 2), F(1, 3)) + else: + e = (F(1, 3), F(2, 3), F(2, 3)) + perp = [(F(2, 3), F(1, 3), F(-2, 3)), (F(2, 3), F(-2, 3), F(1, 3))] + x = (F(3, 2), F(1, 3), F(-2, 5)) + r = F(1, 5) + M = tuple(-r / 2 * u for u in basis[0]) + S = tuple(r / 2 * u for u in basis[0]) + xp = tuple(xi + delta * ei for xi, ei in zip(x, e)) + pins = [(M, []), (S, [])] + [(P, [b]) for P in (M, S) for b in basis] + grad_x = [(x, [b]) for b in basis] + hess_pairs = [(basis[i], basis[j]) for i in range(d) for j in range(i, d)] + return dict(e=e, perp=perp, x=x, M=M, S=S, xp=xp, pins=pins, grad_x=grad_x, hess_pairs=hess_pairs, basis=basis) + + +def check_rank(): + out = {} + ok_zero = ok_pos = ok_neg = True + for d, D in ((2, 7), (3, 6)): + J = jet_lists(d, F(0)) + He = [(J["x"], [J["e"], b]) for b in J["basis"]] + if MUT == "jet-duplicate": + He = [(J["xp"], [b]) for b in J["basis"]] # grad f(x + 0 e) in place of H_x e + A = [(J["x"], [J["perp"][i], J["perp"][j]]) for i in range(d - 1) for j in range(i, d - 1)] + T = [(J["x"], [J["e"]] * 3)] + val = [(J["x"], [])] + HM = [(J["M"], list(p)) for p in J["hess_pairs"]] + HS = [(J["S"], list(p)) for p in J["hess_pairs"]] + # (I15) positivity list at delta = 0: pins, G_0 = (grad f(x), H_x e), A, T, f(x), H_M, H_S + funcs = J["pins"] + J["grad_x"] + He + A + T + val + HM + HS + expected = 2 * (d + 1) + d + d + (d - 1) * d // 2 + 1 + 1 + d * (d + 1) + ok_zero &= len(funcs) == expected and rank(functional_rows(funcs, d, D)) == expected + # delta > 0: pins, grad f(x), grad f(x + delta e), f(x) (G_delta is an invertible transform of these) + for delta in (F(1, 7), F(2, 3)): + Jd = jet_lists(d, delta) + funcs_d = Jd["pins"] + Jd["grad_x"] + [(Jd["xp"], [b]) for b in Jd["basis"]] + [(Jd["x"], [])] + ok_pos &= rank(functional_rows(funcs_d, d, D)) == 2 * (d + 1) + 2 * d + 1 + # negative control: at delta = 0, grad f(x + 0 e) duplicates grad f(x); rank drops by exactly d + dup = J["pins"] + J["grad_x"] + [(J["xp"], [b]) for b in J["basis"]] + ok_neg &= rank(functional_rows(dup, d, D)) == 2 * (d + 1) + d + out["delta0_positivity_list_full_rank_d2_d3"] = ok_zero + out["delta_positive_frame_full_rank_d2_d3"] = ok_pos + out["undivided_gradient_frame_degenerates_at_delta0"] = ok_neg + return out + + +def check_cutoff(): + out = {} + J, a, d0 = F(5, 2), F(-3, 4), F(1, 2) + # j(delta) = delta (J + a delta); I_q(eps) = int_eps^d0 delta^-q j(delta) d delta + ok = True + for n in range(2, 9): + eps = F(1, 10 ** n) + I3 = J * (1 / eps - 1 / d0) + a * (d0 - eps) # q = 3 + I4 = J * (1 / eps ** 2 - 1 / d0 ** 2) / 2 + a * (1 / eps - 1 / d0) # q = 4 + ok &= abs(I3 / (J / eps) - 1) <= 4 * eps + ok &= abs(I4 / (J / (2 * eps ** 2)) - 1) <= 4 * eps + out["q3_q4_leading_terms_J_eps_power_over_q_minus_2"] = ok + # q = 2: I_2 = J log(d0/eps) + a (d0 - eps); the rational remainder is bounded, so I_2 ~ J log(d0/eps). + out["q2_log_with_bounded_remainder"] = all(abs(a * (d0 - F(1, 10 ** n))) <= abs(a) * d0 for n in range(2, 9)) + # (I6): P(S <= eps) = int_0^eps (J0/A0) s (1 + b s) ds ~ (J0/(2 A0)) eps^2 + J0, A0, b = F(7), F(3), F(11, 5) + half = F(1) if MUT == "cdf-half" else F(1, 2) + ok = True + for n in range(2, 9): + eps = F(1, 10 ** n) + cdf = J0 / A0 * (eps ** 2 / 2 + b * eps ** 3 / 3) + ok &= abs(cdf / (half * J0 / A0 * eps ** 2) - 1) <= 2 * b * eps + out["small_cdf_has_factor_one_half"] = ok + return out + + +def check_scope(): + out = {} + J0 = F(3) + h = lambda u: u / (1 + u * u) + ok_fixed_r = ok_fixed_s = True + for rn in (1, 2): + r = F(1, 10 ** rn) + # fixed r, delta -> 0: u = delta / r^10 -> 0 and 0 <= h(u) <= u + for m in range(1, 6): + delta = r ** 10 * F(1, 10 ** m) + u = delta / r ** 10 + ok_fixed_r &= 0 <= h(u) <= u + # fixed s, delta = r s: u = s r^-9 -> infinity and 0 <= h(u) <= 1/u + for s in (F(1, 2), F(1), F(3)): + u = r * s / r ** 10 + ok_fixed_s &= 0 <= h(u) <= 1 / u + out["iterated_limits_both_J0_but_coupled_cutoff_sees_J0_plus_half"] = (ok_fixed_r and ok_fixed_s + and J0 + h(F(1)) == J0 + F(1, 2)) + # TV alone does not move unbounded inverse moments: mu_n = (1 - 1/n) mu + (1/n) delta_{n^-2} has TV <= 1/n, + # but the added q = 1 inverse moment is (1/n) n^2 = n. + out["tv_convergence_does_not_control_inverse_moments"] = all( + F(1, n) <= F(1, 10) and F(1, n) * F(n) ** 2 == n for n in (10, 100, 1000)) + return out + + +def flatten(d): + for v in d.values(): + if isinstance(v, dict): + yield from flatten(v) + else: + yield v + + +def main(): + global MUT + ap = argparse.ArgumentParser() + ap.add_argument("--mutant", choices=MUTANTS) + MUT = ap.parse_args().mutant + checks = {"LEDGER": check_ledger(), "ENVELOPE": check_envelope(), "OVERLAP": check_overlap(), + "COEFF": check_coeff(), "PAIR": check_pair(), "RANK": check_rank(), "CUTOFF": check_cutoff(), + "SCOPE": check_scope()} + passed = all(flatten(checks)) + print(json.dumps({"object": "CLAUDE-REVIEW-REMOTE-INVERSE-SEPARATION-20260929-v1", "checks": checks, + "passed": passed, "scope": "exact finite identities only; not an analytic proof"}, + indent=2, sort_keys=True)) + return 0 if passed else 1 + + +if __name__ == "__main__": + sys.exit(main())