diff --git a/.github/workflows/remote-height-decoupling.yml b/.github/workflows/remote-height-decoupling.yml new file mode 100644 index 000000000..52ab5b906 --- /dev/null +++ b/.github/workflows/remote-height-decoupling.yml @@ -0,0 +1,30 @@ +name: Remote within-window height-decoupling controls + +'on': + pull_request: + paths: + - 'frontiers/remote_height_decoupling_20260928/**' + - '.github/workflows/remote-height-decoupling.yml' + workflow_dispatch: + +permissions: + contents: read + +jobs: + exact-height: + runs-on: ubuntu-latest + timeout-minutes: 10 + steps: + - uses: actions/checkout@11d5960a326750d5838078e36cf38b85af677262 + with: + persist-credentials: false + - uses: actions/setup-python@a26af69be951a213d495a4c3e4e4022e16d87065 + with: + python-version: '3.11.16' + - name: Verify exact sources and both-mode semantic controls + env: + PYTHONDONTWRITEBYTECODE: '1' + run: | + set -euo pipefail + python -B -S frontiers/remote_height_decoupling_20260928/verify.py + git diff --exit-code diff --git a/frontiers/remote_height_decoupling_20260928/PROOF.md b/frontiers/remote_height_decoupling_20260928/PROOF.md new file mode 100644 index 000000000..4d7af587d --- /dev/null +++ b/frontiers/remote_height_decoupling_20260928/PROOF.md @@ -0,0 +1,284 @@ +# Faster within-window height decoupling at fixed remote separation + +Object: OA-REMOTE-HEIGHT-DECOUPLING-20260928-v1. +Author: OpenAI / ChatGPT, foreground continuation, 28 September 2026. +Disposition: AUTHOR-SIDE PROOF CANDIDATE; source-bound nonauthor review required. +Scientific effect NONE. No parent source, verdict, graph or scientific status changes. + +## 1. Precise improvement and inputs + +Use the exact fixed-remote setting of RM and RC in SOURCE_MAP.json: the normalized +periodic Gaussian field on the fixed d-dimensional torus, d>=2, fixed rho>0, +compact birth marks b and gap marks 0=1, is within O(r^2) of a +single point with location/index law pi_{r,1} and independent uniform theta. +A measurable point-selection rule on nonempty configurations which returns the +unique point when N_r=1 has the same O(r^2) height-uniformity and own-marginal +independence conclusions. This is not an assertion that a finite-r location and +index are mutually independent. + +The full joint law compared to the LIMITING contact profile pi_E tensor lambda +remains O(r), as before. The stronger height/decoupling estimates do not supply +a faster location-profile convergence rate or a height law for persistence +partners. No numerical C or cutoff, global/no-rho statement, or optimal Gaussian +rate is claimed. + +### Exact imported premises + +RM Sections 2-5 supply the uniform positive covariance sandwich for the transformed +pins U_r plus Y_x=(grad f(x),f(x)), all fixed C^q Gaussian regression moments, +the filtered-determinant estimate (8), Z_r/r^2 bounded above and away from zero, +and the full pre-height-integrated density + + R_{r,j}(x,h)=p_{Y_x|U_r=v_r}(0,h) + E[W_r F_j(H_x)|U_r=v_r,Y_x=(0,h)]/Z_r. (H5) + +Its pointwise contact comparison and positive contact kernels give + + c r^3 |E| <= m_r <= C r^3 |E|. (H6) + +RC Corollary D supplies q_r<=C r^5 |E|. These premises concern the same fixed +remote law and all indices. They are not imported from a global cap event or +from a probability bound in the wrong direction. The new work below is a +same-r comparison in the actual height h, retaining the homogeneous endpoint +constraints so that division by Z_r does not lose r^2. + +## 2. Height regression changes along a smooth homogeneous-pin direction + +Fix r,x and all endpoint marks/frames. Order V_r=(U_r,grad f(x),f(x)), and let e_h +be the target coordinate vector for its last entry. With one unconditioned field +F, use RM's Gaussian regression realization for each height target h: + + F_h(z)=F(z)+Cov(F(z),V_r) Sigma_r^{-1}(a_h-V_r), + a_h=(v_r,0,h), Sigma_r=Cov(V_r). + +For h,h' in the closed between-pin interval this gives the exact pathwise identity + + F_h-F_{h'}=(h-h') g_{r,x}, + g_{r,x}(z)=Cov(F(z),V_r) Sigma_r^{-1} e_h. (H7) + +All fixed derivatives of the cross-covariance in z are uniformly bounded, by +Cauchy-Schwarz and the smooth field's uniform derivative variances. The inverse +covariance is uniformly bounded by RM Section 2. Thus for each fixed q, + + ||g_{r,x}||_{C^q} <= C_q. (H8) + +Applying the observation vector V_r to g_{r,x} gives Sigma_r Sigma_r^{-1}e_h=e_h. +Therefore U_r g=0, grad g(x)=0 and g(x)=1. Since the transformed U_r is invertible +as a re-expression of the ORIGINAL endpoint observations for r>0, + + g(M)=g(S)=0, grad g(M)=grad g(S)=0. (H9) + +This step uses the same exact pin law, not contact pins substituted at finite r. +The direction is deterministic; the conditioned Gaussian residual is shared. +All field supremum moments are uniform over h,h' by RM's extra-height regression +argument. No independence of endpoint and witness Hessians is asserted. + +## 3. The vanishing endpoint columns survive the height comparison + +For any smooth g with both gradient pins zero, the average of D^2g u over the +endpoint segment vanishes. At either endpoint i, + + ||D^2g(i)u|| + <= (1/r) integral_0^r t dt * ||D^3g||_infinity + = (r/2)||D^3g||_infinity. (H10) + +For M, subtract D^2g(M+tu)u from D^2g(M)u inside its zero-average integral; +for S reverse the segment. This is a vector integral identity, not an unjustified +simultaneous vector Rolle point. + +For each conditioned F_h define its endpoint blocks as in RM Section 4: + + H_i(h)=[[r alpha_i(h), r beta_i(h)^T], + [r beta_i(h), A_i(h)]], + K_i(h)=[[alpha_i(h), sqrt(r) beta_i(h)^T], + [sqrt(r) beta_i(h), A_i(h)]]. + +Equations (H7)-(H10) give, uniformly in small r, + + |alpha_i(h)-alpha_i(h')|+||beta_i(h)-beta_i(h')|| + <= C|h-h'|, + ||A_i(h)-A_i(h')|| <= C|h-h'|, + ||K_i(h)-K_i(h')||+||H_x(h)-H_x(h')|| <= C|h-h'|. (H11) + +The normalizations alpha=f_uu/r and beta=grad_perp f_u/r therefore do NOT cause +an r^-1 loss. Every matrix in (H11) has moments of all fixed orders uniformly in +h, by the gradient-pin bounds and the extra-conditioned Gaussian moments. + +Positive congruence gives exactly, including at singular Hessians, + + W_r(F_h)/r^2 = F_d(K_M(h)) F_(d-1)(K_S(h)). (H12) + +## 4. Uniform Lipschitz continuity of the full height density + +The deterministic estimate in RM (8) is + + |F_j(A)-F_j(B)| + <= d max(||A||,||B||)^(d-1)||A-B||. (H13) + +It concerns the determinant TIMES the index indicator, not the indicator alone. +Across index changes the matrix segment reaches determinant zero, so this bound +does not require eigenvalues bounded away from zero. + +Apply (H13), (H11), and the product difference identity to the three factors in + + T_h=F_d(K_M(h))F_(d-1)(K_S(h))F_j(H_x(h)). + +Hölder and the uniform moments give + + |E T_h-E T_{h'}| <= E|T_h-T_{h'}| <= C|h-h'|, + sup_h E|T_h| <= C. (H14) + +The conditional Gaussian density p_{Y_x|U_r=v_r}(0,h) and its first h derivative +are uniformly bounded on this compact target/covariance domain. Its difference +is at most C|h-h'|. Multiply (H14) by this density and by r^2/Z_r, which is bounded +and does NOT depend on the additional witness height h. Equation (H5) yields + + |R_{r,j}(x,h)-R_{r,j}(x,h')| <= L |h-h'| (H15) + +with L uniform over remote x, compact endpoint marks/frames and small r. +This is stronger for within-window variation than comparing each height to the +contact kernel with an O(r) error. No derivative of a discontinuous index +indicator or differentiation under an unbounded expectation is being used. + +## 5. Exact finite-r mean decoupling and its third-order rate + +The finite measure form of weighted Kac-Rice in RM gives, after h=b-l theta, + + mu_r(dx,{j},dtheta)=l R_{r,j}(x,b-l theta) dx dtheta. (H16) + +Write Rbar_{r,j}(x)=integral_0^1 R_{r,j}(x,b-l t)dt. The location/index marginal +of mu_r has density l Rbar. By (H15), + + integral_0^1 |R(x,b-l theta)-Rbar(x)| dtheta + <= L l integral_0^1 integral_0^1 |theta-t| dt dtheta + = L l/3. + +Sum over the d+1 indices and integrate over E. The FULL variation estimate is + + ||mu_r - mu_r^Y tensor lambda||_var + <= (d+1)L l^2 |E|/3 <= C r^6 |E|. (H17) + +Both measures have the SAME mass m_r. Divide by 2m_r and use (H6), obtaining (H1). +Unlike a comparison with the limiting contact profile, there is no normalization +error between two different total masses. The volume factor cancels even when +E_r varies and tends to zero in volume. A zero-volume E has no conditional law +and is explicitly excluded. + +## 6. Conditional singleton law and physical-height moments + +Let sigma be the expected marked measure restricted to N_r=1, of mass p_1. +Let eta be the mean marked measure on N_r>=2, of mass a=E[N_r;N_r>=2]. Then + + mu_r=sigma+eta, m_r=p_1+a, a<=q_r. (H18) + +For small r, p_1>=m_r-q_r>0. The mixture identity implies + + dTV(S_r, mu_r/m_r) <= a/m_r, S_r=sigma/p_1. (H19) + +Marginal contraction gives dTV(pi_{r,1},pi_r)<=a/m_r. Tensoring with a fixed +probability measure preserves TV. The triangle inequality and (H1) therefore give + + dTV(S_r,pi_{r,1} tensor lambda) <= 2a/m_r+C r^3 <= C r^2. + +For the height marginal alone, compare first with mu_r/m_r and then with pi_r +tensor lambda. Its bound is a/m_r+C r^3, again O(r^2). This proves (H2)-(H3). +The factor two in the joint own-marginal comparison is kept, not silently removed. + +Since 0<=theta<=1, TV controls its first two moments: +E theta=1/2+O(r^2), E theta^2=1/3+O(r^2), Var theta=1/12+O(r^2). +Using H=b-l theta and l=k r^3 proves (H4), with uniform compact-k constants. + +Bonferroni and the factorial bound give + + P(N_r>=1)>=m_r-q_r/2, + epsilon_r:=P(N_r>=2 | N_r>=1)<=q_r/(2m_r-q_r)=O(r^2). (H20) + +The nonempty configuration law is a mixture of its singleton part and a +multiple-configuration part with mass epsilon_r. Its TV distance from the +singleton law S_r, embedded into configurations, is exactly epsilon_r. Combining +with (H2) proves the complete-configuration assertion. + +Any measurable rule selecting one actual point from a nonempty configuration +agrees with S_r on N_r=1, hence its selected-mark law differs from S_r by at most +epsilon_r. Applying marginal contraction once more proves O(r^2) decoupling from +its OWN selected location/index marginal, and O(r^2) height uniformity. A rule +may be randomized via a probability kernel; the same mixture argument applies. + +## 7. Why this does not improve the contact-profile rate + +If pi_E is the limiting contact spatial/index profile, RM gives only +TV(pi_r,pi_E)=O(r). Therefore + + TV(S_r,pi_E tensor lambda) <= O(r^2)+TV(pi_{r,1},pi_E)=O(r). + +There is no contradiction with the sharper own-marginal factorization. The old +O(r) comparison can be dominated by spatial/index drift which is common to +all heights and vanishes when that finite-r marginal is retained. + +Nor do the moment premises alone permit O(r^3) conditional height error. For a +simple abstract marked process at two distinct locations A,B, choose m=r^3 and +p_2=r^5/2. A two-point configuration occurs with probability p_2 and contains one +point at each location with a common height uniform on (0,1/2). Choose the +singleton submeasure to make the TOTAL mean mark measure exactly m times the +uniform law on {A,B} times Uniform(0,1): its height density summed over locations +is m-4p_2 on (0,1/2) and m on (1/2,1). These are nonnegative for r<=1/2 and have +mass p_1=m-2p_2. Put the remaining probability 1-m+p_2 on the empty configuration. + +This process has an exactly height-flat mean and q=2p_2=r^5, but its singleton +height TV from uniform is + + p_2/(m-2p_2)=r^2/[2(1-r^2)]. (H21) + +It shows the O(r^2) multiplicity correction cannot be eliminated from just these +mean/factorial premises. It is NOT an example of the conditioned Gaussian field +and does not prove that the rate is optimal for that specific field. + +## 8. Review and verification boundaries + +The new load-bearing analytic step is (H15): the shared regression direction, +homogeneous endpoint constraints, normalized Hessian columns, filtered +polynomial determinant bound, and extra-conditioned moments. The finite tests +check the TV convention, actual finite-r marginal, pair multiplicity weights, +normalizations, the explicit homogeneous-pin polynomial, and the rate-barrier +example. They do not establish a covariance floor, a Gaussian supremum bound, +or Kac-Rice applicability. + +This note does not permit rho->0, changing d/L, unbounded birth marks or k->0, +or field-selected random E. It does not imply global uniqueness, change a +persistence-partner definition, or recover/retry the unrelated blocked code in +Math-#116. Authorship/exposure is OpenAI, including the prior remote source; +independent acceptance requires an actual source-bound nonauthor review. diff --git a/frontiers/remote_height_decoupling_20260928/README.md b/frontiers/remote_height_decoupling_20260928/README.md new file mode 100644 index 000000000..12ab1168b --- /dev/null +++ b/frontiers/remote_height_decoupling_20260928/README.md @@ -0,0 +1,14 @@ +# Within-window height decoupling — author-side candidate + +[PROOF.md](PROOF.md) proves the proposed improvement using the existing fixed-remote +mean and factorial inputs: O(r^3) factorization of the normalized mean against its +own finite-r location/index marginal, and O(r^2) height uniformity/independence for +the actual unique witness. Joint convergence to the limiting contact profile stays +O(r). Physical height mean and variance errors become O(r^5) and O(r^8). + +Scientific effect NONE. No parent source or scientific status is changed. +This is a new derivation, not a replay of the absent Math-#116 algebra suite. + +Run `python -B -S verify.py` or `python -B -O -S verify.py` from this directory. +The finite standard-library tests and semantic mutants do not certify the Gaussian +argument. Source identities and comparison scope are in SOURCE_MAP.json. diff --git a/frontiers/remote_height_decoupling_20260928/RECONNAISSANCE.md b/frontiers/remote_height_decoupling_20260928/RECONNAISSANCE.md new file mode 100644 index 000000000..5fb3e4816 --- /dev/null +++ b/frontiers/remote_height_decoupling_20260928/RECONNAISSANCE.md @@ -0,0 +1,22 @@ +# Reconnaissance and attribution — 28 September 2026 + +This is a source-consumer derivation, not an independent Gaussian-field theory +or a novelty/priority claim. The existing remote mean proof is read at its exact +Git blob in SOURCE_MAP.json. Its same-r conditional Gaussian field construction, +filtered determinant estimate and full normalizer are the load-bearing inputs. +The same-r height-Lipschitz consequence and finite-r marginal target are derived +explicitly in PROOF.md rather than inferred from an integrated mean. + +The neighboring primary-source Kac-Rice framework is Armentano, Azais and Leon, +On a general Kac-Rice formula for the measure of a level set, +arXiv:2304.07424v3. It is the underlying reference of the consumed remote source, +not a new direct theorem import here. Gaussian regression, vector integral +Taylor bounds, TV contraction and the singleton/mean mixture are classical. +The earlier HEIGHT_MARKS and remote-singleton records are credited in the proof; +neither is silently rewritten or treated as new independent review. + +The current Consensus request returned its monthly quota error. The continuation +used direct primary-source records instead; no Consensus search hit or full-text +read is fabricated. A future novelty audit would need substantially broader +search than this dependency-focused pass. The finite tests do not prove the +Gaussian covariance or expected-integral premises. diff --git a/frontiers/remote_height_decoupling_20260928/RESULTS.json b/frontiers/remote_height_decoupling_20260928/RESULTS.json new file mode 100644 index 000000000..82f2f3aef --- /dev/null +++ b/frontiers/remote_height_decoupling_20260928/RESULTS.json @@ -0,0 +1,11 @@ +{ + "scientific_effect": "NONE", + "baseline": { + "errors": [], + "failures": [], + "passed": true, + "tests": 12 + }, + "scope": "Finite identities, normalization and counterexamples only; no Gaussian continuum verification.", + "nonauthor_acceptance": false +} diff --git a/frontiers/remote_height_decoupling_20260928/SOURCE_FILES.json b/frontiers/remote_height_decoupling_20260928/SOURCE_FILES.json new file mode 100644 index 000000000..606647ba8 --- /dev/null +++ b/frontiers/remote_height_decoupling_20260928/SOURCE_FILES.json @@ -0,0 +1,40 @@ +{ + "schema": 1, + "files": [ + { + "path": "PROOF.md", + "bytes": 13747, + "sha256": "67249f0311342beab7833cb60c3239d9888df96befda4fbae3ec29a66f8cd78e" + }, + { + "path": "README.md", + "bytes": 860, + "sha256": "172f89489a5dbcae5723a4ef25a2bf311d40f2063355a8e58915667dffa4f76d" + }, + { + "path": "RECONNAISSANCE.md", + "bytes": 1417, + "sha256": "c1c847aeca81d809dc15a578a960f3c0873db991d1a75303a8dc0db68d08a3ae" + }, + { + "path": "RESULTS.json", + "bytes": 271, + "sha256": "ed08787edd576df6a3ddc78904c78e7f90fcdd2c837f8aead4af632f04e589e7" + }, + { + "path": "SOURCE_MAP.json", + "bytes": 1327, + "sha256": "21c033a48551ebdc084e44845a0172e36ebeba4ef8879c81cad7943fe81d5e0d" + }, + { + "path": "check.py", + "bytes": 5189, + "sha256": "3edbfc286c1660b5beb3a3b10df85d0d2dc51d256320a58f360682ab5db2adfc" + }, + { + "path": "verify.py", + "bytes": 3024, + "sha256": "7f057116ee8a0fa2c81dde06a821b5f717795a6bb06bf763af1ee3e9f81460f2" + } + ] +} diff --git a/frontiers/remote_height_decoupling_20260928/SOURCE_MAP.json b/frontiers/remote_height_decoupling_20260928/SOURCE_MAP.json new file mode 100644 index 000000000..fe7f8e5c7 --- /dev/null +++ b/frontiers/remote_height_decoupling_20260928/SOURCE_MAP.json @@ -0,0 +1,27 @@ +{ + "scientific_effect": "NONE", + "source_repository": "d6g8k5htny-coder/Math-", + "inputs": [ + { + "commit": "4b2aa45b2f995fc27c16ec37cccb081821eda74c", + "path": "frontiers/remote_window_20260924/PROOF.md", + "git_blob": "b383bfcc88ec4ad497dff01fb6640e429ba24a84", + "use": "Sections 2-5: same-r height regression, extra-conditioned moments, filtered determinant Lipschitz inequality, full normalizer, pre-height mean kernel and its positive contact limit." + }, + { + "commit": "4b2aa45b2f995fc27c16ec37cccb081821eda74c", + "path": "frontiers/remote_collision_20260928/PROOF.md", + "git_blob": "7b48a88e2af54e759e89a8c8219573bb450a65ea", + "use": "Corollary D: fixed-remote all-index factorial moment O(r^5)|E|." + }, + { + "commit": "0507e3a1dbd3dede84cbeb805947c70aa16ebc36", + "path": "frontiers/window_multiplicity_laws_20260928/HEIGHT_MARKS.md", + "git_blob": "015d769675d9a2cf191286979d3b8c877cd91bdc", + "use": "Comparison and attribution only: prior O(r) target is the limiting contact profile, not the new finite-r marginal. Its blocked code is not consumed." + } + ], + "new_analytic_obligation": "Uniform Lipschitz height density via homogeneous endpoint regression directions.", + "nonauthor_acceptance": false, + "global_extension_claimed": false +} diff --git a/frontiers/remote_height_decoupling_20260928/check.py b/frontiers/remote_height_decoupling_20260928/check.py new file mode 100644 index 000000000..5e52cf0f5 --- /dev/null +++ b/frontiers/remote_height_decoupling_20260928/check.py @@ -0,0 +1,132 @@ +"""Exact finite controls for the new same-r height-decoupling argument. + +This is not a Gaussian-field simulator or a continuum theorem verifier. +""" +import argparse +from fractions import Fraction as F +import io +import json +import unittest + +MUTANT = None + +def tv(p, q): + if len(p) != len(q): + raise ValueError('matching finite mark spaces required') + scale = 1 if MUTANT == 'tv-factor' else F(1, 2) + return scale*sum(abs(a-b) for a,b in zip(p,q)) + + +def own_spatial_product(mu): + if len(mu) != 4 or any(v < 0 for v in mu): + raise ValueError('four nonnegative mark masses required') + mass=sum(mu) + if mass == 0: + if MUTANT == 'allow-zero': + return [F(0)]*4 + raise ValueError('positive mean mass required') + if MUTANT == 'wrong-marginal': + return [F(1, 4)]*4 + divisor=F(2) if MUTANT == 'ignore-mass' else 2*mass + return [(mu[0]+mu[1])/divisor]*2+[(mu[2]+mu[3])/divisor]*2 + + +def normalized_mean(singletons, pair_mass): + if len(singletons) != 4 or pair_mass < 0 or any(v < 0 for v in singletons): + raise ValueError('nonnegative configuration weights required') + mu=list(singletons) + mu[0] += pair_mass + if MUTANT != 'drop-pair-weight': + mu[2] += pair_mass + mass=sum(mu) + if mass <= 0: + raise ValueError('positive mean mass required') + return [v/mass for v in mu] + + +class HeightTests(unittest.TestCase): + def test_probability_tv_half_convention(self): + self.assertEqual(tv([F(1), F(0)], [F(0), F(1)]), 1) + + def test_equal_probability(self): + self.assertEqual(tv([F(1, 3), F(2, 3)], [F(1, 3), F(2, 3)]), 0) + + def test_own_not_contact_marginal(self): + self.assertEqual(own_spatial_product([F(3, 10), F(3, 10), F(1, 5), F(1, 5)]), + [F(3, 10), F(3, 10), F(1, 5), F(1, 5)]) + + def test_normalization_handles_small_mass(self): + self.assertEqual(own_spatial_product([F(3, 100), F(3, 100), F(1, 50), F(1, 50)]), + [F(3, 10), F(3, 10), F(1, 5), F(1, 5)]) + + def test_zero_mass_excluded(self): + with self.assertRaises(ValueError): + own_spatial_product([F(0)]*4) + + def test_mean_needs_two_pair_points(self): + # Four mark bins: A0,A1,B0,B1. A multiple configuration has A0 and B0. + p = F(1, 100) + self.assertEqual(normalized_mean([p, 2*p, p, 2*p], p), [F(1, 4)]*4) + + def test_pair_mixture_bound(self): + for r in (F(1, 2), F(1, 3), F(1, 10)): + mass = r**3; p2 = r**5/2 + sig = [mass/4-p2, mass/4, mass/4-p2, mass/4] + p1 = sum(sig) + mean = normalized_mean(sig, p2) + single = [v/p1 for v in sig] + self.assertEqual(mean, [F(1, 4)]*4) + self.assertEqual(tv(single, mean), r*r/(2*(1-r*r))) + self.assertLessEqual(tv(single, mean), r*r) + + def test_mean_uniform_does_not_force_singleton_uniform(self): + r = F(1, 10); mass = r**3; p2 = r**5/2 + sig = [mass/4-p2, mass/4, mass/4-p2, mass/4] + single = [v/sum(sig) for v in sig] + self.assertGreater(tv(single, [F(1, 4)]*4), r**3) + + def test_exact_height_change_of_variables(self): + for r in (F(1, 2), F(1, 7)): + k = F(6, 5); length = k*r**3 + # An affine within-window density gives TV = slope*length/(8*mean). + base = F(2); slope = F(3) + average = base-slope*length/2 + self.assertEqual((slope*length*length/4)/(2*length*average), + slope*length/(8*average)) + + def test_average_distance_integral(self): + # Integral_0^1 [theta^2/2+(1-theta)^2/2] dtheta = 1/3. + self.assertEqual(F(1, 6)+F(1, 6), F(1, 3)) + + def test_homogeneous_gradient_pin_cancellation(self): + # g=x^2*z-r^2*z/4+(x^2-r^2/4)^2. Both values/gradients vanish at M,S. + for r in (F(1, 2), F(1, 11), F(1, 101)): + for x in (-r/2, r/2): + self.assertEqual(x*x-r*r/4, 0) + self.assertEqual(4*x*(x*x-r*r/4), 0) + beta = (2*x)/r + alpha = (12*x*x-r*r)/r + self.assertEqual(abs(beta), 1) + self.assertEqual(alpha, 2*r) + self.assertLessEqual(abs(alpha), 1) + + def test_tv_marginal_contraction(self): + p=[F(1, 10),F(2, 10),F(3, 10),F(4, 10)]; q=[F(1, 4)]*4 + self.assertLessEqual(tv([p[0]+p[2], p[1]+p[3]], [F(1, 2)]*2), tv(p,q)) + + +def main(): + parser=argparse.ArgumentParser() + parser.add_argument('--mutant', choices=['tv-factor', 'wrong-marginal', 'drop-pair-weight', 'ignore-mass', 'allow-zero']) + args=parser.parse_args() + global MUTANT + MUTANT=args.mutant + suite=unittest.defaultTestLoader.loadTestsFromTestCase(HeightTests) + result=unittest.TextTestRunner(stream=io.StringIO()).run(suite) + 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 + +if __name__=='__main__': + raise SystemExit(main()) diff --git a/frontiers/remote_height_decoupling_20260928/verify.py b/frontiers/remote_height_decoupling_20260928/verify.py new file mode 100644 index 000000000..3d12c5453 --- /dev/null +++ b/frontiers/remote_height_decoupling_20260928/verify.py @@ -0,0 +1,73 @@ +"""Verify the exact flat packet, execute both modes, reject semantic mutants.""" +import hashlib +import json +from pathlib import Path +import subprocess +import sys + +EXPECTED_FAILURE = { + 'tv-factor':'test_probability_tv_half_convention', + 'wrong-marginal':'test_own_not_contact_marginal', + 'drop-pair-weight':'test_mean_needs_two_pair_points', + 'ignore-mass':'test_normalization_handles_small_mass', + 'allow-zero':'test_zero_mass_excluded', +} + +def unique(items): + result={} + for key,value in items: + if key in result: + raise ValueError('duplicate JSON key: '+key) + result[key]=value + return result + +def load(text): + return json.loads(text,object_pairs_hook=unique) + +def check_sources(root): + entries=load((root/'SOURCE_FILES.json').read_text())['files'] + names=[e['path'] for e in entries] + if len(names)!=len(set(names)) or any(Path(n).name!=n for n in names): + raise ValueError('invalid flat source paths') + if sorted(p.name for p in root.iterdir())!=sorted(names+['SOURCE_FILES.json']): + raise ValueError('packet membership differs') + for e in entries: + p=root/e['path'] + if p.is_symlink() or not p.is_file(): + raise ValueError('nonregular source') + data=p.read_bytes() + if len(data)!=e['bytes'] or hashlib.sha256(data).hexdigest()!=e['sha256']: + raise ValueError('source identity differs: '+p.name) + +def main(): + root=Path(__file__).resolve().parent + check_sources(root) + baseline=load((root/'RESULTS.json').read_text())['baseline'] + records=[] + for case in ['baseline',*EXPECTED_FAILURE]: + outs=[] + for flags in (['-B','-S'],['-B','-O','-S']): + command=[sys.executable,*flags,str(root/'check.py')] + if case!='baseline': + command+=['--mutant',case] + process=subprocess.run(command,capture_output=True,timeout=30) + result=load(process.stdout.decode()) + if process.stderr or result['errors']: + raise ValueError('execution error rather than semantic failure') + if case=='baseline': + if process.returncode!=0 or result!=baseline: + raise ValueError('baseline mismatch') + elif process.returncode!=1 or result['passed'] or EXPECTED_FAILURE[case] not in result['failures']: + raise ValueError('semantic mutant not rejected: '+case) + outs.append(process.stdout) + if outs[0]!=outs[1]: + raise ValueError('normal and optimized outputs differ') + records.append({'case':case,**load(outs[0].decode())}) + check_sources(root) + print(json.dumps({'scientific_effect':'NONE','nonauthor_acceptance':False, + 'tests_per_mode':baseline['tests'],'mutants_per_mode':len(EXPECTED_FAILURE), + 'exact_sources':'PASS','all_output_pairs_identical':True,'cases':records}, + indent=2,sort_keys=True)) + +if __name__=='__main__': + main()