diff --git a/.github/workflows/elder-dimension-lift-review.yml b/.github/workflows/elder-dimension-lift-review.yml new file mode 100644 index 000000000..6a708cba4 --- /dev/null +++ b/.github/workflows/elder-dimension-lift-review.yml @@ -0,0 +1,61 @@ +name: Elder dimension-lift nonauthor review checks + +'on': + pull_request: + paths: + - 'reviews/elder_dimension_lift_claude_20260928/**' + - '.github/workflows/elder-dimension-lift-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/elder_dimension_lift_claude_20260928').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 / 'dimension_lift_review_check.py') + expected = (root / 'RESULTS.json').read_bytes() + mutants = ['raw-a-in-plane', 'shear-sign', 'drop-transverse-pin-term', + 'no-cross-schur', 'planar-point-is-critical', 'stable-scale-r', + 'density-dr', 'threshold-two-thirds', 'weight-2d'] + 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/elder-dimension-lift.yml b/.github/workflows/elder-dimension-lift.yml new file mode 100644 index 000000000..fcb467a25 --- /dev/null +++ b/.github/workflows/elder-dimension-lift.yml @@ -0,0 +1,33 @@ +name: Elder dimension-lift exact controls + +'on': + pull_request: + paths: + - 'frontiers/elder_dimension_lift_20260928/**' + - '.github/workflows/elder-dimension-lift.yml' + push: + branches: [main] + paths: + - 'frontiers/elder_dimension_lift_20260928/**' + - '.github/workflows/elder-dimension-lift.yml' + workflow_dispatch: + +permissions: + contents: read + +jobs: + finite-dimension-lift: + 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: Exact sources, both modes and intended semantic failures + run: | + set -euo pipefail + python -B -S frontiers/elder_dimension_lift_20260928/verify.py --output "${RUNNER_TEMP}/dimension-lift-${GITHUB_RUN_ID}-${GITHUB_RUN_ATTEMPT}" + git diff --exit-code diff --git a/.github/workflows/remote-pair-law-review.yml b/.github/workflows/remote-pair-law-review.yml new file mode 100644 index 000000000..9a4c5c2d9 --- /dev/null +++ b/.github/workflows/remote-pair-law-review.yml @@ -0,0 +1,60 @@ +name: Remote pair-law nonauthor review checks + +'on': + pull_request: + paths: + - 'reviews/remote_pair_law_claude_20260928/**' + - '.github/workflows/remote-pair-law-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_pair_law_claude_20260928').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 / 'remote_pair_review_check.py') + expected = (root / 'RESULTS.json').read_bytes() + mutants = ['exponent-d', 'chi-orientation', 'coefficient-power', 'beta-normalizer', + 'overlap-exponent'] + 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/docs/integration/2026-09-29-reviewed-dimension-and-pair.md b/docs/integration/2026-09-29-reviewed-dimension-and-pair.md new file mode 100644 index 000000000..4c42d40f9 --- /dev/null +++ b/docs/integration/2026-09-29-reviewed-dimension-and-pair.md @@ -0,0 +1,85 @@ +# Reviewed dimensional lower and remote pair source integration + +Date: 2026-09-29 UTC (2026-09-28 research cycle). +Integrator: OpenAI / ChatGPT. Scientific effect: NONE for this additive integration. +This is a one-time source-custody receipt, not a second status register. + +## Exact included sources and reviews + +The current base is `82247833b5dd58e04291d55353b52938d73ec614`, the separately +completed D1 scoped reconciliation from Math-#126. That reconciliation and its +mandatory reading-rule components remain unchanged. + +- Math-#125: full `frontiers/elder_dimension_lift_20260928/` packet from + `e3f10b390ae5ddd998d238206add5958d5b720bb`, tree + `079961c04cb0bf2dbeeb81b880133f6488de5b9e`, plus its unchanged workflow. + PROOF.md: 23971 bytes, blob `7303bd791a68a1139251f0f6e403a9f7cc89b006`, + SHA256 `b529fe3780e1909014b3cb144b9a74156d976bbdc19b6711d0c5b1a1da9e5669`. +- Math-#127: both complete Anthropic review packets and workflows from + `a18bd244b132df3b512c60636bc4af5514b2522f`. The correction from `32bec6a...` + changes only two review texts and their manifests, not the check programs, + stored results or scoped verdicts. OpenAI integration review 5346156960 + confirms the requested clarification is present. +- Math-#116 C3 ONLY: `frontiers/window_multiplicity_laws_20260928/REMOTE_PAIR_LAW.md` + copied verbatim from `0507e3a1dbd3dede84cbeb805947c70aa16ebc36`. + It is 15878 bytes, blob `3fb602040b37158b16ba61bdfc62cc8df1ccc616`, + SHA256 `b818a11f1abcf37616d592ecda6341b0d99365cf3ac5047bc2dbaede95da4c5e`. + +The #125 source head and amended #127 review head are integration ancestors. +The #116 head is deliberately NOT an ancestor. Its already imported C1/C2 +modules and source map remain intact; only C3 is newly imported. The partial +directory does not claim to be the original complete executable packet. + +## Mathematical scope retained + +The dimensional direct lower event is reviewed at each FIXED dimension d>=2, +fixed torus and compact birth/positive-gap ranges: 1-p_r>=c r^3 under the original +full determinant tilt and ordinary elder selector. Two extra index-(d-1) window +points give a multiple-occurrence and factorial LOWER bound. N_r can be the +torus-wide additional count; the event also supplies the same lower bound for +the deterministic C_d r ball. No higher-dimensional global first-moment upper +bound or conditional nonuniqueness lower constant is inferred. + +The two-sided selection order, compact-mark density loss and rejected-pair +inverse-lifetime boundary p<5/3 are separately sourced compositions with LP's +reconciled upper/density inputs. Positive-length mark windows are required for +positive integrated coefficients. No numerical constant/cutoff, uniform-in-d +estimate or unrestricted-mark difference is introduced. + +C3's reviewed claim is the fixed-remote, fixed-positive-volume Borel-region +ordered factorial-pair mean r^5 coefficient, positive precisely for adjacent +indices, and its factorial-weighted height-gap Beta(2/3,2) limit. This is not +an event-conditioned pair law or a persistence-lifetime distribution. The full +endpoint-only normalizer comes from RM; the endpoint weight limit under EXTRA +pair conditioning uses RP's coupled moments and RM's deterministic pin identities. +The unconditioned D1 normalizer theorem alone is not that extra-conditioned argument. + +The reviewer discloses authorship of RC and the D1 reconciliation, as well as +prior reviews of the planar inputs. Source-distinct review is not additional +independence for a reviewer's own imported theorem, and the shared GitHub account +is not organizational independence. OpenAI's check of these review records is +source-exposed integration work, not another nonauthor-provider discharge. + +## Verification and exclusions + +The unchanged #125 author packet was freshly replayed locally in this session: +18 tests and 10 intended semantic mutants in EACH normal/optimized mode, all +paired outputs identical, exact source membership/identities preserved. The two +reviewer programs were read through their review records but were NOT executed +locally by this integrator. Their combined hosted execution must be inspected +alongside the author workflow and required downstream/formal aggregate before +merging. The current-run check/receipt and any subsequent postmerge observations +are recorded in the integration PR, not fabricated prospectively here. + +Floating numerical roots and finitely many quartic ratios in the dimensional +review are illustrations only. The written uniform Taylor and inverse-function +argument supplies existence and order. Reviewer return-code mutation controls +are not described as the author's stronger parsed-predicate guards. The existing +Lean scalar package is not formalization of all these Gaussian proofs. + +#116 remains open for its remaining unreviewed modules, including C4's positive +separation-moment transition. #128's new inverse-separation candidate is NOT +included and obtains no acceptance from this integration. The original #116 +blocked executable is neither recovered nor retried. No old proof is edited, +no scientific-status/graph/lemma/prize change is made, and no stopped agent or +timer is restarted. Any later status reconciliation is a separate reviewed act. diff --git a/frontiers/elder_dimension_lift_20260928/PROOF.md b/frontiers/elder_dimension_lift_20260928/PROOF.md new file mode 100644 index 000000000..7303bd791 --- /dev/null +++ b/frontiers/elder_dimension_lift_20260928/PROOF.md @@ -0,0 +1,480 @@ +# One soft transverse direction: an elder-failure lower event in every fixed dimension + +Object: OA-ELDER-DIMENSION-LIFT-20260928-v1. +Author: OpenAI / ChatGPT, foreground research continuation, 28 September 2026. +Disposition: AUTHOR-SIDE MATHEMATICAL CANDIDATE; source-bound nonauthor review required. +Scientific effect NONE. No existing proof, review verdict, registry, lemma flag or prize is changed. + +## 1. Model, precise claims, and dependence boundaries + +Fix d>=2, L>0, a compact birth interval B, and a compact gap interval +K=[k_-,k_+] with k_->0. Use exactly LP's variance-one periodized Gaussian field, + + Cov(f(x),f(y)) = sum_{n in Z^d} exp(-|x-y+Ln|^2/2) + / sum_{n in Z^d} exp(-|Ln|^2/2). + +All constants may depend on d,L,B,K. The dimension is fixed: no uniform-in-d +claim is made. All orthonormal pin frames R are allowed, without assuming the +periodized field is invariant under arbitrary rotations. Set u=R e_1 and + + M=-(r/2)u, S=(r/2)u; + f(M)=b, f(S)=b-k r^3, grad f(M)=grad f(S)=0. + +Q_r denotes continuous Gaussian regression on these original 2(d+1) observations. +Let F_j(H)=|det H| for a nonsingular Hessian with j negative eigenvalues, and zero +otherwise. Retain the ORIGINAL determinant tilt and FULL endpoint normalizer: + + W_r=F_d(H_M) F_(d-1)(H_S), Z_r=E_Qr W_r, + dQ_r^W=(W_r/Z_r)dQ_r. + +There is no adjacency conditioning. Let p_r(b,k,R) be the probability that S is +M's global ordinary superlevel elder-death partner, exactly as in LP Section 1. +On its generic locus the death height is the maximin from LP Section 8: + + d_f(M)=sup_{gamma(0)=M, f(gamma(1))>b} min_t f(gamma(t)). (A1) + +The already integrated planar source EL proves an explicit path obstruction in +d=2. This note extends that mechanism to all fixed d. The new issue is the raw +Gaussian mass of a nearly flat transverse direction coupled to d-2 stable +negative directions. Requiring every extra matrix entry to be O(r) would lose +the desired probability power. A Schur-complement coordinate chart avoids that. + +**Theorem A (direct lower event).** For all sufficiently small r, uniformly over +b,k,R in the specified ranges, there is an event E_r such that + + Q_r^W(E_r)>=c r^3, + E_r implies d_f(M)>=b-k r^3/4>f(S). (A2) + +In particular + + 1-p_r(b,k,R)>=c r^3. (A3) + +The event can be chosen also to contain two distinct additional critical points +of index d-1 and heights strictly between b-k r^3 and b, within distance C_d r +of the midpoint. If N_r counts all additional critical points in that height +window, then + + Q_r^W(N_r>=2)>=c r^3, + E_Qr^W[N_r(N_r-1)]>=c r^3. (A4) + +The second expectation may be extended-valued; this argument supplies no finite +upper bound. For d>2 it does NOT establish Q(N_r>=2)=Theta(r^3), a uniform lower +bound on Q(N_r>=2 | N_r>=1), or a global first-moment upper bound. Those would +need their own inputs. A torus-wide O(r^5) factorial bound is excluded by (A4). +The event lower bound is likewise an obstruction of order at least r^3 to any +approximation supported solely on empty and singleton configurations. + +**Corollary B (separate parent-dependent compositions).** Consuming LP Theorem A +at its stated scope gives, in every fixed d>=2, + + c r^3<=1-p_r<=C r^3. (A5) + +Consuming additionally LP's compact-mark density identity, for positive-length +B,K, gives + + nu_cand(ell)-nu_eld(ell)=Theta(ell^(2/3)) (A6) + +for its COMPACT-MARK densities. The leading constant, a numerical c or r_*, +unrestricted-mark differences, and any identification with historical q-symbols +remain outside this statement. The d=3,L=24 specialization changes none of those +limitations. The direct lower (A3) does not consume the parent upper theorem. + +**Corollary C (sharp rejected-pair inverse-moment boundary).** Under the same +compact-mark density premises, let the nonselected counting measure count +candidate pairs which are not ordinary elder pairs. Directly on that measure, + + E sum_{nonselected, 00. In the finite regime it is Theta(t^(5/3-p)). At +p=5/3 the lower-cutoff divergence is logarithmic; above it it is a power. This +is not subtraction of two infinite individual inverse-moment expectations. + +The proof below uses only the positive spectrum/contact-frame and uniform +regression facts explicitly displayed in LP Sections 2-4, elementary Taylor +estimates, a stable negative block, and the original maximin definition. It does +not consume the pending remote pair/distance limits or a SARD-G theorem. + +## 2. Complete physical third-order jets after the pin frame + +Write the orthonormal local coordinates as (x,y), with x axial and y in R^m, +m=d-1. LP's nonsingular frame U_r is an invertible re-expression of the exact pins +for r>0; it has bounded target v_r and converges, uniformly in covariance and +fixed derivative cross-covariances, to + + U_0=(f,f_x,f_xx,f_xxx,f_y1,f_xy1,...,f_ym,f_xym) at 0. (A7) + +Append the physical midpoint vector J consisting of: + +- all independent entries A=D_y^2 f(0) of the transverse Hessian; +- all independent third-order derivatives T_alpha=partial^alpha f(0), |alpha|=3, + except f_xxx (which is already in U_0). + +At r=0 the entries of (U_0,J) are exactly every independent derivative of orders +0 through 3, once each. Their count is binom(d+3,3). No repeated symmetric entries +are presented as independent coordinates. + +Every Fourier weight of the periodized covariance is positive. A zero-variance +linear combination of these derivatives would give a polynomial vanishing at +every point of the rotated dual lattice. Pulling back by the invertible rotation +gives a polynomial vanishing on Z^d. Induction on dimension, using the univariate +root theorem on each lattice line, makes it identically zero. Thus the complete +jet covariance is positive definite in every frame. + +Continuity of U_r and compactness of O(d) give a uniform covariance floor and +ceiling for (U_r,J), for r in [0,r_1]. Schur complementation then gives a uniform +covariance sandwich for the Gaussian vector J under Q_r. Its mean is bounded +because v_r is bounded. Consequently, for EVERY fixed compact set of physical +J-targets, there is a uniform positive lower bound on its Lebesgue density there. +This is a bound for RAW jets, not for a falsely Gaussian nonlinear eigenvector +or normalized-Schur variable. + +## 3. A unit-Jacobian chart around one soft transverse direction + +For d=2 use the planar argument, or interpret the empty stable block below with +determinant one. We now give the new construction for d>=3. Write y=(z,w), +w in R^n, n=d-2, and decompose + + A = [[a, v^T], [v, D]], + sigma=a-v^T D^(-1)v. (A8) + +Restrict D to a fixed positive-volume box of symmetric matrices near -I_n, with + + -3I_n/2 < D < -I_n/2. + +Restrict v to a sufficiently small fixed box of positive volume, independent of +r, such that q=D^(-1)v satisfies ||q||<=1/9. The possible physical jets remain +bounded on this domain. Use the deterministic linear shear, frozen separately +for each realization of these midpoint jets, + + y = S(z,w) = (z,w-qz), + S=[[1,0],[-q,I_n]], det S=1, + S^T A S=diag(sigma,D). (A9) + +The full coordinate transformation is L=diag(1,S) after the orthonormal pin +frame. Its determinant has absolute value one. It preserves the axis x and the +original pin points. Both L and its inverse have uniformly bounded norms. It is +not generally orthogonal, and no rotation-invariance argument is applied to it. + +Define tilde f(x,z,w)=f(R L(x,z,w)). Here R,L are CONSTANT in spatial variables +within each realization. Thus differentiating tilde f does not differentiate a +randomly varying frame. Its midpoint transverse mixed quadratic terms are zero +exactly, its stable Hessian is D, and its soft second derivative is sigma. + +Let tau be the third derivatives of tilde f, except tau_xxx. For fixed v,D the +map from the original third derivatives to tau is invertible. Explicitly + + partial_z(tilde f)= (partial_z-q.partial_w)f, + partial_w(tilde f)=partial_w f, partial_x(tilde f)=partial_x f. + +On symmetric third-derivative coordinates this substitution is triangular with +unit diagonal when ordered by z degree. The pure xxx coordinate is fixed and +uncoupled; deleting it leaves determinant one. This observation is about finite +coordinate transformations, not the law of the resulting random variables. + +The map + + (sigma,v,D,tau) -> (a,v,D,T), + a=sigma+v^T D^(-1)v (A10) + +therefore has absolute Jacobian one. Its derivative is block triangular: the +Hessian part has derivative one in sigma and identity in the other coordinates; +the cubic part has determinant one, although it depends on v,D. Only D is +inverted; the chart remains regular when A is singular at sigma=0. + +This is the step preventing a dimension-dependent loss. Neither v nor the other +n(n+1)/2 stable entries has a shrinking width. The raw entry a itself need NOT +be O(r): it follows the O(1) surface v^T D^(-1)v within an O(r) band. + +## 4. The raw rare set has volume and probability of order r + +Fix a small epsilon>0, eventually independent of r, and retain the fixed D,v +boxes. In the chart require + + |sigma+(3k/2)r|=c_J r. (A13) + +The sheared jets need not be jointly Gaussian. We integrate the RAW Gaussian +density using the explicitly justified Jacobian; we never assign an independent +or rotation-invariant distribution to sigma, v, D or tau. Replacing sigma by +sigma/r without its r Jacobian would be incorrect. + +## 5. Remainder control is conditioned after ALL the physical jets + +Regress the full smooth field on V=(U_r,J) at each target (v_r,j) in the raw set. +For one unconditioned copy F the conditional realization is + + F(z)+Cov(F(z),V)Cov(V)^(-1)((v_r,j)-V). (A14) + +The normalized pin rows are integral averages of derivatives of order at most +three. Positive-spectrum rapid Fourier summability supplies uniform derivative +cross-covariance bounds through C^4, and all finite C^4 supremum moments of F. +The joint inverse covariance from Section 2 is bounded. The targets j lie in a +fixed compact set. Therefore, for each fixed finite p, + + sup E[||f||_C4^p | U_r=v_r,J=j] < infinity. (A15) + +Choose K_4 finite so the conditional probability of ||f||_C4<=K_4 is at least +1/2 at EVERY target in the raw rare set. Integrating (A15) over that set yields + + Q_r{rare jets AND ||f||_C4<=K_4} >= (c_J/2)r. (A16) + +The bounded shear converts this to a uniform local bound on ||tilde f||_C4. +There is no assertion of independence between the jet event and the remainder. +Subtracting a fixed unconditioned tail from a mass of order r is not used. + +The constants can be selected without circularity. Fix the D,v boxes and a +compact raw-target container valid for all epsilon<=1 and small r. Choose a +uniform K_4 from that container. Then choose epsilon for the planar stability +margins, and finally reduce r_* using K_4 and those margins. The positive c_J +may shrink with epsilon, but is fixed independently of r. + +## 6. Exact pinned planar normal form on the sheared plane + +Restrict to w=0, and put + + F_r(X,Z)=[tilde f(rX,rZ,0)-b]/r^3, + s=sigma/r, a_3=tau_xxz, beta=tau_xzz, c_3=tau_zzz. + +The original axial height and gradient pins, including the transverse gradient +pins in the sheared direction, are still exact. Taylor expansion as in the +planar source gives + + F_r = 2kX^3-3kX/2-k/2+(s/2)Z^2 + +(a_3/2)(X^2-1/4)Z+(beta/2)XZ^2+(c_3/6)Z^3 + + O_C2(B3)(r K_4), (A17) + +with a dimension-dependent constant absorbing the shear norm. For clarity the +potentially dangerous coefficients follow from the pin identities: + + tilde f_xxx(0)=12k+O(rK_4), + tilde f_x(0)=-(r^2/8)tilde f_xxx(0)+O(r^3K_4), + tilde f_z(0)=-(r^2/8)tilde f_xxz(0)+O(r^3K_4), + tilde f_xx(0), tilde f_xz(0)=O(r^2K_4), + tilde f(0)-b=-(r^3/24)tilde f_xxx(0)+O(r^4K_4). + +The second-derivative z^2 coefficient is sigma, not the raw a. No stable +quadratic term survives on w=0 because (A9) eliminates it exactly. +The term -a_3 Z/8 is necessary for the transverse gradient pins. + +On (A11), the polynomial part is O(epsilon k)-close in C^2(B3) to + + G_k(X,Z)=k(2X^3-3X/2-1/2-3Z^2/4-XZ^2). (A18) + +Choose epsilon and then r_* so the C^0 difference is strictly below k/64 and the +C^2 difference meets the endpoint and saddle stability tolerances below. +The higher-dimensional directions have introduced no extra r^-1 remainder. + +## 7. Stable path above the death pin + +Use the fixed polygonal path in the sheared plane + + (-1/2,0) -> (-3/4,0) -> (-3/4,9/4) -> (-1,9/4). (A19) + +Dividing by k, the restrictions of G_k to its three consecutive segments are + + -3t^2/16-t^3/32, + -7/32, + -7/32+51t/64-9t^2/32-t^3/32, 0<=t<=1. + +Their minimum is -7/32 and the final value is 17/64. The first is nonincreasing; +the third has derivative at least 9/64. Every segment is inside B(0,3), since +the maximal endpoint squared norm is 97/16<9 and the ball is convex. +A perturbation below k/64 leaves the path above -15k/64>-k/4 and its endpoint +above k/4. After applying the fixed shear, rotation and physical r scaling, the +path starts at the actual M and ends at a point above b, entirely above +b-k r^3/4. It remains inside an embedded O(r) ball by reducing r_*. + +This is a path in the physical torus, not a separatrix claim. It proves the +second statement in (A2) for every field in the event of (A16). The use of a +plane chosen from midpoint jets causes no probabilistic problem: existence of +ONE such path suffices, and the chart is a smooth measurable function of those +jets on the chosen stable-block domain. + +## 8. Full endpoint Hessians: only two directions are soft + +In the (x,z;w) shear frame, the physical endpoint Hessians have blocks + + H_i^tilde = [[r P_i+O(r^2 K_4), C_i], [C_i^T,D_i]], + ||C_i||<=C r K_4, D_i=D+O(r K_4), (A20) + +where P_i is the Hessian of the polynomial in (A17) at the corresponding scaled +endpoint. To verify the cross-block bound, at the midpoint tilde f_zw=0 exactly +by the shear, and tilde f_xw=O(r^2K_4) by the zero endpoint w-gradients. Moving +to either endpoint changes these entries by O(rK_4). The stable block remains +uniformly negative with bounded inverse for small r. + +The exact Schur complement is + + K_i=r P_i+O(r^2 K_4)-C_i D_i^(-1) C_i^T, + K_i/r=P_i+O(r K_4+r K_4^2). (A21) + +The correction must be included. The fact that it is smaller than r, rather +than zero, is what makes the construction stable. The target two-dimensional +endpoint Hessians are diag(-6k,-k/2) and diag(6k,-5k/2), with determinants 3k^2 +and -15k^2. Uniform smallness of epsilon and r preserves their indices and +strict determinant floors after (A21). + +Block congruence gives inertia(H_i^tilde)=inertia(D_i)+inertia(K_i), and + + det H_i^tilde = det D_i det K_i. (A22) + +Hence the physical endpoints have precisely the required indices d and d-1, +and EACH determinant has magnitude at least c r^2. The d-2 stable eigenvalues +remain O(1), not O(r). Because the shear determinant has absolute value one, +physical and sheared Hessian determinants agree; general invertible congruence +preserves their inertia as well. Thus on the event + + W_r >= c_W r^4. (A23) + +The r^4 power is independent of fixed d. Replacing it by r^(2d) would correspond +to incorrectly shrinking every spatial direction's curvature. + +For the FULL normalizer, the original endpoint gradient pins give zero averages +of H u along the axial segment. Thus ||H_i u||<=C r ||f||_C3. Hadamard yields +|det H_i|<=C r (1+||f||_C3)^d, so + + Z_r <= C_Z r^2 (A24) + +by the endpoint-conditioned moment bounds of LP Section 4. The positive event +(A16),(A23) ensures Z_r>0. No restricted normalizer is used. Combining gives + + Q_r^W(E_r) >= (c_J c_W/(2C_Z)) r*r^4/r^2 = c r^3. (A25) + +Together with the path, this proves (A2)-(A3), in every fixed d>=3; EL covers +d=2. No parent upper selection theorem entered this argument. + +## 9. Two additional saddles with a stable negative complement + +A planar restriction critical point is NOT automatically a full-dimensional +critical point. We explicitly correct the stable coordinates. + +Near either planar saddle P_+ or P_- of G_k, with + + P_+/-=(-3/4,+/-sqrt(15/8)), G_k(P_+/-)=-7k/32, + det H_2 G_k(P_+/-)=-15k^2/2, + +write x=rX, z=rZ, w=r^2 W. Consider the rescaled FULL gradient map + + H_r(X,Z,W)=r^(-2) grad tilde f(rX,rZ,r^2W). (A26) + +On bounded (X,Z,W) sets, Taylor and the pin identities give in C^1 + + H_r = (grad P(X,Z), D W+Q(X,Z)) + O(r C(K_4)), (A27) + +where P is the two-dimensional polynomial in (A17), and the stable-vector +quadratic polynomial is + + Q_j(X,Z)=(tau_xxwj/2)(X^2-1/4) + +tau_xzwj XZ+(tau_zzwj/2) Z^2. (A28) + +In particular the -tau_xxwj/8 term comes from tilde f_wj(0), and is retained. +All its coefficients lie in fixed small boxes. The absence of an order-r +linear z term in the stable gradient uses tilde f_zw(0)=0 exactly. The two soft +gradient components have no O(1) dependence on W because their physical mixed +Hessian is O(r); varying w by r^2 W contributes only O(r) after /r^2. +The C^1 estimates require at most the uniform C^4 bound, not an assumed exact +cubic random field. + +For epsilon small, P has one nondegenerate saddle near each P_+/- by ordinary +C^2 stability. At such a point p, the limit vector map in (A27) has a zero at +(p,-D^(-1)Q(p)). Its derivative is block triangular with diagonal blocks H_2P(p) +and D, so its inverse is uniformly bounded over the compact jet boxes. These +zeros persist for the C^1-small perturbation (A27), uniformly after reducing r_*. +This can equivalently be obtained by a quantitative inverse-function argument +on fixed disjoint neighborhoods. The solutions have w=O(r^2); they are not +assumed to lie exactly in the w=0 plane. + +Their physical heights are b+r^3[G_k(P_+/-)+O(epsilon k)+O(r C(K_4))], strictly +inside the height window for small epsilon,r. Their full Hessian has a negative +stable block and a two-dimensional Schur complement with one negative and one +positive eigenvalue, just as in (A20)-(A22). Both therefore have index d-1. +Their physical positions lie in an O(r) ball and are distinct from each other +and the original pins. This proves the additional event in (A4); the factorial +inequality follows from N(N-1)>=2 on that event. + +Uniformity here is on the compact family of jets and stable blocks for a FIXED +d. It does not assert a uniform number of all critical points or the persistence +pairing of either extra saddle. The separate strict path gives the elder +obstruction; mere extra-point existence would not do so. + +## 10. Parent-dependent selection and density consequences + +LP Theorem A gives the opposite inequality 1-p_r<=C r^3. When consumed with +(A3), it proves (A5) and shows the Gaussian order r^3 is sharp at every fixed +d, not merely for the matrix relaxation or the planar model. + +For LP's ordered compact-mark candidate/elder densities, its exact radial ledger +is r A_r(b,k,u) dr db dk d sigma(u), with A_r uniformly positive and bounded, +and ell=k r^3. Consequently the density difference is + + ell^(-1/3)/3 * integral k^(-2/3) A_((ell/k)^(1/3))(b,k,u) + [1-p_((ell/k)^(1/3))(b,k,u)] d sigma dk db. + +The lower factor (A3) contributes ell/k. The upper factor is supplied separately +by LP Theorem A. Both bounding integrands are proportional to +ell^(2/3) k^(-5/3), integrable and of positive integral on positive-length compact +B,K and the ordinary sphere measure. This proves (A6). Integrating over +0-1, proving +(A6a). At p=5/3, truncation to eta5/3 it +gives Theta(eta^(5/3-p)) as eta decreases to zero for fixed small t. In the +finite regime the result is Theta(t^(5/3-p)), not a claimed leading constant. +The ordinary candidate and elder inverse-moment threshold 2/3 from LP Section 12 +is different. Here a rejected-pair measure is used, never infinity minus infinity. +For d=2 this is already a consequence of the integrated planar lower and LP; +for d>2 it additionally uses the new dimensional lower proof. + +For d>2 we do not import the PLANAR global first-moment estimate (IW I5) to +claim a global multiple-occurrence upper bound or conditional nonuniqueness +bounded away from zero. Only (A4) and the corresponding unconditioned TV lower +obstruction follow without another global upper input. This is intentionally +weaker than those extra planar conclusions in LOCAL_MULTIPLICITY.md. + +## 11. What is new, what is checked, and what remains for review + +The planar cubic, path and raw-jet conditioning mechanism are credited to the +unchanged EL/LOCAL sources. The new step is the full-dimensional raw Schur chart: +one shrinking scalar band, determinant-one data-dependent shear, all other +coordinates in fixed-volume boxes, and a stable negative complement. The +Gaussian law is never changed to an independently rotated or sheared ensemble. + +The exact suite checks nonorthogonal shear cancellation, the chart through a +singular contact Hessian, unit cubic-jet Jacobians, the complete nonduplicated +jet list, a finite polynomial-lattice unisolvence illustration, exact planar +pins, the path, full-dimensional Hessian determinants/inertia, the cross-block +Schur correction, stable-coordinate displacement scaling, and exponent ledgers. +It deliberately rejects replacing r by r^(d-1), r^4 by r^(2d), dropping the raw +band Jacobian, dropping transverse pin terms, and reversing the stable sign. + +Finite checks do NOT prove covariance floors, uniform conditional C^4 estimates, +uniform inverse-function neighborhoods or the Gaussian probability inequality. +Those arguments are the written Sections 2-9 and require an actual nonauthor +analytic review. The finite Fourier illustration is not substituted for positivity +of the infinite exact periodized spectrum. The code is a new shear/Schur module, +not recovery or a retry of the blocked author algebra.py from #116. + +Source identities, limited primary-source reconnaissance, and the precise role +of each parent are in SOURCE_MAP.json and RECONNAISSANCE.md. This candidate +changes no old source or canonical scientific status and claims no historical +priority. All constants and cutoffs in the Gaussian result remain existential. diff --git a/frontiers/elder_dimension_lift_20260928/README.md b/frontiers/elder_dimension_lift_20260928/README.md new file mode 100644 index 000000000..716c27595 --- /dev/null +++ b/frontiers/elder_dimension_lift_20260928/README.md @@ -0,0 +1,31 @@ +# Dimensional lift of the direct elder-failure lower event + +Author-side candidate; nonauthor analytic review required. Scientific effect NONE. + +[PROOF.md](PROOF.md) extends the original planar cubic/path mechanism to every +fixed d>=2 using a physical Hessian Schur chart and a determinant-one shear. +Only one raw scalar band has width O(r); stable transverse modes stay O(1). +The proposed direct result is 1-p_r>=c r^3 under the original full determinant +tilt. Two additional index-(d-1) window critical points persist after correcting +the stable coordinates by O(r^2). + +With separately named LP upper/density premises: the r^3 order and compact-mark +ell^(2/3) density loss are sharp in every fixed dimension. The rejected-pair +inverse-moment threshold is p<5/3; its endpoint divergence is logarithmic. +This does not assert any new all-height/global factorial upper bound, uniform-in-d +constant, numerical cutoff, unrestricted-mark difference or legacy q/p identity. + +Run the complete source/finite-control verification: + + python -B -S verify.py --output /path/to/new-output + python -B -O -S verify.py --output /path/to/other-new-output + +The output directory must be new and outside this source directory. Each runner +checks exact membership/bytes/SHA256/Git blob identities, executes both Python +modes, and requires every semantic negative to fail the intended assertion with +valid JSON and no execution errors. The 18 finite tests and 10 semantic mutants +are not proofs of the Gaussian uniformity or inverse-function arguments. + +[Source map](SOURCE_MAP.json) separates direct inputs from conditional corollary +inputs. [Reconnaissance](RECONNAISSANCE.md) records the limited literature read +and Consensus quota limitation. No frozen source or review is rewritten. diff --git a/frontiers/elder_dimension_lift_20260928/RECONNAISSANCE.md b/frontiers/elder_dimension_lift_20260928/RECONNAISSANCE.md new file mode 100644 index 000000000..dd56b21f2 --- /dev/null +++ b/frontiers/elder_dimension_lift_20260928/RECONNAISSANCE.md @@ -0,0 +1,35 @@ +# Limited primary-source reconnaissance — 28 September 2026 + +Scope: derivative geometry and critical-point correlations near collisions; +not a claim of novelty, first discovery, or an exhaustive priority audit. + +Consensus was called for Gaussian critical points, higher-dimensional Hessian +Schur complements and elder persistence. It returned its monthly 30-search quota +error with an October 1 reset. No result was invented or cited from that call. + +The following primary-source abstracts/publisher records were inspected with web +search. No external theorem is used as an unexamined replacement for this proof: + +1. Jean-Marc Azaïs and Céline Delmas, *Mean number and correlation function of + critical points of isotropic Gaussian fields and some results on GOE random + matrices*, arXiv:1911.02300; Stochastic Processes and their Applications 150 + (2022), 411-445, DOI 10.1016/j.spa.2022.04.013. + https://arxiv.org/abs/1911.02300 + This already studies adjacent-index short-range correlation effects in the + unconditioned isotropic setting. Such adjacency by itself is not a novelty + claim for this project. It does not by its abstract establish this exact + pair-conditioned full-tilt elder obstruction or its compact-window loss. +2. Louis Gass and Michele Stecconi, *The number of critical points of a Gaussian + field: finiteness of moments*, Probability Theory and Related Fields 190 + (2024), 1167-1197, DOI 10.1007/s00440-024-01273-5. + https://doi.org/10.1007/s00440-024-01273-5 + The record addresses finite moments under jet nondegeneracy. Its conclusions + are not automatically uniform at this coalescing conditioned pair, and no + global O(r^3) first moment or factorial upper bound is imported from it. + +The actual positive-spectrum, pin-frame and uniform-regression ingredients are +read from the exact LP source in SOURCE_MAP.json. The new construction is proved +thereafter with a raw physical-jet chart, not an assumed isotropic GOE law or +independent soft eigenvector. Schur complementation, congruence, Taylor bounds, +and nondegenerate-zero stability are classical; the proof writes out their role. +The generic peer-review and governing status boundaries remain separate. diff --git a/frontiers/elder_dimension_lift_20260928/RESULTS.json b/frontiers/elder_dimension_lift_20260928/RESULTS.json new file mode 100644 index 000000000..457fcb8bc --- /dev/null +++ b/frontiers/elder_dimension_lift_20260928/RESULTS.json @@ -0,0 +1,8 @@ +{ + "tests_per_mode": 18, + "semantic_mutants_per_mode": 10, + "identical_output_pairs": 11, + "all_intended_failures": true, + "scientific_effect": "NONE", + "gaussian_analysis_verified_by_code": false +} diff --git a/frontiers/elder_dimension_lift_20260928/SOURCE_FILES.json b/frontiers/elder_dimension_lift_20260928/SOURCE_FILES.json new file mode 100644 index 000000000..11a80bd6d --- /dev/null +++ b/frontiers/elder_dimension_lift_20260928/SOURCE_FILES.json @@ -0,0 +1,54 @@ +{ + "schema": 1, + "scientific_effect": "NONE", + "files": [ + { + "path": "PROOF.md", + "bytes": 23971, + "sha256": "b529fe3780e1909014b3cb144b9a74156d976bbdc19b6711d0c5b1a1da9e5669", + "git_blob": "7303bd791a68a1139251f0f6e403a9f7cc89b006" + }, + { + "path": "README.md", + "bytes": 1771, + "sha256": "64950f041cee272079f4dd5e04dcf2293f5ed6d8c3ee231df8817d2d10fce2ac", + "git_blob": "716c275954910521102d1e154ef526360f19d908" + }, + { + "path": "RECONNAISSANCE.md", + "bytes": 2214, + "sha256": "d6f0bb97f4555ebb44b06df5d35d12f90fb746bbef45fb2053b8294d6621ed28", + "git_blob": "dd56b21f2da20be803f431357c5de49e6efbf452" + }, + { + "path": "RESULTS.json", + "bytes": 205, + "sha256": "57dba071afd0e53e1317f165b5170dd0a69a456fef41d50b2f775d33ffd123f5", + "git_blob": "457fcb8bc2bcd84ad0b25c67be8869fefb9681b8" + }, + { + "path": "SOURCE_MAP.json", + "bytes": 2106, + "sha256": "8cdedee5300ecc64bc5e38ea94d9bf263f0d87c4b75ccba67fb108edcf7013b1", + "git_blob": "713cad893e3d922c971a866f9b6accd89758f6d1" + }, + { + "path": "lift.py", + "bytes": 5514, + "sha256": "e17fa8384b6d5e516223499efff26354da0d84de9ba3e9ea3d96cfe75373ee9d", + "git_blob": "03d6827ac66afeb04f70153108aa195668e58a22" + }, + { + "path": "test_lift.py", + "bytes": 6109, + "sha256": "6901d40a216db622ee6cf82dc2092cdd7cd7dae261ea81b2c00fbb72a6f4a02b", + "git_blob": "c3ff861519c6b522ad8ca049c2f1aebecebae623" + }, + { + "path": "verify.py", + "bytes": 4910, + "sha256": "f79ba38b27c40ec86b5d2bbec4f5c9891fbe27c62ba328b6d58769b6f04469dd", + "git_blob": "7bbd0612ebae56c8b05c97d22142f0086a3549cd" + } + ] +} diff --git a/frontiers/elder_dimension_lift_20260928/SOURCE_MAP.json b/frontiers/elder_dimension_lift_20260928/SOURCE_MAP.json new file mode 100644 index 000000000..713cad893 --- /dev/null +++ b/frontiers/elder_dimension_lift_20260928/SOURCE_MAP.json @@ -0,0 +1,42 @@ +{ + "scientific_effect": "NONE", + "source_repository": "d6g8k5htny-coder/Math-", + "source_commit": "d39dbbc25c25a7bc3f6c15b21f957a7fcac30615", + "inputs": [ + { + "id": "LP", + "path": "imports/lifetime_parent_20260925/UNIFORM_MATRIX_CAP_AND_LIFETIME.md", + "bytes": 40261, + "sha256": "9350ad6eaba6626b93c3dedeef9e2ff816e5cdf1c8318e85fb27499141c84bc7", + "git_blob": "dfed3b8d318a3ab1950957f393307733a4bef3f2", + "direct_use": "Exact model, original pins/tilt/selector, Sections 2-4 positive spectrum and contact regression; Section 8 generic locus/maximin.", + "conditional_corollary_use": "Theorem A upper bound and Sections 9-12 compact-mark density ledger/moments; not required for the new direct lower proof." + }, + { + "id": "EL", + "path": "frontiers/window_multiplicity_laws_20260928/ELDER_LOWER_AND_DENSITY_GAP.md", + "bytes": 10229, + "sha256": "8ce05a43bde8e0d718f09e2da1ffe75d3ec5893489254afdbf5b58b602cdba0c", + "git_blob": "aaefc8da9668e819591dd9db0b34442394f2362e", + "use": "Unchanged planar cubic/path and lower event; basis of d=2 and credited mechanism, not an assumed d>2 proof." + }, + { + "id": "LOCAL", + "path": "frontiers/window_multiplicity_laws_20260928/LOCAL_MULTIPLICITY.md", + "bytes": 13100, + "sha256": "e6272e8709835ca6290fecb7034fa84832dde08c3c4cc990a48b8019e89e7c8d", + "git_blob": "b5c18aac5529c5f975ee5bb056b304debafc6697", + "use": "Planar normal-form and extra-saddle data. Its planar global first-moment upper estimate is NOT imported for d>2." + } + ], + "new_obligations": [ + "Complete physical-jet covariance floor in every fixed dimension", + "Nonlinear raw Schur/shear chart with unit Jacobian and one shrinking coordinate", + "Conditional C4 control on raw jets before choosing the spatial shear", + "Full-dimensional endpoint Schur bounds and anisotropic saddle persistence" + ], + "pending_pair_distance_sources_consumed": false, + "historical_blocked_code_consumed_or_retried": false, + "nonauthor_acceptance": false, + "governing_status_changed": false +} diff --git a/frontiers/elder_dimension_lift_20260928/lift.py b/frontiers/elder_dimension_lift_20260928/lift.py new file mode 100644 index 000000000..03d6827ac --- /dev/null +++ b/frontiers/elder_dimension_lift_20260928/lift.py @@ -0,0 +1,149 @@ +"""Exact finite helpers for the one-soft-transverse-direction construction. + +No Gaussian continuum claim follows from these computations. Standard library only. +""" +from fractions import Fraction as F +from itertools import product +from math import factorial + +MUTANT=None + +def eye(n): return [[F(int(i==j)) for j in range(n)] for i in range(n)] +def tr(A): return [list(c) for c in zip(*A)] +def mm(A,B): + return [[sum((x*y for x,y in zip(row,col)),F(0)) for col in zip(*B)] for row in A] + +def solve(A,b): + n=len(A) + if n==0 or len(b)!=n or any(len(row)!=n for row in A): + raise ValueError('nonempty square linear system required') + W=[[F(x) for x in row]+[F(b[i])] for i,row in enumerate(A)] + for j in range(n): + p=next((i for i in range(j,n) if W[i][j]),None) + if p is None: raise ValueError('singular matrix') + W[j],W[p]=W[p],W[j] + pivot=W[j][j]; W[j]=[x/pivot for x in W[j]] + for i in range(n): + if i!=j: + v=W[i][j]; W[i]=[x-v*y for x,y in zip(W[i],W[j])] + return [row[-1] for row in W] + +def det(A): + n=len(A) + if not n:return F(1) + W=[[F(x) for x in row] for row in A]; out=F(1) + for j in range(n): + p=next((i for i in range(j,n) if W[i][j]),None) + if p is None:return F(0) + if p!=j:W[j],W[p]=W[p],W[j];out=-out + pivot=W[j][j];out*=pivot + for i in range(j+1,n): + z=W[i][j]/pivot + for k in range(j+1,n):W[i][k]-=z*W[j][k] + return out + +def rank(A): + W=[[F(x) for x in row] for row in A] + if not W:return 0 + h=0 + for j in range(len(W[0])): + p=next((i for i in range(h,len(W)) if W[i][j]),None) + if p is None:continue + W[h],W[p]=W[p],W[h];pivot=W[h][j] + for i in range(h+1,len(W)): + z=W[i][j]/pivot + if z: + for k in range(j,len(W[0])):W[i][k]-=z*W[h][k] + h+=1 + if h==len(W):break + return h + +def chart(D,v,sigma): + q=solve(D,v);n=len(D) + sign=-1 if MUTANT=='wrong-schur-sign' else 1 + a=F(sigma)+sign*sum((x*y for x,y in zip(v,q)),F(0)) + A=[[a,*v]]+[[v[i],*D[i]] for i in range(n)] + S=eye(n+1) + for i in range(n):S[i+1][0]=F(0) if MUTANT=='omit-shear' else -q[i] + return A,S + +def multiindices(d,degree,upto=False): + return [a for a in product(range(degree+1),repeat=d) if sum(a)<=degree] if upto else [a for a in product(range(degree+1),repeat=d) if sum(a)==degree] + +def monomial(x,a): + out=1 + for u,p in zip(x,a):out*=u**p + return out + +def jet_labels(d): + zero=(0,)*d; e=[tuple(int(i==j) for j in range(d)) for i in range(d)] + plus=lambda a,b:tuple(x+y for x,y in zip(a,b)) + ex=e[0]; two=plus(ex,ex);three=plus(two,ex) + U=[zero,ex,two,three] + for j in range(1,d):U += [e[j],plus(ex,e[j])] + J=[a for a in multiindices(d,3,upto=True) if a not in U] + if MUTANT=='duplicate-cubic-pin':J[-1]=three + return U,J + +def _pmul(P,Q): + R={} + for a,c in P.items(): + for b,e in Q.items(): + k=tuple(x+y for x,y in zip(a,b));R[k]=R.get(k,F(0))+c*e + return {a:c for a,c in R.items() if c} + +def cubic_change(d,q): + """Map third-derivative coordinates by f -> f(x,z,w-q z); pure xxx stays fixed.""" + labels=multiindices(d,3);M=[[F(0) for _ in labels] for _ in labels] + unit=[tuple(int(i==j) for j in range(d)) for i in range(d)] + substitutions=[{u:F(1)} for u in unit] + for j,v in enumerate(q):substitutions[j+2][unit[1]]=-v + def mf(a): + out=1 + for x in a:out*=factorial(x) + return out + for j,a in enumerate(labels): + P={(0,)*d:F(1,mf(a))} + for i,power in enumerate(a): + for _ in range(power):P=_pmul(P,substitutions[i]) + for i,b in enumerate(labels):M[i][j]=P.get(b,F(0))*mf(b) + return labels,M + +def rare_power(d):return d-1 if MUTANT=='rare-every-direction' else 1 +def weight_power(d):return 2*d if MUTANT=='all-directions-soft' else 4 +def band_width(r,k,epsilon):return 2*epsilon*k*(1 if MUTANT=='drop-band-jacobian' else r) + +def plane(X,Z,k,s,a,beta,c): + lin=0 if MUTANT=='drop-transverse-linear' else F(1,4) + value=2*k*X**3-F(3,2)*k*X-k/2+s*Z*Z/2+a*(X*X-lin)*Z/2+beta*X*Z*Z/2+c*Z**3/6 + dx=6*k*X*X-F(3,2)*k+a*X*Z+beta*Z*Z/2 + dz=s*Z+a*(X*X-lin)/2+beta*X*Z+c*Z*Z/2 + return value,[dx,dz] + +def blocks(A,C,D): + return [list(A[i])+list(C[i]) for i in range(len(A))]+[list(row)+list(D[i]) for i,row in enumerate(tr(C))] + +def schur(A,C,D): + invC=tr([solve(D,row) for row in C]);Q=mm(C,invC) + if MUTANT=='ignore-cross-schur':Q=[[F(0) for _ in A] for _ in A] + return [[A[i][j]-Q[i][j] for j in range(len(A))] for i in range(len(A))] + +def endpoint_model(d,r,k): + stable=1 if MUTANT=='positive-stiff' else -1 + def diag(vals):return [[v if i==j else F(0) for j in range(d)] for i,v in enumerate(vals)] + return diag([-6*k*r,-k*r/2]+[F(stable)]*(d-2)),diag([6*k*r,-5*k*r/2]+[F(stable)]*(d-2)) + +def inertia(A): + """Exact Descartes signs for a real-rooted characteristic polynomial of a symmetric matrix.""" + n=len(A);coef=[F(1)];B=eye(n) + for k in range(1,n+1): + AB=mm(A,B);c=-sum(AB[i][i] for i in range(n))/k + coef.append(c);B=[[AB[i][j]+(c if i==j else 0) for j in range(n)] for i in range(n)] + asc=list(reversed(coef));z=0 + while z0 for i,v in enumerate(asc) if v] + neg=sum(a!=b for a,b in zip(signs,signs[1:])) + return neg,z + +def loss_powers(): + return (F(-1,3)+(0 if MUTANT=='omit-loss-factor' else 1),F(-2,3)-1) diff --git a/frontiers/elder_dimension_lift_20260928/test_lift.py b/frontiers/elder_dimension_lift_20260928/test_lift.py new file mode 100644 index 000000000..c3ff86151 --- /dev/null +++ b/frontiers/elder_dimension_lift_20260928/test_lift.py @@ -0,0 +1,146 @@ +"""Finite exact controls, not a Gaussian-field theorem checker.""" +import itertools +import unittest +from fractions import Fraction as F +import lift as m + +class LiftTests(unittest.TestCase): + def test_nonorthogonal_shear_cancels_midpoint_cross_terms(self): + D = [[F(-2), F(1,5)], [F(1,5), F(-3)]] + v = [F(1,4), F(-1,7)] + sigma = F(-3,200) + A, S = m.chart(D,v,sigma) + wanted = [[sigma,F(0),F(0)], [F(0),*D[0]], [F(0),*D[1]]] + self.assertEqual(m.mm(m.tr(S),m.mm(A,S)),wanted) + self.assertNotEqual(m.mm(m.tr(S),S),m.eye(3)) + self.assertEqual(m.det(S),1) + + def test_raw_soft_entry_need_not_be_order_r(self): + A,_ = m.chart([[F(-1)]],[F(1,5)],F(-1,100)) + self.assertEqual(A[0][0],F(-1,20)) + self.assertEqual(A[0][0]-F(1,5)**2/F(-1),F(-1,100)) + + def test_chart_extends_through_singular_contact(self): + A,S = m.chart([[F(-1)]],[F(1,5)],F(0)) + self.assertEqual(m.det(A),0) + self.assertEqual(m.det(S),1) + + def test_full_dimension_determinant_identity(self): + for n in range(1,5): + D = [[-F(i+2) if i==j else F(0) for j in range(n)] for i in range(n)] + v = [F(i+1,20) for i in range(n)] + A,_ = m.chart(D,v,F(-1,17)) + self.assertEqual(m.det(A),F(-1,17)*m.det(D)) + + def test_cubic_tensor_change_has_unit_jacobian(self): + for d in range(3,6): + labels,T = m.cubic_change(d,[F(i+1,20) for i in range(d-2)]) + self.assertEqual(m.det(T),1) + pure = labels.index((3,)+(0,)*(d-1)) + self.assertEqual(T[pure],[F(int(j==pure)) for j in range(len(labels))]) + reduced = [[v for j,v in enumerate(row) if j!=pure] + for i,row in enumerate(T) if i!=pure] + self.assertEqual(m.det(reduced),1) + + def test_raw_chart_volume_is_one_power_of_r(self): + for d in range(2,9): + self.assertEqual(m.rare_power(d),1) + r = F(1,13) + self.assertEqual(m.band_width(r,F(6,5),F(1,100)),F(12,6500)) + + def test_complete_contact_jet_labels(self): + for d in range(2,8): + U,J = m.jet_labels(d) + self.assertEqual(len(U),2*(d+1)) + self.assertEqual(len(U+J),len(set(U+J))) + self.assertEqual(set(U+J),set(m.multiindices(d,3,upto=True))) + + def test_polynomial_lattice_unisolvence(self): + for d in (2,3,4): + labels = m.multiindices(d,3,upto=True) + V = [[m.monomial(n,a) for a in labels] for n in itertools.product(range(4),repeat=d)] + self.assertEqual(m.rank(V),len(labels)) + self.assertEqual(m.rank([row+[row[0]] for row in V]),len(labels)) + + def test_plane_pins_with_free_transverse_cubic(self): + k,s,a,beta,c = F(6,5),F(-2),F(3,7),F(-4,5),F(2,3) + for X,val in ((F(-1,2),0),(F(1,2),-k)): + f,g = m.plane(X,F(0),k,s,a,beta,c) + self.assertEqual(f,val) + self.assertEqual(g,[0,0]) + + def test_plane_path_polynomials(self): + k=F(6,5) + for t in [F(i,16) for i in range(17)]: + pts=[(-F(1,2)-t/4, F(0)),(-F(3,4),9*t/4),(-F(3,4)-t/4,F(9,4))] + want=[-3*t*t/16-t**3/32,F(-7,32),-F(7,32)+51*t/64-9*t*t/32-t**3/32] + for (X,Z),w in zip(pts,want): + f,_=m.plane(X,Z,k,-3*k/2,0,-2*k,0) + self.assertEqual(f,k*w) + self.assertGreater(F(-7,32)-F(1,64),F(-1,4)) + self.assertGreater(F(17,64)-F(1,64),0) + + def test_path_survives_bounded_spatial_shear(self): + q=F(1,9) + maxnorm=F(97,16) + self.assertLess((1+q)**2*maxnorm,16) + + def test_two_extra_saddle_data(self): + X,z2=F(-3,4),F(15,8) + self.assertEqual(6*X*X-F(3,2)-z2,0) + self.assertEqual(F(3,2)+2*X,0) + self.assertEqual(2*X**3-F(3,2)*X-F(1,2)-(F(3,4)+X)*z2,F(-7,32)) + self.assertEqual(-4*z2,F(-15,2)) + self.assertLess(X*X+z2,4) + + def test_stiff_modes_do_not_change_weight_power(self): + for d in range(2,9): + self.assertEqual(m.weight_power(d),4) + for r in (F(1,4),F(1,16),F(1,64)): + HM,HS=m.endpoint_model(d,r,F(1)) + self.assertEqual(abs(m.det(HM)*m.det(HS)),45*r**4) + self.assertEqual(m.inertia(HM),(d,0)) + self.assertEqual(m.inertia(HS),(d-1,0)) + + def test_endpoint_cross_blocks_need_schur_correction(self): + D=[[F(-2),F(0)],[F(0),F(-3)]] + for r in (F(1,4),F(1,16),F(1,64)): + A=[[-6*r,F(0)],[F(0),-r/2]] + C=[[r/7,r/11],[r/13,r/17]] + H=m.blocks(A,C,D) + K=m.schur(A,C,D) + self.assertEqual(m.det(H),m.det(D)*m.det(K)) + self.assertNotEqual(K,A) + self.assertEqual(m.inertia(H),(4,0)) + error=max(abs((K[i][j]-A[i][j])/r) for i in range(2) for j in range(2)) + self.assertLess(error,r) + + def test_stiff_elimination_is_order_r_squared(self): + D=[[F(-2),F(0)],[F(0),F(-3)]] + Q=[F(1,7),F(-2,9)] + z=m.solve(D,Q) + for r in (F(1,4),F(1,16),F(1,64)): + ell=[r*r*v for v in Q] + w=[-r*r*v for v in z] + for i in range(2): + self.assertEqual(sum(D[i][j]*w[j] for j in range(2))+ell[i],0) + correction=sum(w[i]*D[i][j]*w[j]/2 for i in range(2) for j in range(2))+sum(ell[i]*w[i] for i in range(2)) + self.assertEqual(correction/r**3,-r*sum(Q[i]*z[i] for i in range(2))/2) + + def test_determinant_tilt_ledger_all_dimensions(self): + for d in range(2,9): + self.assertEqual(m.rare_power(d)+m.weight_power(d)-2,3) + + def test_density_loss_ledger(self): + self.assertEqual(m.loss_powers(),(F(2,3),F(-5,3))) + self.assertEqual(F(2,3)+1,F(5,3)) + # ell=u^3 gives ell^(2/3-p) d ell = 3 u^(4-3p) du. + self.assertEqual(4-3*F(5,3),-1) + self.assertGreater(4-3*F(3,2),-1) + self.assertLess(4-3*F(2),-1) + + def test_singular_stable_block_is_excluded(self): + with self.assertRaises(ValueError): + m.chart([[F(0)]],[F(1)],F(1)) + +if __name__=='__main__': unittest.main() diff --git a/frontiers/elder_dimension_lift_20260928/verify.py b/frontiers/elder_dimension_lift_20260928/verify.py new file mode 100644 index 000000000..7bbd0612e --- /dev/null +++ b/frontiers/elder_dimension_lift_20260928/verify.py @@ -0,0 +1,96 @@ +"""Source-bound exact finite controls; not a verification of Gaussian analysis.""" +import argparse +import hashlib +import io +import json +from pathlib import Path +import subprocess +import sys +import unittest + +ROOT=Path(__file__).resolve().parent +MUTANTS={ + 'wrong-schur-sign':'test_nonorthogonal_shear_cancels_midpoint_cross_terms', + 'omit-shear':'test_nonorthogonal_shear_cancels_midpoint_cross_terms', + 'rare-every-direction':'test_raw_chart_volume_is_one_power_of_r', + 'all-directions-soft':'test_stiff_modes_do_not_change_weight_power', + 'drop-band-jacobian':'test_raw_chart_volume_is_one_power_of_r', + 'duplicate-cubic-pin':'test_complete_contact_jet_labels', + 'drop-transverse-linear':'test_plane_pins_with_free_transverse_cubic', + 'ignore-cross-schur':'test_endpoint_cross_blocks_need_schur_correction', + 'positive-stiff':'test_stiff_modes_do_not_change_weight_power', + 'omit-loss-factor':'test_density_loss_ledger', +} + +def require(ok,message): + if not ok:raise ValueError(message) + +def decode(text): + def unique(items): + d={} + for k,v in items: + require(k not in d,'duplicate JSON key: '+k);d[k]=v + return d + return json.loads(text,object_pairs_hook=unique) + +def ident(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 sources(): + ident(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(ident(ROOT/e['path'])=={k:e[k] for k in ['bytes','sha256','git_blob']},'source identity differs: '+e['path']) + return {p.name:ident(p) for p in sorted(ROOT.iterdir())} + +def child(mutant): + import lift + import test_lift + lift.MUTANT=mutant + result=unittest.TextTestRunner(stream=io.StringIO()).run(unittest.defaultTestLoader.loadTestsFromModule(test_lift)) + print(json.dumps({'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)},sort_keys=True)) + return 0 if result.wasSuccessful() else 1 + +def replay(out): + out=out.resolve() + require(not out.exists() and not out.is_relative_to(ROOT),'new output outside source required') + before=sources();out.mkdir(parents=True) + records={} + for case in ['baseline',*MUTANTS]: + pair=[] + for mode,flags in [('normal',[]),('optimized',['-O'])]: + command=[sys.executable,'-B',*flags,'-S',str(ROOT/'verify.py'),'--child'] + if case!='baseline':command+=['--mutant',case] + proc=subprocess.run(command,capture_output=True,timeout=30) + (out/(case+'_'+mode+'.stdout')).write_bytes(proc.stdout) + (out/(case+'_'+mode+'.stderr')).write_bytes(proc.stderr) + result=decode(proc.stdout.decode()) + require(not proc.stderr and not result['errors'],'execution error: '+case) + require(result['tests']==18,'wrong test count') + if case=='baseline':require(proc.returncode==0 and result['passed'] and not result['failures'],'baseline failed') + else:require(proc.returncode==1 and not result['passed'] and MUTANTS[case] in result['failures'],'intended semantic failure absent: '+case) + pair.append(proc.stdout) + require(pair[0]==pair[1],'Python modes disagree: '+case) + records[case]=decode(pair[0].decode()) + summary={'tests_per_mode':18,'semantic_mutants_per_mode':10,'identical_output_pairs':11, + 'all_intended_failures':True,'scientific_effect':'NONE','gaussian_analysis_verified_by_code':False} + require(summary==decode((ROOT/'RESULTS.json').read_text()),'stored summary differs') + require(sources()==before,'sources changed during replay') + report={**summary,'source_identities':before,'sources_unchanged':True,'cases':records} + (out/'REPORT.json').write_text(json.dumps(report,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/REMOTE_PAIR_LAW.md b/frontiers/window_multiplicity_laws_20260928/REMOTE_PAIR_LAW.md new file mode 100644 index 000000000..3fb602040 --- /dev/null +++ b/frontiers/window_multiplicity_laws_20260928/REMOTE_PAIR_LAW.md @@ -0,0 +1,325 @@ +# The leading remote factorial-pair measure and its universal height-gap law + +Object: OA-WINDOW-MULTIPLICITY-REMOTE-20260928-v1. +Author: OpenAI / ChatGPT, foreground research session, 28 September 2026. +Disposition: AUTHOR-SIDE PROOF CANDIDATE; NONAUTHOR ANALYTIC REVIEW REQUIRED. +Scientific effect: NONE. No old source, review verdict, or governing status is changed. + +## 1. Exact setting and count convention + +Use the exact field, pins, Q_r, W_r, Z_r and positive compact gap-mark range of +[RM] and [RC] in SOURCE_MAP.json. Dimension d>=2 and torus side L are fixed; +0=rho}. +Let N_j(E) count index-j critical points of height in I_r=(b-k r^3,b), and +N(E)=sum_j N_j(E). Let T_ij(E) count **ordered distinct pairs** (x,x') of indices +i,j, both in E and with both heights in I_r. Thus T_ii=N_i(N_i-1), T_ij=N_iN_j +for i!=j, and sum_ij T_ij=N(N-1). + +[RC] gives E_Qr^W T_ij(E)<=C r^5 |E|. This note proposes the leading coefficient, +its index support, and a normalized **factorial-pair mean** height law. It does +not infer a pair-occurrence probability asymptotic from a factorial expectation. + +## 2. Contact coefficient + +Let U_0=v_0 be the endpoint contact observations from [RM, (4)]: in the pin frame, + + U_0=(f,f_x,f_xx,f_xxx,f_yj,f_xyj) at 0, + v_0=(b,0,0,12k,0,...,0), Q_0=Law(f | U_0=v_0). + +Let B_0 be the transverse Hessian at 0 on u-perp, and define + + w_0=(6k)^2 (det B_0)^2 1{B_0<0}, z_0=E_Q0 w_0>0. + +For x in D_rho and unit e, put + + Y_{x,e}=(grad f(x), H_x e, f(x)), + T=D^3 f(x)[e,e,e], A=H_x restricted to e-perp. (R1) + +Use the conditional Gaussian density p_{Y|Q0} at (0,0,b), and keep all dependence +between B_0, A and T inside conditional expectations. Define chi_ij(A,T) as follows, +where a is the negative index of a nonsingular A: + + T>0: chi_ij=1 iff (i,j)=(a+1,a); + T<0: chi_ij=1 iff (i,j)=(a,a+1); + T=0 or det A=0: chi_ij=0. (R2) + +The values on singular A and T=0 do not affect the following product. With ordinary +unnormalized surface measure de on S^{d-1}, define + + K_ij(x;b,k,u) + = (3/40) 12^(2/3) k^(5/3) / z_0 + * integral_S p_{Y|Q0}(0,0,b) + E_Q0[w_0 |T|^(4/3) (det A)^2 chi_ij(A,T) + | Y_{x,e}=(0,0,b)] de. (R3) + +Choice of an orthonormal basis of e-perp or u-perp has no effect on determinants, +indices, or this expectation. Local orthonormal frames suffice; no global frame +section over the sphere is assumed. + +**Theorem R.** For every fixed E as above, + + E_Qr^W T_ij(E) = r^5 integral_E K_ij(x) dx + o(r^5). (R4) + +The coefficient is continuous and finite on the fixed compact parameter ranges. +It is strictly positive for adjacent indices |i-j|=1, and identically zero for +all other index pairs. Moreover K_ij=K_ji after integration in e. Consequently + + E_Qr^W[N(E)(N(E)-1)] ~ r^5 integral_E sum_ij K_ij > 0, + E_Qr^W[N_j(E)(N_j(E)-1)] = o(r^5). (R5) + +These are fixed-domain qualitative asymptotics; no numerical remainder or rate +for the little-o is asserted. The convergence can be taken uniform in the fixed +compact mark/frame ranges for a given fixed E. It is **not** asserted uniform over +arbitrary r-dependent oscillatory sets E_r. Null-volume E has zero counts by [RM]. + +## 3. The conditional collision frame and its actual coupling + +For x'=x+delta e, 00. All frame entries +are point evaluations or integral derivative averages; covariance and derivative +cross-covariances extend continuously to r=delta=0. The positive joint covariance +floor persists there. Therefore, as r,delta->0 and y->b, this representation +converges in every fixed L^p(C^q), uniformly on compact x,e,frame,mark,t sets, to +the corresponding regression on (U_0,V_0)=(v_0,0,0,b,t). The density of V_delta +under Q_r converges on the same bounded target sets to the density of V_0 under +Q_0. The Gaussian conditional means need not be zero. + +At the limit, T=-12t. Away from the origin the derivative orders 0,1,2,3 in +(U_0,V_0) are independent linear functionals. The order-two block H->He is onto. +Adding the independent entries of B_0 and A completes the Hessian entries at their +respective sites. Positive Fourier weights then give full conditional support for +(B_0,A,T) given (U_0,Y), using the distributional jet-independence argument of [RM]. +This also proves the uniform conditional moment bounds used with (R3). + +## 4. Two determinant limits without inverse Hessians + +Under the exact pair-gradient conditions, Taylor's integral identity gives + + H_x e / delta = -(1/2) D^3 f(x)[e,e,.] + O(delta ||f||C4), + H_x' e / delta = +(1/2) D^3 f(x)[e,e,.] + O(delta ||f||C4). (R7) + +Indeed integrate the gradient difference over the segment and expand its Hessian +once. The second identity follows from the other endpoint. The C^4 control is +valid under the extra observations by Section 3. In a frame beginning with e, +congruence by diag(delta^(-1/2),I) gives limits + + K_x -> diag(-T/2,A), K_x' -> diag(T/2,A). + +The off-diagonal scaled entries are O(sqrt(delta)||f||C3); the lower-right entries +converge to A. Congruence preserves inertia and changes determinant by delta^{-1}. +For each j, the function F_j is continuous even on singular matrices, with the +polynomial Lipschitz bound established in [RM, (8)]. Hence under the coupled +conditional fields, + + F_i(H_x)/delta -> F_i(diag(-T/2,A)), + F_j(H_x')/delta -> F_j(diag(T/2,A)) (R8) + +in L^p for each finite p on bounded target sets. This avoids a division by det A, +a lower eigenvalue assumption, or a discontinuous type-indicator limit. + +The same exact pin identities as [RM, Section 4], now under this additional +conditioning, give W_r/r^2 -> w_0 in L^p. The full endpoint-only normalizer is +Z_r/r^2 -> z_0; it is not changed to a pair-conditioned normalizer. The product +limit in (R8) is + + (T^2/4)(det A)^2 chi_ij(A,T). + +Thus it vanishes at leading order unless the two indices are adjacent. Same-index +pairs are not impossible at positive delta: for example, with a nonzero mixed +third derivative and T=0, a cubic can give two saddle determinants of order delta^2 +rather than delta. The finite negative control records this distinction. + +## 5. Blow-up delta=r s, dominated convergence, and the coefficient + +Apply the already justified marked pair Kac-Rice formula [RC, (3.1)] under the +Gaussian Q_r, using W_r once and each witness determinant once, then divide by +Z_r once. Polar coordinates contribute delta^{d-1}; the joint value-gradient +change of variables contributes delta^{-d-3}. With + + y=b-r^3 z, delta=r s, t=(y'-y)/delta^3, + +we have dy'=delta^3 dt. The two windows are exactly + + 0 0. + +On bounded s,t regions the remaining density is uniformly bounded. The displayed +translation estimate removes the second indicator in L^1; the integrable envelope +controls the tails. This proves the same limit for every fixed Borel E without +assuming a smooth boundary. It does not supply a uniform estimate for arbitrary +oscillating E_r, which is why that extension is excluded in Theorem R. + +Integrating z in (R9) gives (k-s^3|t|)_+. For t!=0, + + integral_0^infinity s(k-s^3|t|)_+ ds + =(3/10) k^(5/3)|t|^(-2/3). (R10) + +Multiply by 36t^2. Integrating the last observation and converting T=-12t to its +conditional Gaussian distribution yields + + (54/5) k^(5/3) E[|T/12|^(4/3) ... |Y] + =(3/40)12^(2/3)k^(5/3) E[|T|^(4/3) ... |Y]. (R11) + +This is exactly (R3), including the surface-measure and ordered-pair conventions. +One may first restrict |t|>epsilon, apply Tonelli to nonnegative functions, and +then let epsilon decrease to zero. The resulting |T|^(4/3) moment is finite; +t=0 is a Lebesgue-null exceptional target. No cancellation of an undefined +zero-times-infinity value is required. + +Separated pairs delta>=eta_0 contribute O(r^6)|E|^2 by [RC, Lemma 5] and are +negligible after division by r^5. This proves (R4). + +Full conditional Gaussian support makes the integrand positive on an open set +B_0<0, A of any chosen index a, and T of either chosen nonzero sign. Therefore +K_ij>0 precisely for adjacent indices. Continuity follows from regression and +polynomial domination. The weighted indicator is continuous at every possible +index boundary because det A or T vanishes there. Compactness gives finite upper +bounds and positive lower bounds for each adjacent coefficient. The substitution +e->-e flips T, preserves A and w_0, and changes H e only by a sign at its zero +target; it exchanges i and j without a density Jacobian. This proves symmetry +and (R5). For unordered total pairs, divide the total coefficient by two. + +## 6. Universal height marks under the factorial-pair mean + +For each counted critical point define its normalized height deficit + + theta(x)=(b-f(x))/(k r^3) in (0,1). + +Define a probability measure on (0,1)^2 by normalizing the **expected ordered-pair +count measure**: + + Pi_r(C)= E_Qr^W sum_{x!=x' counted in E} + 1{(theta(x),theta(x')) in C} + / E_Qr^W[N(E)(N(E)-1)]. (R12) + +This is a factorial-moment normalization, sometimes called pair weighting. It is +not the law obtained by first conditioning on N>=2 and then choosing a pair +uniformly from that realized configuration. Those two sampling procedures need +not agree when configurations have different multiplicities. + +**Theorem H2.** In probability total variation (one half of the full signed +variation norm), Pi_r converges to the density + + h(a,b)=(5/9)|a-b|^(-1/3), 0-e symmetry gives equal total mass to the two triangles. This proves (R13) +and its index-resolved version. The separated-pair mass is o(r^5), so it does not +change the normalized limit. Notice that the argument pushes forward to HEIGHT +marks: it does not claim total-variation convergence of unscaled distinct spatial +pairs to a measure supported on the spatial diagonal, which would be impossible. + +The gap g=|a-b| therefore has the **Beta(2/3,2)** density and CDF + + f_gap(g)=(10/9)g^(-1/3)(1-g), + F_gap(g)=(5/3)g^(2/3)-(2/3)g^(5/3), 0<=g<=1. (R14) + +Given g, the smaller deficit is uniform on (0,1-g). Useful exact consequences are + + E[g^n]=10/((3n+2)(3n+5)), n=0,1,..., + E[g]=1/4, E[g^2]=5/44, Var(g)=9/176; + E[a]=E[b]=1/2, E[a^2]=29/88, E[ab]=3/11, + Corr(a,b)=2/7. (R15) + +The marginal pair-weighted deficit density is +(5/6)(a^(2/3)+(1-a)^(2/3)), not uniform. For comparison, two independent uniform +heights would have mean absolute difference 1/3 rather than 1/4. None of these +pair-weighted assertions is a persistence-lifetime law. + +## 7. Explicit limits of the result + +The coefficient in (R3) is a Gaussian conditional integral, not a numerical +enclosure. Positivity and the r^5 order do not by themselves prove +Q_r^W(N>=2)~(r^5/2) integral sum K: triples or higher multiplicities would require +additional estimates. A finite probability-law counterexample in the tests +exhibits a factorial moment asymptotic of order r^5 with much smaller event +probability. No third factorial moment or event-conditioned pair-gap law is claimed. + +The spatial exclusion remains fixed. The local theorem in LOCAL_MULTIPLICITY.md +shows that global multiple occurrences have order r^3 in d=2, so neither (R4) nor +(R13) is silently extended to pairs near the pins. Other exclusions are changing +L or d, k->0, random field-selected E, arbitrary oscillating E_r for the sharp +asymptotic, all-height counts, elder pairing and governing-status transitions. + +The new obligations are the extra-conditioned determinant limits, L^1 domination +through the collision, the fixed-Borel translation step, the coefficient constants, +and the factorial-mean interpretation of the beta law. Finite exact controls test +algebra, not those continuum arguments. Literature context and the limits of the +reconnaissance are recorded separately; no historical-priority claim is made. diff --git a/reviews/elder_dimension_lift_claude_20260928/RESULTS.json b/reviews/elder_dimension_lift_claude_20260928/RESULTS.json new file mode 100644 index 000000000..59e62fdcd --- /dev/null +++ b/reviews/elder_dimension_lift_claude_20260928/RESULTS.json @@ -0,0 +1,81 @@ +{ + "checks": { + "CHART": { + "raw_chart_full_jacobian_is_one_d3_d4": true, + "rotated_lattice_unisolvence_degree3": true, + "schur_shear_cancels_and_det_A_equals_sigma_det_D_n1to4": true + }, + "LEDGER": { + "density_loss_ell_2_3_k_minus_5_3": true, + "inverse_moment_threshold_5_3": true, + "jet_count_U0_plus_J_is_binom_d3_3": true, + "ledger_r_r4_over_r2_is_r3_all_d": true + }, + "PATH": { + "path_segments_margins_and_saddle_data": true + }, + "PHYSICAL": { + "Hu_order_r": true, + "endpoint_blocks_A20": true, + "gradient_pin_average_A24": true, + "normal_form_A17_exact": true, + "pins": true, + "schur_det_inertia_A21_A22": true, + "shear_recovers_sigma_D_tau": true, + "weight_order_r4": true + }, + "QUARTIC": { + "A17_remainder_halves_with_r": true, + "Hu_halves_with_r": true, + "_rates": { + "A17_remainder": { + "3": [ + 2.0, + 2.0, + 2.0 + ], + "4": [ + 2.0, + 2.0, + 2.0 + ] + }, + "H_S_u": { + "3": [ + 1.9944, + 1.9972, + 1.9986 + ], + "4": [ + 2.0023, + 2.0011, + 2.0006 + ] + } + }, + "contact_frame_nonsingular": true, + "pins_exact_after_solve": true + }, + "SADDLES": { + "_ratios": { + "3": [ + 1.1962, + 1.1312 + ], + "4": [ + 1.0019, + 1.6157 + ] + }, + "distinct_from_each_other_and_pins": true, + "heights_inside_window": true, + "index_d_minus_1": true, + "planar_critical_point_not_full_critical": true, + "stable_displacement_W_converges_at_rate_r": true, + "two_extra_critical_points_exist": true + } + }, + "object": "CLAUDE-REVIEW-ELDER-DIMENSION-LIFT-20260928-v1", + "passed": true, + "scope": "exact chart/field identities and one labelled numerical saddle group; not an analytic proof" +} diff --git a/reviews/elder_dimension_lift_claude_20260928/REVIEW.md b/reviews/elder_dimension_lift_claude_20260928/REVIEW.md new file mode 100644 index 000000000..e2b9fcdc8 --- /dev/null +++ b/reviews/elder_dimension_lift_claude_20260928/REVIEW.md @@ -0,0 +1,200 @@ +# Nonauthor analytic review: the elder lower event in every fixed dimension (Math-#125) + +Scientific effect: **NONE**. This file does not change `lemma_closed`, prizes, premises, `STATUS`, `PROOF_INDEX`, +`GRAPH`, landing claims or any author source. It records verdicts on the OpenAI candidate below. Integration is a +separate act. + +## Object + +| Field | Value | +|---|---| +| Object | OA-ELDER-DIMENSION-LIFT-20260928-v1 (OpenAI / ChatGPT) | +| Branch / head | `chatgpt/elder-dimension-lift-20260928` / `e3f10b390ae5ddd998d238206add5958d5b720bb` ([Math-#125](https://github.com/d6g8k5htny-coder/Math-/pull/125)), base `d39dbbc` | +| `PROOF.md` | Git blob `7303bd791a68a1139251f0f6e403a9f7cc89b006`, 23971 B, SHA256 `b529fe3780e1909014b3cb144b9a74156d976bbdc19b6711d0c5b1a1da9e5669`, 480 lines | +| Consumed, already on main | [LP] `imports/lifetime_parent_20260925/UNIFORM_MATRIX_CAP_AND_LIFETIME.md` (blob `dfed3b8d…`): §1 selector, §§2–4 spectrum, contact frame and regression, §8 maximin; Theorem A and §§9–12 for the corollaries only. [EL] `frontiers/window_multiplicity_laws_20260928/ELDER_LOWER_AND_DENSITY_GAP.md` (blob `aaefc8da…`): the planar cubic, path and d = 2 case. [LOCAL] `LOCAL_MULTIPLICITY.md` (blob `b5c18aac…`): planar saddle data. | + +## Provenance + +| 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 read `PROOF.md` in full, plus the packet README, SOURCE_MAP, RECONNAISSANCE, `lift.py`, `test_lift.py` and `verify.py`. I wrote the nonauthor review of [EL]/[LOCAL] (`reviews/d1_elder_lower_claude_20260928/`), the #106 review of LP Theorem A, and the D1 chain reconciliation (Math-#126, merged at `8224783`). Corollary B's upper half consumes LP Theorem A, whose reconciliation I authored, so for that half this review is **not** independent of its inputs. The direct lower Theorem A (A2)–(A4) consumes none of those objects except [EL]'s unchanged planar cubic and path, which this review re-derives. | +| Independent derivation | Before seeing #125 I had planned a d ≥ 3 lower proof by a nonlinear ridge reduction `y = φ(x, z)` in the stable directions. Its reduced midpoint Hessian is the same Schur complement `σ = f_zz − f_zw f_ww⁻¹ f_wz`. #125's linear shear reaches the same rare set with less machinery (N3), so I review #125 instead of writing a competing candidate. | +| Author code | I ran `verify.py --output` in `-B -S` and `-B -O -S` on the exact head: 18 tests per mode, 10 intended mutant failures, identical output pairs. Source identities match. | +| Independent checks | `dimension_lift_review_check.py` is my own suite, written from `PROOF.md` without reusing `lift.py`. It checks finite identities exactly, plus one labelled floating-point group. Every Gaussian step below was argued by hand and is not replaced by those checks. | + +## Verdicts + +| Interface (PROOF.md lines) | Verdict | +|---|---| +| §2 (98–130): complete 3-jet `(U_0, J)` of size `C(d+3,3)`, positive definite in every frame; uniform floor for `(U_r, J)`; raw-jet density floor under `Q_r` | **ACCEPT**; see §1 below. | +| §3 (132–187): Schur shear (A8)–(A9), unit-Jacobian raw chart (A10) | **ACCEPT**. Exact check `CHART`, including the full Jacobian by dual numbers. | +| §4 (189–216): raw rare set (A11), volume (A12), `Q_r ≥ c_J r` (A13) | **ACCEPT**; see §2 below. | +| §5 (218–246): `C^4` control after conditioning on all physical jets (A14)–(A16); constant order | **ACCEPT**; see §3 below. | +| §6 (248–282): sheared-plane normal form (A17), pin identities, target (A18) | **ACCEPT**. Hand-derived. Exact on physical cubic fields in d = 3, 4, 5 (zero remainder); `O(r)` remainder on quartic fields. | +| §7 (284–308): path (A19), margins `k/64`, `d_f(M) ≥ b − kr³/4 > f(S)` | **ACCEPT**. Identical to [EL] (E5)–(E6); recomputed. | +| §8 (310–361): endpoint blocks (A20), Schur (A21), inertia and determinant (A22), `W ≥ c r⁴` (A23), `Z ≤ C r²` (A24), ledger (A25) | **ACCEPT**; see §4 below. | +| **Theorem A (A2)–(A3)**: `1 − p_r ≥ c r³` for every fixed d ≥ 3 (d = 2 is [EL]) | **ACCEPT** at its stated existential scope. | +| §9 (363–415), **(A4)**: two extra index-(d−1) critical points, `Q^W(N_r ≥ 2) ≥ c r³`, factorial lower bound | **ACCEPT**; see §5 below. | +| **Corollary B (A5)**: `c r³ ≤ 1 − p_r ≤ C r³` in every fixed d | **ACCEPT** as a composition with LP Theorem A (1.1), consumable at existential scope under the D1 reconciliation (Math-#126, merged at `8224783`); see §6 below. | +| **(A6)**: compact-mark loss `ν_cand − ν_eld = Θ(ℓ^{2/3})` in every fixed d | **ACCEPT** as a composition with LP's compact-mark ledger and (A5). | +| **Corollary C (A6a)**: rejected-pair inverse moments finite iff `p < 5/3`; `Θ(t^{5/3−p})`; logarithmic endpoint | **ACCEPT** as a composition with (A6). | + +No defect was found. Notes N1–N5 record observations that sharpen or delimit the text without changing it. + +--- + +## §1 — the jet floor (§2 of PROOF.md) + +The count is exact. `U_0` has `4 + 2(d−1) = 2(d+1)` entries (lines 101–105), one per pin observation. `J` has the +`m(m+1)/2` transverse Hessian entries (`m = d − 1`) and the `C(d+2,3) − 1` third derivatives other than `f_xxx`. +Order by order, `U_0 ∪ J` is every derivative of order 0–3 exactly once. Order 2 has `d` entries in `U_0` (`f_xx`, +`f_xy_j`) and `m(m+1)/2` in `J`, total `d(d+1)/2`. The total is `C(d+3,3)` (`LEDGER`, d = 2…12). + +Positivity: the periodized covariance has Fourier weights `∝ exp(−|ω|²/2) > 0` on `(2π/L)Z^d`. A linear functional +`Σ c_α ∂^α f(0)` has variance `Σ_ω w_ω |Σ c_α (iω)^α|²`. If that variance is zero, the polynomial `Σ c_α (iω)^α` vanishes +on the dual lattice, rotated by the frame. Pulled back, it vanishes on `Z^d`, hence identically. So the complete jet +covariance is positive definite for each frame. Compactness of `O(d)` and continuity make the floor uniform. +`CHART.rotated_lattice_unisolvence_degree3` illustrates this exactly on Cayley-rational rotated lattices for d = 2, 3. + +`U_r → U_0` uniformly as `r → 0` is LP §§2–4. The quartic group re-solves the `2(d+1)` U_0 jets from the pins through +that frame and finds it nonsingular. Conditioning on `U_r = v_r` is Schur complementation, so the conditional covariance +of `J` is sandwiched between the joint floor and ceiling, and its mean `Cov(J,U_r)Cov(U_r)⁻¹v_r` is bounded. A Gaussian +density with sandwiched covariance and bounded mean is bounded below on every fixed compact set. The claim is about +**raw** jets (line 129), which is what §4 integrates. + +Note on `J` being free under `Q_r`: the pins tie `f_y(0)` to `f_xxy` at order `r²`, since +`f_y(0) = −(r²/8) f_xxy + O(r³)`. That relation lives inside the `U_r` rows, not as a constraint on `J`. The +`PHYSICAL` group builds fields with arbitrary `J` and verifies all `2(d+1)` pins exactly. + +## §2 — the chart and the rare set (§§3–4) + +With `q = D⁻¹v`, `y = (z, w − qz)` gives +`yᵀAy = az² + 2z vᵀ(w − qz) + (w − qz)ᵀD(w − qz)`. The `zw` terms cancel because `qᵀD = vᵀ`. The `z²` coefficient is +`a − 2vᵀD⁻¹v + vᵀD⁻¹v = σ`. So `SᵀAS = diag(σ, D)` and `det A = σ det D` (checked exactly, n = 1…4). The chart +`(σ, v, D, τ) ↦ (a, v, D, T)` is block triangular in the order `(v, D), σ, τ`, with diagonal blocks `I`, `1` and the +substitution `w ↦ w + qz` on third-derivative coordinates, which is unipotent. + +`f_xxx` is untouched, and no other coordinate depends on it: `∂_z` of the sheared field only introduces `∂_w`, which +preserves the number of `x` indices. So deleting `xxx` leaves determinant one. My check does not rely on the triangular +argument. It differentiates the whole map with exact dual numbers for d = 3 (12 variables) and d = 4 (25 variables), +and finds a full Jacobian determinant of exactly 1. + +The rare box (A11) is a product: an interval of length `2εkr` in `σ`, fixed boxes in `v` and `D`, and width-`2εk` boxes +in the `q_3 = C(d+2,3) − 1` coordinates of `τ`. Its raw volume is therefore (A12). All inverse-chart images lie in one +compact set, because `D⁻¹`, `q` and `σ` are bounded. So (A13) follows from §1. The raw entry `a` sits on the `O(1)` +surface `vᵀD⁻¹v`, inside a band of width `O(r)`. Only one scalar shrinks. That is why the power is `r¹` in every d +(line 185). Requiring all `m(m+1)/2` transverse entries to be `O(r)` would give `r^{m(m+1)/2}` instead. No law is +assigned to the sheared variables (lines 213–216): the raw Gaussian density is integrated against a unit Jacobian. + +## §3 — conditioning order and constants (§5) + +The field is regressed on `V = (U_r, J)` at each target. The pin rows are integral averages of derivatives of order +≤ 3, so the cross-covariances of the field's derivatives through order 4 with `V` are uniformly bounded. `Cov(V)⁻¹` is +bounded by §1, and the targets are compact. Hence (A15) holds uniformly. Markov's inequality gives `K_4` with conditional +mass ≥ 1/2 at every target, and integrating over the rare set gives (A16). No independence between jets and remainder is +used, and no unconditional tail is subtracted from an `O(r)` mass. + +The constant order is sound. The raw container is valid for all `ε ≤ 1`, so `K_4` is chosen first. `ε` is then chosen +for the planar `O(εk)` margins, which do not involve `K_4`. Finally `r_*` absorbs every `O(rK_4)` and `O(rK_4²)` term. + +## §4 — normal form, endpoints, weight and normalizer (§§6, 8) + +(A17): I rederived every pin identity (lines 266–270) from the axial restrictions `φ(x) = g(x,0)` and +`ψ(x) = g_z(x,0)`. The sums of `φ'(±r/2)` and `ψ(±r/2)` give `g_x` and `g_z`. Their differences give `g_xx` and `g_xz`. +The height difference gives `g_xxx = 12k + O(rK_4)`. The `Z²` coefficient is `σ/r`, not `a/r`. The `−a_3 Z/8` term comes +from `g_z(0)`. + +Two independent exact checks support this: + +- **Cubic fields.** On physical cubic fields in d = 3, 4, 5, built from chart data with all pins imposed and then + sheared, (A17) holds with **zero** remainder. The sheared midpoint jets reproduce `σ`, `D` and `τ` exactly + (`PHYSICAL`). +- **Quartic fields.** On quartic fields, where the pins are re-solved through the contact frame, the sup of + `F_r − P` over the rational grid in `B(0,3)` halves as `r` halves (successive ratios 2.0000 to four decimals), for + `r = 1/8 … 1/64` in d = 3, 4 + (`QUARTIC`). + +The mutants `raw-a-in-plane` and `drop-transverse-pin-term` are rejected. + +(A20)–(A22): for cubic fields the endpoint blocks are exactly `r P_i` (soft), `C_i = ±(r/2)(τ_xxw; τ_xzw)` (cross) and +`D ± (r/2) τ_xww` (stable). Then `det H = det D_i · det K_i`, and inertia(H) = inertia(D_i) + inertia(K_i), with index +d at `M` and d − 1 at `S`. `|K_i/r − P_i| ≤ rk`. All of this is checked exactly, with the physical Hessian computed +independently of the sheared one. Dropping the cross-block correction is rejected (`no-cross-schur`). The target planar +Hessians `diag(−6k, −k/2)` and `diag(6k, −5k/2)` are recomputed in `PATH`. Since `|det L| = 1`, physical and sheared +determinants agree, so `W_r ≥ c r⁴` with the power independent of d. + +(A24): `∇f(S) − ∇f(M) = r∫_{−1/2}^{1/2} H(tru)u dt = 0` (checked exactly). So `H_i u = O(r‖f‖_{C³})`. On cubic +fields `H_i u = ±(r/2)(f_xxx, f_xxy_j)` exactly, and on quartic fields it halves with `r`. Hadamard's inequality gives +`|det H_i| ≤ C r (1 + ‖f‖_{C³})^d`, and LP §4's endpoint-conditioned moments give `Z_r ≤ C_Z r²`. The ledger is +`r · r⁴ / r² = r³` in every d (`LEDGER`; `weight-2d` rejected). + +## §5 — the extra saddles (§9) + +The rescaling `x = rX, z = rZ, w = r²W` is the right one. I rederived (A27) term by term: + +- **Soft components.** These are `∇F_r` plus `r⁻²·r²W·f̃_{w,(x,z)}(rX, rZ, 0) = O(rK_4|W|)`. The mixed soft–stable + Hessian is `O(rK_4)` in the `O(r)` ball, because `f̃_zw(0) = 0` exactly and `f̃_xw(0) = O(K_4 r²)`. +- **Stable components.** These are `r⁻²[f̃_w(0) + f̃_wx rX + ½(τ_xxw r²X² + 2τ_xzw r²XZ + τ_zzw r²Z²) + r²DW] + O(rK_4)`, + with `f̃_w(0) = −(r²/8)τ_xxw + O(K_4 r³)`. This is `DW + Q(X,Z)` with `Q` as in (A28). +- **C¹ closeness.** `∂_X` of the stable part is `r⁻¹f̃_wx(…) = ∂_X Q + O(rK_4)`. `∂_W` of the soft part is `O(rK_4)`. + Second derivatives of `H_r` are bounded by `K_4`, so the quantitative inverse-function theorem applies uniformly + around the block-triangular nondegenerate zero `(p, −D⁻¹Q(p))`. + +Heights are `b + r³(F_r(p) + O(r))`, strictly inside the window. The index is `n + 1 = d − 1`, by the same Schur +argument as §4. + +`SADDLES` illustrates this in floating point on quartic fields in d = 3, 4 for `r = 1/16 … 1/128`. It is a numerical +illustration only: existence and the `O(r)` estimate come from the uniform inverse-function argument above, not from +the solver or finite samples. + +- Newton finds two numerical roots of the full gradient near `(rP_±, r²W*)`, with gradient residual below `1e−15`, + index d − 1 and heights in `(b − kr³, b)`. They are distinct from each other and from the pins. +- `|w/r² − W*|/r` stays within a factor 2 across the range. This is consistent with the `O(r)` estimate proved + analytically above; finite samples do not establish it. Scaling `w` by `r` instead of `r²` is rejected. +- At the planar restriction's critical point, `∂_w f̃/r²` is nonzero. This confirms the manuscript's warning (line + 365) that a planar critical point is not a full critical point. + +## §6 — the corollaries (§10) + +(A5) consumes LP Theorem A (1.1). The D1 reconciliation (Math-#126, `reviews/d1_chain_reconciliation_20260928/`, merged at `8224783`) +records (1.1) as ACCEPT at existential scope in every fixed d ≥ 2, read with the congruence erratum, the §9 replacement +v1.1, wording W1 and `r < L/(4√2)`. Its consumption contract (§7 there) permits exactly this use. #126 is +now merged, so (A5)'s upper half rests on a reconciled register entry. The direct lower half never depended on it. + +(A6): with `ℓ = kr³` at fixed `k`, `r dr = (1/3)ℓ^{−1/3}k^{−2/3} dℓ`. Multiplying by `1 − p ≍ r³ = ℓ/k` gives +`ℓ^{2/3}k^{−5/3}`, which is integrable with positive integral on compact `K` with `k_− > 0`. For small `ℓ` every radius +is below the common cutoff. (A6a) follows: `∫_0^t ℓ^{2/3−p} dℓ` is finite iff `p < 5/3`, logarithmic at `p = 5/3`. The +rejected-pair measure is integrated directly, never as a difference of infinities (line 444). + +**Consequence for the D1 chain.** With this review and #126, Theorem A's cubic order is **two-sided** `Θ(r³)` in every +fixed d ≥ 2, and the compact-mark density loss is `Θ(ℓ^{2/3})` in every fixed d. #126 deliberately says "no d ≥ 3 lower +bound". That caveat can be lifted by a later register PR once both #125 and #126 are integrated, not inside either. + +## Notes + +- **N1.** (A20)'s bound `‖C_i‖ ≤ CrK_4` can be read more finely as `C_i = ±(r/2)(τ_xxw; τ_xzw) + O(K_4 r²)`, so the + Schur correction is `O(r²(εk + K_4 r)²)`. Not needed, but it shows the correction is small even before `r_*` is fixed. +- **N2.** (A4) should say whether `N_r` counts additional window critical points anywhere on the torus or only in the + `C_d r` ball. The lower bounds hold for either reading, since both counts are ≥ 2 on the event. +- **N3.** Why a *linear* shear suffices. The path obstruction needs field values on one plane only. The endpoint and + saddle data need only Schur complements with `O(r)` cross blocks. A nonlinear ridge `y = φ(x,z)` would give the same + midpoint Schur complement at the cost of implicit-function bookkeeping. Neither route needs the other. +- **N4.** The bound `‖q‖ ≤ 1/9` (line 146) is used only through a uniform bound on `‖L‖`. Any fixed bound works after + adjusting `r_*`. +- **N5.** `lift.py`'s tests are finite controls of the listed identities. The end-to-end physical-field checks here + (building `f`, imposing pins, shearing and recovering) are additional to them, not a replacement. + +## What this review does not do + +It does not accept a numerical `c`, `r_*` or cutoff, a uniform-in-d bound, an unrestricted-mark difference, a +leading loss constant, a global factorial upper bound, or any identification with historical `q`/`p` symbols. The +manuscript claims none of these. It changes no register. Integration, and any register transition that lifts #126's +d ≥ 3 caveat, are separate acts for a non-Claude integrator. + +## Reproduce + + python -B -S dimension_lift_review_check.py # prints RESULTS.json byte for byte + python -B -O -S dimension_lift_review_check.py # identical + python -B -S dimension_lift_review_check.py --mutant M # exit 1 for each of the 9 mutants diff --git a/reviews/elder_dimension_lift_claude_20260928/SOURCE_FILES.json b/reviews/elder_dimension_lift_claude_20260928/SOURCE_FILES.json new file mode 100644 index 000000000..4fce098c6 --- /dev/null +++ b/reviews/elder_dimension_lift_claude_20260928/SOURCE_FILES.json @@ -0,0 +1,37 @@ +{ + "schema": 1, + "scientific_effect": "NONE", + "review_status": "NONAUTHOR_REVIEW", + "reviewed_object": { + "pr": "d6g8k5htny-coder/Math-#125", + "head": "e3f10b390ae5ddd998d238206add5958d5b720bb", + "paths": [ + { + "path": "frontiers/elder_dimension_lift_20260928/PROOF.md", + "git_blob": "7303bd791a68a1139251f0f6e403a9f7cc89b006", + "bytes": 23971, + "sha256": "b529fe3780e1909014b3cb144b9a74156d976bbdc19b6711d0c5b1a1da9e5669" + } + ] + }, + "files": [ + { + "path": "REVIEW.md", + "bytes": 17030, + "sha256": "032bb4c79e4a985e5b53f5abb6bb06da4d643ec7345e4df9591e2046fb287e12", + "git_blob": "e2b9fcdc8d24f6a4d532afb7d02627e4716158d1" + }, + { + "path": "RESULTS.json", + "bytes": 2035, + "sha256": "97a323d1d383c6bf5a8fe8d616e681d7a2ae1c2d4acee51eb6405ec8df55e8f4", + "git_blob": "59e62fdcd2e30e324ac74263a6b904b3da3d2b6e" + }, + { + "path": "dimension_lift_review_check.py", + "bytes": 37826, + "sha256": "768b0d8f84b66616f2c649c5f7ae132fa701563ead85b8f5aa20a30f2bc0bda8", + "git_blob": "36f258676a9aeb7f1b63e1f1267c3e4ebce52bb6" + } + ] +} diff --git a/reviews/elder_dimension_lift_claude_20260928/dimension_lift_review_check.py b/reviews/elder_dimension_lift_claude_20260928/dimension_lift_review_check.py new file mode 100644 index 000000000..36f258676 --- /dev/null +++ b/reviews/elder_dimension_lift_claude_20260928/dimension_lift_review_check.py @@ -0,0 +1,872 @@ +"""Independent nonauthor checks for OA-ELDER-DIMENSION-LIFT-20260928-v1 (Math- PR 125). + +Python standard library only. Written from the manuscript, not from the author's lift.py/test_lift.py. +Groups (exact rational arithmetic unless marked NUMERIC): + + CHART the Schur shear S^T A S = diag(sigma, D); the full raw chart (sigma,v,D,tau) -> (a,v,D,T) has + Jacobian determinant exactly one (forward-mode dual numbers over Fractions, d = 3, 4); the xxx + coordinate decouples; rational-orthogonal rotated lattices are unisolvent for degree <= 3. + PHYSICAL end to end on actual physical cubic fields in d = 3, 4, 5: build f from chart data and the + 2(d+1) pins, verify the pins, shear it, recover (sigma, D, tau) exactly, and check the planar + normal form (A17) with zero remainder, the endpoint blocks (A20), the Schur/determinant/inertia + identities (A21)-(A22), the gradient-pin average behind (A24) and |H u| = O(r). + QUARTIC physical quartic fields with pins re-solved through the 2(d+1)-row contact frame: the frame is + nonsingular, (A17)'s remainder is O(r) (exact values on a grid at r = 1/8 ... 1/64), and + H_i u = O(r). + SADDLES NUMERIC (floats): on the quartic fields the two extra critical points exist near (rP+-, r^2 W*), + have index d-1 and window heights, w/r^2 -> -D^{-1} Q(p) at rate O(r), and the planar + restriction's critical point is not a full critical point. + PATH the polygonal path (A19) and saddle data (A18), recomputed from the polynomial class. + LEDGER jet counts, the r * r^4 / r^2 = r^3 ledger, the density change of variables (A6) and the + inverse-moment threshold 5/3 (A6a). + +Mutants (each must make the checks fail): raw-a-in-plane, shear-sign, drop-transverse-pin-term, +no-cross-schur, planar-point-is-critical, stable-scale-r, density-dr, threshold-two-thirds, weight-2d. +This is not an analytic proof of the Gaussian covariance floor, conditional C^4 bounds or inverse-function +estimates; those are reviewed in REVIEW.md. +""" +import argparse +import json +import math +import random +import sys +from fractions import Fraction as F +from itertools import product +from math import comb, factorial + +MUTANTS = ("raw-a-in-plane", "shear-sign", "drop-transverse-pin-term", "no-cross-schur", + "planar-point-is-critical", "stable-scale-r", "density-dr", "threshold-two-thirds", "weight-2d") +MUT = None + + +# --------------------------------------------------------------------------------------------------------------- +# Polynomials: dict {exponent tuple: coefficient} +# --------------------------------------------------------------------------------------------------------------- + +def padd(*ps): + out = {} + for p in ps: + for e, c in p.items(): + out[e] = out.get(e, 0) + c + return {e: c for e, c in out.items() if c} + + +def pscale(p, s): + return {e: c * s for e, c in p.items() if c * s} + + +def pmul(p, q): + out = {} + for e1, c1 in p.items(): + for e2, c2 in q.items(): + e = tuple(a + b for a, b in zip(e1, e2)) + out[e] = out.get(e, 0) + c1 * c2 + return {e: c for e, c in out.items() if c} + + +def pconst(c, n): + return {(0,) * n: c} if c else {} + + +def pvar(i, n, c=1): + return {tuple(int(j == i) for j in range(n)): c} + + +def pcompose(p, subs, n_out): + """p(subs[0], ..., subs[n-1]) where each subs[i] is a polynomial in n_out variables.""" + out = {} + cache = {} + for e, c in p.items(): + term = pconst(c, n_out) + for i, power in enumerate(e): + if power: + key = (i, power) + if key not in cache: + acc = pconst(1, n_out) + for _ in range(power): + acc = pmul(acc, subs[i]) + cache[key] = acc + term = pmul(term, cache[key]) + out = padd(out, term) + return out + + +def pdiff(p, i): + out = {} + for e, c in p.items(): + if e[i]: + e2 = list(e) + e2[i] -= 1 + out[tuple(e2)] = out.get(tuple(e2), 0) + c * e[i] + return {e: c for e, c in out.items() if c} + + +def peval(p, pt): + total = 0 + for e, c in p.items(): + term = c + for x, k in zip(pt, e): + if k: + term *= x ** k + total += term + return total + + +def pderiv_at0(p, alpha): + """partial^alpha p (0).""" + return p.get(tuple(alpha), 0) * math.prod(factorial(a) for a in alpha) + + +def from_jets(jets, n): + """Polynomial sum_alpha jets[alpha] x^alpha / alpha!.""" + return {e: F(c) / math.prod(factorial(a) for a in e) for e, c in jets.items() if c} + + +def multi(n, deg): + return [e for e in product(range(deg + 1), repeat=n) if sum(e) == deg] + + +def unit(n, i): + return tuple(int(j == i) for j in range(n)) + + +def eplus(*es): + return tuple(map(sum, zip(*es))) + + +# --------------------------------------------------------------------------------------------------------------- +# Small exact linear algebra +# --------------------------------------------------------------------------------------------------------------- + +def solve(A, b): + n = len(A) + W = [list(map(F, row)) + [F(b[i])] for i, row in enumerate(A)] + for j in range(n): + p = next(i for i in range(j, n) if W[i][j] != 0) + W[j], W[p] = W[p], W[j] + piv = W[j][j] + W[j] = [x / piv for x in W[j]] + for i in range(n): + if i != j and W[i][j] != 0: + f = W[i][j] + W[i] = [x - f * y for x, y in zip(W[i], W[j])] + return [row[-1] for row in W] + + +def det(A): + n = len(A) + W = [list(row) for row in A] + out = 1 + for j in range(n): + p = next((i for i in range(j, n) if W[i][j] != 0), None) + if p is None: + return 0 * out + if p != j: + W[j], W[p] = W[p], W[j] + out = -out + out = out * W[j][j] + for i in range(j + 1, n): + f = W[i][j] / W[j][j] + for k in range(j, n): + W[i][k] = W[i][k] - f * W[j][k] + return out + + +def inertia(A): + """(negatives, positives, zeros) of a symmetric Fraction matrix via symmetric pivoting (Sylvester).""" + n = len(A) + W = [list(map(F, row)) for row in A] + idx = list(range(n)) + neg = pos = 0 + while idx: + j = next((i for i in idx if W[i][i] != 0), None) + if j is None: + # 2x2 pivot on a nonzero off-diagonal entry + pair = next(((i, l) for i in idx for l in idx if i < l and W[i][l] != 0), None) + if pair is None: + return neg, pos, len(idx) + i, l = pair + neg += 1 + pos += 1 + blk = [[W[i][i], W[i][l]], [W[l][i], W[l][l]]] + dB = blk[0][0] * blk[1][1] - blk[0][1] * blk[1][0] + inv = [[blk[1][1] / dB, -blk[0][1] / dB], [-blk[1][0] / dB, blk[0][0] / dB]] + rest = [m for m in idx if m not in (i, l)] + for a in rest: + for b in rest: + ca = [W[a][i], W[a][l]] + cb = [W[i][b], W[l][b]] + W[a][b] -= sum(ca[s] * inv[s][t] * cb[t] for s in range(2) for t in range(2)) + idx = rest + continue + piv = W[j][j] + neg += piv < 0 + pos += piv > 0 + rest = [m for m in idx if m != j] + for a in rest: + for b in rest: + W[a][b] -= W[a][j] * W[j][b] / piv + idx = rest + return neg, pos, 0 + + +def rank(rows): + W = [list(map(F, r)) for r in rows] + h = 0 + ncol = len(W[0]) if W else 0 + for j in range(ncol): + p = next((i for i in range(h, len(W)) if W[i][j] != 0), None) + if p is None: + continue + W[h], W[p] = W[p], W[h] + for i in range(h + 1, len(W)): + f = W[i][j] / W[h][j] + if f: + W[i] = [x - f * y for x, y in zip(W[i], W[h])] + h += 1 + return h + + +def matmul(A, B): + return [[sum(A[i][k] * B[k][j] for k in range(len(B))) for j in range(len(B[0]))] for i in range(len(A))] + + +def transpose(A): + return [list(r) for r in zip(*A)] + + +# --------------------------------------------------------------------------------------------------------------- +# Dual numbers over Fractions (forward-mode derivatives for the chart Jacobian) +# --------------------------------------------------------------------------------------------------------------- + +class Dual: + __slots__ = ("v", "g") + + def __init__(self, v, g=None): + self.v = F(v) + self.g = g or {} + + @staticmethod + def lift(x): + return x if isinstance(x, Dual) else Dual(x) + + def __add__(self, o): + o = Dual.lift(o) + g = dict(self.g) + for k, c in o.g.items(): + g[k] = g.get(k, 0) + c + return Dual(self.v + o.v, g) + + __radd__ = __add__ + + def __neg__(self): + return Dual(-self.v, {k: -c for k, c in self.g.items()}) + + def __sub__(self, o): + return self + (-Dual.lift(o)) + + def __rsub__(self, o): + return Dual.lift(o) - self + + def __mul__(self, o): + o = Dual.lift(o) + g = {k: c * o.v for k, c in self.g.items()} + for k, c in o.g.items(): + g[k] = g.get(k, 0) + c * self.v + return Dual(self.v * o.v, g) + + __rmul__ = __mul__ + + def __truediv__(self, o): + o = Dual.lift(o) + inv = Dual(1 / o.v, {k: -c / (o.v * o.v) for k, c in o.g.items()}) + return self * inv + + def __rtruediv__(self, o): + return Dual.lift(o) / self + + def __ne__(self, o): + return self.v != Dual.lift(o).v + + def __eq__(self, o): + return self.v == Dual.lift(o).v + + def __hash__(self): + return hash(self.v) + + +# --------------------------------------------------------------------------------------------------------------- +# The chart +# --------------------------------------------------------------------------------------------------------------- + +def rat(rng, lo, hi, steps=1000): + """A random rational in [lo, hi] on a grid of `steps` intervals (lo, hi may be Fractions).""" + lo, hi = F(lo), F(hi) + return lo + (hi - lo) * F(rng.randint(0, steps), steps) + + +def sample_chart(d, rng, r, k, eps=F(1, 100)): + """Chart data (sigma, v, D, tau) inside the manuscript's rare set; variables ordered (x, z, w_1..w_n).""" + n = d - 2 + D = [[F(0)] * n for _ in range(n)] + for i in range(n): + D[i][i] = -1 + rat(rng, -1 / 10, 1 / 10) + for j in range(i): + D[i][j] = D[j][i] = rat(rng, -1 / (10 * n), 1 / (10 * n)) + v = [rat(rng, -1 / (20 * n), 1 / (20 * n)) for _ in range(n)] + sigma = r * (F(-3, 2) * k + rat(rng, -eps, eps) * k) + tau = {} + for e in multi(d, 3): + tau[e] = rat(rng, -eps, eps) * k + xz, x, z = unit(d, 0), unit(d, 0), unit(d, 1) + tau[eplus(x, x, x)] = 12 * k # cubic model: pins force f_xxx = 12k exactly + tau[eplus(x, z, z)] = -2 * k + rat(rng, -eps, eps) * k + return sigma, v, D, tau + + +def shear_subs(d, q, sign=-1): + """Substitution (x, z, w) -> (x, z, w + sign*q z) as polynomials in d variables.""" + subs = [pvar(0, d), pvar(1, d)] + for j in range(d - 2): + subs.append(padd(pvar(j + 2, d), pvar(1, d, sign * q[j]))) + return subs + + +def build_physical_cubic(d, sigma, v, D, tau, r, k, b): + """Physical cubic f(x, y) with the 2(d+1) pins, transverse Hessian A = [[a, v^T], [v, D]] and physical third + derivatives T obtained from tau through the inverse shear y_w = w - q z, i.e. w = y_w + q y_z.""" + n = d - 2 + q = solve(D, v) if n else [] + a = sigma + sum(vi * qi for vi, qi in zip(v, q)) + cubic_tilde = from_jets({e: c for e, c in tau.items()}, d) + cubic_phys = pcompose(cubic_tilde, shear_subs(d, q, sign=+1), d) + T = {e: pderiv_at0(cubic_phys, e) for e in multi(d, 3)} + x = unit(d, 0) + jets = dict(T) + # transverse Hessian over y = (z, w) + A = [[a] + list(v)] + [[v[i]] + list(D[i]) for i in range(n)] + for i in range(d - 1): + for j in range(d - 1): + jets[eplus(unit(d, i + 1), unit(d, j + 1))] = A[i][j] + # pin-determined lower order jets (exact for cubic fields) + jets[(0,) * d] = b - k * r ** 3 / 2 + jets[x] = -F(3, 2) * k * r ** 2 + for j in range(1, d): + jets[unit(d, j)] = -r * r / 8 * T[eplus(x, x, unit(d, j))] + jets[eplus(x, unit(d, j))] = F(0) + jets[eplus(x, x)] = F(0) + return from_jets(jets, d), A, T, q, a + + +def hessian_at(p, pt, d): + return [[peval(pdiff(pdiff(p, i), j), pt) for j in range(d)] for i in range(d)] + + +def gradient_at(p, pt, d): + return [peval(pdiff(p, i), pt) for i in range(d)] + + +def planar_normal_form(k, s, a3, beta, c3): + """(A17) polynomial in (X, Z).""" + X, Z = pvar(0, 2), pvar(1, 2) + lin = F(0) if MUT == "drop-transverse-pin-term" else F(1, 4) + terms = [pscale(pmul(pmul(X, X), X), 2 * k), pscale(X, -F(3, 2) * k), pconst(-k / 2, 2), + pscale(pmul(Z, Z), s / 2), + pscale(pmul(padd(pmul(X, X), pconst(-lin, 2)), Z), a3 / 2), + pscale(pmul(X, pmul(Z, Z)), beta / 2), pscale(pmul(Z, pmul(Z, Z)), c3 / 6)] + return padd(*terms) + + +def scaled_plane(ftilde, d, r, b): + """F_r(X, Z) = [tilde f(rX, rZ, 0) - b] / r^3.""" + subs = [pvar(0, 2, r), pvar(1, 2, r)] + [{} for _ in range(d - 2)] + return pscale(padd(pcompose(ftilde, subs, 2), pconst(-b, 2)), 1 / r ** 3) + + +# --------------------------------------------------------------------------------------------------------------- +# CHART group +# --------------------------------------------------------------------------------------------------------------- + +def check_chart(): + out = {} + rng = random.Random(125001) + ok_cancel = True + for n in (1, 2, 3, 4): + for _ in range(3): + d = n + 2 + sigma, v, D, _ = sample_chart(d, rng, F(1, 16), F(1)) + q = solve(D, v) + a = sigma + sum(x * y for x, y in zip(v, q)) + A = [[a] + list(v)] + [[v[i]] + list(D[i]) for i in range(n)] + sgn = 1 if MUT == "shear-sign" else -1 + S = [[F(int(i == j)) for j in range(n + 1)] for i in range(n + 1)] + for i in range(n): + S[i + 1][0] = sgn * q[i] + B = matmul(transpose(S), matmul(A, S)) + want = [[sigma] + [F(0)] * n] + [[F(0)] + list(D[i]) for i in range(n)] + ok_cancel &= B == want and det(S) == 1 and det(A) == sigma * det(D) + out["schur_shear_cancels_and_det_A_equals_sigma_det_D_n1to4"] = ok_cancel + + # Full raw-chart Jacobian with dual numbers. + ok_jac = True + for d in (3, 4): + n = d - 2 + sigma, v, D, tau = sample_chart(d, rng, F(1, 16), F(1)) + names = ["sigma"] + [f"v{i}" for i in range(n)] + [f"D{i}{j}" for i in range(n) for j in range(i, n)] + cubic_labels = [e for e in multi(d, 3) if e != eplus(unit(d, 0), unit(d, 0), unit(d, 0))] + names += [f"tau{e}" for e in cubic_labels] + sd = Dual(sigma, {"sigma": F(1)}) + vd = [Dual(v[i], {f"v{i}": F(1)}) for i in range(n)] + Dd = [[None] * n for _ in range(n)] + for i in range(n): + for j in range(i, n): + Dd[i][j] = Dd[j][i] = Dual(D[i][j], {f"D{i}{j}": F(1)}) + td = {e: Dual(tau[e], {f"tau{e}": F(1)}) for e in cubic_labels} + # q = D^{-1} v with duals (Gauss-Jordan) + W = [list(Dd[i]) + [vd[i]] for i in range(n)] + for j in range(n): + piv = W[j][j] + W[j] = [x / piv for x in W[j]] + for i in range(n): + if i != j: + f = W[i][j] + W[i] = [x - f * y for x, y in zip(W[i], W[j])] + qd = [W[i][-1] for i in range(n)] + ad = sd + sum((vd[i] * qd[i] for i in range(n)), Dual(0)) + # T = substitution w -> w + q z applied to tau (dual coefficients). + cub = {e: td[e] / math.prod(factorial(x) for x in e) for e in cubic_labels} + subs = [pvar(0, d), pvar(1, d)] + [padd(pvar(j + 2, d), {unit(d, 1): qd[j]}) for j in range(n)] + phys = {} + for e, c in cub.items(): + term = {(0,) * d: c} + for i, power in enumerate(e): + for _ in range(power): + new = {} + for e1, c1 in term.items(): + for e2, c2 in subs[i].items(): + key = tuple(s + t for s, t in zip(e1, e2)) + new[key] = new.get(key, Dual(0)) + c1 * c2 + term = new + for key, c in term.items(): + phys[key] = phys.get(key, Dual(0)) + c + Td = {e: phys.get(e, Dual(0)) * math.prod(factorial(x) for x in e) for e in cubic_labels} + outputs = [ad] + vd + [Dd[i][j] for i in range(n) for j in range(i, n)] + [Td[e] for e in cubic_labels] + J = [[o.g.get(nm, F(0)) for nm in names] for o in outputs] + ok_jac &= len(J) == len(names) and det(J) == 1 + # xxx decouples: no output depends on it and it is not an input (it is pinned in U_0). + out["raw_chart_full_jacobian_is_one_d3_d4"] = ok_jac + + # Rotated-lattice unisolvence for degree <= 3 (Cayley rational orthogonal frames). + ok_uni = True + for d in (2, 3): + labels = [e for deg in range(4) for e in multi(d, deg)] + for s in ((F(1, 2),), (F(1, 3), F(2, 5), F(-1, 7))): + K = [[F(0)] * d for _ in range(d)] + idx = 0 + for i in range(d): + for j in range(i + 1, d): + K[i][j] = s[idx % len(s)] + K[j][i] = -K[i][j] + idx += 1 + I = [[F(int(i == j)) for j in range(d)] for i in range(d)] + IpK = [[I[i][j] + K[i][j] for j in range(d)] for i in range(d)] + ImK = [[I[i][j] - K[i][j] for j in range(d)] for i in range(d)] + # R = (I - K)^{-1}(I + K) + cols = [solve(ImK, [IpK[i][j] for i in range(d)]) for j in range(d)] + R = transpose(cols) + ok_uni &= matmul(transpose(R), R) == I + pts = [[sum(R[i][j] * p[j] for j in range(d)) for i in range(d)] for p in product(range(4), repeat=d)] + rows = [[math.prod(x ** a for x, a in zip(pt, e)) for e in labels] for pt in pts] + ok_uni &= rank(rows) == len(labels) == comb(d + 3, 3) + out["rotated_lattice_unisolvence_degree3"] = ok_uni + return out + + +# --------------------------------------------------------------------------------------------------------------- +# PHYSICAL group (exact cubic fields) +# --------------------------------------------------------------------------------------------------------------- + +def check_physical(): + out = {} + rng = random.Random(125002) + k, b = F(6, 5), F(1, 3) + res = {key: True for key in ("pins", "shear_recovers_sigma_D_tau", "normal_form_A17_exact", "endpoint_blocks_A20", + "schur_det_inertia_A21_A22", "gradient_pin_average_A24", "Hu_order_r", + "weight_order_r4")} + for d in (3, 4, 5): + n = d - 2 + for r in (F(1, 8), F(1, 32)): + sigma, v, D, tau = sample_chart(d, rng, r, k) + f, A, T, q, a = build_physical_cubic(d, sigma, v, D, tau, r, k, b) + M = [-r / 2] + [F(0)] * (d - 1) + S = [r / 2] + [F(0)] * (d - 1) + res["pins"] &= (peval(f, M) == b and peval(f, S) == b - k * r ** 3 + and all(g == 0 for g in gradient_at(f, M, d) + gradient_at(f, S, d))) + ft = pcompose(f, shear_subs(d, q, sign=+1 if MUT == "shear-sign" else -1), d) + Ht0 = hessian_at(ft, [F(0)] * d, d) + rec = (Ht0[1][1] == sigma and all(Ht0[1][j + 2] == 0 for j in range(n)) + and all(Ht0[i + 2][j + 2] == D[i][j] for i in range(n) for j in range(n)) + and all(pderiv_at0(ft, e) == tau[e] for e in multi(d, 3))) + res["shear_recovers_sigma_D_tau"] &= rec + # (A17): exact for cubic fields. + s_coef = (a if MUT == "raw-a-in-plane" else Ht0[1][1]) / r + x, z = unit(d, 0), unit(d, 1) + a3, beta, c3 = pderiv_at0(ft, eplus(x, x, z)), pderiv_at0(ft, eplus(x, z, z)), pderiv_at0(ft, eplus(z, z, z)) + Fr = scaled_plane(ft, d, r, b) + res["normal_form_A17_exact"] &= Fr == planar_normal_form(k, s_coef, a3, beta, c3) + # Endpoint blocks in the (x, z; w) shear frame. + P = planar_normal_form(k, Ht0[1][1] / r, a3, beta, c3) + dets = [] + for sgn, pt in ((-1, M), (1, S)): + H = hessian_at(ft, pt, d) + Xs = F(sgn, 2) + Pi = [[peval(pdiff(pdiff(P, i), j), [Xs, F(0)]) for j in range(2)] for i in range(2)] + soft = [[H[i][j] for j in range(2)] for i in range(2)] + C = [[H[i][j + 2] for j in range(n)] for i in range(2)] + Di = [[H[i + 2][j + 2] for j in range(n)] for i in range(n)] + ok20 = soft == [[r * Pi[i][j] for j in range(2)] for i in range(2)] + xxw = [pderiv_at0(ft, eplus(x, x, unit(d, j + 2))) for j in range(n)] + xzw = [pderiv_at0(ft, eplus(x, z, unit(d, j + 2))) for j in range(n)] + ok20 &= C == [[sgn * r / 2 * c for c in xxw], [sgn * r / 2 * c for c in xzw]] + ok20 &= all(Di[i][j] == D[i][j] + sgn * r / 2 * pderiv_at0(ft, eplus(x, unit(d, i + 2), unit(d, j + 2))) + for i in range(n) for j in range(n)) + res["endpoint_blocks_A20"] &= ok20 + # Schur complement K_i = soft - C D_i^{-1} C^T + DinvCT = transpose([solve(Di, [C[i][j] for j in range(n)]) for i in range(2)]) + corr = matmul(C, DinvCT) + if MUT == "no-cross-schur": + corr = [[F(0)] * 2 for _ in range(2)] + K = [[soft[i][j] - corr[i][j] for j in range(2)] for i in range(2)] + Hphys = hessian_at(f, pt, d) + ok22 = det(Hphys) == det(H) == det(Di) * det(K) + negD, _, _ = inertia(Di) + negK, posK, zK = inertia(K) + negH, posH, zH = inertia(Hphys) + ok22 &= negD == n and zK == 0 and zH == 0 and negH == negD + negK + ok22 &= (negH == d) if sgn < 0 else (negH == d - 1) + # K/r - P_i = O(r): exact size check against the explicit bound |C|^2 |D_i^{-1}| / r + ok22 &= max(abs(K[i][j] / r - Pi[i][j]) for i in range(2) for j in range(2)) <= r * k + res["schur_det_inertia_A21_A22"] &= ok22 + dets.append(abs(det(Hphys))) + # H_i u = O(r): H(0) u = 0 exactly by pins, so H_i u = sgn (r/2) (f_xxx, f_xxy...). + Hu = [Hphys[i][0] for i in range(d)] + third = [pderiv_at0(f, eplus(x, x, unit(d, i))) for i in range(d)] + res["Hu_order_r"] &= Hu == [sgn * r / 2 * c for c in third] + res["weight_order_r4"] &= (dets[0] * dets[1] / r ** (8 if MUT == "weight-2d" else 4)) > F(1, 1000) + # Gradient-pin average: r * int_{-1/2}^{1/2} H(t r u) u dt = grad f(S) - grad f(M) = 0. + t = pvar(0, 1) + line = [pscale(t, r)] + [{} for _ in range(d - 1)] + avg = [] + for i in range(d): + col = pcompose(pdiff(pdiff(f, i), 0), line, 1) + prim = {(e[0] + 1,): c / (e[0] + 1) for e, c in col.items()} + avg.append(r * (peval(prim, [F(1, 2)]) - peval(prim, [F(-1, 2)]))) + res["gradient_pin_average_A24"] &= all(v_ == 0 for v_ in avg) + out.update(res) + return out + + +# --------------------------------------------------------------------------------------------------------------- +# QUARTIC group: pins re-solved through the contact frame, O(r) remainder +# --------------------------------------------------------------------------------------------------------------- + +def build_quartic(d, rng, r, k, b, sigma, v, D, tau, quartic): + """Physical quartic field: free jets (transverse Hessian, third derivatives except xxx) from the chart, a fixed + quartic part, and the 2(d+1) U_0 jets (f, f_x, f_xx, f_xxx, f_y, f_xy) solved from the pins.""" + n = d - 2 + q = solve(D, v) if n else [] + a = sigma + sum(vi * qi for vi, qi in zip(v, q)) + x = unit(d, 0) + tau_free = {e: c for e, c in tau.items() if e != eplus(x, x, x)} + cubic_phys = pcompose(from_jets(tau_free, d), shear_subs(d, q, sign=+1), d) + base = padd(cubic_phys, quartic) + A = [[a] + list(v)] + [[v[i]] + list(D[i]) for i in range(n)] + for i in range(d - 1): + for j in range(i, d - 1): + e = eplus(unit(d, i + 1), unit(d, j + 1)) + base = padd(base, {e: A[i][j] / math.prod(factorial(t) for t in e)}) + U0 = [(0,) * d, x, eplus(x, x), eplus(x, x, x)] + for j in range(1, d): + U0 += [unit(d, j), eplus(x, unit(d, j))] + basis = [from_jets({e: 1}, d) for e in U0] + M = [-r / 2] + [F(0)] * (d - 1) + S = [r / 2] + [F(0)] * (d - 1) + rows, rhs = [], [] + for pt, val in ((M, b), (S, b - k * r ** 3)): + rows.append([peval(p, pt) for p in basis]) + rhs.append(val - peval(base, pt)) + for pt in (M, S): + for i in range(d): + rows.append([peval(pdiff(p, i), pt) for p in basis]) + rhs.append(-peval(pdiff(base, i), pt)) + frame_det = det(rows) + coeffs = solve(rows, rhs) + f = padd(base, *[pscale(p, c) for p, c in zip(basis, coeffs)]) + return f, q, frame_det + + +def random_quartic(d, rng, size): + return {e: rat(rng, -size, size) for e in multi(d, 4)} + + +def check_quartic(): + out = {} + rng = random.Random(125003) + k, b = F(6, 5), F(1, 3) + ok_frame = ok_pins = True + rates = {} + hu_rates = {} + grid = [F(i, 4) for i in range(-8, 9)] + for d in (3, 4): + quartic = random_quartic(d, rng, F(1, 2)) + base_rng_state = rng.getstate() + errs, hus = [], [] + for r in (F(1, 8), F(1, 16), F(1, 32), F(1, 64)): + rng.setstate(base_rng_state) + sigma, v, D, tau = sample_chart(d, rng, r, k) + f, q, frame_det = build_quartic(d, rng, r, k, b, sigma, v, D, tau, quartic) + ok_frame &= frame_det != 0 + M = [-r / 2] + [F(0)] * (d - 1) + S = [r / 2] + [F(0)] * (d - 1) + ok_pins &= (peval(f, M) == b and peval(f, S) == b - k * r ** 3 + and all(g == 0 for g in gradient_at(f, M, d) + gradient_at(f, S, d))) + ft = pcompose(f, shear_subs(d, q), d) + x, z = unit(d, 0), unit(d, 1) + s_coef = hessian_at(ft, [F(0)] * d, d)[1][1] / r + P = planar_normal_form(k, s_coef, pderiv_at0(ft, eplus(x, x, z)), pderiv_at0(ft, eplus(x, z, z)), + pderiv_at0(ft, eplus(z, z, z))) + Fr = scaled_plane(ft, d, r, b) + diff = padd(Fr, pscale(P, -1)) + errs.append(max(abs(peval(diff, [X, Z])) for X in grid for Z in grid if X * X + Z * Z <= 9)) + Hs = hessian_at(f, S, d) + hus.append(max(abs(Hs[i][0]) for i in range(d))) + rates[d] = [float(errs[i] / errs[i + 1]) for i in range(3)] + hu_rates[d] = [float(hus[i] / hus[i + 1]) for i in range(3)] + out["contact_frame_nonsingular"] = ok_frame + out["pins_exact_after_solve"] = ok_pins + out["A17_remainder_halves_with_r"] = all(1.6 < x_ < 2.4 for rs in rates.values() for x_ in rs) + out["Hu_halves_with_r"] = all(1.6 < x_ < 2.4 for rs in hu_rates.values() for x_ in rs) + out["_rates"] = {"A17_remainder": {str(d_): [round(x_, 4) for x_ in v_] for d_, v_ in rates.items()}, + "H_S_u": {str(d_): [round(x_, 4) for x_ in v_] for d_, v_ in hu_rates.items()}} + return out + + +# --------------------------------------------------------------------------------------------------------------- +# SADDLES group (NUMERIC) +# --------------------------------------------------------------------------------------------------------------- + +def to_float_poly(p): + return {e: float(c) for e, c in p.items()} + + +def fl_eval(p, pt): + return sum(c * math.prod(x ** k_ for x, k_ in zip(pt, e)) for e, c in p.items()) + + +def lin_solve_float(A, b): + n = len(A) + W = [list(A[i]) + [b[i]] for i in range(n)] + for j in range(n): + p = max(range(j, n), key=lambda i: abs(W[i][j])) + W[j], W[p] = W[p], W[j] + for i in range(n): + if i != j: + f = W[i][j] / W[j][j] + W[i] = [x - f * y for x, y in zip(W[i], W[j])] + return [W[i][-1] / W[i][i] for i in range(n)] + + +def float_inertia(A): + n = len(A) + W = [list(r) for r in A] + neg = 0 + for j in range(n): + piv = W[j][j] + if piv == 0: + return None + neg += piv < 0 + for i in range(j + 1, n): + f = W[i][j] / piv + for l in range(j, n): + W[i][l] -= f * W[j][l] + return neg + + +def newton(grad, hess, x0, steps=60): + x = list(x0) + for _ in range(steps): + g = [fl_eval(p, x) for p in grad] + H = [[fl_eval(p, x) for p in row] for row in hess] + dx = lin_solve_float(H, [-t for t in g]) + x = [a + b for a, b in zip(x, dx)] + if max(abs(t) for t in dx) < 1e-15: + break + return x + + +def check_saddles(): + out = {} + rng = random.Random(125004) + k, b = F(6, 5), F(1, 3) + ok_exist = ok_index = ok_height = ok_distinct = ok_not_planar = True + conv = {} + for d in (3, 4): + n = d - 2 + quartic = random_quartic(d, rng, F(1, 2)) + state = rng.getstate() + errs = [] + for r in (F(1, 16), F(1, 32), F(1, 64), F(1, 128)): + rng.setstate(state) + sigma, v, D, tau = sample_chart(d, rng, r, k) + f, q, _ = build_quartic(d, rng, r, k, b, sigma, v, D, tau, quartic) + ft = pcompose(f, shear_subs(d, q), d) + x, z = unit(d, 0), unit(d, 1) + s_coef = hessian_at(ft, [F(0)] * d, d)[1][1] / r + P = planar_normal_form(k, s_coef, pderiv_at0(ft, eplus(x, x, z)), pderiv_at0(ft, eplus(x, z, z)), + pderiv_at0(ft, eplus(z, z, z))) + Pf = to_float_poly(P) + gP = [to_float_poly(pdiff(P, i)) for i in range(2)] + hP = [[to_float_poly(pdiff(pdiff(P, i), j)) for j in range(2)] for i in range(2)] + ftf = to_float_poly(ft) + g = [to_float_poly(pdiff(ft, i)) for i in range(d)] + h = [[to_float_poly(pdiff(pdiff(ft, i), j)) for j in range(d)] for i in range(d)] + # stable quadratic Q(X, Z) of (A28) from the actual sheared third derivatives + Qs = [] + for j in range(n): + wj = unit(d, j + 2) + t_xx, t_xz, t_zz = (pderiv_at0(ft, eplus(x, x, wj)), pderiv_at0(ft, eplus(x, z, wj)), + pderiv_at0(ft, eplus(z, z, wj))) + Qs.append((float(t_xx), float(t_xz), float(t_zz))) + Df = [[float(D[i][j]) for j in range(n)] for i in range(n)] + rf = float(r) + pts = [] + for sgnZ in (1, -1): + p = newton(gP, hP, [-0.75, sgnZ * math.sqrt(15 / 8)]) + Qp = [t0 / 2 * (p[0] ** 2 - 0.25) + t1 * p[0] * p[1] + t2 / 2 * p[1] ** 2 for (t0, t1, t2) in Qs] + Wstar = lin_solve_float(Df, [-t for t in Qp]) + # the planar restriction's critical point is not a full critical point + grad_w_planar = [fl_eval(g[j + 2], [rf * p[0], rf * p[1]] + [0.0] * n) / rf ** 2 for j in range(n)] + if MUT == "planar-point-is-critical": + ok_not_planar &= max(abs(t) for t in grad_w_planar) < 1e-12 + else: + ok_not_planar &= max(abs(t) for t in grad_w_planar) > 1e-4 + scale_w = rf if MUT == "stable-scale-r" else rf ** 2 + x0 = [rf * p[0], rf * p[1]] + [rf ** 2 * t for t in Wstar] + sol = newton(g, h, x0) + gn = max(abs(fl_eval(gi, sol)) for gi in g) + ok_exist &= gn < 1e-15 and math.dist(sol[:2], x0[:2]) < 8 * rf ** 2 # O(r) shift in scaled units + H = [[fl_eval(hij, sol) for hij in row] for row in h] + ok_index &= float_inertia(H) == d - 1 + height = fl_eval(ftf, sol) + ok_height &= float(b) - float(k) * rf ** 3 < height < float(b) + Wn = [t / scale_w for t in sol[2:]] + errs.append(max(abs(a_ - b_) for a_, b_ in zip(Wn, Wstar)) / rf) + pts.append(sol) + ok_distinct &= math.dist(pts[0], pts[1]) > 0.5 * rf and all( + math.dist(pp, [s_ * rf / 2] + [0.0] * (d - 1)) > 0.5 * rf for pp in pts for s_ in (-1, 1)) + conv[d] = errs + # |w/r^2 - W*| = O(r): the normalized error |w/r^2 - W*| / r stays within a factor 2 over r = 1/16 ... 1/128, + # separately for the + and - saddle (entries alternate + / - per r). + ratios = {d_: [max(e[i::2]) / min(e[i::2]) for i in (0, 1)] for d_, e in conv.items()} + out["two_extra_critical_points_exist"] = ok_exist + out["index_d_minus_1"] = ok_index + out["heights_inside_window"] = ok_height + out["distinct_from_each_other_and_pins"] = ok_distinct + out["planar_critical_point_not_full_critical"] = ok_not_planar + out["stable_displacement_W_converges_at_rate_r"] = all(x_ < 2 for rs in ratios.values() for x_ in rs) + out["_ratios"] = {str(d_): [round(x_, 4) for x_ in rs] for d_, rs in ratios.items()} + return out + + +# --------------------------------------------------------------------------------------------------------------- +# PATH and LEDGER groups +# --------------------------------------------------------------------------------------------------------------- + +def check_path(): + k = F(1) + G = planar_normal_form(k, F(-3, 2), F(0), F(-2), F(0)) + t = pvar(0, 1) + segs = [((F(-1, 2), F(0)), (F(-3, 4), F(0))), ((F(-3, 4), F(0)), (F(-3, 4), F(9, 4))), + ((F(-3, 4), F(9, 4)), (F(-1), F(9, 4)))] + want = [{(2,): F(-3, 16), (3,): F(-1, 32)}, {(0,): F(-7, 32)}, + {(0,): F(-7, 32), (1,): F(51, 64), (2,): F(-9, 32), (3,): F(-1, 32)}] + ok = True + for (p0, p1), w in zip(segs, want): + line = [padd(pconst(p0[i], 1), pscale(t, p1[i] - p0[i])) for i in range(2)] + ok &= pcompose(G, line, 1) == w + ok &= max(p0[0] ** 2 + p0[1] ** 2, p1[0] ** 2 + p1[1] ** 2) <= F(97, 16) < 9 + d3 = {(0,): F(51, 64), (1,): F(-9, 16), (2,): F(-3, 32)} + ok &= min(peval(d3, [F(i, 64)]) for i in range(65)) >= F(9, 64) and peval(d3, [F(1)]) == F(9, 64) + ok &= F(-7, 32) - F(1, 64) > F(-1, 4) and F(17, 64) - F(1, 64) == F(1, 4) + ok &= peval(G, [F(-1, 2), F(0)]) == 0 and peval(G, [F(1, 2), F(0)]) == -1 + # extra saddles of G + Z2 = F(15, 8) + gx = pdiff(G, 0) + ok &= peval(gx, [F(-3, 4), F(0)]) + (-Z2) == 0 # G_X = 6X^2 - 3/2 - Z^2 at X=-3/4 vanishes iff Z^2 = 15/8 + ok &= F(3, 2) + 2 * F(-3, 4) == 0 # G_Z = -Z(3/2 + 2X) vanishes at X = -3/4 + ok &= 2 * F(-3, 4) ** 3 - F(3, 2) * F(-3, 4) - F(1, 2) - (F(3, 4) + F(-3, 4)) * Z2 == F(-7, 32) + ok &= 12 * F(-3, 4) * 0 - 4 * Z2 == F(-15, 2) # det [[-9, -2Z], [-2Z, 0]] = -4 Z^2 + ok &= F(9, 16) + Z2 < 9 + hm = [[peval(pdiff(pdiff(G, i), j), [F(-1, 2), F(0)]) for j in range(2)] for i in range(2)] + hs = [[peval(pdiff(pdiff(G, i), j), [F(1, 2), F(0)]) for j in range(2)] for i in range(2)] + ok &= hm == [[-6, 0], [0, F(-1, 2)]] and hs == [[6, 0], [0, F(-5, 2)]] + return {"path_segments_margins_and_saddle_data": ok} + + +def check_ledger(): + out = {} + ok = True + for d in range(2, 13): + m = d - 1 + U = 2 * (d + 1) + J = m * (m + 1) // 2 + comb(d + 2, 3) - 1 + ok &= U + J == comb(d + 3, 3) + out["jet_count_U0_plus_J_is_binom_d3_3"] = ok + rare, weight, norm = 1, (2 * 4 if MUT == "weight-2d" else 4), 2 + out["ledger_r_r4_over_r2_is_r3_all_d"] = rare + weight - norm == 3 + # ell = k r^3 at fixed k: r dr = (1/3) ell^(-1/3) k^(-2/3) d ell; times (1 - p) ~ r^3 = ell/k. + r_exp = F(1, 3) # r = ell^(1/3) k^(-1/3) + jac_exp_ell = r_exp - 1 + jac_exp_k = -r_exp + measure_ell = (0 if MUT == "density-dr" else r_exp) + jac_exp_ell + measure_k = (0 if MUT == "density-dr" else -r_exp) + jac_exp_k + loss_ell, loss_k = measure_ell + 1, measure_k - 1 + out["density_loss_ell_2_3_k_minus_5_3"] = (measure_ell, measure_k, loss_ell, loss_k) == ( + F(-1, 3), F(-2, 3), F(2, 3), F(-5, 3)) + threshold = F(2, 3) if MUT == "threshold-two-thirds" else loss_ell + 1 + ok_t = threshold == F(5, 3) + for p in (F(1), F(3, 2), F(8, 5)): + ok_t &= (loss_ell - p) > -1 # integrable at 0 + for p in (F(5, 3), F(2)): + ok_t &= (loss_ell - p) <= -1 # not integrable at 0 (log at 5/3) + out["inverse_moment_threshold_5_3"] = ok_t + return out + + +def flatten(d): + for k_, v_ in d.items(): + if k_.startswith("_"): + continue + 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 = {"CHART": check_chart(), "PHYSICAL": check_physical(), "QUARTIC": check_quartic(), + "SADDLES": check_saddles(), "PATH": check_path(), "LEDGER": check_ledger()} + passed = all(flatten(checks)) + print(json.dumps({"object": "CLAUDE-REVIEW-ELDER-DIMENSION-LIFT-20260928-v1", "checks": checks, + "passed": passed, + "scope": "exact chart/field identities and one labelled numerical saddle group; " + "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_pair_law_claude_20260928/RESULTS.json b/reviews/remote_pair_law_claude_20260928/RESULTS.json new file mode 100644 index 000000000..efa24bfa6 --- /dev/null +++ b/reviews/remote_pair_law_claude_20260928/RESULTS.json @@ -0,0 +1,37 @@ +{ + "checks": { + "COEFF": { + "coefficient_54_over_5_times_12_minus_4_3_is_3_40_12_2_3": true + }, + "HEIGHT": { + "beta_normalizer_9_over_10": true, + "gap_moments_R15": true, + "h_integrates_to_one": true, + "independent_uniform_mean_gap_is_one_third": true, + "marginal_and_correlation_R15": true, + "pushforward_jacobian": true, + "triangle_density_integrates_to_one": true + }, + "LEDGER": { + "delta_exponent_is_one_all_d": true, + "r_power_is_five_all_d": true + }, + "OVERLAP": { + "R10_overlap_integral_exact": true, + "envelope_s_min_1_s_minus3_is_3_over_2": true + }, + "PAIR": { + "R2_orientation_matches_exact_inertia": true, + "R8_congruence_limits_with_O_delta_error": true, + "e_to_minus_e_exchanges_ordered_indices": true, + "pair_fields_have_both_critical_points": true, + "same_index_pairs_only_at_order_delta_squared": true + }, + "WINDOW": { + "R9_z_length_is_k_minus_s3_abs_t": true + } + }, + "object": "CLAUDE-REVIEW-REMOTE-PAIR-LAW-20260928-v1", + "passed": true, + "scope": "exact finite identities only; not an analytic proof" +} diff --git a/reviews/remote_pair_law_claude_20260928/REVIEW.md b/reviews/remote_pair_law_claude_20260928/REVIEW.md new file mode 100644 index 000000000..d45accbbc --- /dev/null +++ b/reviews/remote_pair_law_claude_20260928/REVIEW.md @@ -0,0 +1,182 @@ +# Nonauthor analytic review: the leading remote factorial-pair measure and its height-gap law (Math-#116, C3) + +Scientific effect: **NONE**. This file changes no register, status, graph node, lemma flag, prize or author source. +It records a verdict on candidate C3 of `reviews/candidates_pending_20260928/CANDIDATES.md`. Integration is a +separate act. + +## Object + +| Field | Value | +|---|---| +| Object | OA-WINDOW-MULTIPLICITY-REMOTE-20260928-v1 (OpenAI / ChatGPT) | +| Branch / head | `chatgpt/window-multiplicity-laws-20260928` / `0507e3a1dbd3dede84cbeb805947c70aa16ebc36` ([Math-#116](https://github.com/d6g8k5htny-coder/Math-/pull/116)) | +| `REMOTE_PAIR_LAW.md` | Git blob `3fb602040b37158b16ba61bdfc62cc8df1ccc616`, 15878 B, SHA256 `b818a11f1abcf37616d592ecda6341b0d99365cf3ac5047bc2dbaede95da4c5e`, 325 lines | +| Consumed, on main | [RC] `frontiers/remote_collision_20260928/PROOF.md` (blob `7b48a88e…`): (3.1), (4.1)–(4.3), Lemmas 1, 2, 3, 5. [RM] `frontiers/remote_window_20260924/PROOF.md` (blob `b383bfcc…`): contact frame, (8), the §4 deterministic endpoint identities, and its full endpoint-only normalizer `Z_r/r² → z_0` (the same limit as D1 (I), reconciled in Math-#126, merged at `8224783`). | +| Request | [Owner comment 5880152796](https://github.com/d6g8k5htny-coder/Math-/pull/116#issuecomment-5880152796); claimed in [5880826796](https://github.com/d6g8k5htny-coder/Math-/pull/116#issuecomment-5880826796) | + +## 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 Lemmas 1, 2 and 5 and formula (3.1) C3 imports verbatim. I also reviewed LP Theorem A (#106), IW (#109) and C1/C2 (#123), and I reconciled D1 (#126). This review therefore checks that C3 uses [RC] correctly. It is not independent evidence for [RC] itself. [RC]'s nonauthor review is the xAI/Harper review 5342481786 on #110, which accepted its finite identities, the (3.1) mark and the Lemma 1 mechanism. | +| Author code | `algebra.py` is absent from the tree, as `PUBLICATION.json` discloses. I did not run, request or reconstruct it. | +| Independent checks | `remote_pair_review_check.py` is my own exact-rational suite, written from the markdown. It covers finite identities only. | + +## Verdicts + +| Interface (lines) | Verdict | +|---|---| +| §1 (8–26): ordered-pair count `T_ij`, `Σ T_ij = N(N−1)`; no event asymptotic inferred | **ACCEPT** | +| §3 (81–121): coupled regression on `(U_r, V_δ)`; convergence to the `(U_0, V_0)` regression; full conditional support of `(B_0, A, T)` | **ACCEPT**; see §1 below. | +| §4 (123–159): (R7) and the congruence limits (R8); `W_r/r² → w_0`; adjacency; same-index pairs are higher order | **ACCEPT**; see §2 below. | +| §5 (161–233): blow-up ledger, windows (R9), domination, fixed-Borel translation, (R10), coefficient (R11) = (R3), separated pairs, positivity and symmetry | **ACCEPT**; see §3 below. | +| **Theorem R (R4)–(R5)**: `E T_ij(E) = r⁵ ∫_E K_ij + o(r⁵)`; `K_ij > 0` iff `|i−j| = 1`; `E N_j(N_j−1) = o(r⁵)` | **ACCEPT** at the stated fixed-`E`, fixed-`ρ`, existential scope | +| **Theorem H2 (R12)–(R15)**: TV convergence of the factorial-pair height measure to `(5/9)|a−b|^{−1/3}`; Beta(2/3, 2) gap; moments | **ACCEPT**; see §4 below. | +| §7 (306–325) exclusions | **ACCEPT** as stated. They are needed: see N2. | + +No defect was found. Notes N1–N4 delimit the result without changing it. + +--- + +## §1 — the coupled conditional frame (§3) + +`V_δ` is exactly [RC] (4.1). Its `δ = 0` extension (R6) follows from the Peano form [RC] (4.2), where +`D3_δ → −(1/12)∂_e³f(x)`. + +[RC] Lemma 1 gives the covariance sandwich for `(U_r, V_δ)` on the compact parameter set, including +`r = δ = 0`. [RC] Lemma 2 gives conditional moments polynomial in `t` and a target density decaying faster than any +power of `t`. + +C3's extra step: regress one smooth field on `O_{r,δ} = (U_r, V_δ)` and let `(r, δ) → 0`. This is sound. The +regression coefficients `Cov(F(z), O)Cov(O)⁻¹` converge because every entry is an integral derivative average +against kernels that tend to point masses, and the inverse is uniformly bounded by the floor. The targets +`a_{r,δ} → (v_0, 0, 0, b, t)`. Hence convergence holds in `L^p(C^q)` on compact target sets. The mean need not +vanish, and C3 does not claim it does (line 114). + +**Full conditional support.** The functionals `(U_0, B_0)` at `0` and `(Y, A, T)` at `x`, with `|x| ≥ ρ`, are +distinct jets of order ≤ 3 at two distinct torus points. They are jointly nondegenerate. A null combination gives +`P(ω) + Q(ω)e^{iω·x} = 0` on the dual lattice. Choose a lattice direction `v` with `v·x ∉ 2πℤ`. Along each lattice +line in direction `v`, a polynomial in `n` would equal a polynomial times `e^{in v·x}`. That forces both polynomials +to vanish, so `P = Q = 0`. + +This argument is mine; the manuscript cites [RM]'s distributional argument. It gives full support of `(B_0, A, T)` +given `(U_0, Y)`. `H ↦ He` is onto `ℝ^d`, and `He` together with `A` exhausts the Hessian entries at `x`. + +## §2 — determinant limits without inverses (§4) + +(R7): on `∇f(x) = ∇f(x+δe) = 0`, +`0 = ∫_0^δ H(x+τe)e dτ = δH_x e + (δ²/2)D³f(x)[e,e,·] + O(δ³‖f‖_{C⁴})`, which is the first line. The second follows +from `H_{x'}e = H_x e + δD³f[e,e,·] + O(δ²)`. + +In a frame beginning with `e`, conjugate by `diag(δ^{−1/2}, I)`: +- the `ee` entry becomes `∓T/2 + O(δ)`; +- the cross entries are `O(√δ)`; +- the lower block is exactly `A` at `x` and `A + O(δ)` at `x'`. + +Congruence preserves inertia and multiplies determinants by `δ^{−1}`. `F_j` is continuous everywhere, including on +singular matrices: it is `|det|` times an index indicator, and `|det| → 0` at the index boundaries. Polynomial moments +then give (R8) in `L^p`. The limit product `(T²/4)(det A)²χ_ij` has index `a+1` at `x` and `a` at `x'` when `T > 0`, +which is (R2). + +The weight and normalizer limits have two separate sources. `Z_r` is [RM]'s full endpoint-only normalizer, so +`Z_r/r² → z_0` is unconditioned; it is the same limit as D1 (I). The weight limit `W_r/r² → w_0` is needed *under the +additional pair conditioning* on `V_δ`. It follows from C3 §3's coupled conditional moment bounds together with +[RM] §4's deterministic endpoint identities, which use the congruence `D_r = diag(r^{−1/2}, I)`. The unconditioned D1 +normalizer limit alone would not establish this extra-conditioned weight limit. + +Exact checks (`PAIR`) use the explicit field +`f(u,v) = (T/6)u³ − (T/4)δu² + ½vᵀAv + (u² − δu)c·v` in d = 2, 3, 4: +- `∇f` vanishes at `0` and `δe`; +- `det H/δ ∓ (T/2)det A = −δ·cᵀadj(A)c` exactly; +- the orientation rule (R2) matches the exact inertia for both signs of `T` and every index of `A`. + +The same-index remark (lines 156–159) is confirmed: `f = c·v(u² − δu) + (λ/2)v²` has `T = 0`, two saddles, and +`det = −c²δ²`, which is order `δ²`. + +## §3 — blow-up, domination, translation, coefficient (§5) + +**Ledger.** The factors are: +- polar coordinates: `δ^{d−1}`; +- the value-gradient change of variables [RC] (4.3): `δ^{−d−3}`; +- the second height `dy' = δ³dt`; +- the determinants: `δ²`. + +The δ-exponent is `(d−1) − (d+3) + 3 + 2 = 1` for every d. With `δ = rs`, `y = b − r³z` and `W/Z → w_0/z_0`, the +r-power is `d + 3 + 3 − (d+3) + 2 = 5` (`LEDGER`, d = 2…10). + +**Windows (R9).** Both heights in `(b − kr³, b)` means `0 < z < k` and `s³t < z < k + s³t`. The `z`-length is +`(k − s³|t|)_+`. This is checked exactly on 400 rational instances (`WINDOW`). + +**Domination.** [RC] Lemmas 3–4 give `W_r ≤ r²K^{2d}` and `|det H_x det H_{x'}| ≤ δ²K^{2d}/4`. [RC] Lemma 2 gives +the envelope `Cs(1+|t|)^{−p}1_{(R9)}`. Integrating over `z` and `t` gives `≤ Cs·min(1, s^{−3})`, whose integral is +finite (`∫_0^∞ s·min(1,s^{−3})ds = 3/2`). The envelope is uniform in `r` and in the compact parameters, and +zero-extension beyond `s < η_0/r` is harmless. Dominated convergence applies. + +**Fixed Borel E.** The factor `1_E(x+rse)` is removed by continuity of translation in `L¹(torus)`. On bounded `s` the +shifts are at most `rS_0`, and the envelope controls `s > S_0`. No boundary regularity is used, and none is claimed +for `r`-dependent `E_r`. The argument is correct as written (lines 193–203). + +**Coefficient.** Integrating `z` gives `(k − s³|t|)_+`. Then +`∫_0^{s_max} s(k − s³|t|) ds = (3/10)k·s_max² = (3/10)k^{5/3}|t|^{−2/3}` (R10), checked exactly (`OVERLAP`). +Multiplying by `36t²` gives `(54/5)k^{5/3}|t|^{4/3}`. With `t = −T/12`, this becomes +`(54/5)·12^{−4/3} = (3/40)·12^{2/3}`, since `54/5 = (3/40)·144` (`COEFF`). The conditional density of `t` given `Y` +converts to `E[·|Y]` with no extra Jacobian. The surface measure and the ordered-pair convention match (R3). Tonelli +away from `t = 0` is the right way to handle the `|t|^{−2/3}` factor. + +**Separated pairs.** [RC] Lemma 5 gives `O(r⁶)|E|²`, which is `o(r⁵)` for fixed `E`. + +**Positivity and symmetry.** The integrand is positive on an open set by §1. Under `e ↦ −e`, `T ↦ −T` while `A` and +`w_0` are unchanged, and the linear map on `Y` has `|det| = 1` at the symmetric target `(0,0,b)`. So +`χ_ij(A,−T) = χ_ji(A,T)` (checked), and `∫_S K_ij = ∫_S K_ji`. Hence (R5). + +## §4 — the factorial-pair height law (§6) + +(R12) is a normalized factorial-moment measure. §6 says explicitly that it is not the event-conditioned pair law, and +this review accepts only the former. + +The dominated convergence of §3 is `L¹` convergence of the blown-up nonnegative densities, not only of their masses. +Pushforward to `(θ, θ') = (z/k, (z − s³t)/k)` contracts TV, and dividing by the converging positive total mass +preserves TV convergence. + +**Jacobian.** With `g = s³|t|/k`, `s ds = (1/3)(k/|t|)^{2/3}g^{−1/3}dg`. This is checked as the exact identity +`s/(dg/ds) = k/(3s|t|)` (`HEIGHT`). With `dz = k dθ` and `θ ∈ (0, 1−g)`, each sign of `T` gives a density +proportional to `g^{−1/3}` on its triangle, of mass `∫_0^1 g^{−1/3}(1−g)dg = 9/10`. The two triangles carry equal +mass by `e ↦ −e`. + +This gives `h = (5/9)|a−b|^{−1/3}`. The index-resolved density is `(10/9)(b−a)^{−1/3}` on `a < b` for `i = j+1`: the +index-`(a+1)` point lies above its adjacent partner. The gap is Beta(2/3, 2), and the following are all exact +(`HEIGHT`): +- the CDF (R14); +- `E g^n = 10/((3n+2)(3n+5))`; +- `E g = 1/4` and `Var g = 9/176`; +- the marginal `(5/6)(a^{2/3} + (1−a)^{2/3})`; +- `E a² = 29/88`, `E ab = 3/11` and `Corr = 2/7`. + +## Notes + +- **N1.** (R3) has hidden `k`-dependence beyond `k^{5/3}`, because `Q_0` conditions on `f_xxx = 12k`. Nothing in + C3 claims otherwise. The coefficient should be read as "`k^{5/3}` times a `k`-dependent Gaussian conditional + integral". +- **N2.** The fixed exclusion `ρ` is load-bearing. [RC] Lemma 1's floor is not uniform as `ρ → 0` ([RC] §8). + Near the pins, the integrated planar LOCAL_MULTIPLICITY result gives an `r³` lower obstruction for the probability + of multiple occurrences (and a factorial *lower* bound). It does not establish an all-dimensional or global exact + `r³` factorial asymptotic. §7's exclusions are therefore required, not cosmetic. +- **N3.** A factorial-moment asymptotic does not give `Q(N ≥ 2) ~ (r⁵/2)∫ΣK` without higher factorial moments. + §7 says so, and this review adds nothing there. +- **N4.** Novelty boundary: generic adjacent-index attraction of critical points in the unconditioned isotropic + setting is prior work (Azaïs–Delmas, arXiv:1911.02300). What this review accepts is the pinned, tilted, fixed-`ρ` + coefficient (R3) and the factorial-pair height law (R13), at existential scope. + +## What this review does not do + +It does not review C4 (`REMOTE_DISTANCE_MOMENTS.md`), C5 or C6. It does not accept an event-conditioned pair law, a +global factorial upper bound, uniformity in `ρ → 0` or in oscillating `E_r`, or any numerical coefficient. It does +not run or reconstruct `algebra.py`, and it changes no register. + +## Reproduce + + python -B -S remote_pair_review_check.py # prints RESULTS.json byte for byte + python -B -O -S remote_pair_review_check.py # identical + python -B -S remote_pair_review_check.py --mutant M # exit 1 for each of the 5 mutants diff --git a/reviews/remote_pair_law_claude_20260928/SOURCE_FILES.json b/reviews/remote_pair_law_claude_20260928/SOURCE_FILES.json new file mode 100644 index 000000000..05948195f --- /dev/null +++ b/reviews/remote_pair_law_claude_20260928/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_PAIR_LAW.md", + "git_blob": "3fb602040b37158b16ba61bdfc62cc8df1ccc616", + "bytes": 15878, + "sha256": "b818a11f1abcf37616d592ecda6341b0d99365cf3ac5047bc2dbaede95da4c5e" + } + ] + }, + "files": [ + { + "path": "REVIEW.md", + "bytes": 12618, + "sha256": "b08f1cdca8e179d9910be89e37e4a03a864b8c1cbcbc6e71cd1fdc359d2a391f", + "git_blob": "d45accbbc92756c24e7eada96ddd0bea0a703c22" + }, + { + "path": "RESULTS.json", + "bytes": 1153, + "sha256": "cab1fe5b10031de837bd8064090db7f276328940fe17d668ec5b6c3645b19fa4", + "git_blob": "efa24bfa60d576063c841c4c9794761a0dbf3b71" + }, + { + "path": "remote_pair_review_check.py", + "bytes": 11665, + "sha256": "2cd9b7f06d15aa26d0c3305294ed95f210689bda52ef149e8d6a43b637dbf9ad", + "git_blob": "20bc1ae2ba45b57143a89344c2f1e6289b159526" + } + ] +} diff --git a/reviews/remote_pair_law_claude_20260928/remote_pair_review_check.py b/reviews/remote_pair_law_claude_20260928/remote_pair_review_check.py new file mode 100644 index 000000000..20bc1ae2b --- /dev/null +++ b/reviews/remote_pair_law_claude_20260928/remote_pair_review_check.py @@ -0,0 +1,247 @@ +"""Independent nonauthor checks for OA-WINDOW-MULTIPLICITY-REMOTE-20260928-v1 (Math-#116, REMOTE_PAIR_LAW.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: + + LEDGER radial and r-power ledgers of the blown-up pair Kac-Rice integral: (d-1)-(d+3)+3+2 = 1 and r^5, d = 2..10. + WINDOW (R9): for rational (z-range, s, t) the admissible z-length is exactly (k - s^3|t|)_+. + OVERLAP (R10) on exact instances with k/|t| a rational cube; the envelope integral of s*min(1, s^-3) is 3/2. + COEFF 36*(3/10) = 54/5 and (54/5)*12^(-4/3) = (3/40)*12^(2/3), i.e. 54/5 = (3/40)*144. + PAIR explicit polynomial fields in d = 2, 3, 4 with critical points at x and x + delta*e: exact congruence limits + F_i(H_x)/delta -> F_i(diag(-T/2, A)), F_j(H_x')/delta -> F_j(diag(T/2, A)) with O(delta) error, the + orientation rule (R2) for both signs of T and every index of A, the e -> -e exchange, and the negative + control: T = 0 with a mixed cubic gives two same-index points with determinants of order delta^2. + HEIGHT the pushforward Jacobian s ds = (1/3)(k/|t|)^(2/3) g^(-1/3) dg; the Beta(2/3, 2) normalization 9/10; h + integrates to 1; the index-resolved triangle density (10/9)(b-a)^(-1/3); moments (R15) and Corr = 2/7. + +Mutants (each must fail): exponent-d, chi-orientation, coefficient-power, beta-normalizer, overlap-exponent. +Not an analytic proof: the Gaussian limit, domination and translation steps are reviewed in REVIEW.md. +""" +import argparse +import json +import random +import sys +from fractions import Fraction as F + +MUTANTS = ("exponent-d", "chi-orientation", "coefficient-power", "beta-normalizer", "overlap-exponent") +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 negatives(A): + """Number of negative eigenvalues of a symmetric rational matrix (sign changes of leading minors, generic).""" + n = len(A) + minors = [F(1)] + [det([row[:k] for row in A[:k]]) for k in range(1, n + 1)] + if any(m == 0 for m in minors): + return None + return sum(1 for a, b in zip(minors, minors[1:]) if (a > 0) != (b > 0)) + + +def chi(i, j, neg_a, T): + """(R2): orientation of the adjacent pair; zero on T = 0.""" + if T == 0: + return 0 + sign = 1 if (T > 0) != (MUT == "chi-orientation") else -1 + return int((i, j) == ((neg_a + 1, neg_a) if sign > 0 else (neg_a, neg_a + 1))) + + +# --------------------------------------------------------------------------------------------------------------- + +def check_ledger(): + ok_delta = ok_r = True + for d in range(2, 11): + polar, density, second_height, dets = d - 1, -(d + 3), 3, 2 + if MUT == "exponent-d": + polar = d + ok_delta &= polar + density + second_height + dets == 1 + # r-powers with delta = r s, y = b - r^3 z: polar r^d, dy r^3, dy' = r^3 s^3 dt, density r^(-d-3), dets r^2, + # W/Z -> w0/z0 (r^2 / r^2). + ok_r &= d + 3 + 3 - (d + 3) + 2 == 5 + return {"delta_exponent_is_one_all_d": ok_delta, "r_power_is_five_all_d": ok_r} + + +def check_window(): + rng = random.Random(116301) + ok = True + for _ in range(400): + k = F(rng.randint(1, 40), rng.randint(1, 9)) + s = F(rng.randint(1, 30), rng.randint(1, 9)) + t = F(rng.randint(-60, 60), rng.randint(1, 9)) + # z in (0,k) and (z-k)/s^3 < t < z/s^3 <=> s^3 t < z < k + s^3 t + lo, hi = max(F(0), s ** 3 * t), min(k, k + s ** 3 * t) + length = max(F(0), hi - lo) + ok &= length == max(F(0), k - s ** 3 * abs(t)) + return {"R9_z_length_is_k_minus_s3_abs_t": ok} + + +def check_overlap(): + ok = True + for m in (1, 2, 3, 5): + for tt in (F(1), F(2), F(1, 3), F(7, 5)): + k = F(m) ** 3 * tt # then s_max = (k/|t|)^(1/3) = m + smax = F(m) + integral = k * smax ** 2 / 2 - tt * smax ** 5 / 5 + expo = F(1, 3) if MUT == "overlap-exponent" else F(2, 3) + # (3/10) k^(5/3) |t|^(-2/3) = (3/10) k (k/|t|)^(2/3) = (3/10) k smax^(3*expo) + ok &= integral == F(3, 10) * k * smax ** (3 * expo) + envelope = F(1, 2) + F(1) # int_0^1 s ds + int_1^inf s^-2 ds + return {"R10_overlap_integral_exact": ok, "envelope_s_min_1_s_minus3_is_3_over_2": envelope == F(3, 2)} + + +def check_coeff(): + # (54/5) 12^(-4/3) = c 12^(2/3) <=> 54/5 = c 12^2 ; mutant uses 12^(-2/3) on the right, i.e. 54/5 = c 12^(2/3+2/3) + power = F(2) if MUT != "coefficient-power" else F(4, 3) + c = F(3, 40) + ok = F(36) * F(3, 10) == F(54, 5) and (power.denominator == 1 and F(54, 5) == c * 12 ** int(power)) + return {"coefficient_54_over_5_times_12_minus_4_3_is_3_40_12_2_3": ok} + + +def pair_field_hessians(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). + grad f vanishes at (0,0) and (delta,0); returns the two Hessians and the gradients there.""" + 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] + return hess(F(0)), hess(delta), grad(F(0)), grad(delta) + + +def check_pair(): + rng = random.Random(116302) + ok_crit = ok_limit = ok_orient = ok_swap = True + for d in (2, 3, 4): + n = d - 1 + for trial in range(12): + # A diagonal-dominant with a chosen number of negative eigenvalues + a_neg = trial % (n + 1) + A = [[F(0)] * n for _ in range(n)] + for i in range(n): + A[i][i] = F(-(i + 2)) if i < a_neg else F(i + 2) + for j in range(i): + A[i][j] = A[j][i] = F(rng.randint(-2, 2), 10) + if negatives(A) != a_neg: + continue + c = [F(rng.randint(-9, 9), 7) for _ in range(n)] + T = F(rng.choice([-1, 1]) * rng.randint(1, 20), 3) + detA = det(A) + errs = [] + for delta in (F(1, 10), F(1, 100), F(1, 1000)): + Hx, Hy, gx, gy = pair_field_hessians(T, A, c, delta) + ok_crit &= all(v == 0 for v in gx + gy) + # exact: det H / delta -/+ (T/2) det A = -delta c^T adj(A) c, so (error / delta) is delta-independent + errs.append(((det(Hx) / delta - (-T / 2) * detA) / delta, (det(Hy) / delta - (T / 2) * detA) / delta)) + nx, ny = negatives(Hx), negatives(Hy) + if nx is not None and ny is not None: + ok_orient &= all(chi(i, j, a_neg, T) == int((i, j) == (nx, ny)) + for i in range(d + 1) for j in range(d + 1)) + # the limit error is exactly linear in delta, with the same slope at both witnesses + ok_limit &= len(set(errs)) == 1 and errs[0][0] == errs[0][1] + # e -> -e flips T and exchanges the ordered indices + ok_swap &= all(chi(i, j, a_neg, -T) == chi(j, i, a_neg, T) for i in range(d + 1) for j in range(d + 1)) + # Negative control: T = 0 and a mixed cubic give two same-index points with det of order delta^2. + ok_neg = 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_neg &= det(H0) == det(H1) == -(cc * delta) ** 2 + ok_neg &= det(H0) / delta ** 2 == -cc * cc # order delta^2, so zero at the delta^1 scale of (R8) + return {"pair_fields_have_both_critical_points": ok_crit, + "R8_congruence_limits_with_O_delta_error": ok_limit, + "R2_orientation_matches_exact_inertia": ok_orient, + "e_to_minus_e_exchanges_ordered_indices": ok_swap, + "same_index_pairs_only_at_order_delta_squared": ok_neg} + + +def check_height(): + out = {} + # pushforward Jacobian on rational points: s ds/dg = k/(3 s |t|) equals (1/3)(k/|t|)^(2/3) g^(-1/3), g = s^3|t|/k. + ok = True + for s, tt, k in ((F(2), F(1), F(8)), (F(3, 2), F(4, 3), F(9, 4)), (F(1, 2), F(5), F(5, 8))): + g = s ** 3 * tt / k + lhs = s / (3 * s * s * tt / k) # s / (dg/ds) + # (k/|t|)^(2/3) g^(-1/3) = (k/|t|)^(2/3) (k/(s^3 |t|))^(1/3) = (k/|t|) / s + rhs = F(1, 3) * (k / tt) / s + ok &= lhs == rhs + out["pushforward_jacobian"] = ok + # int_0^1 g^(-1/3) (1-g) dg = 3/2 - 3/5 = 9/10 + norm = F(3, 2) - F(3, 5) + target = F(1) if MUT == "beta-normalizer" else F(9, 10) + out["beta_normalizer_9_over_10"] = norm == F(9, 10) and norm == target + # h(a,b) = (5/9)|a-b|^(-1/3) integrates to 1: 2 * int_0^1 int_0^b (b-a)^(-1/3) da db = 2 * (3/2)(3/5) + out["h_integrates_to_one"] = F(5, 9) * 2 * F(3, 2) * F(3, 5) == 1 + # index-resolved triangle density (10/9)(b-a)^(-1/3) on a= 1 and rational q > 0: B(p,q) = (p-1)! / (q (q+1) ... (q+p-1)).""" + assert p.denominator == 1 and p >= 1 + out = F(1) + for i in range(int(p) - 1): + out *= F(i + 1) + den = F(1) + for i in range(int(p)): + den *= (q + i) + return out / den + + +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(), "WINDOW": check_window(), "OVERLAP": check_overlap(), "COEFF": check_coeff(), + "PAIR": check_pair(), "HEIGHT": check_height()} + passed = all(flatten(checks)) + print(json.dumps({"object": "CLAUDE-REVIEW-REMOTE-PAIR-LAW-20260928-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())