From 36e939d0af615f8ead6c73c9127fd5763e235516 Mon Sep 17 00:00:00 2001 From: Dylan Roy <249851642+d6g8k5htny-coder@users.noreply.github.com> Date: Mon, 5 Oct 2026 17:43:28 -0700 Subject: [PATCH 1/7] Add explicit d3 Cap I4 spectral pushforward and ninth-moment proposal --- .../PROOF.md | 242 ++++++++++++++++++ 1 file changed, 242 insertions(+) create mode 100644 reviews/cap_i4_d3_spectral_adapter_20261005/PROOF.md diff --git a/reviews/cap_i4_d3_spectral_adapter_20261005/PROOF.md b/reviews/cap_i4_d3_spectral_adapter_20261005/PROOF.md new file mode 100644 index 000000000..c30e3f5ff --- /dev/null +++ b/reviews/cap_i4_d3_spectral_adapter_20261005/PROOF.md @@ -0,0 +1,242 @@ +# Cap I4 in d=3: explicit spectral pushforward and a ninth-moment envelope + +**Object:** CAP-I4-D3-SPECTRAL-20261005-v1.0. +**Author:** OpenAI / GPT-6 Astra Pro, session `cap-i4-explicit-d3-adapter-20261005`, acting for Dylan Roy. +**Disposition:** additive ordinary-mathematical proposal; nonauthor review pending. No Lean implementation or kernel verification of this new adapter is claimed. Scientific/status effect NONE; organizational-independence credit 0. +**Pickup:** main#229 comment 6006586304. + +## 1. Source and scope + +Repository `d6g8k5htny-coder/Math-`, source cut `f4c33a98a982d50aa490e49ce9327c755682527c`. + +P is `imports/lifetime_parent_20260925/UNIFORM_MATRIX_CAP_AND_LIFETIME.md`, Git blob `dfed3b8d318a3ab1950957f393307733a4bef3f2`. Consumed interfaces: matrix-density majorant (3.5), full-field residual independence and moments (4.2)-(4.3), full normalizer (5.5), typed determinant inequality (6.2), and the depth/exception events in section 7. Read section 5 with `ERRATUM_CONGRUENCE.md`, not its historical multiplying-sqrt(r) wording. No re-review of every ancestor is claimed. + +The existing Cap companion at `f4079f65a3e5e95c9993e51ac5995a54344d4130`, `companions/cap_i4_source_bridge_20261005/CapI4.lean`, blob `4769930d132a485f88b75c4f4d901a3c4db7d43e`, proves the conditional integral/normalizer ledger. It does not prove its concrete `MatrixDepthTransport` premise. The general spectral-measure reduction in main#229 comment 6006128867 is credited as motivation, not consumed as an already-accepted theorem. + +This note proves the 2x2 version of the spectral measure domination directly by trace and polar coordinates, fixes its exact volume convention, and retains one more hard-eigenvalue factor in the depth estimate. The resulting sufficient residual moment is order **9**, instead of order 10 in P's coarser m=2 envelope. This is a moment-sufficiency refinement, not an optimality claim or a guaranteed improvement in the numerical size of the constant. + +Fixed ambient dimension d=3, so the transverse dimension is m=2. There is no assertion for m=1 by inserting zero-dimensional coordinates, no d>=4 theorem, no numerical coefficient c_(3,L), no evaluated finite-radius threshold, and no all-mark or all-volume uniformity. Exact scalar moment algebra is not a continuum or Lean proof. + +## 2. Volume conventions and the exact change of variables + +Write + + B = [[a,b],[b,d]], dB_entry = da db dd, + t = (a+d)/2, x = (a-d)/2, y = b. + +Thus `||B||_F^2 = a^2+2b^2+d^2 = 2(t^2+x^2+y^2)` and + + dB_entry = 2 dt dx dy. (1) + +On the complement of the polar cut and origin, put `x=rho cos(theta)`, `y=rho sin(theta)`, with `rho>0` and `-pi(t,rho)` is 1/2. Combining it with (1) and the polar determinant rho gives + + dB_entry = ((Lambda-lambda)/2) d lambda d Lambda d theta. (2) + +For a direct check, the derivative of `(a,b,d)` with respect to `(lambda,Lambda,theta)` is + + [[(1-cos theta)/2, (1+cos theta)/2, -rho sin theta], + [-sin theta/2, sin theta/2, rho cos theta], + [(1+cos theta)/2, (1-cos theta)/2, rho sin theta]]. + +Its determinant is `rho(cos^2 theta+sin^2 theta)=rho`, not twice rho. This parameterization covers each nonscalar matrix once off the polar cut. There is no extra factor for the signs of eigenvectors and no unordered-eigenvalue factorial. The eigenvector rotation angle would be half theta, with a different interval and Jacobian; that is not the coordinate used here. + +For a nonnegative measurable function p on entry space, its positive-cone spectral pushforward has density, almost everywhere on `0=0, c>0. (4) + +No invariance is assumed for p. The majorant is radial in Frobenius coordinates. By (3), + + q_+(lambda,Lambda) + <= pi C0 (Lambda-lambda) exp(-c(lambda^2+Lambda^2)) + 1_{00}) <= sigma_2, + sigma_2 = pi C0 (Lambda-lambda) exp(-c(lambda^2+Lambda^2)) + 1_{0=delta>0, ||m||<=M, + +then one valid choice is + + c=1/(4S), + C_F=(2pi)^(-3/2) delta^(-1/2) exp(M^2/(2S)), + C0=sqrt(2)C_F. (6) + +Indeed, `(X-m)^T Sigma^(-1)(X-m)>=||X-m||^2/S`, and + + ||X-m||^2 >= ||X||^2/2-||m||^2, + +because the difference is `||X-2m||^2/2>=0`. Insert these estimates in the Gaussian density. Formula (6) is conditional on valid covariance/mean bounds; it is not an evaluated bound for any given L or r. P(3.5) already supplies the existence of uniform C0,c on its fixed-d,L compact-mark/frame family. + +## 4. Probability and weight hypotheses + +Work on a probability space with original law Q. Assume: + +1. B is a measurable symmetric 2x2 matrix satisfying (4). J is measurable, `J>=1`, independent of the **entire B**, and `E_Q[J^9]<=M9=k_floor>0`, K>0. W is nonnegative and integrable. On `{W>0}`, B>0, h=M3>=0, `h<=K(J+Lambda)`, and the m=2 case of P(6.2) holds: + + W <= r^2 h^2/4 * lambda(lambda+(3/2)rh) * Lambda(Lambda+rh). (7) + +3. The depth event is `E_lambda={lambda<=[4/(3k)] r h^2}`. Outside `{W>0}`, the values of h and the event do not affect its weighted numerator. All events used for normalized probabilities are measurable. + +P(4.3) gives `h<=K0(J+||B||_F)`; on the positive cone `||B||_F<=sqrt(2)Lambda`, so choosing `K=sqrt(2)K0` suffices. This norm-conversion factor must not be dropped. The source has moments of every finite order, so the ninth moment here is available at its stated compact scope. + +The proof never conditions the original independence assumption on the typed event. Typing can couple B and J. Instead we majorize the weighted integrand on typed support by a function of B,J and then integrate under the ORIGINAL product law. Independence of W, h, or separate eigenvalues is neither assumed nor inferred. + +## 5. Retain the hard eigenvalue: the r^5 numerator from moment nine + +Set + + U=J+Lambda>=1, D=4K^2/(3k_floor), E=3K/2, + A=K^2(1+K)/4, B_* = D^3/3+ED^2/2. + +On weighted depth support, `0Lambda. Its bound by Lambda has already been made on the original domain. + +The exact inner integral, also proved in the existing companion, is + + r^3[(D^3/3)U^6+(ED^2/2)U^5]. + +Therefore + + E_Q[W 1_E_lambda] + <= pi C0 A r^5 E_J integral_0^infty Lambda^2 exp(-cLambda^2) + [(D^3/3)U^9+(ED^2/2)U^8]d Lambda + <= pi C0 A B_* r^5 E_J integral_0^infty Lambda^2 (J+Lambda)^9 + exp(-cLambda^2)d Lambda. (9) + +All steps use nonnegative integration, so Tonelli applies before integrability has been established. The following finite bound supplies integrability afterwards: + + (J+Lambda)^9 <= 256(J^9+Lambda^9), + integral_0^infty Lambda^2 exp(-cLambda^2)d Lambda = sqrt(pi)/(4c^(3/2)), + integral_0^infty Lambda^11 exp(-cLambda^2)d Lambda = 60/c^6. + +Consequently a fully displayed sufficient constant is + + C_depth = 256 pi C0 A B_* [M9 sqrt(pi)/(4c^(3/2)) + 60/c^6], + E_Q[W 1_E_lambda] <= C_depth r^5. (10) + +The two Gaussian integrals follow by `y=c Lambda^2` and Gamma(3/2)=sqrt(pi)/2, Gamma(6)=120. No Monte Carlo, unweighted tail substitution, inverse eigenvalue, or positive hard-eigenvalue cutoff is used. The estimate covers corank-two NEIGHBORHOODS and the small-Lambda region directly. + +Order nine is sufficient, not claimed necessary. A family with bounded eighth moment and unbounded ninth moment shows only that one cannot replace M9 by M8 in the particular separated envelope (9) without another argument. It does not refute the possibility of a better proof under fewer moments. + +## 6. Full normalization and the separate E4 input + +Assume the actual FULL normalizer `Z=E_Q W>=cZ r^2`, cZ>0. Divide (10) exactly once: + + Q^W(E_lambda) <= (C_depth/cZ)r^3. (11) + +This neither adds a pin density nor normalizes on the good event. For +`E4={3k/100 supplied by the deterministic source therefore give + + Q^W(G^c) <= (C_depth/cZ)r^3 + + M4joint/[cZ(3k_floor/10)^4]r^4. (13) + +The implication need only hold Q-a.e. on positive-weight support, not globally off typed support. The moment-nine refinement is for the depth numerator; it does not eliminate the separate weighted E4 moment assumption. + +For a parameter family, C0,c,K,k_floor,M9,cZ,M4joint must have the stated common bounds. P supplies them only after restricting to its fixed L, fixed dimension and compact birth/positive-gap/frame sets and sufficiently small radius. No common probability-one statement across uncountably many conditioned laws is asserted. + +## 7. The smaller formal task now exposed + +Here is a concrete sufficient **unimplemented theorem signature**, rather than another hypothesis equal to the desired probability estimate. Use entry coordinates `V=(R x R) x R`, z=((a,b),d), and define + + frobSq(z)=a^2+2b^2+d^2, + eig2(z)=((a+d)/2-sqrt(((a-d)/2)^2+b^2), + (a+d)/2+sqrt(((a-d)/2)^2+b^2)). + +The target is the measure inequality + +```lean +-- Proposed signature only. No proof body, axiom, or kernel status is asserted. +theorem sym2_positive_spectral_domination + (mu : Measure ((Real × Real) × Real)) + (C0 c : Real) (hC0 : 0 ≤ C0) (hc : 0 < c) + (hdom : mu ≤ volume.withDensity + (fun z => ENNReal.ofReal (C0 * Real.exp (-c * frobSq z)))) : + Measure.map eig2 (mu.restrict {z | 0 < (eig2 z).1}) ≤ + volume.withDensity (fun e : Real × Real => + if 0 < e.1 ∧ e.1 < e.2 then + ENNReal.ofReal (Real.pi * C0 * (e.2 - e.1) * + Real.exp (-c * (e.1 ^ 2 + e.2 ^ 2))) + else 0) +``` + +The displayed `frobSq` and `eig2` are definitions to be supplied, not imported existing names. Product Lebesgue volume is intended on both sides. The inequality permits equality of the eigenvalues on the left because (4) gives zero mass there. A separate proof must establish measurability and perform the two linear coordinate changes around the polar formula; it must not interpret a zero-totalized nonintegrable Bochner integral as a finite estimate. + +**Available pinned interface, actually inspected:** mathlib commit `d13f23b723b8a846827a245b89c10fc7d3f11612`, `Mathlib/Analysis/SpecialFunctions/PolarCoord.lean`, blob `053dcbf1bcd84f42dcc8273dd4afb0d87a6755e6`, already contains `lintegral_comp_polarCoord_symm`, `det_fderivPolarCoordSymm`, and `polarCoord_source_ae_eq_univ`. Its polar target is `(0,infinity) x (-pi,pi)`, exactly the convention used above. Thus d=3 does not require formalizing a general-dimensional Weyl integration theorem or constructing a measurable eigenbasis just to prove (S2). + +After (S2), the residual product law, pointwise inequality (8), nonnegative product integration and Gaussian moments (9)-(10) still need Lean implementation, together with concrete source-model instantiation. The existing original `MatrixDepthTransport` may alternatively be reached by replacing the retained hard factor in (8) with the coarser U^4 factor; its already-compiled consumer then applies. The ninth-moment refinement has a different envelope, so it is NOT falsely claimed as a new fact already proved by that consumer. + +## 8. Verification, review boundary and references + +`test_adapter.py` first ran with no `algebra.py`: all 14 methods failed with their named missing implementations. After implementation, all 14 pass in both standard-library normal/optimized modes, with byte-identical deterministic stdout. Checks cover the 3x3 derivative determinant at rational circle points, trace/determinant/Frobenius identities, angle/volume factors, both soft terms, hard-factor and ordered-domain bounds, moment/radius algebra, Gaussian-mean square identity, exact Gamma recurrences, full normalization, weighted support, a dependent-marginal counterexample, and small-hard-eigenvalue cases. Five named altered-formula copies are rejected by the replay protocol. These are finite algebra checks, not proofs of general change of variables, Gaussian regression, measurability, or the arbitrary-real inequalities. + +No local Lean executable or full repository checkout is available; direct GitHub DNS in this container failed. The published packet uses only Python's standard library. No prior accepted source, formal seal, review body, scientific flag or coefficient output is changed. + +Primary sources: +- P and its congruence erratum at the source cut above. +- Existing `CapI4.lean` at f4079f65, as identified in section 1. +- Exact pinned mathlib polar-coordinate source identified in section 7; current public documentation was used only for discovery, not to substitute a new library version. + +Consensus was attempted in this pass and returned a rate-limit error. No Consensus paper was retrieved or credited. No literature novelty claim is made. A separate mathematical reader should check the measure convention, polar multiplicity, null strata, original-law independence, order of domain extension, moment-nine exponent, separate E4 requirement, and compact-family quantifiers before disposition. From 176aab2e8d03579b3de30b3fe72a1d22d4cc1930 Mon Sep 17 00:00:00 2001 From: Dylan Roy <249851642+d6g8k5htny-coder@users.noreply.github.com> Date: Mon, 5 Oct 2026 17:43:50 -0700 Subject: [PATCH 2/7] Add exact rational helpers for Cap d3 adapter controls --- .../algebra.py | 97 +++++++++++++++++++ 1 file changed, 97 insertions(+) create mode 100644 reviews/cap_i4_d3_spectral_adapter_20261005/algebra.py diff --git a/reviews/cap_i4_d3_spectral_adapter_20261005/algebra.py b/reviews/cap_i4_d3_spectral_adapter_20261005/algebra.py new file mode 100644 index 000000000..15105cfad --- /dev/null +++ b/reviews/cap_i4_d3_spectral_adapter_20261005/algebra.py @@ -0,0 +1,97 @@ +"""Rational identities used by the d=3 spectral-adapter checks. + +No random field, Gaussian distribution, integral evaluator, or Lean kernel is +implemented here. Irrational Gaussian-moment constants are tracked symbolically. +""" +from fractions import Fraction as F +from math import factorial + + +def det3(a): + if len(a) != 3 or any(len(row) != 3 for row in a): + raise ValueError('expected a 3 by 3 matrix') + return (a[0][0]*(a[1][1]*a[2][2]-a[1][2]*a[2][1]) + -a[0][1]*(a[1][0]*a[2][2]-a[1][2]*a[2][0]) + +a[0][2]*(a[1][0]*a[2][1]-a[1][1]*a[2][0])) + + +def spectral_entries(lam, top, cosine, sine): + if lam > top or cosine*cosine+sine*sine != 1: + raise ValueError('ordered eigenvalues and a unit-circle point required') + t=(lam+top)/2; rho=(top-lam)/2 + return t+rho*cosine, rho*sine, t-rho*cosine + + +def normalization_ledger(): + return {'entry_angular_over_pi': F(1), + 'cartesian_to_trace_absdet': F(2), + 'spectral_to_trace_absdet': F(1,2), + 'frobenius_over_entry_squared': F(2)} + + +def soft_primitive(upper, shift): + return upper**3/3 + shift*upper**2/2 + + +def weight_majorant(lam, top, J, r, K): + if not (0 <= lam <= top and J >= 1 and 0 < r <= 1 and K > 0): + raise ValueError('outside positive ordered compact-radius domain') + U=J+top; A=K*K*(1+K)/4; E=3*K/2 + return A*r*r*top*U**3*lam*(lam+E*r*U) + + +def post_soft_majorant(top, J, r, K, k_floor): + if not (top >= 0 and J >= 1 and 0 < r <= 1 and K > 0 and k_floor > 0): + raise ValueError('positive radius, moments and mark floor required') + D=4*K*K/(3*k_floor); E=3*K/2; A=K*K*(1+K)/4 + return A*(D**3/3+E*D*D/2)*r**5*top*top*(J+top)**9 + + +def ninth_power_envelope(J, top): + if J < 0 or top < 0: + raise ValueError('nonnegative inputs required') + return 256*(J**9+top**9) + + +def gaussian_half_moment(n, sqrt_c): + """Return (rational coefficient, multiply_by_sqrt_pi) for c=sqrt_c**2.""" + if type(n) is not int or n < 0 or sqrt_c <= 0: + raise ValueError('nonnegative integer degree and positive sqrt(c) required') + if n % 2: + k=(n-1)//2 + return F(factorial(k),2)/sqrt_c**(2*k+2), False + k=n//2 + coeff=F(1,2) + for j in range(1,k+1): + coeff*=F(2*j-1,2) + return coeff/sqrt_c**(2*k+1), True + + +def gaussian_square_gap(z, mean): + if len(z) != len(mean): + raise ValueError('incompatible vectors') + return sum(((a-2*b)**2/2 for a,b in zip(z,mean)),F(0)) + + +def normalized_depth(C, z_floor, r): + if C < 0 or z_floor <= 0 or r <= 0: + raise ValueError('invalid full-normalizer inputs') + return (C*r**5)/(z_floor*r**2) + + +def diagonal_bernoulli(): + return {(0,0):F(1,2),(1,1):F(1,2)} + + +def support_transfer_sums(atoms): + if any(W < 0 or (W > 0 and good and not G) for W,good,G in atoms): + raise ValueError('weighted-support implication not supplied') + return (sum((W for W,good,G in atoms if not G),F(0)), + sum((W for W,good,G in atoms if not good),F(0))) + + +def two_atom_moments(T): + if T <= 1: + raise ValueError('T must exceed one') + p=1/T**8 + return (1-p)+p*T**8, (1-p)+p*T**9 From cf951abb2af938c0f3bbdae08be5139bc53820b6 Mon Sep 17 00:00:00 2001 From: Dylan Roy <249851642+d6g8k5htny-coder@users.noreply.github.com> Date: Mon, 5 Oct 2026 17:44:41 -0700 Subject: [PATCH 3/7] Add 14 exact finite-algebra and omitted-hypothesis controls --- .../test_adapter.py | 165 ++++++++++++++++++ 1 file changed, 165 insertions(+) create mode 100644 reviews/cap_i4_d3_spectral_adapter_20261005/test_adapter.py diff --git a/reviews/cap_i4_d3_spectral_adapter_20261005/test_adapter.py b/reviews/cap_i4_d3_spectral_adapter_20261005/test_adapter.py new file mode 100644 index 000000000..72eb98c29 --- /dev/null +++ b/reviews/cap_i4_d3_spectral_adapter_20261005/test_adapter.py @@ -0,0 +1,165 @@ +"""Exact finite-algebra controls, not a Gaussian-model or Lean proof.""" +from fractions import Fraction as F +import importlib.util +import json +from math import factorial +from pathlib import Path +import unittest + +HERE = Path(__file__).resolve().parent + +class AdapterChecks(unittest.TestCase): + @classmethod + def setUpClass(cls): + path = HERE / 'algebra.py' + cls.alg = None + if path.is_file(): + spec = importlib.util.spec_from_file_location('cap_d3_algebra', path) + cls.alg = importlib.util.module_from_spec(spec) + spec.loader.exec_module(cls.alg) + + def call(self, name, *args): + fn = getattr(self.alg, name, None) + self.assertTrue(callable(fn), f'missing implementation: {name}') + return fn(*args) + + def test_jacobian_from_three_by_three_derivative(self): + for c,s in [(F(1),F(0)),(F(0),F(1)),(F(3,5),F(4,5)),(F(-5,13),F(12,13))]: + for rho in [F(0),F(1,1000),F(1,3),F(7)]: + rows = [[(1-c)/2,(1+c)/2,-rho*s],[-s/2,s/2,rho*c],[(1+c)/2,(1-c)/2,rho*s]] + self.assertEqual(self.call('det3',rows),rho) + + def test_spectral_trace_determinant_and_frobenius(self): + for lam in [F(-2),F(0),F(1,100),F(3)]: + for gap in [F(0),F(1,1000),F(2),F(7)]: + top=lam+gap + for c,s in [(F(1),F(0)),(F(3,5),F(4,5)),(F(-5,13),F(12,13))]: + a,b,d=self.call('spectral_entries',lam,top,c,s) + self.assertEqual(a+d,lam+top) + self.assertEqual(a*d-b*b,lam*top) + self.assertEqual(a*a+2*b*b+d*d,lam*lam+top*top) + + def test_angle_and_volume_normalizations(self): + data=self.call('normalization_ledger') + # Relative to pi times the gap, entry measure has coefficient one. + self.assertEqual(data['entry_angular_over_pi'],F(1)) + self.assertEqual(data['cartesian_to_trace_absdet'],F(2)) + self.assertEqual(data['spectral_to_trace_absdet'],F(1,2)) + # Frobenius volume differs by sqrt(2), so its squared ratio is two. + self.assertEqual(data['frobenius_over_entry_squared'],F(2)) + # Whole-space radial Gaussian: 4 * integral_0^inf rho exp(-2rho^2) = 1. + self.assertEqual(data['entry_angular_over_pi']*4*F(1,4),1) + + def test_soft_primitive_retains_mixed_term(self): + for r in [F(1,100),F(1,3),F(1)]: + for D in [F(1,4),F(2)]: + for E in [F(0),F(3,2)]: + for U in [F(1),F(7,3),F(10)]: + actual=self.call('soft_primitive',D*r*U*U,E*r*U) + self.assertEqual(actual,r**3*(D**3*U**6/3+E*D**2*U**5/2)) + + def test_typed_determinant_hard_factor_retained(self): + for r in [F(1,100),F(1,2),F(1)]: + for K in [F(1,3),F(1),F(3)]: + for J in [F(1),F(5)]: + for top in [F(1,10000),F(1,2),F(8)]: + for frac in [F(1,7),F(1)]: + lam=frac*top; U=J+top; h=K*U + source=r*r*h*h/4*lam*(lam+F(3,2)*r*h)*top*(top+r*h) + major=self.call('weight_majorant',lam,top,J,r,K) + self.assertLessEqual(source,major) + + def test_order_bound_precedes_interval_extension(self): + for top in [F(1,10),F(1),F(4)]: + for upper in [top/10,top,10*top]: + for shift in [F(0),F(1,3),F(5)]: + a=min(top,upper) + # Integral t(t+b)(top-t), on the ORIGINAL nonnegative interval. + actual=top*a**3/3+top*shift*a*a/2-a**4/4-shift*a**3/3 + widened=top*self.call('soft_primitive',upper,shift) + self.assertGreaterEqual(actual,0) + self.assertLessEqual(actual,widened) + self.assertLess(F(1)-F(2),0) # Do not retain the signed gap after widening. + + def test_ninth_moment_radius_factorization(self): + for r in [F(1,100),F(1,2),F(1)]: + for K in [F(1,3),F(2)]: + for k in [F(1,5),F(3)]: + D=4*K*K/(3*k); E=3*K/2; A=K*K*(1+K)/4 + for J,top in [(F(1),F(1,10)),(F(3),F(4)),(F(10),F(1,1000))]: + U=J+top + integrated=A*r*r*top*top*U**3*self.call('soft_primitive',D*r*U*U,E*r*U) + exact=A*r**5*top*top*(D**3*U**9/3+E*D*D*U**8/2) + self.assertEqual(integrated,exact) + upper=self.call('post_soft_majorant',top,J,r,K,k) + self.assertLessEqual(exact,upper) + + def test_power_envelope_and_gaussian_moments(self): + for J in [F(1),F(3,2),F(9)]: + for top in [F(0),F(1,10000),F(2),F(7)]: + self.assertLessEqual((J+top)**9,self.call('ninth_power_envelope',J,top)) + # Recurrence: even coefficients multiply sqrt(pi), odd are rational. + for scale in [F(1,3),F(1),F(2)]: + c=scale*scale + self.assertEqual(self.call('gaussian_half_moment',2,scale),(F(1,4)/scale**3,True)) + self.assertEqual(self.call('gaussian_half_moment',11,scale),(F(60)/c**6,False)) + for n in range(10): + a,pa=self.call('gaussian_half_moment',n,scale) + b,pb=self.call('gaussian_half_moment',n+2,scale) + self.assertEqual(pa,pb) + self.assertEqual(b,F(n+1,2)/c*a) + + def test_gaussian_mean_majorant(self): + for z in [(F(0),F(0),F(0)),(F(2),F(-1),F(3)),(F(1,7),F(1),F(-2))]: + for mean in [(F(0),F(0),F(0)),(F(1),F(-2),F(1,3))]: + gap=self.call('gaussian_square_gap',z,mean) + expected=sum((a-b)**2 for a,b in zip(z,mean))-sum(a*a for a in z)/2+sum(b*b for b in mean) + self.assertEqual(gap,expected) + self.assertGreaterEqual(gap,0) + + def test_full_normalizer_once(self): + for r in [F(1,100),F(1,2),F(1)]: + for C,z in [(F(3),F(1,7)),(F(1,5),F(4))]: + self.assertEqual(self.call('normalized_depth',C,z,r),(C/z)*r**3) + + def test_dependent_marginals_not_product_domination(self): + joint=self.call('diagonal_bernoulli') + self.assertEqual(sum(joint.values()),1) + self.assertEqual(sum(p for (x,y),p in joint.items() if x==1),F(1,2)) + self.assertEqual(sum(p for (x,y),p in joint.items() if y==1),F(1,2)) + self.assertGreater(joint[(1,1)],F(1,2)*F(1,2)) + + def test_weighted_support_not_global_implication(self): + # good=>G fails at the zero-weight atom, but the weighted transfer is exact. + atoms=[(F(0),True,False),(F(2),True,True),(F(3),False,False)] + left,right=self.call('support_transfer_sums',atoms) + self.assertEqual((left,right),(F(3),F(3))) + self.assertTrue(any(good and not G for W,good,G in atoms)) + + def test_no_claim_eighth_moment_controls_ninth(self): + ratios=[] + for T in [F(2),F(4),F(8),F(16)]: + m8,m9=self.call('two_atom_moments',T) + self.assertLessEqual(m8,2) + self.assertGreaterEqual(m9,T) + ratios.append(m9/m8) + self.assertTrue(all(a Date: Mon, 5 Oct 2026 17:45:05 -0700 Subject: [PATCH 4/7] Add source-bound replay with exact named altered-formula failure checks --- .../replay.py | 98 +++++++++++++++++++ 1 file changed, 98 insertions(+) create mode 100644 reviews/cap_i4_d3_spectral_adapter_20261005/replay.py diff --git a/reviews/cap_i4_d3_spectral_adapter_20261005/replay.py b/reviews/cap_i4_d3_spectral_adapter_20261005/replay.py new file mode 100644 index 000000000..66dabbc72 --- /dev/null +++ b/reviews/cap_i4_d3_spectral_adapter_20261005/replay.py @@ -0,0 +1,98 @@ +"""Source-bound finite-algebra replay; never interprets an arbitrary crash as a mutant PASS.""" +from __future__ import annotations +import argparse +import hashlib +import json +from pathlib import Path +import subprocess +import sys +import tempfile + +HERE=Path(__file__).resolve().parent +PAYLOAD={'PROOF.md','README.md','algebra.py','test_adapter.py','replay.py'} +MUTANTS={ + 'double_angle': ("'entry_angular_over_pi': F(1)","'entry_angular_over_pi': F(2)", + {'test_angle_and_volume_normalizations'}), + 'omit_frobenius_scale': ("'frobenius_over_entry_squared': F(2)","'frobenius_over_entry_squared': F(1)", + {'test_angle_and_volume_normalizations'}), + 'drop_mixed_soft': ('return upper**3/3 + shift*upper**2/2','return upper**3/3', + {'test_soft_primitive_retains_mixed_term','test_ninth_moment_radius_factorization', + 'test_order_bound_precedes_interval_extension'}), + 'eighth_envelope': ('*top*top*(J+top)**9','*top*top*(J+top)**8', + {'test_ninth_moment_radius_factorization'}), + 'wrong_normalizer': ('return (C*r**5)/(z_floor*r**2)','return (C*r**5)/(z_floor*r**5)', + {'test_full_normalizer_once'}), +} + +def sha(data): return hashlib.sha256(data).hexdigest() + +def strict_json(text): + def pairs(items): + out={} + for key,value in items: + if key in out: raise ValueError('duplicate JSON key') + out[key]=value + return out + def invalid(value): raise ValueError('nonfinite JSON constant: '+value) + return json.loads(text,object_pairs_hook=pairs,parse_constant=invalid) + +def authenticate(): + raw=(HERE/'SOURCES.json').read_bytes() + manifest=strict_json(raw.decode('utf-8')) + if manifest['schema']!=1 or set(manifest['files'])!=PAYLOAD: + raise ValueError('manifest payload inventory mismatch') + if {p.name for p in HERE.iterdir()}!=PAYLOAD|{'SOURCES.json'}: + raise ValueError('unexpected/missing packet member') + result={'SOURCES.json':sha(raw)} + for name in sorted(PAYLOAD): + p=HERE/name + if p.is_symlink() or not p.is_file(): raise ValueError('nonregular payload') + data=p.read_bytes(); row=manifest['files'][name] + blob=hashlib.sha1(b'blob '+str(len(data)).encode()+b'\0'+data).hexdigest() + if len(data)!=row['bytes'] or sha(data)!=row['sha256'] or blob!=row['git_blob']: + raise ValueError('payload identity mismatch: '+name) + result[name]=sha(data) + return result + +def run_suite(directory,flags,expected): + done=subprocess.run([sys.executable,*flags,'test_adapter.py'],cwd=directory, + capture_output=True,text=True,timeout=20) + summary=strict_json(done.stdout) + fields={'scope','tests','failures','errors','success'} + if (set(summary)!=fields or type(summary['tests']) is not int or summary['tests']!=14 + or type(summary['success']) is not bool or not isinstance(summary['failures'],list) + or len(summary['failures'])!=len(set(summary['failures'])) or summary['errors']!=[] + or set(summary['failures'])!=expected or summary['success']!=(not expected) + or done.returncode!=(1 if expected else 0)): + raise ValueError('wrong exit, test inventory, or rejection reason') + if f'Ran 14 tests in ' not in done.stderr: + raise ValueError('missing unittest execution record') + return {'exit':done.returncode,'summary':summary, + 'stdout_sha256':sha(done.stdout.encode()),'stderr':done.stderr} + +def main(): + ap=argparse.ArgumentParser(description=__doc__) + ap.add_argument('--mode',choices=['normal','optimized'],required=True) + ap.add_argument('--evidence',type=Path) + args=ap.parse_args(); before=authenticate() + flags=['-B','-S'] if args.mode=='normal' else ['-B','-O','-S'] + records={'baseline':run_suite(HERE,flags,set())} + algebra=(HERE/'algebra.py').read_text(); tests=(HERE/'test_adapter.py').read_text() + for name,(old,new,expected) in MUTANTS.items(): + if algebra.count(old)!=1: raise ValueError('mutant replacement not unique: '+name) + with tempfile.TemporaryDirectory(prefix='cap-d3-'+name+'-') as td: + directory=Path(td) + (directory/'algebra.py').write_text(algebra.replace(old,new)) + (directory/'test_adapter.py').write_text(tests) + records[name]=run_suite(directory,flags,expected) + if authenticate()!=before: raise ValueError('source changed during execution') + result={'scope':'finite algebra only; no analytic or Lean acceptance','mode':args.mode, + 'baseline_tests':14,'intended_mutants':len(MUTANTS),'source_sha256':before, + 'pass':True,'executions':records} + if args.evidence: + args.evidence.parent.mkdir(parents=True,exist_ok=True) + with args.evidence.open('x') as f: json.dump(result,f,indent=2,sort_keys=True); f.write('\n') + print(json.dumps({k:v for k,v in result.items() if k!='executions'},indent=2,sort_keys=True)) + +if __name__=='__main__': + main() From 5012c2965bbf43eb03c4892fcbb1988d944db933 Mon Sep 17 00:00:00 2001 From: Dylan Roy <249851642+d6g8k5htny-coder@users.noreply.github.com> Date: Mon, 5 Oct 2026 17:48:07 -0700 Subject: [PATCH 5/7] Document d3 spectral adapter scope and reproduction --- .../README.md | 29 +++++++++++++++++++ 1 file changed, 29 insertions(+) create mode 100644 reviews/cap_i4_d3_spectral_adapter_20261005/README.md diff --git a/reviews/cap_i4_d3_spectral_adapter_20261005/README.md b/reviews/cap_i4_d3_spectral_adapter_20261005/README.md new file mode 100644 index 000000000..d4cdeb9c0 --- /dev/null +++ b/reviews/cap_i4_d3_spectral_adapter_20261005/README.md @@ -0,0 +1,29 @@ +# Cap I4: explicit d=3 spectral adapter + +**Author-side analytic proposal; not a new Lean proof. Scientific/status effect NONE.** + +The transverse matrix is 2x2. An entry-coordinate density bound +`p(B)<=C0 exp(-c||B||_F^2)` gives the positive ordered-eigenvalue upper density +`pi C0 (Lambda-lambda)exp(-c(lambda^2+Lambda^2))` by two linear changes and planar polar coordinates. The proof fixes the often-hidden entry-volume/Frobenius-volume factor sqrt(2). It needs neither matrix-law isotropy nor measurable eigenvectors. + +Keeping one hard-eigenvalue factor gives a depth numerator bounded by + + C_depth r^5, + C_depth=256 pi C0 [K^2(1+K)/4] [D^3/3+ED^2/2] + * [M9 sqrt(pi)/(4c^(3/2))+60/c^6], + D=4K^2/(3k_floor), E=3K/2, M9>=E[J^9]. + +This is a sufficient ninth-moment envelope, not an optimality claim or an evaluated field constant. The full normalizer, actual density/residual inputs, measurable cap implication and weighted fourth-derivative moment remain explicit. The source field's compact-family inputs come from P; no unrestricted k,L,d statement is added. + +`PROOF.md` gives the complete ordinary proof, source identities, a concrete proposed Lean measure-domination signature, and the exact already-existing polar API at the project mathlib pin. `SOURCES.json` authenticates this packet's mathematical/test files; hashes establish identity, not acceptance. The original Cap branch, its separate engineering child, the formal manifests, and the active integration queue are untouched. + +## Replay + +```sh +python -B -S replay.py --mode normal +python -B -O -S replay.py --mode optimized +``` + +Each mode authenticates packet membership and hashes, executes all 14 finite-algebra tests, then executes five altered-formula controls and requires the exact intended failed-test set with no test errors. Wrong exit, malformed result, skipped/missing tests, duplicate JSON keys, or an unexpected rejection reason is not success. Outputs are deterministic JSON summaries; source hashes are read again after execution. Run from this directory or pass the script's full path. Standard library only. + +The tests do not prove the continuum source, and the proposed Lean signature has not been implemented/compiled. The original kernel-checked CapI4 consumer remains conditional. No self-merge or independent mathematical acceptance is claimed. Actual author: OpenAI / GPT-6 Astra Pro, session `cap-i4-explicit-d3-adapter-20261005`; Dylan Roy delegated work. Pickup main#229/6006586304. From 7231945cfc6a3652b8ae903425ceab242a2330a9 Mon Sep 17 00:00:00 2001 From: Dylan Roy <249851642+d6g8k5htny-coder@users.noreply.github.com> Date: Mon, 5 Oct 2026 17:48:33 -0700 Subject: [PATCH 6/7] Pin d3 adapter payload and consumed sources including congruence erratum --- .../SOURCES.json | 60 +++++++++++++++++++ 1 file changed, 60 insertions(+) create mode 100644 reviews/cap_i4_d3_spectral_adapter_20261005/SOURCES.json diff --git a/reviews/cap_i4_d3_spectral_adapter_20261005/SOURCES.json b/reviews/cap_i4_d3_spectral_adapter_20261005/SOURCES.json new file mode 100644 index 000000000..120236b62 --- /dev/null +++ b/reviews/cap_i4_d3_spectral_adapter_20261005/SOURCES.json @@ -0,0 +1,60 @@ +{ + "files": { + "PROOF.md": { + "bytes": 16999, + "git_blob": "c30e3f5ff600b058a30087ff794c7cf304e4aafc", + "sha256": "3b79ca614682a453a9bbb35e95f65d9891155bcbc531ffcfaf55ba0d5d840633" + }, + "README.md": { + "bytes": 2487, + "git_blob": "d4cdeb9c02eb6b0d154423254b1c8c8801ce0c81", + "sha256": "253e99a49359bfe80d8f306d1c6e46a9b82813621b18322aed2af56033d41166" + }, + "algebra.py": { + "bytes": 3155, + "git_blob": "15105cfade673679f067586ad4012d7999340a7d", + "sha256": "78304cb360e050102b031d14719b7dd11b312a1a37a1454a4cc05394e09fbf0c" + }, + "replay.py": { + "bytes": 5024, + "git_blob": "66dabbc728e8a8f7b74fd3ca38ed5b0b850c6d28", + "sha256": "b0dfc58bba0933d05fce31288af43f09f1d2802c92245b2cbbfcb6dd30bb9767" + }, + "test_adapter.py": { + "bytes": 8339, + "git_blob": "72eb98c29af4ca3e83819c400bc35a032acb9850", + "sha256": "54fdee783095fd36d81fa284bf4353c264749ac5c001de83514256bdfd76d9bb" + } + }, + "schema": 1, + "scientific_effect": "NONE", + "source_cut": "f4c33a98a982d50aa490e49ce9327c755682527c", + "sources": [ + { + "blob": "dfed3b8d318a3ab1950957f393307733a4bef3f2", + "consumed": "(3.5),(4.2)-(4.3),(5.5),(6.2),section7; section5 with existing congruence erratum", + "path": "imports/lifetime_parent_20260925/UNIFORM_MATRIX_CAP_AND_LIFETIME.md", + "repo": "d6g8k5htny-coder/Math-" + }, + { + "blob": "213594d6ca6a86fb938110f4d166d9ce275a02d0", + "consumed": "inverse congruence required for P section5 full-normalizer argument", + "path": "imports/lifetime_parent_20260925/ERRATUM_CONGRUENCE.md", + "repo": "d6g8k5htny-coder/Math-" + }, + { + "blob": "4769930d132a485f88b75c4f4d901a3c4db7d43e", + "commit": "f4079f65a3e5e95c9993e51ac5995a54344d4130", + "consumed": "conditional scalar primitive and full-normalizer interface only", + "path": "companions/cap_i4_source_bridge_20261005/CapI4.lean", + "repo": "d6g8k5htny-coder/Math-" + }, + { + "blob": "053dcbf1bcd84f42dcc8273dd4afb0d87a6755e6", + "commit": "d13f23b723b8a846827a245b89c10fc7d3f11612", + "consumed": "nonnegative polar change-of-variables interface; no new Lean implementation claimed", + "path": "Mathlib/Analysis/SpecialFunctions/PolarCoord.lean", + "repo": "leanprover-community/mathlib4" + } + ] +} From 8e90773b28ecce66ed30458d58aef1b6cb83666a Mon Sep 17 00:00:00 2001 From: Dylan Roy <249851642+d6g8k5htny-coder@users.noreply.github.com> Date: Mon, 5 Oct 2026 17:50:17 -0700 Subject: [PATCH 7/7] Run d3 adapter finite controls with pinned source and exact-head receipts --- .github/workflows/cap-i4-d3-adapter.yml | 83 +++++++++++++++++++++++++ 1 file changed, 83 insertions(+) create mode 100644 .github/workflows/cap-i4-d3-adapter.yml diff --git a/.github/workflows/cap-i4-d3-adapter.yml b/.github/workflows/cap-i4-d3-adapter.yml new file mode 100644 index 000000000..6a797ef39 --- /dev/null +++ b/.github/workflows/cap-i4-d3-adapter.yml @@ -0,0 +1,83 @@ +name: Cap I4 d3 adapter finite controls +on: + push: + branches: [chatgpt/cap-i4-d3-spectral-adapter-20261005] + paths: + - reviews/cap_i4_d3_spectral_adapter_20261005/** + - imports/lifetime_parent_20260925/UNIFORM_MATRIX_CAP_AND_LIFETIME.md + - imports/lifetime_parent_20260925/ERRATUM_CONGRUENCE.md + - .github/workflows/cap-i4-d3-adapter.yml + pull_request: + paths: + - reviews/cap_i4_d3_spectral_adapter_20261005/** + - imports/lifetime_parent_20260925/UNIFORM_MATRIX_CAP_AND_LIFETIME.md + - imports/lifetime_parent_20260925/ERRATUM_CONGRUENCE.md + - .github/workflows/cap-i4-d3-adapter.yml +permissions: + contents: read +jobs: + replay: + runs-on: ubuntu-latest + timeout-minutes: 8 + strategy: + fail-fast: false + matrix: + mode: [normal, optimized] + env: + MODE: ${{ matrix.mode }} + steps: + - uses: actions/checkout@11bd71901bbe5b1630ceea73d27597364c9af683 + with: + fetch-depth: 0 + - uses: actions/setup-python@5fda3b95a4ea91299a34e894583c3862153e4b97 + with: + python-version: '3.13.5' + - name: Authenticate source and execute finite algebra controls + shell: bash + run: | + set -euo pipefail + REL=reviews/cap_i4_d3_spectral_adapter_20261005 + OUT="$PWD/.lake/cap-i4-d3-$MODE" + test ! -e "$OUT" + mkdir -p "$OUT" + source_record() { + python -B -S - <<'PY' + import hashlib, json, os, subprocess + from pathlib import Path + rel = Path('reviews/cap_i4_d3_spectral_adapter_20261005') + manifest = rel / 'SOURCES.json' + if manifest.is_symlink() or hashlib.sha256(manifest.read_bytes()).hexdigest() != '7d15141f245ca1a79c4a6c21fc8dc4a2abe5c140fe04aeaf16584c66821e341b': + raise ValueError('frozen manifest mismatch') + pins = { + 'imports/lifetime_parent_20260925/UNIFORM_MATRIX_CAP_AND_LIFETIME.md': 'dfed3b8d318a3ab1950957f393307733a4bef3f2', + 'imports/lifetime_parent_20260925/ERRATUM_CONGRUENCE.md': '213594d6ca6a86fb938110f4d166d9ce275a02d0', + } + for path, expected in pins.items(): + actual = subprocess.check_output(['git', 'hash-object', path], text=True).strip() + if actual != expected: raise ValueError('consumed source mismatch: ' + path) + workflow = '.github/workflows/cap-i4-d3-adapter.yml' + subprocess.run(['git','diff','--exit-code','HEAD','--',str(rel),workflow,*pins],check=True) + head = subprocess.check_output(['git','rev-parse','HEAD'],text=True).strip() + if head != os.environ['GITHUB_SHA']: raise ValueError('tested head mismatch') + print(json.dumps({'head':head,'run':os.environ['GITHUB_RUN_ID'], + 'attempt':os.environ['GITHUB_RUN_ATTEMPT'],'mode':os.environ['MODE'], + 'workflow_sha256':hashlib.sha256(Path(workflow).read_bytes()).hexdigest(), + 'manifest_sha256':hashlib.sha256(manifest.read_bytes()).hexdigest(), + 'source_blobs':pins},sort_keys=True)) + PY + } + source_record | tee "$OUT/before.json" + FLAGS=(-B -S) + if [ "$MODE" = optimized ]; then FLAGS+=(-O); fi + python "${FLAGS[@]}" "$REL/replay.py" --mode "$MODE" --evidence "$OUT/replay.json" | tee "$OUT/stdout.json" + source_record | tee "$OUT/after.json" + cmp "$OUT/before.json" "$OUT/after.json" + (cd "$OUT" && sha256sum -- *.json > SHA256SUMS) + - name: Preserve execution evidence even on failure + if: always() + uses: actions/upload-artifact@ea165f8d65b6e75b540449e92b4886f43607fa02 + with: + name: cap-i4-d3-${{ matrix.mode }}-${{ github.sha }} + path: .lake/cap-i4-d3-${{ matrix.mode }}/ + include-hidden-files: true + if-no-files-found: warn