From 9706a2cb3ca4cc2df792b33ab440c92ee7c76dcc Mon Sep 17 00:00:00 2001 From: Dylan Roy Date: Wed, 30 Sep 2026 11:10:06 -0500 Subject: [PATCH] Respond to D1 external audit with a complete cap-to-global-elder reconstruction Source-exposed audit, not independent-human acceptance. Reconstruct all cap faces, vector ridge bounds and both maximin inequalities; derive exterior invariance and an exact endpoint-jet-only counterexample. Bind P/CAP/errata/Borel repair and classify outdated versus genuinely open validation claims. D2 O(1) remainder is distinguished from D1 leading and compact difference statements. No parent/source/status/graph/formal-scope modifications. Fresh21 tests per Python mode; 1728 finite-graph exterior variants; all9 packet blobs and tree matched locally. Historical source authentication remains hosted. Issue193; no self-merge. --- .github/workflows/d1-external-cap-audit.yml | 45 +++ reviews/d1_external_audit_20260930/AUDIT.md | 327 ++++++++++++++++++ .../d1_external_audit_20260930/MANIFEST.json | 54 +++ reviews/d1_external_audit_20260930/README.md | 57 +++ .../d1_external_audit_20260930/SOURCES.json | 79 +++++ .../d1_external_audit_20260930/VALIDATION.md | 43 +++ .../d1_external_audit_20260930/cap_audit.py | 195 +++++++++++ .../test_cap_audit.py | 123 +++++++ .../test_sources.py | 53 +++ .../verify_sources.py | 92 +++++ 10 files changed, 1068 insertions(+) create mode 100644 .github/workflows/d1-external-cap-audit.yml create mode 100644 reviews/d1_external_audit_20260930/AUDIT.md create mode 100644 reviews/d1_external_audit_20260930/MANIFEST.json create mode 100644 reviews/d1_external_audit_20260930/README.md create mode 100644 reviews/d1_external_audit_20260930/SOURCES.json create mode 100644 reviews/d1_external_audit_20260930/VALIDATION.md create mode 100644 reviews/d1_external_audit_20260930/cap_audit.py create mode 100644 reviews/d1_external_audit_20260930/test_cap_audit.py create mode 100644 reviews/d1_external_audit_20260930/test_sources.py create mode 100644 reviews/d1_external_audit_20260930/verify_sources.py diff --git a/.github/workflows/d1-external-cap-audit.yml b/.github/workflows/d1-external-cap-audit.yml new file mode 100644 index 000000000..531472589 --- /dev/null +++ b/.github/workflows/d1-external-cap-audit.yml @@ -0,0 +1,45 @@ +name: D1 external cap audit controls + +'on': + pull_request: + paths: + - 'reviews/d1_external_audit_20260930/**' + - '.github/workflows/d1-external-cap-audit.yml' + workflow_dispatch: + +permissions: + contents: read + +jobs: + exact-and-source: + runs-on: ubuntu-latest + timeout-minutes: 10 + steps: + - uses: actions/checkout@11d5960a326750d5838078e36cf38b85af677262 + with: + persist-credentials: false + fetch-depth: 0 + - uses: actions/setup-python@a26af69be951a213d495a4c3e4e4022e16d87065 + with: + python-version: '3.11.16' + - name: Authenticate the frozen source set + env: + GIT_NO_REPLACE_OBJECTS: '1' + run: | + set -euo pipefail + git fetch --no-tags origin 3e0a91b69892b9717564c592e7a966492a81566a + python -B -S reviews/d1_external_audit_20260930/verify_sources.py + - name: Exact finite controls in both interpreter modes + env: + PYTHONDONTWRITEBYTECODE: '1' + GIT_NO_REPLACE_OBJECTS: '1' + run: | + set -euo pipefail + cd reviews/d1_external_audit_20260930 + python -B -S -m unittest -v + python -B -O -S -m unittest -v + python -B -S cap_audit.py > "$RUNNER_TEMP/cap-normal.json" + python -B -O -S cap_audit.py > "$RUNNER_TEMP/cap-optimized.json" + cmp "$RUNNER_TEMP/cap-normal.json" "$RUNNER_TEMP/cap-optimized.json" + python -B -S verify_sources.py + git diff --exit-code diff --git a/reviews/d1_external_audit_20260930/AUDIT.md b/reviews/d1_external_audit_20260930/AUDIT.md new file mode 100644 index 000000000..fdfccaf53 --- /dev/null +++ b/reviews/d1_external_audit_20260930/AUDIT.md @@ -0,0 +1,327 @@ +# D1 external-audit response: the separating cap really gives a global elder pair + +Object: OA-D1-CAP-AUDIT-20260930-v1. Author/executor: OpenAI / GPT-6 Astra Pro. +Requested by Dylan in the current conversation; coordination: Math- issue #193. +Source cut: `3e0a91b69892b9717564c592e7a966492a81566a`. + +**Disposition:** source/author-exposed reconstruction and new explanatory corollaries; +new nonauthor review requested. Not an independent-human or institutional review. +Scientific effect NONE: no original proof, verdict, GRAPH, STATUS, prize, premise +or formal-scope change. The executor is exposed to the original OpenAI proof chain. + +## 1. What this audit resolves, and what it does not + +The external critique identifies the right load-bearing question: why does a local +Hessian event identify the GLOBAL ordinary superlevel H0 elder partner? Sections +2–7 reconstruct that implication without relying on an ACCEPT label. The crucial +information is stronger than endpoint jets: a closed neighborhood has no exit above +the saddle height, and a separately constructed path reaches an older point at +exactly that height. Remote excursions, loops and reentry cannot avoid the first exit. +No deterministic gap was found in CAP §§1–5 under their full hypotheses. + +This is not a fresh audit of all Gaussian estimates or of the entire D1 theorem. +The matrix boundary layer, pinned genericity, marked Kac–Rice extension and source +coefficient identification remain their own analytic interfaces. `SOURCES.json` +binds the exact source set; an identity match never establishes its truth. + +The critique also contains a statement that is correct for D1 alone but outdated +for the program: a separate, source-bound reviewed D2 theorem already supplies an +unrestricted **O(1) additive remainder**, not the stronger compact O(ell^(2/3)) +difference. Section8 separates this update from genuine open validation and +numerical-constant requirements. Institutional external review and a complete Lean +formalization are not provided by this response and are not marked resolved. + +## 2. The topological lemma, independent of Gaussian probability + +Let X be a compact smooth manifold, f continuous, M in the interior of a compact +set C, b=f(M), and sb and f>=s everywhere on it. + +Define the connection value + + d_f(M)=sup_{gamma(0)=M, f(gamma(1))>b} min_{t in[0,1]} f(gamma(t)). (A1) + +Then **d_f(M)=s**. + +Proof of the upper bound: every older endpoint f(z)>b is outside C by C1. Since M +is interior, a continuous path to that endpoint has a first boundary exit. Its +value is <=s by C2, so the path minimum is <=s. Later excursions or reentry cannot +remove that already-encountered value. Taking the supremum proves d_f(M)<=s. +C3 proves the opposite inequality and also shows that the path family is nonempty. +This argument needs no smooth boundary, no absence of remote critical points, +no stochastic independence, and no identification of a ridge with a flow line. + +For a Morse f with distinct critical values, this is precisely the ordinary +superlevel-component elder death level. One can see it directly from the rule: +for sh} cannot contain a point above b, since an +open connected manifold subset is path connected and that would contradict the +upper bound. Thus no older maximum has merged with M's class at those levels. +For every hh} and reaches a point above b, so +the component now contains an older maximum. A component containing such a point +has a maximum of value greater than b: maximize f on its compact closure. Since +the maximum is above h, it lies in the component interior, not its level-h boundary. +Therefore death occurs at level s, not above or below it. The nonempty older path +excludes the essential global-maximum class. If a unique critical point S has +critical value s, that point is the elder death saddle. + +The argument does NOT say that a path with minimum s by itself determines death: +it proves only d_f(M)>=s. Nor does an exit barrier alone guarantee finite death: +without an older endpoint the class can be essential. Both directions are necessary. + +## 3. The exact local hypotheses in D1 + +Write local coordinates (x,y) in R x R^(d-1), with d>=2. For r>0 the full cylinder is + + D=[-2r,2r] x closed_ball(0,2r). + +For the torus X=R^d/(LZ^d), impose `r0 and a C4 function near D with +critical pins M=(-r/2,0), S=(r/2,0), f(M)=b, f(S)=s=b-kr^3. +For j=3,4 use exactly the partial-block operator norms from CAP: + + M_j=max_{a+c=j} sup_D ||partial_x^a D_y^c f||_op, + lambda=lambda_min(-D_y^2 f(M)). + +The event used in P §7 is + + G_r: lambda > (4/(3k))r M_3^2, rM_4 <= 3k/10. (A2) + +These are bounds on the WHOLE CYLINDER, not just the Hessians or jets at M and S. +Using arbitrary-coordinate entry maxima without the appropriate dimension factors +would not be the same event. The transverse Hessian inequality is a matrix-order +inequality, not an entrywise scalar assertion. + +Normalize by f_tilde=f/(6k). Its gap is r^3/6. Put m=M_3/(6k), n=M_4/(6k), and +lambda_tilde=lambda/(6k). The hypotheses become + + lambda_tilde>8r m^2, rn<=1/20. (A3) + +In Sections4–6 all derivatives/heights refer to f_tilde. Write b_tilde=b/(6k), +s_tilde=b_tilde-r^3/6, a=-r/2 and c=r/2. + +## 4. Reconstructing the transverse ridge without a vector Rolle shortcut + +The two critical pins yield the exact Hermite identity + + f_tilde(c,0)-f_tilde(a,0) + =-1/2 integral_a^c (x-a)(c-x) f_tilde_xxx(x,0) dx. (A4) + +The positive kernel has integral r^3/6. Its weighted derivative average is therefore +2; in particular m>=2, and f_tilde_xxx=2 somewhere in the pin interval. Each point +of D is at product distance <5r from that point and from M. The block norms give + + f_tilde_xxx>=2-5rn>=7/4, + D_y^2 f_tilde <= -delta I, + delta=lambda_tilde-5rm>rm(8m-5). (A5) + +Let K=8m-5>=11 and w(x)=grad_y f_tilde(x,0). Both endpoint values of w are zero. +Apply the two-node scalar interpolation remainder to each unit-vector projection: + + ||w(x)|| <= (m/2)|x^2-r^2/4| <=(15/8)mr^2<2mr^2. (A6) + +This also holds outside the pin interval: use the convex hull of x,a,c when +applying the scalar interpolation remainder. For its derivative, use the average: + + w'(x)=r^-1 integral_a^c [w'(x)-w'(t)]dt, + ||w'(x)|| <=(m/r) integral_a^c |x-t|dt <=2mr. (A7) + +There is no assertion of one point where all components of w' vanish. Indeed the +exact vector w=(x^2-1/4, x^3-x/4) has both endpoint zeros but no common zero of w'. + +On ||y||=2r, strong concavity gives + + grad_y f_tilde(x,y).y <= ||w(x)|| ||y||-delta||y||^2<0. + +The maximum in each compact transverse ball is interior and unique. Call it h(x). +The implicit-function theorem gives h in C3, h(a)=h(c)=0 and + + ||h||<2r/K, + ||h'||<(2/K)+(2/K^2)<=24/121, + m||h'|| <=(1+6/K+5/K^2)/4<=48/121. (A8) + +For example h'=-(D_y^2 f_tilde)^(-1) partial_x grad_y f_tilde; (A7) plus the +mixed derivative bound at h gives the second inequality. All estimates use vector +operator norms and have no hidden dimension-dependent coordinate sum. + +## 5. The reduced derivative and EVERY boundary face + +Let g(x)=f_tilde(x,h(x)) and F=g'. Put v=(1,h'). Differentiating the transverse +critical equation gives (H_f_tilde v)_y=0. In the third derivative of g, the +h'' term pairs this Hessian vector with a purely transverse vector and is zero; +the h''' term pairs grad_y f_tilde=0. Therefore exactly + + F''=f_xxx+3f_xxy[h']+3f_xyy[h',h']+f_yyy[h',h',h']. (A9) + +This does not make h a gradient-flow trajectory. The adverse part in (A9) is at +most (48/121)[3+3(24/121)+(24/121)^2]=2554128/1771561. Hence + + F''>7/4-2554128/1771561=2184415/7086244>1/4. (A10) + +Since F(a)=F(c)=0, strict convexity gives F<0 between the pins and F>0 outside. +It also gives F'(a)<0=s_tilde+9r^3/32=b_tilde+11r^3/96. (A11) + +For the lateral boundary ||y||=2r, (A5)–(A8) give delta>22r and +||y-h||>20r/11. Hence, for every x in the cap, + + f_tilde(x,y)<=g(x)-(delta/2)||y-h||^2 + b_tilde. +This establishes C3. A path through S at level s is not an above-s preemption path. + +Multiplication by6k returns to the original function. The axial drop/rise is at +least (27/16)kr^3; the older-point excess is at least (11/16)kr^3; the lateral drop +is greater than (26400/121)kr^3. Heights b,s and all critical points retain their +order. By Section2 the global elder partner is S on the Morse/distinct-value +locus. This is the desired implication (A2), in all fixed d>=2. + +The optional ascending-branch conclusion also follows: an ascent-unstable vector +at S cannot lie in the negative transverse hyperplane. One half-branch enters C +at height>s and cannot leave it. Its omega-limit lies among the finitely many +critical points in C; the strictly increasing gradient Lyapunov function excludes +S, so the limit is M. The other half-branch cannot cross the boundary at height>s +or approach the interior point M. The same reasoning works with a smooth positive +definite Riemannian metric; no Morse–Smale property is used. The branch claim is +not needed for the elder maximin proof. + +## 6. Two useful audit consequences + +### Exterior invariance + +Let f satisfy the preceding cylinder hypotheses. Any other compact Morse extension +f_hat that agrees with f on a neighborhood of D and has distinct critical values +also pairs M with S, regardless of its values outside D. The proof uses exactly +the same cap C, boundary and older-reaching ridge segment. Thus modifying remote +maxima, creating remote saddles or providing an exterior high corridor cannot +preempt the pair while these protected data remain unchanged. This is a corollary +of the first-exit proof, not a probabilistic decorrelation assertion. + +### Endpoint jets alone are insufficient: an exact local counterexample + +For r=k=1, in two variables put + + q(x)=2x^3-(3/2)x-1/2, + f0(x,y)=q(x)-128y^2, + f1(x,y)=f0(x,y)+65536y^4+y^5. (A13) + +Both pins M=(-1/2,0), S=(1/2,0) have the same heights0,-1 and identical jets through +order3. Both have the same max/saddle Hessian types. The unmodified f0 has M3=12, +M4=0 and lambda=256>192, so its local cylinder satisfies (A2). + +For f1 the vertical path x=-1/2,0<=y<=1/16 has values + + 65536(y^2-1/1024)^2-1/16+y^5 >=-1/16>-1, + +and its endpoint has value 1/2+1/16^5>0. It connects M to an older point above the +candidate saddle level. Therefore S cannot be its elder partner in any extension +preserving this path. This is an exact continuous path inequality, not an endpoint +sampling argument. The example does not contradict CAP: f1_yyyy(M)=24*65536, so it +violates the required whole-neighborhood fourth-derivative bound severely. It +shows why local pictures, pins or third jets alone cannot replace (A2). + +## 7. How the deterministic audit plugs into D1, and the corrected reading set + +P §7 uses exactly (A2). P §8 establishes Morse/distinct-value genericity for each +fixed conditional law and transfers it to Q^W by absolute continuity; no common +null set for all uncountably many parameters is asserted. The cap proof therefore +implies pointwise on that full-measure locus + + 1{S not the ordinary elder partner of M} <= 1{G_r fails}. + +Its expectation under the ORIGINAL full weight is bounded by Q^W(G_r^c). The +separate matrix calculation in P §§3–7 gives E_Q[W 1{G_r^c}]=O(r^5), while the +full Z_r is of order r^2; that supplies the O(r^3) probability bound. Today's +deterministic proof does not independently re-establish those stochastic inputs. +No regional D5 witness-collision mechanism is used to prove this implication. + +The citable parent is NOT its immutable uncorrected text in isolation: + +- P §5 must use E1: `D_r=diag(r^(-1/2),I)`. For H=[[r alpha,r beta^t],[r beta,A]], + `D_r H D_r=[[alpha,sqrt(r) beta^t],[sqrt(r) beta,A]]` and det(D_r H D_r)=det(H)/r. + The old diag(sqrt(r),I) would give r^2 alpha, not alpha. +- REC §5 W1 supplies the correct joint-convergence reading for the type argument; + it does not pretend arbitrary conditioned fields live in an unspecified common + almost-sure coupling. +- P §9 is replaced by E2's Borel marked Kac–Rice proof; an elder indicator is not + assumed continuous. This is a second essential amendment, not just typography. +- REC supplies the explicit embedding radius r F(4, 3)*r*m3*m3/k and r*m4 <= F(3, 10)*k + + +def diagonal_congruence(matrix, diag): + n = len(diag) + diag = list(map(rational, diag)) + if len(matrix) != n or any(len(row) != n for row in matrix): + raise ValueError('square matrix/diagonal size mismatch') + return [[diag[i]*rational(matrix[i][j])*diag[j] for j in range(n)] for i in range(n)] + + +def falsifier(): + f0 = {(3, 0): F(2), (1, 0): -F(3, 2), (0, 0): -F(1, 2), + (0, 2): F(-128)} + return f0, add(f0, {(0, 4): F(65536), (0, 5): F(1)}) + + +def graph_data(weights, edges, start): + if start not in weights: + raise ValueError('missing start vertex') + weights = {v: rational(w) for v, w in weights.items()} + adj = {v: set() for v in weights} + for a, b in edges: + if a not in weights or b not in weights: + raise ValueError('edge refers to absent vertex') + adj[a].add(b) + adj[b].add(a) + return weights, adj + + +def graph_maximin(weights, edges, start): + """Widest-path algorithm to any strictly older vertex; None means essential.""" + weights, adj = graph_data(weights, edges, start) + score = {start: weights[start]} + done = set() + while True: + candidates = [v for v in score if v not in done] + if not candidates: + return None + v = max(candidates, key=lambda z: score[z]) + if weights[v] > weights[start]: + return score[v] + done.add(v) + for w in adj[v]-done: + bottleneck = min(score[v], weights[w]) + if w not in score or bottleneck > score[w]: + score[w] = bottleneck + + +def graph_threshold_oracle(weights, edges, start): + """Independent threshold-connectedness oracle; no widest-path labels.""" + weights, adj = graph_data(weights, edges, start) + for threshold in sorted(set(weights.values()), reverse=True): + if weights[start] < threshold: + continue + pending = [start] + seen = {start} + while pending: + v = pending.pop() + if weights[v] > weights[start]: + return threshold + for w in adj[v]: + if w not in seen and weights[w] >= threshold: + seen.add(w) + pending.append(w) + return None + + +def main(): + print(json.dumps({'scope': 'finite exact controls only; not D1 formal verification', + 'scientific_effect': 'NONE', + 'constants': {key: str(x) for key, x in constants().items()}}, + indent=2, sort_keys=True)) + + +if __name__ == '__main__': + main() diff --git a/reviews/d1_external_audit_20260930/test_cap_audit.py b/reviews/d1_external_audit_20260930/test_cap_audit.py new file mode 100644 index 000000000..73110a5f1 --- /dev/null +++ b/reviews/d1_external_audit_20260930/test_cap_audit.py @@ -0,0 +1,123 @@ +from fractions import Fraction as F +from itertools import product, combinations +import unittest +import cap_audit as c + +class ExactGeometry(unittest.TestCase): + def test_constants(self): + a=c.constants() + self.assertEqual(a['ridge_lower'],F(2184415,7086244)) + self.assertGreater(a['ridge_lower'],F(1,4)) + self.assertEqual(a['axis_drop_normalized'],F(9,32)) + self.assertEqual(a['axis_excess_normalized'],F(11,96)) + self.assertEqual(a['side_drop_normalized'],F(4400,121)) + def test_forced_hermite_mean(self): + # Exact positive Hermite kernel, not a sampled derivative. + ker={(0,):F(1,4),(2,):F(-1)} + self.assertEqual(c.integral(ker,F(-1,2),F(1,2)),F(1,6)) + self.assertEqual(-F(1,2)*2*c.integral(ker,F(-1,2),F(1,2)),-F(1,6)) + def test_general_mark_scaling(self): + for r in (F(1),F(1,10),F(1,100)): + for k in (F(1,6),F(1),F(3)): + m=12*k; n=0; lam=200*k*r + self.assertTrue(c.good_event(r,k,m,n,lam)) + self.assertTrue(c.good_event(r,F(1,6),m/(6*k),n,lam/(6*k))) + self.assertEqual(6*k*F(9,32)*r**3,F(27,16)*k*r**3) + def test_depth_and_fourth_derivative_are_required(self): + self.assertFalse(c.good_event(1,1,12,0,192)) + self.assertTrue(c.good_event(1,1,12,F(3,10),256)) + self.assertFalse(c.good_event(1,1,12,F(31,100),256)) + def test_invalid_rational_inputs(self): + for x in (True,1.0,'1'): + with self.assertRaises((TypeError,ValueError)):c.good_event(x,1,12,0,256) + with self.assertRaises(ValueError):c.good_event(1,0,12,0,256) + def test_vector_average_no_common_rolle_zero(self): + # w=(x^2-1/4, x^3-x/4), w(+/-1/2)=0; + # w'_1=2x vanishes only at0, w'_2(0)=-1/4. + w1={(2,):F(1),(0,):-F(1,4)}; w2={(3,):F(1),(1,):-F(1,4)} + for x in (F(-1,2),F(1,2)): + self.assertEqual(c.value(w1,(x,)),0);self.assertEqual(c.value(w2,(x,)),0) + self.assertEqual(c.value(c.derivative(w1,0),(F(0),)),0) + self.assertEqual(c.value(c.derivative(w2,0),(F(0),)),-F(1,4)) + self.assertEqual(c.integral(c.derivative(w1,0),F(-1,2),F(1,2)),0) + self.assertEqual(c.integral(c.derivative(w2,0),F(-1,2),F(1,2)),0) + def test_vector_ridge_third_derivative(self): + # f=q(x)-lambda_i/2 (y_i-h_i(x))^2; g=q independently. + dim=3; x=c.variable(dim,0); y=c.variable(dim,1); z=c.variable(dim,2) + one={(0,0,0):F(1)} + q=c.add(c.scale(c.power(x,3),2),c.scale(x,-F(3,2)),c.scale(one,-F(1,2))) + for t in (F(-2),F(1,3),F(2)): + h1=c.scale(c.add(c.power(x,2),c.scale(one,-F(1,4))),t) + h2=c.scale(c.add(c.power(x,3),c.scale(x,-F(1,4))),t) + f=c.add(q,c.scale(c.power(c.add(y,c.scale(h1,-1)),2),-7),c.scale(c.power(c.add(z,c.scale(h2,-1)),2),-11)) + for xx in (F(-3,4),F(0),F(2,3)): + pt=(xx,c.value(h1,(xx,0,0)),c.value(h2,(xx,0,0))) + vv=(F(1),c.value(c.derivative(h1,0),pt),c.value(c.derivative(h2,0),pt)) + answer=F(0) + for i,j,k in product(range(dim),repeat=3): + dd=c.derivative(c.derivative(c.derivative(f,i),j),k) + answer+=c.value(dd,pt)*vv[i]*vv[j]*vv[k] + self.assertEqual(answer,12) + self.assertEqual(c.value(c.derivative(f,1),pt),0) + self.assertEqual(c.value(c.derivative(f,2),pt),0) + def test_congruence_erratum(self): + t=F(1,4);r=t*t; a=-6;b=3;A=-2 + H=[[r*a,r*b],[r*b,A]] + correct=c.diagonal_congruence(H,[1/t,1]);wrong=c.diagonal_congruence(H,[t,1]) + self.assertEqual(correct,[[F(-6),F(3,4)],[F(3,4),F(-2)]]) + self.assertNotEqual(wrong,correct) + self.assertEqual(wrong[0][0],r*r*a) + +class JetFalsifier(unittest.TestCase): + def test_same_three_jets_but_older_route(self): + f0,f1=c.falsifier() + for xx in (F(-1,2),F(1,2)): + for total in range(4): + for i in range(total+1): + a,b=f0,f1 + for _ in range(i):a=c.derivative(a,0);b=c.derivative(b,0) + for _ in range(total-i):a=c.derivative(a,1);b=c.derivative(b,1) + self.assertEqual(c.value(a,(xx,0)),c.value(b,(xx,0))) + self.assertEqual(c.value(f0,(F(-1,2),0)),0) + self.assertEqual(c.value(f0,(F(1,2),0)),-1) + self.assertTrue(c.good_event(1,1,12,0,256)) + self.assertGreater(c.value(f1,(F(-1,2),F(1,16))),0) + def test_entire_shortcut_not_just_endpoints(self): + # Along x=-1/2, polynomial is 65536(y^2-1/1024)^2 -1/16 + y^5. + y=c.variable(2,1);one={(0,0):F(1)} + exact=c.add(c.scale(c.power(c.add(c.power(y,2),c.scale(one,-F(1,1024))),2),65536),c.scale(one,-F(1,16)),c.power(y,5)) + f0,f1=c.falsifier() + section={} + for (i,j),a in f1.items():section[(0,j)]=section.get((0,j),F(0))+a*F(-1,2)**i + self.assertEqual(c.clean(section),c.clean(exact)) + # y>=0 gives the path-wide lower bound -1/16 > saddle height -1. + self.assertGreater(-F(1,16),-1) + def test_changed_neighborhood_norm_blocks_false_promotion(self): + _,f1=c.falsifier();four=f1 + for _ in range(4):four=c.derivative(four,1) + self.assertEqual(c.value(four,(F(-1,2),0)),24*65536) + self.assertFalse(c.good_event(1,1,12,24*65536,256)) + +class TopologyAnalogue(unittest.TestCase): + def test_ridge_alone_not_sufficient(self): + weights={'M':F(0),'S':F(-1),'O':F(1),'B':-F(1,2)} + edges=[('M','S'),('S','O'),('M','B'),('B','O')] + self.assertEqual(c.graph_maximin(weights,edges,'M'),-F(1,2)) + self.assertEqual(c.graph_maximin(weights,edges[:2],'M'),-1) + def test_boundary_alone_not_sufficient(self): + self.assertIsNone(c.graph_maximin({'M':F(0),'S':F(-1)},[('M','S')],'M')) + def test_equal_birth_is_not_an_older_endpoint(self): + self.assertIsNone(c.graph_maximin({'M':F(0),'S':F(-1),'T':F(0)},[('M','S'),('S','T')],'M')) + def test_arbitrary_exterior_does_not_bypass_full_cut(self): + count=0;ext=['O','A','B','C'];optional=list(combinations(ext,2)) + for vals in product((F(-3),-F(1,2),F(2)),repeat=3): + weights={'M':F(0),'I':-F(1,4),'S':F(-1),'L':F(-2),'O':F(1),**dict(zip(ext[1:],vals))} + for mask in range(1<>j&1] + got=c.graph_maximin(weights,edges,'M') + self.assertEqual(got,-1) + self.assertEqual(got,c.graph_threshold_oracle(weights,edges,'M')) + count+=1 + self.assertEqual(count,1728) + +if __name__=='__main__':unittest.main() diff --git a/reviews/d1_external_audit_20260930/test_sources.py b/reviews/d1_external_audit_20260930/test_sources.py new file mode 100644 index 000000000..76850b642 --- /dev/null +++ b/reviews/d1_external_audit_20260930/test_sources.py @@ -0,0 +1,53 @@ +"""Local real-Git fixtures test custody behavior, not the project premises.""" +import hashlib +import os +from pathlib import Path +import subprocess +import tempfile +import unittest +import verify_sources as v + +class SourcesTests(unittest.TestCase): + def setUp(self): + t=tempfile.TemporaryDirectory();self.addCleanup(t.cleanup);self.repo=Path(t.name) + (self.repo/'imports').mkdir();self.data=b'fixture source only\n' + (self.repo/'imports/P.md').write_bytes(self.data) + self.git('init','-q');self.git('add','imports');self.git('commit','-qm','original') + self.commit=self.git('rev-parse','HEAD').decode().strip() + self.entry={'path':'imports/P.md','git_blob':self.git('rev-parse','HEAD:imports/P.md').decode().strip(), + 'bytes':len(self.data),'sha256':hashlib.sha256(self.data).hexdigest()} + self.nested=self.repo/'reviews/packet';self.nested.mkdir(parents=True) + def git(self,*args): + env=os.environ.copy();env.pop('GIT_NO_REPLACE_OBJECTS',None) + return subprocess.run(['git','-c','user.name=Fixture','-c','user.email=fixture@example.invalid',*args], + cwd=self.repo,env=env,capture_output=True,check=True,timeout=15).stdout + def test_valid_from_nested_directory(self): + self.assertEqual(v.verify_bindings(self.nested,self.commit,[self.entry]),1) + def test_bad_identities(self): + for key,val in [('git_blob','0'*40),('bytes',0),('sha256','0'*64)]: + with self.subTest(key=key),self.assertRaises(ValueError): + v.verify_bindings(self.nested,self.commit,[dict(self.entry,**{key:val})]) + def test_bad_paths_and_inventories(self): + for path in ['../P.md','/imports/P.md','imports//P.md','missing.md']: + with self.subTest(path=path),self.assertRaises(ValueError): + v.verify_bindings(self.nested,self.commit,[dict(self.entry,path=path)]) + with self.assertRaises(ValueError):v.verify_bindings(self.nested,self.commit,[]) + with self.assertRaises(ValueError):v.verify_bindings(self.nested,self.commit,[self.entry,self.entry]) + def test_only_real_commit(self): + for obj in ['HEAD^{tree}','HEAD:imports/P.md']: + with self.subTest(obj=obj),self.assertRaises(ValueError): + v.verify_bindings(self.nested,self.git('rev-parse',obj).decode().strip(),[self.entry]) + def test_symlink_source(self): + p=self.repo/'imports/P.md';p.unlink();p.symlink_to('../target') + self.git('add','imports');self.git('commit','-qm','link') + with self.assertRaises(ValueError):v.verify_bindings(self.nested,self.git('rev-parse','HEAD').decode().strip(),[self.entry]) + def test_replacement_does_not_forge_or_invalidate(self): + forged=b'replaced\n';(self.repo/'imports/P.md').write_bytes(forged) + self.git('add','imports');self.git('commit','-qm','replacement') + new=self.git('rev-parse','HEAD').decode().strip();self.git('replace',self.commit,new) + self.assertEqual(self.git('show',self.commit+':imports/P.md'),forged) + self.assertEqual(v.verify_bindings(self.nested,self.commit,[self.entry]),1) + altered=dict(self.entry,git_blob=self.git('rev-parse','HEAD:imports/P.md').decode().strip(),bytes=len(forged),sha256=hashlib.sha256(forged).hexdigest()) + with self.assertRaises(ValueError):v.verify_bindings(self.nested,self.commit,[altered]) + +if __name__=='__main__':unittest.main() diff --git a/reviews/d1_external_audit_20260930/verify_sources.py b/reviews/d1_external_audit_20260930/verify_sources.py new file mode 100644 index 000000000..2a8606478 --- /dev/null +++ b/reviews/d1_external_audit_20260930/verify_sources.py @@ -0,0 +1,92 @@ +"""Verify packet and historical source bytes; this never certifies their mathematics.""" +import argparse +import hashlib +import json +import os +from pathlib import Path, PurePosixPath +import re +import subprocess + +IDS = {'P','CAP','E1','E2','REC','R','R_REVIEW','SIDE24','REGION','FORMAL'} + + +def read_json(path): + def unique(pairs): + out={} + for k,v in pairs: + if k in out:raise ValueError('duplicate JSON key') + out[k]=v + return out + if path.is_symlink() or not path.is_file():raise ValueError('regular JSON required') + out=json.loads(path.read_text(encoding='utf-8'),object_pairs_hook=unique) + if not isinstance(out,dict):raise ValueError('JSON object required') + return out + + +def safe_path(path): + if not isinstance(path,str) or not path:raise ValueError('path required') + p=PurePosixPath(path) + if p.is_absolute() or str(p)!=path or any(x in ('.','..') or not re.fullmatch('[A-Za-z0-9_.-]+',x) for x in p.parts): + raise ValueError('unsafe source path') + return p.parts + + +def git(root,*args): + result=subprocess.run(['git','--no-replace-objects',*args],cwd=root, + env=dict(os.environ,GIT_NO_REPLACE_OBJECTS='1'),capture_output=True,timeout=45) + if result.returncode:raise ValueError('historical Git object unavailable: '+result.stderr.decode(errors='replace')[:180]) + return result.stdout + + +def identity(data,entry): + blob=hashlib.sha1(b'blob '+str(len(data)).encode()+b'\0'+data).hexdigest() + if blob!=entry['git_blob']:raise ValueError('Git blob mismatch: '+entry['path']) + if 'bytes' in entry and (type(entry['bytes']) is not int or len(data)!=entry['bytes']): + raise ValueError('size mismatch: '+entry['path']) + if 'sha256' in entry and hashlib.sha256(data).hexdigest()!=entry['sha256']: + raise ValueError('SHA256 mismatch: '+entry['path']) + + +def verify_bindings(root,commit,entries): + if not isinstance(commit,str) or not re.fullmatch('[0-9a-f]{40}',commit):raise ValueError('full commit required') + if not entries or len({e['path'] for e in entries})!=len(entries):raise ValueError('nonempty unique inventory required') + if git(root,'cat-file','-t',commit).strip()!=b'commit':raise ValueError('not a commit object') + for entry in entries: + ps=safe_path(entry['path']) + for j in range(1,len(ps)+1): + prefix='/'.join(ps[:j]) + rows=[x for x in git(root,'ls-tree','--full-tree','-z',commit,'--',prefix).split(b'\0') if x] + if len(rows)!=1:raise ValueError('missing source path') + meta,name=rows[0].split(b'\t',1);mode,kind,blob=meta.decode().split() + if name.decode()!=prefix:raise ValueError('path mismatch') + if j