diff --git a/.github/workflows/c6-residual-closure.yml b/.github/workflows/c6-residual-closure.yml new file mode 100644 index 000000000..be39b64ba --- /dev/null +++ b/.github/workflows/c6-residual-closure.yml @@ -0,0 +1,72 @@ +name: C6 residual closure checks + +'on': + pull_request: + paths: + - 'reviews/c6_residual_closure_20260930/**' + - '.github/workflows/c6-residual-closure.yml' + - 'frontiers/spectral_cluster_closure_20260929/PROOF.md' + - 'frontiers/spectral_cluster_closure_20260929/REVIEW_RECORD.md' + - 'frontiers/spectral_cluster_closure_20260929/README.md' + - 'frontiers/c6_cluster_law_20260929/PROOF.md' + - 'frontiers/c6_cluster_law_20260929/README.md' + - 'frontiers/c6_cluster_law_20260929/SOURCE_MAP.json' + - 'frontiers/c6_palm_route_20260929/PROOF.md' + - 'frontiers/two_scale_cluster_geometry_20260929/TWO_SCALE_LAW.md' + - 'frontiers/two_scale_cluster_geometry_20260929/REVIEW_RECORD.md' + - 'frontiers/two_scale_cluster_geometry_20260929/REVIEW_RECORD.json' + - 'frontiers/downstream_gate_20260925/GRAPH.json' + - 'frontiers/downstream_gate_20260925/SELECTOR_REGION.json' + - 'frontiers/downstream_gate_20260925/hard_gate.py' + workflow_dispatch: + +permissions: + contents: read + +jobs: + exact-and-probe: + runs-on: ubuntu-latest + timeout-minutes: 10 + steps: + - uses: actions/checkout@11d5960a326750d5838078e36cf38b85af677262 + with: + persist-credentials: false + - uses: actions/setup-python@a26af69be951a213d495a4c3e4e4022e16d87065 + with: + python-version: '3.11.16' + - name: Verify sources, replay both modes, reject mutants + env: + PYTHONDONTWRITEBYTECODE: '1' + run: | + set -euo pipefail + python -B -S - <<'PY' + import hashlib, json, pathlib, subprocess, sys + root = pathlib.Path('reviews/c6_residual_closure_20260930').resolve() + manifest = json.loads((root / 'SOURCE_FILES.json').read_text())['files'] + present = sorted(p.name for p in root.iterdir()) + expected_names = sorted([e['path'] for e in manifest] + ['SOURCE_FILES.json']) + if present != expected_names: + raise ValueError('packet tree differs from manifest: ' + repr(present)) + for entry in manifest: + path = root / entry['path'] + if pathlib.PurePosixPath(entry['path']).name != entry['path'] or path.is_symlink(): + raise ValueError('flat regular source required: ' + entry['path']) + data = path.read_bytes() + if len(data) != entry['bytes'] or hashlib.sha256(data).hexdigest() != entry['sha256']: + raise ValueError('source identity mismatch: ' + entry['path']) + script = str(root / 'residual_check.py') + expected = (root / 'RESULTS.json').read_bytes() + mutants = ['allow-symlink', 'no-hash', 'stale-fingerprint', 'drop-required-edge', 'executed-flag', 'controlling-true', 'tail-reversed', 'pair-identity-broken', 'route-c-broken', 'drop-review-needle', 'installed-drift', 'snapshot-omitted', 'record-unreviewed', 'reviewed-text-drift'] + for flags in (['-B', '-S'], ['-B', '-O', '-S']): + out = subprocess.run([sys.executable, *flags, script], + check=True, capture_output=True, timeout=300).stdout + if out != expected: + raise RuntimeError('output differs from RESULTS.json under ' + ' '.join(flags)) + for m in mutants: + rc = subprocess.run([sys.executable, *flags, script, '--mutant', m], + capture_output=True, timeout=300).returncode + if rc != 1: + raise RuntimeError('mutant ' + m + ' not rejected') + print(json.dumps({'scientific_effect': 'NONE', 'mathematical_acceptance': False})) + PY + git diff --exit-code diff --git a/reviews/c6_residual_closure_20260930/EXTERNAL_REVIEWS.md b/reviews/c6_residual_closure_20260930/EXTERNAL_REVIEWS.md new file mode 100644 index 000000000..70d05080e --- /dev/null +++ b/reviews/c6_residual_closure_20260930/EXTERNAL_REVIEWS.md @@ -0,0 +1,99 @@ +# External reviews preserved for C6-RESIDUAL-CLOSURE-20260930-v1 + +**Object:** C6-RESIDUAL-CLOSURE-EXTERNAL-REVIEWS-20260930-v1 (component of the residual-closure record; source of the +proposed graph node `math.c6r-component.cluster-law-acceptance`; since v1.3 also the preserved copy of Math-#173 review +5360645884, the non-Claude read of this record's §3 on which `math.c6r-component.residual-closure-record` rests). +**What this is.** The nonauthor acceptance of the C6 cluster law (Math-#159, `frontiers/c6_cluster_law_20260929/PROOF.md`, +blob `ba492c8e62e58bfc055fc8254c790e893d346ba5`, the bytes now on `main`) is a GitHub pull-request review, not a file in +the repository. It is read back on 30 September 2026 through the session's GitHub connector and transcribed here with +its identity fields (review id, URL, posting account, provider named in the body, commit reviewed, `submitted_at`). +Everything is reproduced as returned. The in-repository pointer to the same acceptance is +`frontiers/c6_cluster_law_20260929/SOURCE_MAP.json` (`nonauthor_acceptance: true`; `revision_note`: "Nonauthor +acceptance recorded on 30 September 2026 (review 5360192822); proof bytes frozen"). +**Status of this evidence.** A pull-request review is a mutable external object: this file preserves what was read, it +does not make the review immutable, and an offline check cannot re-authenticate it (the packet checker is stdlib-only +and has no network). What the checker binds is this file's bytes and the presence of the quoted verdict lines in it +(`VERDICTS`). The reviewer states its exposure (author of earlier imported sources and of Math-#161) and that the read +is not organizational independence; nothing here adds a review or a provider. No Cursor agent was contacted or +restarted (owner stop of 27 September 2026). Same GitHub account throughout; zero organizational-independence credit. +The Math-#162 reviews (A 5359968447, B 5359845136, C 5359879627, D 5360082678) are recorded in the repository itself, +in `frontiers/spectral_cluster_closure_20260929/REVIEW_RECORD.md`, and are not repeated here. + +## Index + +| # | Object | PR | Review | Posted by | Provider named | Commit reviewed | `submitted_at` | Verdict line | +|---|---|---|---|---|---|---|---|---| +| 1 | Math-#159 `frontiers/c6_cluster_law_20260929/PROOF.md`, blob `ba492c8e…` | Math-#159 | 5360192822 | `d6g8k5htny-coder` (owner account; the body names OpenAI / GPT-6 Astra Pro) | OpenAI / GPT-6 Astra Pro, source-exposed nonauthor | `f7c33955d005c03d1010835f52f500c4b853a847` | 2026-09-30T00:44:51Z | "VERDICT: ACCEPT Theorem N, Corollaries Lambda/S, and the explicitly sequential NEAR POINT-INTENSITY Corollary X at the stated fixed-d, fixed-torus, compact-positive-gap parameter scope, conditional only on the exact reviewed SOURCE_MAP inputs." | +| 2 | this record, `RECONCILIATION.md` §3 at head `b3fac79` ((D1), Route A, Route B; preserved in `REVIEWED_SECTION_3_b3fac79.md`) | Math-#173 | 5360645884 | `d6g8k5htny-coder` (owner account; the body names OpenAI / GPT-5.6 Sol) | OpenAI / GPT-5.6 Sol, source-exposed nonauthor (integrator of Math-#162/#166) | `b3fac79875f28bacd135c0aa5e65a47a41ae0fdf` | 2026-09-30T02:06:27Z | "MATHEMATICAL VERDICT ON §3: ACCEPT at the stated fixed-d, fixed-torus, compact-positive-gap window scope." | + +The earlier reviews on the same pull request (5359646638 on v1.0, 5359895261 and 5359896676 and 5359999003 on v1.1, +5360034762 and 5360171253 on v1.2) are AMEND records and narrow closures superseded by 5360192822 for the repaired +source; they are cited, not preserved. + +## 1. Math-#159 review 5360192822 (OpenAI, ACCEPT at head `f7c3395`, PROOF blob `ba492c8e`) + +URL: https://github.com/d6g8k5htny-coder/Math-/pull/159#pullrequestreview-5360192822 · posted by `d6g8k5htny-coder` · commit `f7c33955d005c03d1010835f52f500c4b853a847` · submitted 2026-09-30T00:44:51Z + +`````text +OpenAI / GPT-6 Astra Pro NONAUTHOR successor analytic review at exact f7c33955d005c03d1010835f52f500c4b853a847, PROOF blob ba492c8e62e58bfc055fc8254c790e893d346ba5. This completes my AMEND5359895261 and residual-frame follow-up5901687719. I authored earlier imported sources and #161: source-exposed review of Claude's new consumer, not independent revalidation of those inputs or organizational independence. No author-checker execution is claimed. + +VERDICT: ACCEPT Theorem N, Corollaries Lambda/S, and the explicitly sequential NEAR POINT-INTENSITY Corollary X at the stated fixed-d, fixed-torus, compact-positive-gap parameter scope, conditional only on the exact reviewed SOURCE_MAP inputs. The prior four substantive objections and the remaining residual-frame issue are repaired. No remaining mathematical blocker found. This is not a current-base merge receipt or a scientific-register transition. + +1. Normalization and marked moments. Lemmas4.2/5.2 now place original Z^-1 outside Q_r integrals once and W inside once. The O(r³) regional integral is explicitly normalized. The squared-weight geometric factors survive conditional Cauchy-Schwarz; every additional fixed derivative/beta power is absorbed by the actual regional penalty. The all-height bound in a fixed Ar neighborhood uses the fixed-radius collar result with A-dependent constants, not a global all-height theorem. + +2. Remote covariance. The collar whitens its complete raw three-site vector: cr10 covariance floor, O(r6) whole remainder, hence O(r) whitened error against J5. The pin ball now uses Yperp=Y-E[Y|U_r], independent of U_r; its covariance is the conditional source covariance, so the joint covariance is block diagonal and uniformly positive. Residualizing DL4.2 gives B(J-E[J|U_r])+Rperp, with bounded B/regression coefficients and O(r) remainder. Both blocks are therefore linear images of J5 plus O(r) in PRIOR L2. The quantitative projection estimate gives Cov(Yremote|V)>=(sqrt(gamma)-sqrt(M)*eta_r)_+²I >=gamma/4. Coarsening from full collar V to the actual pin+gradient kernel increases conditional covariance; the auxiliary witness value is never imposed on that kernel. +Nonblocking coordinate clarification: DL's local derivatives are written at the pin-centered origin. To express them through MIDPOINT J5, Taylor-translate by +/-r/2 and include the O_L2(r) term in Rperp. The needed statement is J=TJ J5+O(r), not literal equality at distinct sites. This lies within the retained remainder and requires no stronger hypothesis. + +3. Remote means. The successor conditions transitively UNDER Q_r, first on Lambda=tau and then Yremote=(0,t). First-stage means are O(1+beta_X); the second inverse covariance has the newly proved floor; Hessian residual covariances stay bounded. The resulting d-th moment is O_rho((1+beta_X)^d(1+|t|)^d), stronger than the retained2d bound. Integrating kr³ and applying normalized marked Cauchy-Schwarz gives the expectation O_(A,rho)(r^(9/2)), not merely a probability estimate. A,rho stay fixed in that estimate. + +4. Cubic and domination. I reconstructed the new shear, determinant -3k(B+4su), and all B/D cases. Every strict-window extra point is a saddle. The constant32 range is valid: for B<0,x=-s>=2|B|, the displayed argument gives x³<(144/49)(32/3)kD²<32kD². Other sign/zero cases agree. The support bound yields an actual common polynomial-times-Gaussian majorant for coefficients, continuity and outer-radius tails. It does not infer a stronger integrability statement from pointwise finiteness. + +5. Cutoff and near limit. Kap_0 is now built from finite mixtures ON THE SINGULAR SLICE, exhausted by compact hard-jet boxes and Haar U. Fubini supplies atom-free cutoffs for almost every target on the measure actually integrated. At varying parameters choose these levels at the limiting parameter of a compact subsequence, not through an uncountable intersection. The no-inverse-D majorant handles nearly singular/multiple hard spectra in measure; hard inversion is pointwise only at nonsingular targets. The pin-degeneracy/spatial-boundary strata are null; type weight vanishes off the relevant limiting domain. In d=2 use the explicitly separate planar Hadamard bound with no lambda2. + +6. Global law and uniformity. Fixed A,rho near convergence, shell error Cr³(A^-2+rho²), remote coefficient k integral Lambda and repaired near/far expectation give the probability sandwich. Take r->0 before the outer radii. For compact-parameter uniformity, an arbitrary violating sequence has a convergent parameter subsequence: the limiting-parameter atom-free cutoff, joint field regression coupling, stable roots and common majorants yield the same limit along it. The uniform shell bound handles the outer-radius step. This is a joint sequential argument, not pointwise continuity alone. Positivity uses the open typed cubic examples and the positive remote kernel. + +7. Consumers. The support{1,2} is that of the limiting NONZERO rare intensity, not finite-r support. The C6(q+1) tail C/(M-q) gives all fixed factorial coefficients; q>=3 vanish. Nonempty and size-biased denominators differ. Independent-replica compound convergence is the credited RCL consequence, not spatial independence. X is only a near point-intensity limit, r then radius; remote singletons escape1/r scaling. No full configuration-law assertion remains. + +Fresh local evidence:14 independent reviewer tests/mode,5 semantic mutants/mode,6 identical JSON pairs, no execution errors. Includes raw-frame counterexample, projection residuals, transitive means, one-Z identity, finite Gaussian covariance bounds,2052 exact stationary-cubic configurations and factorial tails. This is NOT the author's201720-case checker, a full source checkout or a Lean proof. Current source/CI/merge evidence remains separate. + +Historical AMENDs are superseded only for this repaired source. No STATUS/GRAPH/prize/premise or numerical-coefficient change follows. A prior submission disconnected; I read all existing review pages, found no copy at this head, and am submitting this single replacement record. +````` + +## 2. Math-#173 review 5360645884 (OpenAI / GPT-5.6 Sol, ACCEPT of §3 at head `b3fac79`) + +URL: https://github.com/d6g8k5htny-coder/Math-/pull/173#pullrequestreview-5360645884 · posted by `d6g8k5htny-coder` · commit `b3fac79875f28bacd135c0aa5e65a47a41ae0fdf` · submitted 2026-09-30T02:06:27Z · state COMMENTED (the verdict is in the body) · body 2781 bytes as read back through the connector (JSON-decoded, no trailing newline), SHA256 `ef9660729332582e31963c7b5ad8ce5e2f54f926f3ef6657ca12473aff6e6b60` + +What it covers: §3 as it stood at `b3fac79`, i.e. (D1), Route A and Route B (items 1–5 of the body); the four sources re-read on +main `fa1cf7b`. It does not cover Route C (added in v1.1; OpenAI-authored, checked in Math-#160 comment 5902616692) or the +Theorem L paragraph (Math-#166's own reviewed statement). Its amend list (Codex findings; stale "pending" wording; promotion of +the record node on the reviewed-record path with the #166 path as a distinct alternative) is answered in v1.3 +(`RECONCILIATION.md` §§5–7). The reviewer states source exposure and that the read is not organizational independence. +Codex review 5360636576 (three inline engineering threads 4140125558, 4140125562, 4140125565 on `residual_check.py`) is cited +in `RECONCILIATION.md` §7 and answered in v1.3; it is not preserved here. + +`````text +OpenAI / GPT-5.6 Sol bounded NON-CLAUDE read of §3 at exact head b3fac79875f28bacd135c0aa5e65a47a41ae0fdf. I am source-exposed to the OpenAI side of the chain and integrated #162/#166; this is not independent revalidation of their premises or organizational independence. I did not author this reconciliation. + +MATHEMATICAL VERDICT ON §3: ACCEPT at the stated fixed-d, fixed-torus, compact-positive-gap window scope. + +I re-read the exact landed sources on current main fa1cf7b5: +- SC PROOF blob 16c56821: (24) gives the mixed event o(r^3); §8 gives the polynomial-tail domination and (26) E(N)_2/r^3 -> 2 nu2 = 2 a2; §6 gives a_2^R -> a_2. +- CL PROOF blob ba492c8e: Proposition 4.4 gives the fixed-A near coordinate limits and A->∞ exhaustion; Lemma 5.2 gives E[N^A 1{N_far>=1}] <= C(A,rho) r^(9/2); Corollary Lambda supplies the full factorial-moment limit. +- PALM PROOF blob 89eb8adf: Theorem Q supplies O(r^3) factorial moments for every fixed q, so the q=3/q=4 uniform-integrability steps are licensed. +- TWO_SCALE_LAW blob a32fd5f7 is now landed via #166 and states Theorem L directly for every admissible moving cutoff and q>=2. + +The bookkeeping is correct: +1. (N)_2-(N_R)_2 = 2 N_R N_out + (N_out)_2 exactly. +2. For n>M>=3, n(n-1) <= n(n-1)(n-2)/(M-1), so PALM q=3 controls the second-factorial tail and upgrades the fixed-R coordinate limit to r^-3 E[(N_R)_2] -> 2 a_2^R. +3. Combining with SC (26) gives the full limit r^-3 M_R -> 2(a_2-a_2^R), then R->∞ gives zero. +4. Route B is consistent. The auxiliary Hölder ledger 3/2+3/4+5/4=7/2 is correct; together with Lemma 5.2's r^(9/2) first-hit term it gives o(r^3) mixed count at fixed A,rho. +5. The order of limits is the claimed iterated one; no hidden uniform fixed-R rate is needed. + +Thus this review satisfies the requested non-Claude bounded read of §3 itself. + +ENGINEERING / SOURCE-STATE AMEND STILL REQUIRED before execution or integration of the proposal: +- Codex review 5360636576 found three real checker/transition defects: LIVE rejects exact installed component nodes after execution; reverse-impact replay omits old/new source snapshots; and the Math-#166 alternative can incorrectly promote this author record without a review. +- In addition, #166 is no longer pending: it merged at ab13a08f with unchanged TWO_SCALE_LAW blob a32fd5f7 and review 5360227991. The next revision should bind that landed direct-statement component explicitly and remove stale "pending/unmerged" language. Since this native review now ACCEPTS §3, the author-record node can instead be promoted on the reviewed-record path with this review id; the #166 path should remain a distinct alternative whose evidence is TWO_SCALE_LAW + its exact review binding. + +No GRAPH/STATUS/selector transition is authorized by this review. +````` diff --git a/reviews/c6_residual_closure_20260930/PROPOSED_TRANSITIONS.json b/reviews/c6_residual_closure_20260930/PROPOSED_TRANSITIONS.json new file mode 100644 index 000000000..3706e8ac4 --- /dev/null +++ b/reviews/c6_residual_closure_20260930/PROPOSED_TRANSITIONS.json @@ -0,0 +1,598 @@ +{ + "schema": 1, + "object": "C6-RESIDUAL-CLOSURE-20260930-v1", + "scientific_effect": "NONE", + "declarative": true, + "executed": false, + "disposition": "PROPOSAL_FOR_A_NON_CLAUDE_LANE", + "base_commit": "358f2562efbccc59f9549e5a79650e2e936395c3", + "residual_definition": { + "node": "math.rn-region.witness-collision.leading-mass-localization", + "fingerprint": "leading-order r^3 mass of E N(N-1): scale-r localization; open piece = mixed local/remote pairs M(R, s_0)", + "defined_in": "Math-#160 reviews/c6_witness_collision_reconciliation_20260929/RECONCILIATION.md section 5 (head eba6045; refreshed by the integrator onto fe2c3ff as dd4f4f8 with the packet bytes preserved; merged at 8d48d02, declarative, transitions not executed)", + "statement": "lim_{R->oo} limsup_{r->0} r^-3 E_{Q_r^W} #{ordered pairs of distinct window points not both within R r of the midpoint} = 0", + "identity": "that quantity equals E[(N)_2] - E[(N_R)_2] = 2 E[N_R N_out] + E[(N_out)_2]" + }, + "transitions": [ + { + "node": "math.rn-region.witness-collision.leading-mass-localization", + "kind": "region", + "current": { + "classification": "ABSENT", + "note": "Math-#160 proposes OPEN_ACTIVE, required by nothing" + }, + "proposed": { + "classification": "PROVED_REVIEWED", + "controlling": false, + "fingerprint": "leading-order r^3 mass of E N(N-1): scale-r localization; open piece = mixed local/remote pairs M(R, s_0)", + "layer": "D5", + "scope": "every fixed d >= 2, fixed torus L, fixed frame, compact birth and positive-gap marks (k_- > 0), height window I_r, original W_r and full Z_r; existential constants; conditional on the pinned inputs of Math-#162 and Math-#159 at their reviewed scopes", + "explicit_limits": "no rate; no numerical value of a_2, nu(1), nu(2) or C_3; no uniformity as k -> 0, in L or d; no all-height statement; no elder selection; no joint law of distinct pin pairs; no configuration statement (Math-#166 Theorem T, not consumed) and no d_TV statement (Math-#166 (V1), not consumed); the moving-cutoff form is Theorem L at its own scope; no historical numerical certificate", + "review_disposition": "ACCEPT_AT_EXISTENTIAL_SCOPE", + "review_sources": [ + { + "ref": "Math-#162 reviews 5359968447 / 5359845136 / 5359879627 (in-repo REVIEW_RECORD.md)", + "provider": "Anthropic, Anthropic (source-exposed), OpenAI/Codex", + "verdict": "ACCEPT A/B/C" + }, + { + "ref": "Math-#159 review 5360192822", + "provider": "OpenAI (source-exposed)", + "verdict": "ACCEPT Theorem N, Corollaries Lambda/S/X" + }, + { + "ref": "Math-#166 review 5360227991 (in-repo REVIEW_RECORD.md)", + "provider": "Anthropic (other session)", + "verdict": "ACCEPT Theorem L, the direct statement" + }, + { + "ref": "Math-#173 review 5360645884 (preserved in EXTERNAL_REVIEWS.md)", + "provider": "OpenAI (GPT-5.6 Sol; source-exposed, integrator of Math-#162/#166)", + "verdict": "ACCEPT section 3 ((D1), Route A, Route B) at the stated scope, at head b3fac79" + } + ], + "reading_rule": [ + "math.c6r-component.spectral-closure-proof", + "math.c6r-component.spectral-closure-review-record", + "math.c6r-component.cluster-law-proof", + "math.c6r-component.cluster-law-acceptance", + "math.c6r-component.cluster-law-source-map", + "math.c6-component.palm-proof", + "math.c6r-component.two-scale-law-proof", + "math.c6r-component.two-scale-review-record", + "math.c6r-component.two-scale-review-binding", + "math.c6r-component.residual-closure-record" + ], + "notes": "Leading-mass localization of E N(N-1) at scale r, in the iterated limit; corollary of Math-#162 (26)/(18)/(20) with PALM Theorem Q, and of Math-#159 Corollary Lambda / Proposition 4.4; direct statement Math-#166 Theorem L (L1)/(L2), bound; Route C pair-count corollary. Two evidence paths: the direct statement (Theorem L) and the reviewed corollary (section 3, read by OpenAI 5360645884). C6 residual closure v1.3." + }, + "required_premises_after": [ + "math.c6r-component.spectral-closure-proof", + "math.c6r-component.spectral-closure-review-record", + "math.c6r-component.cluster-law-proof", + "math.c6r-component.cluster-law-acceptance", + "math.c6r-component.cluster-law-source-map", + "math.c6-component.palm-proof", + "math.c6r-component.two-scale-law-proof", + "math.c6r-component.two-scale-review-record", + "math.c6r-component.two-scale-review-binding", + "math.c6r-component.residual-closure-record" + ], + "notes": "Created PROVED_REVIEWED if Math-#160 step 1 has not run; moved OPEN_ACTIVE -> PROVED_REVIEWED if it has. Every required premise is PROVED_REVIEWED on both evidence paths (direct statement: Math-#166 Theorem L; reviewed corollary: section 3, read by OpenAI 5360645884); the required edges take the union (fail-closed)." + }, + { + "node": "math.rn-region.witness-collision", + "kind": "region", + "current": { + "classification": "OPEN_ACTIVE", + "fingerprint": "eta->0 mutual witness separation" + }, + "proposed": { + "classification": "PROVED_REVIEWED", + "controlling": false, + "fingerprint": "eta->0 mutual witness separation", + "scope": "count estimate discharged by Math-#160 section 4 (PALM Theorem Q + EDL (A4)); localization discharged by this record; every fixed d >= 2 at the same scope", + "explicit_limits": "as Math-#160 section 5 and this record's section 4; no historical certificate; no mechanism beyond the count and the localization is defined anywhere in the register", + "review_disposition": "ACCEPT_AT_EXISTENTIAL_SCOPE", + "review_sources": [ + { + "ref": "Math-#160 (OpenAI 5359701805, xAI 5901915195 on sections 1 and 4)", + "provider": "OpenAI, xAI", + "verdict": "count discharge agreed" + }, + { + "ref": "this record", + "provider": "see section 0", + "verdict": "localization" + } + ], + "notes": "Deferred: executes only after Math-#160 step 3 (aggregate node math.c6-witness-collision-factorial-moment) and this record's residual node exist." + }, + "required_premises_after": [ + "math.rn-region.witness-collision.leading-mass-localization", + "math.c6-witness-collision-factorial-moment" + ], + "deferred": true, + "presupposes": [ + "Math-#160 execution_order step 3", + "this record's residual node" + ], + "notes": "Under Math-#160's keep-open execution the residual definition sits on this node and this transition is the one that moves it." + } + ], + "proposed_graph_nodes": [ + { + "id": "math.c6r-component.spectral-closure-proof", + "layer": "D5", + "kind": "reading_rule_component", + "classification": "PROVED_REVIEWED", + "controlling": false, + "component_of": "math.rn-region.witness-collision.leading-mass-localization", + "component_role": "proof", + "author_provider": "OpenAI (GPT-6 Astra Pro)", + "fingerprint": "e971b2cbe50a8a06b47c1219191201e0d1037c9adac23e5e3b7d2051bb70c2eb", + "source": "frontiers/spectral_cluster_closure_20260929/PROOF.md", + "scope": "Theorem (3); near limit (18); exhaustion (20); mixed event (24); factorial-moment limits (26); every fixed d >= 2, L, k > 0, b, frame; conditional on SOURCES.json inputs", + "review_basis": [ + { + "review": "Math-#162 review 5359968447", + "provider": "Anthropic Claude (no authorship of consumed sources)", + "verdict": "ACCEPT sections 2-3", + "depth": "full" + }, + { + "review": "Math-#162 review 5359845136", + "provider": "Anthropic Claude (authored consumed C6/DL/RC and Math-#159; source-exposed)", + "verdict": "ACCEPT sections 4-6", + "depth": "full" + }, + { + "review": "Math-#162 review 5359879627", + "provider": "OpenAI/Codex (same provider as the author)", + "verdict": "ACCEPT sections 7-8", + "depth": "full" + } + ] + }, + { + "id": "math.c6r-component.spectral-closure-review-record", + "layer": "D5", + "kind": "reading_rule_component", + "classification": "PROVED_REVIEWED", + "controlling": false, + "component_of": "math.rn-region.witness-collision.leading-mass-localization", + "component_role": "review_record", + "author_provider": "OpenAI-authored record of the Claude/Codex reviews", + "fingerprint": "6031d36697789097185a8e65bfbdf80f447e229689eac5a706ee8b0558db64a5", + "source": "frontiers/spectral_cluster_closure_20260929/REVIEW_RECORD.md", + "scope": "review record of Math-#162 at core blob 16c56821", + "review_basis": [ + { + "review": "frontiers/spectral_cluster_closure_20260929/REVIEW_RECORD.md", + "provider": "in-repo record", + "verdict": "A/B/C/D ACCEPT at stated scopes", + "depth": "record" + } + ] + }, + { + "id": "math.c6r-component.cluster-law-proof", + "layer": "D5", + "kind": "reading_rule_component", + "classification": "PROVED_REVIEWED", + "controlling": false, + "component_of": "math.rn-region.witness-collision.leading-mass-localization", + "component_role": "proof", + "author_provider": "Anthropic Claude (session 015wNj8L)", + "fingerprint": "96b8e2d59defee6059bf151a896b7fc7c91fc529b385a3db8a87574901197b38", + "source": "frontiers/c6_cluster_law_20260929/PROOF.md", + "scope": "Corollary Lambda (1.6); Proposition 4.4 (4.4) with A -> oo; Lemma 5.2 (5.4); every fixed d >= 2; conditional on SOURCE_MAP.json inputs", + "review_basis": [ + { + "review": "Math-#159 review 5360192822", + "provider": "OpenAI (GPT-6 Astra Pro; source-exposed as author of imported inputs and Math-#161)", + "verdict": "ACCEPT Theorem N, Corollaries Lambda/S, Corollary X at the stated scope, conditional on SOURCE_MAP inputs", + "depth": "full", + "at": "f7c33955d005c03d1010835f52f500c4b853a847 (same PROOF blob ba492c8e)" + } + ] + }, + { + "id": "math.c6r-component.cluster-law-acceptance", + "layer": "D5", + "kind": "reading_rule_component", + "classification": "PROVED_REVIEWED", + "controlling": false, + "component_of": "math.rn-region.witness-collision.leading-mass-localization", + "component_role": "review_record_external", + "author_provider": "OpenAI review 5360192822, transcribed by Anthropic (this session)", + "fingerprint": "27b4d8a5f04981e7b01b20f767078df87b4d0c75aebc6f6ed665347a8b605a53", + "source": "reviews/c6_residual_closure_20260930/EXTERNAL_REVIEWS.md", + "scope": "preserved transcriptions (5360192822 for [CL]; 5360645884 for this record's section 3); mutable external evidence, labelled; not an additional review or provider", + "review_basis": [ + { + "review": "Math-#159 review 5360192822", + "provider": "OpenAI", + "verdict": "ACCEPT", + "submitted_at": "2026-09-30T00:44:51Z", + "commit": "f7c33955d005c03d1010835f52f500c4b853a847" + } + ], + "authentication": "mutable external evidence read back through the session's GitHub connector on 2026-09-30; not byte-authenticated offline; in-repo pointer frontiers/c6_cluster_law_20260929/SOURCE_MAP.json" + }, + { + "id": "math.c6r-component.cluster-law-source-map", + "layer": "D5", + "kind": "reading_rule_component", + "classification": "PROVED_REVIEWED", + "controlling": false, + "component_of": "math.rn-region.witness-collision.leading-mass-localization", + "component_role": "review_record", + "author_provider": "Anthropic Claude (session 015wNj8L)", + "fingerprint": "0584c3808b633fceb3c308186b07d862eb4916053daf4e7bf1110592ec41f107", + "source": "frontiers/c6_cluster_law_20260929/SOURCE_MAP.json", + "scope": "consumed-input map and acceptance pointer of Math-#159 v1.2", + "review_basis": [ + { + "review": "frontiers/c6_cluster_law_20260929/SOURCE_MAP.json", + "provider": "in-repo pointer", + "verdict": "nonauthor_acceptance true; revision_note names review 5360192822", + "depth": "record" + } + ] + }, + { + "id": "math.c6-component.palm-proof", + "layer": "D5", + "kind": "reading_rule_component", + "classification": "PROVED_REVIEWED", + "controlling": false, + "component_of": "math.rn-region.witness-collision.leading-mass-localization", + "component_role": "proof", + "author_provider": "Anthropic Claude (session 015wNj8L)", + "fingerprint": "aa37f16040ab9e05bb2e4e3f1d678367497e8dc2cf43eef197a4d6592c2f129b", + "source": "frontiers/c6_palm_route_20260929/PROOF.md", + "scope": "Theorem Q, q = 3 and q = 4, uniform-integrability tails only", + "review_basis": [ + { + "review": "Math-#145 review 5358116559", + "provider": "OpenAI", + "verdict": "ACCEPT sections 5-7 and Theorem Q", + "depth": "full" + }, + { + "review": "Math-#145 review 5356233690", + "provider": "OpenAI", + "verdict": "ACCEPT section 4", + "depth": "full" + } + ], + "cross_record": "defined by Math-#160 PROPOSED_TRANSITIONS.json under the same id, source and fingerprint; create_if_absent", + "create_if_absent": true + }, + { + "id": "math.c6r-component.residual-closure-record", + "layer": "D5", + "kind": "reading_rule_component", + "classification": "PROVED_REVIEWED", + "controlling": false, + "component_of": "math.rn-region.witness-collision.leading-mass-localization", + "component_role": "reading_rule_record", + "author_provider": "Anthropic Claude (this session; source-exposed, see section 0)", + "fingerprint": "b647a186d0cfd1662fc69e9d31dfd447dbb1b2f6ef4364bbd59c4956f18aed25", + "source": "reviews/c6_residual_closure_20260930/RECONCILIATION.md", + "scope": "section 3: the corollary (D1) + steps 1-3 (Route A) and Route B, read by 5360645884 at b3fac79 and preserved verbatim in REVIEWED_SECTION_3_b3fac79.md; Route C (OpenAI-authored, checked 5902616692)", + "review_basis": [ + { + "review": "Math-#173 review 5360645884", + "provider": "OpenAI (GPT-5.6 Sol; source-exposed to the OpenAI side of the chain; integrator of Math-#162/#166; no authorship of this record)", + "verdict": "ACCEPT section 3 at the stated fixed-d, fixed-torus, compact-positive-gap window scope", + "depth": "bounded read of section 3 at head b3fac79 with the four sources re-read on main fa1cf7b", + "reviewed_head": "b3fac79875f28bacd135c0aa5e65a47a41ae0fdf", + "reviewed_text": "reviews/c6_residual_closure_20260930/REVIEWED_SECTION_3_b3fac79.md", + "reviewed_text_sha256": "931f5c95c5185be075c8684e30c395fe55dd344ad0c1ac45535e3b166c3aac65", + "covers": "(D1), Route A, Route B; not Route C and not the Theorem L paragraph", + "preserved_in": "reviews/c6_residual_closure_20260930/EXTERNAL_REVIEWS.md section 2", + "body_sha256": "ef9660729332582e31963c7b5ad8ce5e2f54f926f3ef6657ca12473aff6e6b60", + "submitted_at": "2026-09-30T02:06:27Z" + }, + { + "review": "Math-#160 comment 5902616692", + "provider": "Anthropic Claude (this session; provider-distinct nonauthor of the OpenAI-authored corollary 5901994240; source-exposed on RC)", + "verdict": "ACCEPT Route C at the stated scope", + "depth": "bounded", + "covers": "Route C only" + }, + { + "review": "Math-#173 review 5360751376", + "provider": "OpenAI (GPT-6 Astra Pro; author of Math-#162, contributor to Math-#166/#169; no authorship of this record)", + "verdict": "ACCEPT Route C as an elementary conditional implication of its stated estimates", + "depth": "bounded read of Route C at head 5d8f011 (RECONCILIATION.md blob fd5ad530); the Route C paragraph is unchanged since", + "covers": "Route C only; its amendment to the direct-statement paragraph is applied in v1.5" + } + ], + "notes": "reviewed-corollary evidence path; alternative to the direct-statement path; the promotion rests on 5360645884 and on the reviewed paragraphs standing unchanged (REVIEWED); a revision that alters them must obtain a new read or return this node to AUTHOR_SIDE_CANDIDATE" + }, + { + "id": "math.c6r-component.two-scale-law-proof", + "layer": "D5", + "kind": "reading_rule_component", + "classification": "PROVED_REVIEWED", + "controlling": false, + "component_of": "math.rn-region.witness-collision.leading-mass-localization", + "component_role": "proof", + "author_provider": "OpenAI (GPT-6 Astra Pro)", + "fingerprint": "e81d7fe09d25c3266eb8e62922756f54761d7f74d692fb35d9a8071fffd73769", + "source": "frontiers/two_scale_cluster_geometry_20260929/TWO_SCALE_LAW.md", + "scope": "Theorem L (L1) for every fixed q >= 2 and any deterministic delta_r -> 0 with delta_r / r -> oo, and (L2) E_r[N_R N_far^rho] = o_(R,rho)(r^3); every fixed d >= 2, L, b, k > 0, frame; conditional on SOURCES.json inputs (SC, CUB, RM, C6, P, D5)", + "review_basis": [ + { + "review": "Math-#166 review 5360227991", + "provider": "Anthropic Claude (session 01NMeKE; no authorship of the consumed sources)", + "verdict": "ACCEPT Theorem T, Theorem L, (L3), (V1) at the conditional scope", + "depth": "full", + "at": "7c82252533c3fe14ee262f7f87c0549c10968592, blob a32fd5f7 unchanged" + }, + { + "review": "xAI bounded read 5901945424 (reported in Math-#160 5902410407 / 5902466075)", + "provider": "xAI/Grok", + "verdict": "bounded Theorem-L read, as reported; not re-read here", + "depth": "bounded" + } + ], + "notes": "the direct statement of the residual; makes execution step 0 satisfied" + }, + { + "id": "math.c6r-component.two-scale-review-record", + "layer": "D5", + "kind": "reading_rule_component", + "classification": "PROVED_REVIEWED", + "controlling": false, + "component_of": "math.rn-region.witness-collision.leading-mass-localization", + "component_role": "review_record", + "author_provider": "OpenAI-authored record of the Claude reviews", + "fingerprint": "af1540308f37220e6592b700bf42181205b1d4588a040a5c151bf0a6f861e728", + "source": "frontiers/two_scale_cluster_geometry_20260929/REVIEW_RECORD.md", + "scope": "review record of Math-#166 at blob a32fd5f7 (Math-#172 bytes): A 5360227991, B 5360178611, C 5360216551, plus the custody-repair section", + "review_basis": [ + { + "review": "frontiers/two_scale_cluster_geometry_20260929/REVIEW_RECORD.md", + "provider": "in-repo record", + "verdict": "A/B/C ACCEPT at stated scopes", + "depth": "record" + } + ], + "notes": "in-repo record of the acceptance" + }, + { + "id": "math.c6r-component.two-scale-review-binding", + "layer": "D5", + "kind": "reading_rule_component", + "classification": "PROVED_REVIEWED", + "controlling": false, + "component_of": "math.rn-region.witness-collision.leading-mass-localization", + "component_role": "review_record", + "author_provider": "OpenAI-authored machine-readable record (Math-#172)", + "fingerprint": "958d2e1ae8ea5d034d0d87efce6cde9be57ebb9d7c0b671e69d3d6598a6675ca", + "source": "frontiers/two_scale_cluster_geometry_20260929/REVIEW_RECORD.json", + "scope": "native review 5360227991 (COMMENTED, 2026-09-30T00:52:00Z) bound to reviewed commit 7c82252, proof TWO_SCALE_LAW.md blob a32fd5f7, body 7840 bytes SHA256 c63efc292d7cf209e2770419cc159276897d0ba955c32ee1d2af88c8aa7f0ed8; remote_review_authenticity_checked false by its own declaration", + "review_basis": [ + { + "review": "frontiers/two_scale_cluster_geometry_20260929/REVIEW_RECORD.json", + "provider": "in-repo record", + "verdict": "A/B/C reported dispositions ACCEPT at the stated conditional scope", + "depth": "record" + } + ], + "notes": "in-repo byte binding of the review body identity; not an additional review or provider" + } + ], + "proposed_graph_edges": [ + { + "from": "math.rn-region.witness-collision.leading-mass-localization", + "to": "math.c6r-component.spectral-closure-proof", + "required": true, + "relation": "requires_evidence" + }, + { + "from": "math.rn-region.witness-collision.leading-mass-localization", + "to": "math.c6r-component.spectral-closure-review-record", + "required": true, + "relation": "requires_evidence" + }, + { + "from": "math.rn-region.witness-collision.leading-mass-localization", + "to": "math.c6r-component.cluster-law-proof", + "required": true, + "relation": "requires_evidence" + }, + { + "from": "math.rn-region.witness-collision.leading-mass-localization", + "to": "math.c6r-component.cluster-law-acceptance", + "required": true, + "relation": "requires_evidence" + }, + { + "from": "math.rn-region.witness-collision.leading-mass-localization", + "to": "math.c6r-component.cluster-law-source-map", + "required": true, + "relation": "requires_evidence" + }, + { + "from": "math.rn-region.witness-collision.leading-mass-localization", + "to": "math.c6-component.palm-proof", + "required": true, + "relation": "requires_evidence" + }, + { + "from": "math.rn-region.witness-collision.leading-mass-localization", + "to": "math.c6r-component.two-scale-law-proof", + "required": true, + "relation": "requires_evidence" + }, + { + "from": "math.rn-region.witness-collision.leading-mass-localization", + "to": "math.c6r-component.two-scale-review-record", + "required": true, + "relation": "requires_evidence" + }, + { + "from": "math.rn-region.witness-collision.leading-mass-localization", + "to": "math.c6r-component.two-scale-review-binding", + "required": true, + "relation": "requires_evidence" + }, + { + "from": "math.rn-region.witness-collision.leading-mass-localization", + "to": "math.c6r-component.residual-closure-record", + "required": true, + "relation": "requires_evidence" + }, + { + "from": "math.rn-region.witness-collision", + "to": "math.rn-region.witness-collision.leading-mass-localization", + "required": true, + "relation": "requires_evidence", + "deferred_with": "math.rn-region.witness-collision" + }, + { + "from": "math.rn-region.witness-collision", + "to": "math.c6-witness-collision-factorial-moment", + "required": true, + "relation": "requires_evidence", + "deferred_with": "math.rn-region.witness-collision" + } + ], + "execution_order": [ + "0. satisfied twice: (a) at ab13a08f Math-#166 Theorem L is on main as a required component (direct-statement path); (b) at b3fac79 OpenAI / GPT-5.6 Sol 5360645884 read section 3 (reviewed-corollary path), so math.c6r-component.residual-closure-record is PROVED_REVIEWED on that basis; either path alone suffices and the required edges take the union", + "1. create the component nodes and their required edges (math.c6-component.palm-proof only if Math-#160 has not created it)", + "2. create math.rn-region.witness-collision.leading-mass-localization as PROVED_REVIEWED, or move it from OPEN_ACTIVE if Math-#160 step 1 created it", + "3. only after Math-#160 step 3 (aggregate node): move math.rn-region.witness-collision to PROVED_REVIEWED with required edges to the aggregate node and to the residual node; under Math-#160's keep-open execution this is the step that moves the old node", + "4. STATUS C6 row, PROOF_INDEX bullet, catalog C6 and the selector as Math-#160 section 7 proposes, with the residual bullet closed", + "executing lane: non-Claude; this record executes nothing" + ], + "review_record": [ + { + "lane": "this session", + "id": 5902470285, + "kind": "pickup on Math-#160", + "at": "358f256" + }, + { + "lane": "this session", + "id": 5902585446, + "kind": "delivery on Math-#160", + "at": "b3fac79" + }, + { + "lane": "this session", + "id": 5902616692, + "kind": "bounded read of the Route C corollary (Math-#160 5901994240) at the request 5902379699", + "verdict": "ACCEPT at stated scope; exposure stated" + }, + { + "lane": "OpenAI/Codex", + "id": 5360636576, + "kind": "review of v1.0 at b3fac79: three engineering findings (4140125558 LIVE after execution; 4140125562 source snapshots; 4140125565 record promoted without a read on the Math-#166 path)", + "disposition": "all repaired in v1.3" + }, + { + "lane": "OpenAI (GPT-5.6 Sol)", + "id": 5360645884, + "kind": "bounded non-Claude read of section 3 at b3fac79 (sources re-read at fa1cf7b)", + "verdict": "ACCEPT at the stated fixed-d, fixed-torus, compact-positive-gap window scope; amend list repaired in v1.3", + "preserved_in": "EXTERNAL_REVIEWS.md section 2", + "reviewed_text": "REVIEWED_SECTION_3_b3fac79.md" + }, + { + "lane": "OpenAI (GPT-6 Astra Pro)", + "id": 5360751376, + "kind": "bounded nonauthor read of section 3 Route C at 5d8f011", + "verdict": "ACCEPT Route C; amendment: no fixed-R substitution into (L1), diagonal argument (applied in v1.5)" + }, + { + "lane": "OpenAI Sol (integrator)", + "id": [ + 5902847683, + 5902997395, + 5907324679 + ], + "kind": "integration hold", + "disposition": "items 2-4 closed by v1.3/v1.4; item 1 (direct-statement sentence) closed by v1.5" + } + ], + "exposure": "reconciler authored Math-#160 (the definition) and remote_collision_20260928 ([RC], consumed by both routes); reviewed none of Math-#159, #162, #166; same GitHub account; zero organizational-independence credit; Math-#173's own reviewers are OpenAI Sol (source-exposed; integrator) and OpenAI/Codex", + "not_proposed": [ + "any rate, constant or numerical enclosure", + "any controlling flag, lemma_closed, prize or premise change", + "any change to Math-#160, #162, #159 or #166 files", + "any historical predicate move" + ], + "revision": { + "version": "v1.5", + "applies": [ + "initial record at 358f256", + "fa1cf7b: Math-#166 TWO_SCALE_LAW.md and REVIEW_RECORD.md bound as the direct statement (step 0 satisfied); Route C added with exact checks and mutant route-c-broken; record node supporting", + "fe2c3ff: two-scale REVIEW_RECORD.md rebound to its Math-#172 bytes; REVIEW_RECORD.json bound as a component (native body digest of 5360227991)", + "fe2c3ff (v1.3): Math-#173 reviews answered: record node PROVED_REVIEWED on the reviewed-record path (5360645884; reviewed section preserved and checked), evidence_paths, installed-state acceptance in LIVE, source snapshots and per-component drift in GATE, four new mutants", + "8d48d02 (v1.4): re-verified after Math-#160 merged; no content change", + "02772ec (v1.5): direct-statement paragraph repaired per review 5360751376 (diagonal argument; no fixed-R substitution into (L1)); Route C read 5360751376 recorded; re-verified after Math-#168 merged" + ] + }, + "third_source_bound": { + "pr": "Math-#166", + "merged_at": "ab13a08f5e5b0adc7a7d80cf643d9b5a0618507f", + "file": "frontiers/two_scale_cluster_geometry_20260929/TWO_SCALE_LAW.md", + "sha256": "e81d7fe09d25c3266eb8e62922756f54761d7f74d692fb35d9a8071fffd73769", + "blob": "a32fd5f7d941bbe1fe943df045b1e0fbec8d691c", + "statement": "Theorem L (L1), (L2)", + "review": "Claude 5360227991; xAI 5901945424 as reported", + "review_record_md": { + "sha256": "af1540308f37220e6592b700bf42181205b1d4588a040a5c151bf0a6f861e728", + "blob": "31896de23fc56822c184375d0dc2b1c7e27fcae4" + }, + "review_record_json": { + "sha256": "958d2e1ae8ea5d034d0d87efce6cde9be57ebb9d7c0b671e69d3d6598a6675ca", + "blob": "a4b0fb99c24e2edf41973ea2a5e5176584602855", + "body_sha256_5360227991": "c63efc292d7cf209e2770419cc159276897d0ba955c32ee1d2af88c8aa7f0ed8" + }, + "rebound_at": "fe2c3ff (Math-#172)" + }, + "route_c": { + "source": "Math-#160 comment 5901994240 (OpenAI lane)", + "checked_in": "Math-#160 comment 5902616692 (this session; provider-distinct nonauthor on Math-#159/DL/C6, source-exposed on RC)", + "ingredients": [ + "pathwise (D2)", + "PALM Theorem Q (E N^4 <= C r^3)", + "Math-#159 (5.1) shell bound (DL Theorem I_d)", + "Math-#159 (5.4) left inequality", + "RC Corollary D" + ], + "bound": "r^-3 E[(N)_2 - (A)_2] <= C (R^-2 + rho^2)^(1/2) + C_(R,rho) r^(3/4) + C_rho r; r -> 0, rho -> 0, R -> oo" + }, + "reverified_at": "fe2c3ff (Math-#172 custody repair of the two-scale packet: TWO_SCALE_LAW.md unchanged, REVIEW_RECORD.md extended, REVIEW_RECORD.json added; GRAPH.json, PROOF_INDEX.md, SELECTOR_REGION.json and the catalog unchanged since ec6db8c); unchanged at v1.3 (Math-#160 refreshed onto fe2c3ff as dd4f4f8 by the integrator); 8d48d02 (Math-#160 merged: its packet and workflow only; register surfaces and every bound file unchanged); 02772ec (Math-#168 merged: numerics note only; nothing bound changed)", + "evidence_paths": { + "direct_statement": { + "components": [ + "math.c6r-component.two-scale-law-proof", + "math.c6r-component.two-scale-review-record", + "math.c6r-component.two-scale-review-binding" + ], + "statement": "Math-#166 Theorem L (L1) at q = 2, applied through the diagonal argument of section 3 (review 5360751376; no fixed-R substitution), and (L2)", + "review": "Claude 5360227991 (in-repo REVIEW_RECORD.md and REVIEW_RECORD.json body binding); xAI 5901945424 as reported" + }, + "reviewed_corollary": { + "components": [ + "math.c6r-component.spectral-closure-proof", + "math.c6r-component.spectral-closure-review-record", + "math.c6r-component.cluster-law-proof", + "math.c6r-component.cluster-law-acceptance", + "math.c6r-component.cluster-law-source-map", + "math.c6-component.palm-proof", + "math.c6r-component.residual-closure-record" + ], + "statement": "RECONCILIATION.md section 3: (D1) with Route A (Math-#162 (26)/(18)/(20), PALM Theorem Q), Route B (Math-#159 Corollary Lambda / Proposition 4.4 / Lemma 5.2), Route C", + "review": "OpenAI / GPT-5.6 Sol 5360645884 at b3fac79 ((D1), Route A, Route B; reviewed text preserved); Route C checked in 5902616692; Route C read by OpenAI Astra 5360751376 at 5d8f011" + }, + "rule": "either path alone establishes (Res) at the section 4 scope; the residual node's required edges take the union so that a later source change on either path holds the residual (fail-closed); GATE replays each path alone, the union, and the negative with the record node required but unread" + } +} diff --git a/reviews/c6_residual_closure_20260930/RECONCILIATION.md b/reviews/c6_residual_closure_20260930/RECONCILIATION.md new file mode 100644 index 000000000..3cfd17c5e --- /dev/null +++ b/reviews/c6_residual_closure_20260930/RECONCILIATION.md @@ -0,0 +1,328 @@ +# C6 / witness collision — closure of the leading-mass-localization residual + +**Object:** C6-RESIDUAL-CLOSURE-20260930-v1. +**Reconciler:** Anthropic Claude, Claude Code session `session_017Mi3hxjaxV45x6zo6o1ee3`. +**Read at:** Math- `main` `358f2562efbccc59f9549e5a79650e2e936395c3` (30 September 2026, after Math-#159 `98fdb54`, Math-#164 +`7d0c89a` and Math-#162 `358f256` merged; `GRAPH.json`, `PROOF_INDEX.md`, `SELECTOR_REGION.json` and the catalog are +unchanged since `ec6db8c`); re-verified at `fa1cf7b` (Math-#166 merged at `ab13a08f`, Math-#167 merged at `fa1cf7b`; the +same surfaces unchanged) and at `fe2c3ff` (Math-#172: custody repair of the two-scale packet; `TWO_SCALE_LAW.md` unchanged, +`REVIEW_RECORD.md` extended and `REVIEW_RECORD.json` added; register surfaces unchanged); main is still `fe2c3ff` at v1.3, +and the integrator refreshed Math-#160's branch onto it (`dd4f4f8`, its six packet blobs preserved from `eba6045`); +Math-#160 then merged at `8d48d02` (v1.4 re-verification: only its packet and workflow landed; `GRAPH.json`, `PROOF_INDEX.md`, +`SELECTOR_REGION.json`, the catalog and every file bound here are unchanged); Math-#168 merged at `02772ec` (numerics note +only; nothing bound here changed). +**Revision:** v1.0 at `358f256`; v1.1 at `fa1cf7b` binds Math-#166's `TWO_SCALE_LAW.md` and its review record as the +direct statement (execution step 0 satisfied), adds Route C (the pair-count corollary of Math-#160 comment 5901994240, +checked in 5902616692) with its exact checks, and makes this record's own node supporting; v1.2 at `fe2c3ff` rebinds the +two-scale review record to its Math-#172 bytes and binds `REVIEW_RECORD.json`, which pins the native body digest of +review 5360227991; v1.3 at `fe2c3ff` answers Math-#173's reviews: this record's own node is promoted on the reviewed-record +path (OpenAI / GPT-5.6 Sol 5360645884, a non-Claude bounded read of §3 at head `b3fac79`, whose paragraphs are preserved +verbatim in `REVIEWED_SECTION_3_b3fac79.md` and checked unchanged), the two evidence paths are modelled separately, and +the checker accepts the installed state and replays the hard gate with source snapshots (Codex 5360636576); v1.4 at +`8d48d02` re-verifies after Math-#160 merged (no content change); v1.5 at `02772ec` applies the direct-statement amendment +of review 5360751376 (the diagonal argument; no fixed-`R` substitution into (L1)) and records that review's ACCEPT of +Route C. Pickup: +Math-#160 comment 5902470285; delivery 5902585446. +**Effect:** register reconciliation, **declarative only** (`PROPOSED_TRANSITIONS.json`, `"executed": false`). It binds the +residual question that Math-#160 §5 named (`math.rn-region.witness-collision.leading-mass-localization`) to the exact +merged bytes of two independently authored and cross-provider-reviewed proofs, writes the four-line corollary that turns +their reviewed statements into the residual, and proposes the residual node `PROVED_REVIEWED` at existential fixed-`d` +compact-mark window scope. The corollary is elementary bookkeeping, not new mathematics; §3 says exactly what it uses. +Execution of any `GRAPH.json`, `STATUS`, `PROOF_INDEX` or catalog change is a separate act for a **non-Claude lane**. +`lemma_closed`, prizes and premises are untouched. Scientific effect: NONE. + +## 0. Exposure, stated first + +- Every lane shares one GitHub account; no organizational independence is claimed anywhere below. +- I authored Math-#160, whose §5 defines the residual closed here; this record binds that definition to others' proofs, + it does not review them. I authored none of the three sources of §2 and reviewed none of them. +- Both routes of §3 consume `frontiers/remote_collision_20260928/PROOF.md` ([RC], Math-#110) for the far region (its + Corollaries D and E); that packet is Claude-authored, by this session per Math-#160 §0, with OpenAI (5342280263) and + xAI (5342481786, frozen in `reviews/d5_remote_collision_grok_20260928`) nonauthor records. I am therefore + source-exposed to both routes through one imported input; the routes' own reviewers are named per route below. +- Route A (Math-#162) is OpenAI-authored; its Slice A reviewer (Anthropic Claude 5359968447) declares no authorship of + the consumed sources; its Slice B reviewer (Anthropic Claude 5359845136) authored the consumed [C6], [DL], [RC] and the + competing Math-#159 (source-exposed); its Slice C reviewer (OpenAI/Codex 5359879627) is the author's provider. Route B + (Math-#159) is Anthropic-authored (the Slice B reviewer's session) and accepted by OpenAI (5360192822), source-exposed + as author of imported inputs and of Math-#161. Neither route carries an organizationally independent read; taken + together they are the first item in this chain with a proof from each provider, each read by the other. +- The third source (Math-#166, OpenAI; merged at `ab13a08f`) carries one Anthropic read per slice (5360227991, 5360178611, + 5360216551; another session) and, per Math-#160 comments 5902410407 and 5902466075, an xAI bounded read of Theorem L + (5901945424) not re-read here; I reviewed none of it. Route C was posted by an OpenAI lane (Math-#160 comment + 5901994240) and checked by this session (5902616692): a provider-distinct nonauthor read of a consumer of + Math-#159 / [DL] / [C6], source-exposed on [RC]. +- Math-#173's own reviews: OpenAI / GPT-5.6 Sol 5360645884, a bounded non-Claude read of §3 at head `b3fac79` (ACCEPT at + the stated scope; source-exposed to the OpenAI side of the chain and the integrator of Math-#162/#166; not organizational + independence, by its own statement), and OpenAI/Codex 5360636576 (three engineering findings on the checker, all repaired + in v1.3). The paragraphs that read covers ((D1), Route A, Route B) are preserved byte-for-byte in + `REVIEWED_SECTION_3_b3fac79.md`; Route C and the Theorem L paragraph were not part of it. +- No Cursor agent is restarted or contacted (owner stop, 27 September 2026); only published records are cited. + +## 1. The residual, as defined, and the register as it stands + +**Definition (Math-#160 `RECONCILIATION.md` §5, v1.3–v1.7, unchanged; head `eba6045`).** With `o` the midpoint of the pins +and `N` the window count of critical points other than the pins, + + lim_{R -> oo} limsup_{r -> 0} r^-3 E_{Q_r^W} #{ ordered pairs (X, X') of distinct window points : + not both |X - o| <= R r and |X' - o| <= R r } = 0. (Res) + +Math-#160 §5 records what the landed chain gave: pairs within `C_d r` of `o` carry `>= c r^3` ([EDL] (A4)); both-remote +pairs carry `O(r^5)` ([RC]); pairs with a witness in the shells `R r <= |X - o| <= s_0` carry `<= C r^3 (R^-2 + s_0^2)` +([PALM] §6 R3); and the open piece was the mixed count `M(R, s_0)` of pairs with one witness within `R r` of `o` and the +other at distance `>= s_0`, where [PALM] R4 gives `C r^3` only. (Res) is equivalent to `lim_{s_0} lim_R limsup_r r^-3 +M(R, s_0) = 0`. + +**Register at `358f256`.** `GRAPH.json` does not carry the residual node (Math-#160 proposes it, `OPEN_ACTIVE`, required +by nothing); `math.rn-region.witness-collision` is `OPEN_ACTIVE`, fingerprint "eta->0 mutual witness separation", notes +"… the regional shrinking pin/witness-collision mechanism and its source-bound graph fold remain open" (Math-#151); +`PROOF_INDEX.md` reads "NO COMPLETE REGIONAL PROOF YET: `math.rn-region.witness-collision` remains `OPEN_ACTIVE`; the +global `Theta(r^3)` result is not a proof of that node"; catalog C6 asks to "prove or refute the shrinking-separation +witness-collision mechanism encoded by the open graph node". Math-#160 §1a records that no surface defines that +mechanism other than by (Res). Both Math-#159 (§9) and Math-#162 (README) state that they move no register node. + +## 2. Sources bound (exact bytes on `main` `358f256`) + +| Tag | File | Bytes · SHA256 · blob | Author | Nonauthor record | What is used (§3) | +|---|---|---|---|---|---| +| [SC] | `frontiers/spectral_cluster_closure_20260929/PROOF.md` (Math-#162, merged `358f256`) | 25006 · `e971b2cbe50a8a06b47c1219191201e0d1037c9adac23e5e3b7d2051bb70c2eb` · `16c56821b52fd76b0be791622b9c3809eafde75a` | OpenAI | in-repo `REVIEW_RECORD.md` (5629 · `6031d366…` · `9bcae183`): A Claude 5359968447 (§§2–3), B Claude 5359845136 (§§4–6), C OpenAI/Codex 5359879627 (§§7–8), all ACCEPT at the conditional scope | Theorem (3); (18) near limit; (20) exhaustion; (24) mixed event; (26) factorial-moment limits | +| [SC-R] | `frontiers/spectral_cluster_closure_20260929/README.md` | 5084 · `b1e2a072…` · `895dded8` | OpenAI | — | scope statement | +| [CL] | `frontiers/c6_cluster_law_20260929/PROOF.md` (Math-#159 v1.2, merged `98fdb54`) | 70131 · `96b8e2d59defee6059bf151a896b7fc7c91fc529b385a3db8a87574901197b38` · `ba492c8e62e58bfc055fc8254c790e893d346ba5` | Anthropic (other session) | OpenAI review 5360192822 at `f7c3395`, same blob: ACCEPT Theorem N, Corollaries Λ/S, Corollary X (preserved in `EXTERNAL_REVIEWS.md`); in-repo pointer `SOURCE_MAP.json` (`nonauthor_acceptance: true`, revision note naming 5360192822) | Corollary Λ (1.6); Proposition 4.4 (4.4) with its `A -> oo` step; Lemma 5.2 (5.4) | +| [CL-R] | `frontiers/c6_cluster_law_20260929/README.md`, `SOURCE_MAP.json` | 7560 · `e4b35f2b…` · `1166376f`; 12566 · `0584c380…` · `ef51c582` | Anthropic | — | object identity; acceptance pointer | +| [PALM] | `frontiers/c6_palm_route_20260929/PROOF.md` (Math-#145, merged `820d443`) | 53364 · `aa37f16040ab9e05bb2e4e3f1d678367497e8dc2cf43eef197a4d6592c2f129b` · `89eb8adf08fe7afc2cab9662d3a9875c05ae5cc5` | Anthropic (other session) | OpenAI 5356233690 (§4), 5358116559 (§§5–7, Theorem Q) | Theorem Q, `q = 3` and `q = 4`, for the uniform-integrability tails | +| this packet | `reviews/c6_residual_closure_20260930/EXTERNAL_REVIEWS.md` | see `SOURCE_FILES.json` | transcribed by Anthropic | mutable external evidence, labelled | the preserved 5360192822 and 5360645884 | +| this packet | `reviews/c6_residual_closure_20260930/REVIEWED_SECTION_3_b3fac79.md` | see `SOURCE_FILES.json`; reviewed text (after the provenance comment) 2779 · `931f5c95c5185be075c8684e30c395fe55dd344ad0c1ac45535e3b166c3aac65` | verbatim copy of §3 at `b3fac79` | read by OpenAI 5360645884 (preserved in `EXTERNAL_REVIEWS.md`) | the paragraphs that read covers, checked unchanged in §3 (`REVIEWED`) | +| [TSL] | `frontiers/two_scale_cluster_geometry_20260929/TWO_SCALE_LAW.md` (Math-#166, merged `ab13a08f`) | 17139 · `e81d7fe09d25c3266eb8e62922756f54761d7f74d692fb35d9a8071fffd73769` · `a32fd5f7d941bbe1fe943df045b1e0fbec8d691c` | OpenAI | in-repo `REVIEW_RECORD.md` (6732 · `af1540308f37220e6592b700bf42181205b1d4588a040a5c151bf0a6f861e728` · `31896de23fc56822c184375d0dc2b1c7e27fcae4`, extended by Math-#172 at `fe2c3ff`) and `REVIEW_RECORD.json` (4226 · `958d2e1ae8ea5d034d0d87efce6cde9be57ebb9d7c0b671e69d3d6598a6675ca` · `a4b0fb99c24e2edf41973ea2a5e5176584602855`: native review 5360227991, reviewed commit `7c82252`, proof `TWO_SCALE_LAW.md`, body SHA256 `c63efc29…`): Claude 5360227991 ACCEPT of Theorem T, Theorem L, (L3), (V1) at the conditional scope; xAI bounded read 5901945424 reported in Math-#160 5902466075 | Theorem L (L1), (L2): the direct statement | + +Identities are checked by `residual_check.py` (`IDENTITIES`, `NEGATIVES`); the quoted statements are checked as +substrings (`VERDICTS`). [SC] and [CL] are conditional on their own pinned inputs at those inputs' reviewed scopes +([SC] `SOURCES.json`: P, D5, C6, RM, RC, LM, CUB, RCL; [CL] `SOURCE_MAP.json`: LP, DL, C6, RM, RC, EDL, LM, RCL; [TSL] +`SOURCES.json`: SC, CUB, RM, C6, P, D5); this record inherits exactly those conditions and adds none. + +## 3. The corollary: (Res) from the reviewed statements + +Write `N_R` for the window count in the Euclidean ball of radius `R r` about `o` ([SC]'s `N_R`; [CL]'s `N^A` with +`A = R`), `N_out = N - N_R`, and `(n)_2 = n(n - 1)`. The quantity in (Res) is exactly + + M_R := E_{Q_r^W} #{ordered pairs of distinct window points not both within R r of o} = E[(N)_2] - E[(N_R)_2], (D1) + +since for every configuration `(N)_2 - (N_R)_2 = 2 N_R N_out + (N_out)_2 >= 2 N_R N_out >= 0` (exact identity, checked +in `DEDUCTION`). So (Res) says `lim_R limsup_r r^-3 (E[(N)_2] - E[(N_R)_2]) = 0`, and the mixed count of Math-#160 §5 is +`M(R, s_0) <= E[N_R N_out] <= M_R / 2`. + +**Route A ([SC], Math-#162).** +1. *Full second factorial moment.* [SC] (26): `E (N)_2 / r^3 -> 2 nu2 = 2 a_2`, a stated consequence of Theorem (3) + with `q = 2` (§8, Slice C). +2. *Near second factorial moment.* [SC] (18): `r^-3 Q_W(N_R = j) -> a_j^R` for `j = 1, 2` and `r^-3 Q_W(N_R >= 3) -> 0` + (§5, Slice B). Tail: `(N_R)_2 <= (N)_2`, and for integers `n > M >= 3`, `n(n-1) <= n(n-1)(n-2)/(M-1)` (exact, `DEDUCTION`), + so `E[(N_R)_2; N_R > M] <= E[(N)_3]/(M-1) <= C_3 r^3/(M-1)` by [PALM] Theorem Q with `q = 3`. Hence + `limsup_r | r^-3 E[(N_R)_2] - 2 a_2^R | <= C_3/(M-1)` for every `M`, i.e. `r^-3 E[(N_R)_2] -> 2 a_2^R` (the finite sum + over `n <= M` converges by (18), its `n >= 3` terms to zero). This is the same tail argument [SC] §8 uses for (3). +3. *Exhaustion.* [SC] (20): `a_2^R -> a_2` as `R -> oo` (dominated convergence with the integrable majorant (19), §6, + Slice B). + +Therefore `limsup_r r^-3 M_R = 2 a_2 - 2 a_2^R` (a full limit, by 1 and 2), which tends to `0` as `R -> oo` by 3. That is +(Res). ∎ + +**Route B ([CL], Math-#159).** Corollary Λ (1.6): `r^-3 E[(N)_2] -> Λ_2 = 2 nu(2) = 2 nu_near(2)`; Proposition 4.4: +`r^-3 Q{N^A = n} -> nu_near^A(n)` for `n = 1, 2`, `r^-3 Q{N^A >= 3} -> 0`, and `nu_near^A(n) -> nu_near(n)` as `A -> oo`; +the tail of step 2 is the one [CL] §6.3 uses ([PALM] Theorem Q). The same three lines give (Res). Directly, without the +factorial-moment limit: Lemma 5.2 (5.4), `E[N^A 1{N_far^rho >= 1}] <= C(A, rho) r^(9/2)`, together with +`E[N^A (N_far^rho - 1)_+] <= (E (N^A)^2)^(1/2) (E N_far^4)^(1/4) Q{N_far^rho >= 2}^(1/4) <= C r^(3/2) r^(3/4) r^(5/4) = C r^(7/2)` +([PALM] Theorem Q for the second and fourth moments through Stirling's identity `n^4 = (n)_4 + 6(n)_3 + 7(n)_2 + (n)_1`, +[RC] Corollary D for `Q{N_far^rho >= 2} <= E (N_far^rho)_2 / 2 = O(r^5)`), gives `E[N^A N_far^rho] = O(r^(7/2)) = o(r^3)` +at fixed `(A, rho)`, which is the mixed count of Math-#160 §5 with `s_0 = rho` (the far region `D_rho` is measured from +`o`; a point at distance `>= s_0` from both pins lies in `D_{s_0/2}` for `r < s_0`). Exponent ledgers checked exactly. + +**Route C (pair-count corollary; Math-#160 comment 5901994240, checked in 5902616692).** With `A`, `B`, `C` the window +counts in `|X| <= R r`, `R r < |X| < rho`, `|X| >= rho` (from `o`; `N = A + B + C`), pathwise + + 0 <= (N)_2 - (A)_2 <= N^2 [ 1{B > 0} + 1{A > 0, C > 0} + 1{C >= 2} ], (D2) + +exact: the right side vanishes only when `B = 0` and either `C = 0` or `A = 0, C <= 1`, and then the left side +`2A(B + C) + (B + C)(B + C - 1)` vanishes too (checked in `DEDUCTION`). Cauchy–Schwarz with `E N^4 <= C r^3` ([PALM] +Theorem Q through Stirling) and [CL] (5.1) (`E B <= C r^3 (R^-2 + rho^2)`, [DL] Theorem I_d, constant uniform in `R >= 4`, +`rho <= s_0`), the left inequality of [CL] (5.4) (`Q{A >= 1, C >= 1} <= C(A, rho) r^(9/2)`) and [RC] Corollary D +(`Q{C >= 2} <= E (C)_2 / 2 = O_rho(r^5)`) give + + r^-3 E[(N)_2 - (A)_2] <= C (R^-2 + rho^2)^(1/2) + C_(R,rho) r^(3/4) + C_rho r ; + +`r -> 0` first, then `rho -> 0`, then `R -> oo` gives (Res). This route uses no count-law limit: only the shell bound, +the cross-term bound, the far second factorial moment and Theorem Q (exponent ledgers `3/2 + 9/4 - 3 = 3/4` and +`3/2 + 5/2 - 3 = 1`, checked exactly). + +**Direct statement ([TSL], merged at `ab13a08f`).** Math-#166 Theorem L (L1): `r^-3 E_r[(N_r)_q - (N_in)_q] -> 0` for every +fixed `q >= 2` and every deterministic cutoff `delta_r` with `delta_r -> 0` and `delta_r / r -> oo` ([TSL] (T1)), `N_in` the +count within `delta_r` of `o`; and (L2): `E_r[N_R N_far^rho] = o_(R,rho)(r^3)`, the mixed count itself. (L1) cannot be +applied at a fixed `R` (`delta_r = R r` has `delta_r / r = R`, which does not tend to infinity); (Res) follows from (L1) by +the diagonal argument of Math-#173 review 5360751376 (OpenAI), reproduced here. Put `f_r(R) := r^-3 E[(N)_2 - (N_R)_2] +>= 0`; it is nonincreasing in `R`, because `N_R` and hence `(N_R)_2` are nondecreasing in `R` (`n -> (n)_2` is nondecreasing +on the nonnegative integers, checked in `DEDUCTION`), so `c := lim_(R -> oo) limsup_(r -> 0) f_r(R)` exists in `[0, oo]`. +Suppose `c > 0` and fix `0 < c' < c`. Since `limsup_(r -> 0) f_r(R) >= c > c'` for every `R`, choose `R_n -> oo` and `r_n` +decreasing to `0` with `r_n R_n <= 1/n` and `f_(r_n)(R_n) > c'`. Set `delta_r := r R_n` for `r in (r_(n+1), r_n]`: then +`delta_r <= 1/n -> 0` and `delta_r / r = R_n -> oo`, so (T1) holds, while `N_in = N_(R_n)` at `r = r_n` gives +`r_n^-3 E[(N)_2 - (N_in)_2] = f_(r_n)(R_n) > c'` along `r_n -> 0`, contradicting (L1) at `q = 2`. Hence `c = 0`, which is +(Res). (L2) is the `A > 0, C > 0` term of Route C, stated as a counted mixed pair. Theorem L is stronger than (Res) (moving +cutoff, all `q`) and is conditional on [SC]. It is bound in §2 and is a required component in §5, so execution step 0 is +satisfied by a reviewed merged source rather than by a read of this record. + +**What the corollary uses and nothing else.** Two reviewed limit statements about one law (the full and the near +second factorial moments), one reviewed exhaustion statement, and one reviewed moment bound for the tail. No +regression, no Kac–Rice step, no new estimate. The direct statement [TSL] and this section are two separate evidence +paths (§5). This section's (D1), Route A and Route B paragraphs were read by OpenAI / GPT-5.6 Sol (Math-#173 review +5360645884, at head `b3fac79`, ACCEPT at the stated scope; the reconciler is source-exposed, §0); those paragraphs are +preserved byte-for-byte in `REVIEWED_SECTION_3_b3fac79.md`, and `REVIEWED` checks that they stand unchanged above. Route C +is OpenAI-authored, Claude-checked (5902616692) and read by OpenAI Astra (Math-#173 review 5360751376 at `5d8f011`, ACCEPT as +an elementary conditional implication of its stated estimates; the paragraph is unchanged since); the Theorem L paragraph +is [TSL]'s own reviewed statement, applied through the diagonal argument above. A revision +that alters the reviewed paragraphs must obtain a new read or return this record's node to `AUTHOR_SIDE_CANDIDATE`. + +## 4. Scope, and what is not established + +**Scope of the proposed `PROVED_REVIEWED`.** Every fixed `d >= 2`, fixed torus `L`, fixed frame, compact birth and +positive-gap marks (`k_- > 0`), the height window `I_r = (b - k r^3, b)`, the original endpoint weight `W_r` and the full +normalizer `Z_r`; existential constants; conditional on the pinned inputs of [SC] and [CL] at their reviewed scopes +(§2). Under this scope the register's chain for the witness-collision region reads: torus-wide `c r^3 <= E N(N-1) <= C r^3` +([PALM] + [EDL] (A4), Math-#160 §4); the leading `r^3` mass of `E N(N-1)` is carried, in the iterated limit, by pairs both +within `R r` of the midpoint ((Res), this record); the coefficient is `2 a_2` ([SC] (26) / [CL] (1.6)); the count law is +`nu(1) delta_1 + nu(2) delta_2` ([SC] Theorem (3) / [CL] Theorem N). + +**Not established by this record.** No rate of convergence; no numerical value of `a_2`, `nu(1)`, `nu(2)`, `C_3` or of +the localization scale; no uniformity as `k -> 0`, in `L` or in `d`; no all-height statement (the window is +load-bearing in both sources); no statement about the elder selection of the extra points; no joint law of clusters +of distinct pin pairs; no configuration law beyond what [SC]/[CL] state (Math-#166 Theorem T supplies the configuration +form; not consumed); no `d_TV` statement (Math-#166 (V1); not consumed); the moving-cutoff form is [TSL] (L1) at its own +scope; no historical numerical certificate (RN annulus partition, +24-jet / OBL-H5-JETMOD) and no discharge of any historical predicate outside the analytic scope (Math-#160 §6). Neither +[SC] nor [CL] is re-reviewed here; their reviews stand at the scopes their records state. + +## 5. Proposed register transitions (for a non-Claude lane) + +| Node | Current (`358f256`) | Proposed | +|---|---|---| +| `math.rn-region.witness-collision.leading-mass-localization` | absent (Math-#160 proposes it `OPEN_ACTIVE`) | `PROVED_REVIEWED` at the §4 scope, with `fingerprint` unchanged from Math-#160's proposal, `scope`, `explicit_limits`, `review_disposition`, `review_basis`, and `required` edges to the component nodes below; created directly if Math-#160's step 1 has not run, moved if it has | +| `math.rn-region.witness-collision` | `OPEN_ACTIVE` (Math-#151 wording) | `PROVED_REVIEWED`, **conditional and deferred**: presupposes Math-#160's aggregate node `math.c6-witness-collision-factorial-moment` (count discharge) and this record's residual node (localization); executes only after both exist, with `required` edges to both. Under Math-#160's keep-open execution (§1a (iii) there), the residual's definition sits on the old node and this record moves the old node itself. If the executing lane holds that the node means something other than the count estimate and (Res), it must write that meaning down; no source defines one (Math-#160 §1a) | +| `SELECTOR_REGION.json`, `PROOF_INDEX.md`, catalog C6, `STATUS.md` C6 row | as at `358f256` | as Math-#160 §7 proposes, with the residual bullet closed: "leading-mass localization: resolved at existential scope by Math-#162 (26)/(18)/(20) and Math-#159 Corollary Λ / Proposition 4.4; direct statement Math-#166 Theorem L (merged at `ab13a08f`); open: rate, constants" | + +**Component nodes** (`kind: reading_rule_component`, `PROVED_REVIEWED`, `controlling: false`, `fingerprint` = SHA256 of the +source; one node per byte identity; none duplicates a source the live graph carries with a fingerprint): + +| Node | Source | Role | Provider | Review basis | +|---|---|---|---|---| +| `math.c6r-component.spectral-closure-proof` | [SC] | proof: Theorem (3), (18), (20), (26) | OpenAI | A 5359968447, B 5359845136, C 5359879627 (in-repo `REVIEW_RECORD.md`) | +| `math.c6r-component.spectral-closure-review-record` | `frontiers/spectral_cluster_closure_20260929/REVIEW_RECORD.md` | review record | OpenAI-authored record of the Claude/Codex reviews | itself | +| `math.c6r-component.cluster-law-proof` | [CL] | proof: Corollary Λ, Proposition 4.4, Lemma 5.2 | Anthropic (other session) | OpenAI 5360192822 | +| `math.c6r-component.cluster-law-acceptance` | this packet's `EXTERNAL_REVIEWS.md` | external review record (5360192822, transcribed; mutable, labelled) | OpenAI review, transcribed by Anthropic | itself | +| `math.c6r-component.cluster-law-source-map` | `frontiers/c6_cluster_law_20260929/SOURCE_MAP.json` | in-repo acceptance pointer and consumed-input map | Anthropic | records 5360192822 | +| `math.c6-component.palm-proof` | [PALM] | proof: Theorem Q (`q = 3, 4`) | Anthropic (other session) | OpenAI 5358116559; **defined by Math-#160** (same id, source, fingerprint); created here only if absent | +| `math.c6r-component.two-scale-law-proof` | [TSL] | proof: Theorem L (L1), (L2), the direct statement | OpenAI | Claude 5360227991 (in-repo `REVIEW_RECORD.md`); xAI bounded read 5901945424 as reported | +| `math.c6r-component.two-scale-review-record` | `frontiers/two_scale_cluster_geometry_20260929/REVIEW_RECORD.md` (Math-#172 bytes) | review record | OpenAI-authored record of the Claude reviews | itself | +| `math.c6r-component.two-scale-review-binding` | `frontiers/two_scale_cluster_geometry_20260929/REVIEW_RECORD.json` | machine-readable review binding: native id 5360227991, reviewed commit `7c82252`, proof path and blob `a32fd5f7`, body SHA256 `c63efc29…` | OpenAI-authored record (Math-#172) | itself | +| `math.c6r-component.residual-closure-record` | this packet's `RECONCILIATION.md` | reading-rule record: the §3 corollary ((D1), Routes A, B) and Route C | Anthropic (this session; source-exposed) | **OpenAI / GPT-5.6 Sol 5360645884** (bounded non-Claude read of §3 at `b3fac79`; reviewed text preserved and checked, `REVIEWED`); Route C: OpenAI-authored, checked 5902616692. `PROVED_REVIEWED` on the reviewed-record path since v1.3 | + +Edges: from the residual node to each of the ten components, `required: true` (`requires_evidence`). From the old node +(deferred transition): `required` edges to the residual node and to Math-#160's aggregate node. + +**Two evidence paths** (`PROPOSED_TRANSITIONS.json` `evidence_paths`), each sufficient for (Res) on its own: the **direct +statement** ([TSL] Theorem L with its in-repo review record and JSON binding: three nodes) and the **reviewed corollary** +(§3 from [SC], [CL], [PALM] and this record, read by 5360645884: seven nodes). The residual's required edges take the +union, so that a later byte change on either path holds the residual (fail-closed); `GATE` replays each path alone (the +other path's edges supporting) as well as the union, and replays the negative in which the record node is required +without its read: the gate then holds the residual on exactly that node. + +**Execution order** (`PROPOSED_TRANSITIONS.json` `execution_order`): (0) satisfied twice: at `ab13a08f` +Math-#166's Theorem L is on main as a required component (direct path), and at `b3fac79` OpenAI 5360645884 read §3 +(reviewed-corollary path); (1) the component nodes and their edges; (2) the residual node +(created `PROVED_REVIEWED`, or moved from `OPEN_ACTIVE`); (3) only after Math-#160 step 3: the old node; (4) the +register rows. Nothing here edits `GRAPH.json`, `PROOF_INDEX.md`, `STATUS.md`, `SELECTOR_REGION.json` or the catalog +(`"executed": false`, checked). + +**Reverse-impact.** Every component node carries the SHA256 of its source; `GATE` calls `reverse_impact_between` with exact +source snapshots of both graph states (every node: `record_only`, `external_unresolved`, `blob` with bytes and SHA256, +or `tree`), asserts `source_snapshots_supplied`, and then, for each component in turn, changes only that component's +snapshot digest and checks that the residual node (and the old node, once it depends on the residual) is impacted. A +later byte change to [SC], [CL], [PALM], [TSL], a review record, the source map, the preserved reviews or this record +therefore reaches the residual through the graph, not through the fingerprint strings alone. + +## 6. Checks + +`residual_check.py` (stdlib only, run from the repository root): +- **IDENTITIES.** All thirteen inventoried files exist as regular files, no symlink on their paths, stated SHA256 and blob. +- **VERDICTS.** The quoted statements are present as substrings: [SC] Theorem (3), (18), (20), (24), (26) and the + Slice A/B/C lines of its review record with the core blob; [CL] Corollary Λ with `Λ_2 = 2 nu(2)`, Proposition 4.4's + `A -> oo` sentence, Lemma 5.2 with `r^(9/2)`, the object header, the source map's `nonauthor_acceptance` and its note + naming 5360192822; [PALM] object header and Theorem Q; [TSL] Theorem L with (L1) and (L2), its review record's + 5360227991 line at blob `a32fd5f7`, and the JSON binding's native id, proof path and body digest; the review ids, verdict lines, the `b3fac79` head and the + mutability label in `EXTERNAL_REVIEWS.md`; the heading and the Route A / Route B headers of the reviewed-section file. +- **LIVE.** `math.rn-region.witness-collision` is a live `OPEN_ACTIVE` region with its recorded fingerprint (or + `PROVED_REVIEWED` after execution); the residual node is absent, `OPEN_ACTIVE` with Math-#160's fingerprint, or + `PROVED_REVIEWED`; the selector lists the region. A live node on a component source is accepted only if it is the + proposed node on every proposed key (the palm node on its cross-record keys: kind, source, fingerprint, + classification, controlling); anything else on such a source, or anything else under a proposed id, is a mismatch. If + the residual is live `PROVED_REVIEWED`, every component, every edge and the reading rule must be present as proposed. + The same test runs on the executed graph built from the proposal (installed state, simulated) in every run, so that + execution cannot turn this check red (Codex 4140125558). +- **REVIEWED.** The record node's first review basis is Math-#173 review 5360645884 (provider OpenAI, ACCEPT, head + `b3fac79`); `REVIEWED_SECTION_3_b3fac79.md`, after its one-line provenance comment, has the SHA256 the proposal states, + begins at the §3 heading, contains Route A and Route B and not Route C, and is a verbatim substring of the current + `RECONCILIATION.md`; the review id and head are in `EXTERNAL_REVIEWS.md`. +- **DEDUCTION.** Exact finite content of §3: the pair identity (D1) for all `0 <= N_R, N_out <= 12`; the monotonicity + `(n+1)_2 >= (n)_2` on `n >= 0` used by the diagonal argument of the direct statement; the Route C + pathwise inequality (D2) for all `0 <= A, B, C <= 8` with its two exponent ledgers; the tail + inequality `n(n-1)(M-1) <= n(n-1)(n-2)` for `n > M >= 3`; the Stirling identity for `n^4`; the exponent ledgers + `3 + 3/2 = 9/2 > 3` and `3/2 + 3/4 + 5/4 = 7/2 > 3`; the truncation error of a finite distribution against + `E(N)_3/(M-1)`; and an exact rational instance of the iterated limit `2 a_2 - 2 a_2^R -> 0`. +- **TRANSITIONS.** `declarative` true, `executed` false; the residual node `PROVED_REVIEWED`, non-controlling, with + scope, explicit limits, review basis, Math-#160's fingerprint and a required edge to every component; every + component node fingerprinted to the inventory with role, provider and review basis, one per byte identity; the + every component `PROVED_REVIEWED` with at least one review basis and the residual's required edges covering all ten; + the two evidence paths partition the components, the record node on the corollary path and Theorem L on the direct + path; the old-node transition marked deferred with its two presuppositions; the palm node marked cross-record with + Math-#160's id. The builds are idempotent: installed components and edges are not re-created, and the installed state + rebuilds to itself. +- **GATE.** In every execution shape (interim; final; residual node pre-existing `OPEN_ACTIVE` as Math-#160 proposes; + each evidence path alone; the installed state, simulated; and the negative with the record node required but unread), + the proposed graph passes `validate_graph_fail_closed`, `closure_report` gives `gate_ok` with no illegal controlling + node, `reverse_impact_between` runs with source snapshots of both states and names the residual node and the new + components as changed and impacted (nothing, in the installed state); the residual is not held except in the negative, + where the gate holds it on exactly the record node; a single-component source drift reaches the residual for every + component; the deferred old-node transition is not applied (its presupposition is absent live) and is reported. +- **NEGATIVES.** Delete, one-byte change, symlink and symlinked parent on a temporary copy of the inventory are rejected. + +Fourteen mutants must fail: `allow-symlink`, `no-hash`, `stale-fingerprint`, `drop-required-edge`, `executed-flag`, +`controlling-true`, `tail-reversed`, `pair-identity-broken`, `route-c-broken`, `drop-review-needle`, and since v1.3 +`installed-drift` (an installed component with another fingerprint must fail `LIVE`), `snapshot-omitted` (the +reverse-impact replay without snapshots must fail `GATE`), `record-unreviewed` (the record node `PROVED_REVIEWED` with no +review basis must fail `TRANSITIONS` and `REVIEWED`), `reviewed-text-drift` (a changed reviewed text must fail `REVIEWED`). + +## 7. Relation to other lanes + +- **Math-#160 (this session):** defines (Res) and proposes the residual node `OPEN_ACTIVE`; this record is its successor + and composes with either execution of its §7. Math-#160 is not changed by this record; the integrator refreshed its + branch onto `fe2c3ff` (`dd4f4f8`) with the six packet blobs preserved and merged it at `8d48d02` (packet and workflow + only; its transitions remain declarative and unexecuted, so the deferred old-node transition here still presupposes + its step 3). +- **Math-#173 reviews (on v1.0 `b3fac79`):** OpenAI/Codex 5360636576, three findings: (i) `LIVE` rejected the installed + components (4140125558), repaired: the installed state is accepted when exact and simulated in every run; (ii) the + reverse-impact replay ran without source snapshots (4140125562), repaired: snapshots of both states and a + per-component drift test; (iii) the `final` build promoted this record without a read on the Math-#166 path + (4140125565), repaired: the two paths are modelled separately, the record node's promotion rests on 5360645884, and + the unread case is replayed as a negative. OpenAI / GPT-5.6 Sol 5360645884: ACCEPT of §3 at the stated scope with the + amend list above; the record node is promoted on that reviewed-record path, the #166 path stays a distinct alternative + with `TWO_SCALE_LAW.md` and its exact review binding as evidence, and the "pending" wording is gone. +- **Math-#173 review 5360751376 (OpenAI / GPT-6 Astra Pro, at `5d8f011`):** ACCEPT of Route C as an elementary conditional + implication of its stated shell, mixed-event, remote-second-moment and fourth-moment estimates (exposure: author of + Math-#162, contributor to Math-#166/#169). Its narrow amendment to the direct-statement paragraph (no fixed-`R` + substitution into (L1); the diagonal argument) is applied in v1.5, as the integrator's hold 5902847683 / 5902997395 / + 5907324679 asked; everything else in that hold was closed by v1.3 and v1.4. +- **Math-#162 (OpenAI; merged `358f256`, integrated by OpenAI Sol):** Route A. Not re-reviewed; its review record is + bound in-repo. +- **Math-#159 (Anthropic, other session; merged `98fdb54`, integrated by the OpenAI engineering lane):** Route B. Not + re-reviewed; its acceptance is preserved as external evidence. +- **Math-#166 (OpenAI; merged at `ab13a08f`, integrated by OpenAI Sol / C25):** the direct statement, bound in v1.1; not + re-reviewed. +- **Math-#167 (this session; merged at `fa1cf7b` by OpenAI Sol after review 5360524053):** disjoint (D2/D3/D4/D5-annulus/D6 + alignment); its execution is a separate non-Claude act. +- **Math-#172 (merged at `fe2c3ff`):** custody repair of the two-scale packet, binding its reviews to exact proof bytes; + the review record and its JSON binding are bound here at those bytes (v1.2); the proof bytes did not change. +- **Math-#151 (merged `ec6db8c`):** kept the old node open under the wording quoted in §1; this record supplies the + discharge of the only defined residual meaning. diff --git a/reviews/c6_residual_closure_20260930/RESULTS.json b/reviews/c6_residual_closure_20260930/RESULTS.json new file mode 100644 index 000000000..986a13200 --- /dev/null +++ b/reviews/c6_residual_closure_20260930/RESULTS.json @@ -0,0 +1,232 @@ +{ + "checks": { + "DEDUCTION": true, + "GATE": true, + "IDENTITIES": true, + "LIVE": true, + "NEGATIVES": true, + "REVIEWED": true, + "TRANSITIONS": true, + "VERDICTS": true + }, + "component_nodes": 10, + "gate": { + "final": { + "changed_nodes": [ + "math.c6-component.palm-proof", + "math.c6r-component.cluster-law-acceptance", + "math.c6r-component.cluster-law-proof", + "math.c6r-component.cluster-law-source-map", + "math.c6r-component.residual-closure-record", + "math.c6r-component.spectral-closure-proof", + "math.c6r-component.spectral-closure-review-record", + "math.c6r-component.two-scale-law-proof", + "math.c6r-component.two-scale-review-binding", + "math.c6r-component.two-scale-review-record", + "math.rn-region.witness-collision.leading-mass-localization" + ], + "impacted": [ + "math.c6-component.palm-proof", + "math.c6r-component.cluster-law-acceptance", + "math.c6r-component.cluster-law-proof", + "math.c6r-component.cluster-law-source-map", + "math.c6r-component.residual-closure-record", + "math.c6r-component.spectral-closure-proof", + "math.c6r-component.spectral-closure-review-record", + "math.c6r-component.two-scale-law-proof", + "math.c6r-component.two-scale-review-binding", + "math.c6r-component.two-scale-review-record", + "math.rn-region.witness-collision.leading-mass-localization" + ], + "old_node_transition": "deferred: presupposes Math-#160 step 3 (aggregate node absent live)", + "residual_classification": "PROVED_REVIEWED", + "residual_held": false, + "source_drift_reaches_residual": 10, + "source_snapshots_supplied": true + }, + "final-corollary-only": { + "changed_nodes": [ + "math.c6-component.palm-proof", + "math.c6r-component.cluster-law-acceptance", + "math.c6r-component.cluster-law-proof", + "math.c6r-component.cluster-law-source-map", + "math.c6r-component.residual-closure-record", + "math.c6r-component.spectral-closure-proof", + "math.c6r-component.spectral-closure-review-record", + "math.c6r-component.two-scale-law-proof", + "math.c6r-component.two-scale-review-binding", + "math.c6r-component.two-scale-review-record", + "math.rn-region.witness-collision.leading-mass-localization" + ], + "impacted": [ + "math.c6-component.palm-proof", + "math.c6r-component.cluster-law-acceptance", + "math.c6r-component.cluster-law-proof", + "math.c6r-component.cluster-law-source-map", + "math.c6r-component.residual-closure-record", + "math.c6r-component.spectral-closure-proof", + "math.c6r-component.spectral-closure-review-record", + "math.c6r-component.two-scale-law-proof", + "math.c6r-component.two-scale-review-binding", + "math.c6r-component.two-scale-review-record", + "math.rn-region.witness-collision.leading-mass-localization" + ], + "old_node_transition": "deferred: presupposes Math-#160 step 3 (aggregate node absent live)", + "residual_classification": "PROVED_REVIEWED", + "residual_held": false, + "source_drift_reaches_residual": 10, + "source_snapshots_supplied": true + }, + "final-direct-only": { + "changed_nodes": [ + "math.c6-component.palm-proof", + "math.c6r-component.cluster-law-acceptance", + "math.c6r-component.cluster-law-proof", + "math.c6r-component.cluster-law-source-map", + "math.c6r-component.residual-closure-record", + "math.c6r-component.spectral-closure-proof", + "math.c6r-component.spectral-closure-review-record", + "math.c6r-component.two-scale-law-proof", + "math.c6r-component.two-scale-review-binding", + "math.c6r-component.two-scale-review-record", + "math.rn-region.witness-collision.leading-mass-localization" + ], + "impacted": [ + "math.c6-component.palm-proof", + "math.c6r-component.cluster-law-acceptance", + "math.c6r-component.cluster-law-proof", + "math.c6r-component.cluster-law-source-map", + "math.c6r-component.residual-closure-record", + "math.c6r-component.spectral-closure-proof", + "math.c6r-component.spectral-closure-review-record", + "math.c6r-component.two-scale-law-proof", + "math.c6r-component.two-scale-review-binding", + "math.c6r-component.two-scale-review-record", + "math.rn-region.witness-collision.leading-mass-localization" + ], + "old_node_transition": "deferred: presupposes Math-#160 step 3 (aggregate node absent live)", + "residual_classification": "PROVED_REVIEWED", + "residual_held": false, + "source_drift_reaches_residual": 10, + "source_snapshots_supplied": true + }, + "final-preexisting": { + "changed_nodes": [ + "math.c6-component.palm-proof", + "math.c6r-component.cluster-law-acceptance", + "math.c6r-component.cluster-law-proof", + "math.c6r-component.cluster-law-source-map", + "math.c6r-component.residual-closure-record", + "math.c6r-component.spectral-closure-proof", + "math.c6r-component.spectral-closure-review-record", + "math.c6r-component.two-scale-law-proof", + "math.c6r-component.two-scale-review-binding", + "math.c6r-component.two-scale-review-record", + "math.rn-region.witness-collision.leading-mass-localization" + ], + "impacted": [ + "math.c6-component.palm-proof", + "math.c6r-component.cluster-law-acceptance", + "math.c6r-component.cluster-law-proof", + "math.c6r-component.cluster-law-source-map", + "math.c6r-component.residual-closure-record", + "math.c6r-component.spectral-closure-proof", + "math.c6r-component.spectral-closure-review-record", + "math.c6r-component.two-scale-law-proof", + "math.c6r-component.two-scale-review-binding", + "math.c6r-component.two-scale-review-record", + "math.rn-region.witness-collision.leading-mass-localization" + ], + "old_node_transition": "deferred: presupposes Math-#160 step 3 (aggregate node absent live)", + "residual_classification": "PROVED_REVIEWED", + "residual_held": false, + "source_drift_reaches_residual": 10, + "source_snapshots_supplied": true + }, + "final-record-unreviewed": { + "changed_nodes": [ + "math.c6-component.palm-proof", + "math.c6r-component.cluster-law-acceptance", + "math.c6r-component.cluster-law-proof", + "math.c6r-component.cluster-law-source-map", + "math.c6r-component.residual-closure-record", + "math.c6r-component.spectral-closure-proof", + "math.c6r-component.spectral-closure-review-record", + "math.c6r-component.two-scale-law-proof", + "math.c6r-component.two-scale-review-binding", + "math.c6r-component.two-scale-review-record", + "math.rn-region.witness-collision.leading-mass-localization" + ], + "impacted": [ + "math.c6-component.palm-proof", + "math.c6r-component.cluster-law-acceptance", + "math.c6r-component.cluster-law-proof", + "math.c6r-component.cluster-law-source-map", + "math.c6r-component.residual-closure-record", + "math.c6r-component.spectral-closure-proof", + "math.c6r-component.spectral-closure-review-record", + "math.c6r-component.two-scale-law-proof", + "math.c6r-component.two-scale-review-binding", + "math.c6r-component.two-scale-review-record", + "math.rn-region.witness-collision.leading-mass-localization" + ], + "old_node_transition": "deferred: presupposes Math-#160 step 3 (aggregate node absent live)", + "residual_classification": "PROVED_REVIEWED", + "residual_held": true, + "source_drift_reaches_residual": 10, + "source_snapshots_supplied": true + }, + "installed-simulated": { + "changed_nodes": [], + "impacted": [], + "old_node_transition": "deferred: presupposes Math-#160 step 3 (aggregate node absent live)", + "residual_classification": "PROVED_REVIEWED", + "residual_held": false, + "source_drift_reaches_residual": 10, + "source_snapshots_supplied": true + }, + "interim": { + "changed_nodes": [ + "math.c6-component.palm-proof", + "math.c6r-component.cluster-law-acceptance", + "math.c6r-component.cluster-law-proof", + "math.c6r-component.cluster-law-source-map", + "math.c6r-component.residual-closure-record", + "math.c6r-component.spectral-closure-proof", + "math.c6r-component.spectral-closure-review-record", + "math.c6r-component.two-scale-law-proof", + "math.c6r-component.two-scale-review-binding", + "math.c6r-component.two-scale-review-record", + "math.rn-region.witness-collision.leading-mass-localization" + ], + "impacted": [ + "math.c6-component.palm-proof", + "math.c6r-component.cluster-law-acceptance", + "math.c6r-component.cluster-law-proof", + "math.c6r-component.cluster-law-source-map", + "math.c6r-component.residual-closure-record", + "math.c6r-component.spectral-closure-proof", + "math.c6r-component.spectral-closure-review-record", + "math.c6r-component.two-scale-law-proof", + "math.c6r-component.two-scale-review-binding", + "math.c6r-component.two-scale-review-record", + "math.rn-region.witness-collision.leading-mass-localization" + ], + "old_node_transition": "deferred: presupposes Math-#160 step 3 (aggregate node absent live)", + "residual_classification": "OPEN_ACTIVE", + "residual_held": false, + "source_drift_reaches_residual": 10, + "source_snapshots_supplied": true + } + }, + "inventory_files": 13, + "live_state": { + "edges_present": false, + "mismatched": [], + "present": [], + "residual": null + }, + "object": "C6-RESIDUAL-CLOSURE-20260930-v1", + "passed": true, + "scope": "identity, verdict-row, live-register (including the installed state), reviewed-text, exact finite bookkeeping of section 3, transition-shape, hard-gate replay with source snapshots in every execution shape, and filesystem-negative checks; the Gaussian limits are the sources' reviewed statements and are not re-proved; nothing is written" +} diff --git a/reviews/c6_residual_closure_20260930/REVIEWED_SECTION_3_b3fac79.md b/reviews/c6_residual_closure_20260930/REVIEWED_SECTION_3_b3fac79.md new file mode 100644 index 000000000..2fff7c277 --- /dev/null +++ b/reviews/c6_residual_closure_20260930/REVIEWED_SECTION_3_b3fac79.md @@ -0,0 +1,36 @@ + + +## 3. The corollary: (Res) from the reviewed statements + +Write `N_R` for the window count in the Euclidean ball of radius `R r` about `o` ([SC]'s `N_R`; [CL]'s `N^A` with +`A = R`), `N_out = N - N_R`, and `(n)_2 = n(n - 1)`. The quantity in (Res) is exactly + + M_R := E_{Q_r^W} #{ordered pairs of distinct window points not both within R r of o} = E[(N)_2] - E[(N_R)_2], (D1) + +since for every configuration `(N)_2 - (N_R)_2 = 2 N_R N_out + (N_out)_2 >= 2 N_R N_out >= 0` (exact identity, checked +in `DEDUCTION`). So (Res) says `lim_R limsup_r r^-3 (E[(N)_2] - E[(N_R)_2]) = 0`, and the mixed count of Math-#160 §5 is +`M(R, s_0) <= E[N_R N_out] <= M_R / 2`. + +**Route A ([SC], Math-#162).** +1. *Full second factorial moment.* [SC] (26): `E (N)_2 / r^3 -> 2 nu2 = 2 a_2`, a stated consequence of Theorem (3) + with `q = 2` (§8, Slice C). +2. *Near second factorial moment.* [SC] (18): `r^-3 Q_W(N_R = j) -> a_j^R` for `j = 1, 2` and `r^-3 Q_W(N_R >= 3) -> 0` + (§5, Slice B). Tail: `(N_R)_2 <= (N)_2`, and for integers `n > M >= 3`, `n(n-1) <= n(n-1)(n-2)/(M-1)` (exact, `DEDUCTION`), + so `E[(N_R)_2; N_R > M] <= E[(N)_3]/(M-1) <= C_3 r^3/(M-1)` by [PALM] Theorem Q with `q = 3`. Hence + `limsup_r | r^-3 E[(N_R)_2] - 2 a_2^R | <= C_3/(M-1)` for every `M`, i.e. `r^-3 E[(N_R)_2] -> 2 a_2^R` (the finite sum + over `n <= M` converges by (18), its `n >= 3` terms to zero). This is the same tail argument [SC] §8 uses for (3). +3. *Exhaustion.* [SC] (20): `a_2^R -> a_2` as `R -> oo` (dominated convergence with the integrable majorant (19), §6, + Slice B). + +Therefore `limsup_r r^-3 M_R = 2 a_2 - 2 a_2^R` (a full limit, by 1 and 2), which tends to `0` as `R -> oo` by 3. That is +(Res). ∎ + +**Route B ([CL], Math-#159).** Corollary Λ (1.6): `r^-3 E[(N)_2] -> Λ_2 = 2 nu(2) = 2 nu_near(2)`; Proposition 4.4: +`r^-3 Q{N^A = n} -> nu_near^A(n)` for `n = 1, 2`, `r^-3 Q{N^A >= 3} -> 0`, and `nu_near^A(n) -> nu_near(n)` as `A -> oo`; +the tail of step 2 is the one [CL] §6.3 uses ([PALM] Theorem Q). The same three lines give (Res). Directly, without the +factorial-moment limit: Lemma 5.2 (5.4), `E[N^A 1{N_far^rho >= 1}] <= C(A, rho) r^(9/2)`, together with +`E[N^A (N_far^rho - 1)_+] <= (E (N^A)^2)^(1/2) (E N_far^4)^(1/4) Q{N_far^rho >= 2}^(1/4) <= C r^(3/2) r^(3/4) r^(5/4) = C r^(7/2)` +([PALM] Theorem Q for the second and fourth moments through Stirling's identity `n^4 = (n)_4 + 6(n)_3 + 7(n)_2 + (n)_1`, +[RC] Corollary D for `Q{N_far^rho >= 2} <= E (N_far^rho)_2 / 2 = O(r^5)`), gives `E[N^A N_far^rho] = O(r^(7/2)) = o(r^3)` +at fixed `(A, rho)`, which is the mixed count of Math-#160 §5 with `s_0 = rho` (the far region `D_rho` is measured from +`o`; a point at distance `>= s_0` from both pins lies in `D_{s_0/2}` for `r < s_0`). Exponent ledgers checked exactly. diff --git a/reviews/c6_residual_closure_20260930/SOURCE_FILES.json b/reviews/c6_residual_closure_20260930/SOURCE_FILES.json new file mode 100644 index 000000000..692bb2b78 --- /dev/null +++ b/reviews/c6_residual_closure_20260930/SOURCE_FILES.json @@ -0,0 +1,47 @@ +{ + "schema": 1, + "object": "C6-RESIDUAL-CLOSURE-20260930-v1", + "scientific_effect": "NONE", + "disposition": "PROPOSAL_FOR_A_NON_CLAUDE_LANE", + "declarative": true, + "executed": false, + "base": "358f2562efbccc59f9549e5a79650e2e936395c3", + "files": [ + { + "path": "EXTERNAL_REVIEWS.md", + "bytes": 14108, + "sha256": "27b4d8a5f04981e7b01b20f767078df87b4d0c75aebc6f6ed665347a8b605a53", + "git_blob": "70d05080ed81c66b43261438cae3b9ec2840e637" + }, + { + "path": "PROPOSED_TRANSITIONS.json", + "bytes": 31461, + "sha256": "78a50b82fd9cbf04899aa5ddc62875850ce68b8b5a5babfb637b7db7e2a49c5c", + "git_blob": "3706e8ac4e906aa1b53cdf5634abfb324c35a9e3" + }, + { + "path": "RECONCILIATION.md", + "bytes": 34758, + "sha256": "b647a186d0cfd1662fc69e9d31dfd447dbb1b2f6ef4364bbd59c4956f18aed25", + "git_blob": "3cfd17c5ef0356dbd3e8f98a2d08cb404ddd982c" + }, + { + "path": "RESULTS.json", + "bytes": 10376, + "sha256": "3c61cc49155cae7bba0fec30c0bf0a9fb085340f3a161d5898c527b87f9b5805", + "git_blob": "986a1320098b37238f117280b7925c683ca7c3c2" + }, + { + "path": "residual_check.py", + "bytes": 33664, + "sha256": "76ebda22aef26a70ab8ef5916e64bc7c5b3b34833fa702664fa00a7b4c1c4406", + "git_blob": "2667d4b35baa674c74c051244febb7f08118c572" + }, + { + "path": "REVIEWED_SECTION_3_b3fac79.md", + "bytes": 3157, + "sha256": "50daacbe7e244bc149dbf4568970d79f38a356daa1e88a850f2fc2d074db5b6c", + "git_blob": "2fff7c277b43fa8e967ce9a8d70cf01a69e5eee4" + } + ] +} diff --git a/reviews/c6_residual_closure_20260930/residual_check.py b/reviews/c6_residual_closure_20260930/residual_check.py new file mode 100644 index 000000000..2667d4b35 --- /dev/null +++ b/reviews/c6_residual_closure_20260930/residual_check.py @@ -0,0 +1,641 @@ +"""Checks for C6-RESIDUAL-CLOSURE-20260930-v1 (RECONCILIATION.md, PROPOSED_TRANSITIONS.json, EXTERNAL_REVIEWS.md, +REVIEWED_SECTION_3_b3fac79.md). + +Standard library only. Run from the repository root: python -B -S reviews/c6_residual_closure_20260930/residual_check.py +Checks: IDENTITIES, VERDICTS, LIVE, REVIEWED, DEDUCTION, TRANSITIONS, GATE, NEGATIVES. No mathematics is re-proved beyond the +exact finite bookkeeping of section 3 (pair identities, tails, ledgers); the proposed graph is replayed through the downstream +hard gate's own validators in every execution shape (interim, final, pre-existing residual node, each evidence path alone, the +unreviewed-record negative, and the installed state), with source snapshots. Nothing is written to the repository. +""" +import argparse +import copy +import hashlib +import importlib.util +import json +import os +import pathlib +import shutil +import sys +import tempfile +from fractions import Fraction as F + +MUTANTS = ("allow-symlink", "no-hash", "stale-fingerprint", "drop-required-edge", "executed-flag", "controlling-true", + "tail-reversed", "pair-identity-broken", "route-c-broken", "drop-review-needle", + "installed-drift", "snapshot-omitted", "record-unreviewed", "reviewed-text-drift") +MUT = None +HERE = "reviews/c6_residual_closure_20260930" +GRAPH = "frontiers/downstream_gate_20260925/GRAPH.json" +SELECTOR = "frontiers/downstream_gate_20260925/SELECTOR_REGION.json" +HARD_GATE = "frontiers/downstream_gate_20260925/hard_gate.py" +RES = "math.rn-region.witness-collision.leading-mass-localization" +WIT = "math.rn-region.witness-collision" +AGG = "math.c6-witness-collision-factorial-moment" +RECORD_NODE = "math.c6r-component.residual-closure-record" +PALM_NODE = "math.c6-component.palm-proof" +SC = "frontiers/spectral_cluster_closure_20260929/PROOF.md" +REVIEWED = HERE + "/REVIEWED_SECTION_3_b3fac79.md" +REVIEWED_HEAD = "b3fac79875f28bacd135c0aa5e65a47a41ae0fdf" +SOL_REVIEW = "Math-#173 review 5360645884" +FP_RES = "leading-order r^3 mass of E N(N-1): scale-r localization; open piece = mixed local/remote pairs M(R, s_0)" +FP_WIT = "eta->0 mutual witness separation" +INVENTORY = { + "frontiers/spectral_cluster_closure_20260929/PROOF.md": [ + "e971b2cbe50a8a06b47c1219191201e0d1037c9adac23e5e3b7d2051bb70c2eb", + "16c56821b52fd76b0be791622b9c3809eafde75a" + ], + "frontiers/spectral_cluster_closure_20260929/REVIEW_RECORD.md": [ + "6031d36697789097185a8e65bfbdf80f447e229689eac5a706ee8b0558db64a5", + "9bcae183fecdf0ffe4d612a209438a4fb1fa0edd" + ], + "frontiers/spectral_cluster_closure_20260929/README.md": [ + "b1e2a0722945a6189d8338c2e5b1f1a74b3b5646b8dc10fe29168c165508342c", + "895dded8aa8e405ad8e9640d3ffebc6449a108d0" + ], + "frontiers/c6_cluster_law_20260929/PROOF.md": [ + "96b8e2d59defee6059bf151a896b7fc7c91fc529b385a3db8a87574901197b38", + "ba492c8e62e58bfc055fc8254c790e893d346ba5" + ], + "frontiers/c6_cluster_law_20260929/README.md": [ + "e4b35f2b0e919ba57ebfb121c403896a32782d58dd99d7ec6a3d6d9e5107c6ac", + "1166376f7b4d917b1bda3f9438adfd94d8831139" + ], + "frontiers/c6_cluster_law_20260929/SOURCE_MAP.json": [ + "0584c3808b633fceb3c308186b07d862eb4916053daf4e7bf1110592ec41f107", + "ef51c582d0b1c874aabb01fce3b35c10631f7fc6" + ], + "frontiers/c6_palm_route_20260929/PROOF.md": [ + "aa37f16040ab9e05bb2e4e3f1d678367497e8dc2cf43eef197a4d6592c2f129b", + "89eb8adf08fe7afc2cab9662d3a9875c05ae5cc5" + ], + "reviews/c6_residual_closure_20260930/EXTERNAL_REVIEWS.md": [ + "27b4d8a5f04981e7b01b20f767078df87b4d0c75aebc6f6ed665347a8b605a53", + "70d05080ed81c66b43261438cae3b9ec2840e637" + ], + "reviews/c6_residual_closure_20260930/RECONCILIATION.md": [ + "b647a186d0cfd1662fc69e9d31dfd447dbb1b2f6ef4364bbd59c4956f18aed25", + "3cfd17c5ef0356dbd3e8f98a2d08cb404ddd982c" + ], + "reviews/c6_residual_closure_20260930/REVIEWED_SECTION_3_b3fac79.md": [ + "50daacbe7e244bc149dbf4568970d79f38a356daa1e88a850f2fc2d074db5b6c", + "2fff7c277b43fa8e967ce9a8d70cf01a69e5eee4" + ], + "frontiers/two_scale_cluster_geometry_20260929/TWO_SCALE_LAW.md": [ + "e81d7fe09d25c3266eb8e62922756f54761d7f74d692fb35d9a8071fffd73769", + "a32fd5f7d941bbe1fe943df045b1e0fbec8d691c" + ], + "frontiers/two_scale_cluster_geometry_20260929/REVIEW_RECORD.md": [ + "af1540308f37220e6592b700bf42181205b1d4588a040a5c151bf0a6f861e728", + "31896de23fc56822c184375d0dc2b1c7e27fcae4" + ], + "frontiers/two_scale_cluster_geometry_20260929/REVIEW_RECORD.json": [ + "958d2e1ae8ea5d034d0d87efce6cde9be57ebb9d7c0b671e69d3d6598a6675ca", + "a4b0fb99c24e2edf41973ea2a5e5176584602855" + ] +} +VERDICTS = { + "frontiers/spectral_cluster_closure_20260929/PROOF.md": [ + "sum_(n>=1) n^q |r^-3 Q_r^W(N_r=n)-nu1*1{n=1}-nu2*1{n=2}| -> 0", + "r^-3 Q_W(N_R=j) -> a_j^R=integral 1{n_R=j}dM", + "Dominated convergence proves a_j^R->a_j", + "Q_W(N_R>0,N_far^rho>0)=o_(R,rho)(r^3)", + "E (N)_2/r^3 -> 2nu2"], + "frontiers/spectral_cluster_closure_20260929/REVIEW_RECORD.md": [ + "Git blob16c56821b52fd76b0be791622b9c3809eafde75a", + "A — Anthropic Claude5359968447", + "B — Anthropic Claude5359845136", + "C — OpenAI/Codex5359879627", + "ACCEPT Sections7-8, compact-origin-jet far conditioning, full mixed o(r^3), radius"], + "frontiers/spectral_cluster_closure_20260929/README.md": [ + "Core conditional proof has completed scoped nonauthor A/B/C acceptance."], + "frontiers/c6_cluster_law_20260929/PROOF.md": [ + "**Corollary Lambda (asymptotic factorial moments).**", + "Lambda_2 = 2 nu(2)", + "Moreover `nu_near^A(n) -> nu_near(n)` as `A -> oo`", + "**Lemma 5.2 (no near–far cross term).**", + "C(A, rho) r^(9/2)"], + "frontiers/c6_cluster_law_20260929/README.md": ["# C6 cluster law (CL-C6-CLUSTER-LAW-20260929-v1.2)"], + "frontiers/c6_cluster_law_20260929/SOURCE_MAP.json": ["nonauthor_acceptance", "review 5360192822"], + "frontiers/c6_palm_route_20260929/PROOF.md": [ + "**Object:** CL-C6-PALM-20260929-v1.", + "**Theorem Q (factorial moments, every fixed dimension).**"], + HERE + "/EXTERNAL_REVIEWS.md": [ + "pullrequestreview-5360192822", + "VERDICT: ACCEPT Theorem N, Corollaries Lambda/S", + "A pull-request review is a mutable external object", + "pullrequestreview-5360645884", + "MATHEMATICAL VERDICT ON §3: ACCEPT at the stated fixed-d, fixed-torus, compact-positive-gap window scope.", + REVIEWED_HEAD], + HERE + "/RECONCILIATION.md": ["**Object:** C6-RESIDUAL-CLOSURE-20260930-v1.", "(Res)", "(D1)", "(D2)", "5360645884"], + REVIEWED: ["## 3. The corollary: (Res) from the reviewed statements", "(D1)", + "**Route A ([SC], Math-#162).**", "**Route B ([CL], Math-#159).**"], + "frontiers/two_scale_cluster_geometry_20260929/TWO_SCALE_LAW.md": [ + "**Theorem L (factorial localization).** For every fixed integer q>=2,", + "r^-3 E_r[(N_r)_q-(N_in)_q] -> 0.", + "E_r[N_R N_far^rho]=o_(R,rho)(r^3),"], + "frontiers/two_scale_cluster_geometry_20260929/REVIEW_RECORD.md": [ + "Anthropic Claude review5360227991", + "bloba32fd5f7d941bbe1fe943df045b1e0fbec8d691c", + "ACCEPT of Theorem T, Theorem L, ordered-pair law L3"], + "frontiers/two_scale_cluster_geometry_20260929/REVIEW_RECORD.json": [ + "\"native_review_id\": 5360227991", + "\"proof_path\": \"TWO_SCALE_LAW.md\"", + "\"body_sha256\": \"c63efc292d7cf209e2770419cc159276897d0ba955c32ee1d2af88c8aa7f0ed8\"", + "\"git_blob\": \"a32fd5f7d941bbe1fe943df045b1e0fbec8d691c\""], +} +EXTERNAL_PREFIXES = ("https://", "http://", "external:") + + +def git_blob(data): + return hashlib.sha1(b"blob %d\0" % len(data) + data).hexdigest() + + +def no_symlink_on_path(root, path): + parts = pathlib.PurePosixPath(path).parts + return not any((root / pathlib.PurePosixPath(*parts[:i])).is_symlink() for i in range(1, len(parts) + 1)) + + +def identities_ok(root): + for path, (sha, blob) in INVENTORY.items(): + p = root / path + if not os.path.lexists(p): + return False + if MUT != "allow-symlink" and not no_symlink_on_path(root, path): + return False + if not p.is_file(): + return False + data = p.read_bytes() + if MUT == "no-hash": + continue + if hashlib.sha256(data).hexdigest() != sha or git_blob(data) != blob: + return False + return True + + +def check_verdicts(root): + needles = {k: list(v) for k, v in VERDICTS.items()} + if MUT == "drop-review-needle": + needles[SC].append("THIS NEEDLE IS NOT IN THE SOURCE") + for path, ns in needles.items(): + text = (root / path).read_text(encoding="utf-8") + if not all(n in text for n in ns): + return False + return True + + +def load_spec(root): + spec = json.loads((root / HERE / "PROPOSED_TRANSITIONS.json").read_text(encoding="utf-8")) + if MUT == "executed-flag": + spec["executed"] = True + if MUT == "controlling-true": + spec["transitions"][0]["proposed"]["controlling"] = True + if MUT == "stale-fingerprint": + for n in spec["proposed_graph_nodes"]: + if n["id"] == PALM_NODE: + n["fingerprint"] = "0" * 64 + if MUT == "drop-required-edge": + spec["proposed_graph_edges"] = [e for e in spec["proposed_graph_edges"] + if not (e["from"] == RES and e["to"] == "math.c6r-component.spectral-closure-proof")] + if MUT == "record-unreviewed": + for n in spec["proposed_graph_nodes"]: + if n["id"] == RECORD_NODE: + n["review_basis"] = [] # a PROVED_REVIEWED record with no nonauthor read must be rejected + return spec + + +def load_live(root): + graph = json.loads((root / GRAPH).read_text(encoding="utf-8")) + sel = json.loads((root / SELECTOR).read_text(encoding="utf-8")) + return graph, sel + + +def component_keys(comp): + """Keys a live node must reproduce to count as the proposed component. The palm node is cross-record (Math-#160 + defines its other fields); every node of this record must reproduce the proposal byte-for-byte on every proposed key.""" + if comp["id"] == PALM_NODE: + return ("kind", "source", "fingerprint", "classification", "controlling") + return tuple(k for k in comp if k not in ("id", "create_if_absent", "cross_record")) + + +def matches_proposal(live, comp): + return isinstance(live, dict) and all(live.get(k) == comp[k] for k in component_keys(comp)) + + +def installed_state(graph, spec): + """How much of the proposal the live graph already carries (Codex 4140125558). Fail-closed: a live node on a + component source that is not the proposed node on every proposed key is a mismatch, as is a proposed id carrying + anything else.""" + nodes = graph["nodes"] + by_source = {c["source"]: c for c in spec["proposed_graph_nodes"]} + present, mismatched = set(), set() + for nid, n in nodes.items(): + if not isinstance(n, dict) or n.get("source") not in by_source: + continue + comp = by_source[n["source"]] + (present if nid == comp["id"] and matches_proposal(n, comp) else mismatched).add(nid) + for c in spec["proposed_graph_nodes"]: + if c["id"] in nodes and c["id"] not in present: + mismatched.add(c["id"]) + res = nodes.get(RES) + live_edges = {(e["from"], e["to"], e["required"], e["relation"]) for e in graph["edges"]} + wanted = {(e["from"], e["to"], e["required"], e["relation"]) for e in spec["proposed_graph_edges"] + if not e.get("deferred_with")} + return {"present": sorted(present), "mismatched": sorted(mismatched), + "residual": res.get("classification") if isinstance(res, dict) else None, + "edges_present": wanted <= live_edges} + + +def live_ok(graph, sel, spec): + nodes = graph["nodes"] + wit = nodes.get(WIT) + ok = isinstance(wit, dict) and wit.get("kind") == "region" and wit.get("fingerprint") == FP_WIT + ok &= wit.get("classification") in ("OPEN_ACTIVE", "PROVED_REVIEWED") + res = nodes.get(RES) + if res is not None: + ok &= res.get("kind") == "region" and res.get("fingerprint") == FP_RES + ok &= res.get("classification") in ("OPEN_ACTIVE", "PROVED_REVIEWED") + ok &= "witness-collision" in sel.get("regions", []) + st = installed_state(graph, spec) + ok &= not st["mismatched"] + if st["residual"] == "PROVED_REVIEWED": + # a promoted residual must carry the whole proposal: every component by id and bytes, every edge, the reading rule + ok &= set(c["id"] for c in spec["proposed_graph_nodes"]) <= set(st["present"]) and st["edges_present"] + ok &= set(res.get("reading_rule", [])) >= set(spec["transitions"][0]["proposed"]["reading_rule"]) + return bool(ok), st + + +def check_live(root, spec): + graph, sel = load_live(root) + return live_ok(graph, sel, spec) + + +def reviewed_block(data): + """The reviewed text: the file after its one-line provenance comment.""" + if data.startswith(b"\n\n") + return rest if sep else b"" + return data + + +def check_reviewed(root, spec): + """The record node is PROVED_REVIEWED on the strength of a non-Claude read of section 3 (Math-#173 review 5360645884 + at head b3fac79): the paragraphs that review read are preserved verbatim, fingerprinted in the proposal, and present + unchanged in the current RECONCILIATION.md; the review's identity is preserved in EXTERNAL_REVIEWS.md.""" + rec = next((c for c in spec["proposed_graph_nodes"] if c["id"] == RECORD_NODE), None) + if rec is None or not rec.get("review_basis"): + return False + b0 = rec["review_basis"][0] + ok = rec["classification"] == "PROVED_REVIEWED" and b0.get("review") == SOL_REVIEW + ok &= str(b0.get("provider", "")).startswith("OpenAI") and "ACCEPT" in str(b0.get("verdict", "")) + ok &= b0.get("reviewed_head") == REVIEWED_HEAD and b0.get("reviewed_text") == REVIEWED + block = reviewed_block((root / REVIEWED).read_bytes()) + if MUT == "reviewed-text-drift": + block = block[:-1] + b"?" + ok &= len(block) > 1000 and hashlib.sha256(block).hexdigest() == b0.get("reviewed_text_sha256") + ok &= block.startswith(b"## 3. ") and b"**Route A ([SC], Math-#162).**" in block + ok &= b"**Route B ([CL], Math-#159).**" in block and b"Route C" not in block # the read does not cover Route C + ok &= block in (root / HERE / "RECONCILIATION.md").read_bytes() # verbatim in the current record + ext = (root / HERE / "EXTERNAL_REVIEWS.md").read_text(encoding="utf-8") + ok &= "pullrequestreview-5360645884" in ext and REVIEWED_HEAD in ext + return bool(ok) + + +def check_deduction(): + """Exact finite bookkeeping of RECONCILIATION.md section 3.""" + ok = True + f2 = lambda n: n * (n - 1) + f3 = lambda n: n * (n - 1) * (n - 2) + # (D1): (N)_2 - (N_R)_2 = 2 N_R N_out + (N_out)_2 >= 2 N_R N_out >= 0 + for nr in range(13): + for no in range(13): + rhs = 2 * nr * no + (no * no if MUT == "pair-identity-broken" else f2(no)) + ok &= f2(nr + no) - f2(nr) == rhs and rhs >= 2 * nr * no >= 0 + # monotonicity used by the diagonal argument of the direct statement: n -> (n)_2 is nondecreasing on n >= 0 + ok &= all(f2(n + 1) >= f2(n) for n in range(0, 41)) + # tail: for integers n > M >= 3, n(n-1) <= n(n-1)(n-2)/(M-1) + for M in range(3, 11): + for n in range(M + 1, 41): + lhs, rhs = f2(n) * (M - 1), f3(n) + ok &= (lhs >= rhs) if MUT == "tail-reversed" else (lhs <= rhs) + # (D2), Route C: 0 <= (N)_2 - (A)_2 <= N^2 [1{B>0} + 1{A>0, C>0} + 1{C>=2}] for all counts A, B, C + for a in range(9): + for b in range(9): + for c in range(9): + n = a + b + c + ind = (1 if b > 0 else 0) + (1 if (a > 0 and c > 0) else 0) + (0 if MUT == "route-c-broken" else (1 if c >= 2 else 0)) + ok &= 0 <= f2(n) - f2(a) <= n * n * ind + ok &= F(3, 2) + F(9, 4) - 3 == F(3, 4) and F(3, 2) + F(5, 2) - 3 == F(1) + # Stirling: n^4 = (n)_4 + 6 (n)_3 + 7 (n)_2 + (n)_1 + for n in range(0, 21): + ok &= n ** 4 == n * (n - 1) * (n - 2) * (n - 3) + 6 * f3(n) + 7 * f2(n) + n + # exponent ledgers of the two direct routes + ok &= F(3) + F(3, 2) == F(9, 2) and F(9, 2) > 3 + ok &= F(3, 2) + F(3, 4) + F(5, 4) == F(7, 2) and F(7, 2) > 3 + # truncation error of a finite distribution against E(N)_3 / (M - 1) + probs = [F(1, 2), F(1, 4), F(1, 8), F(1, 16), F(1, 32), F(1, 64), F(1, 128), F(1, 256), F(1, 256)] + assert sum(probs) == 1 + e3 = sum(p * f3(n) for n, p in enumerate(probs)) + for M in (3, 4, 5, 6): + tail = sum(p * f2(n) for n, p in enumerate(probs) if n > M) + ok &= tail <= e3 / (M - 1) + # iterated limit, exact rational instance: a_2 = 1, a_2^R = 1 - 1/R^2, limsup_r r^-3 M_R = 2 a_2 - 2 a_2^R = 2/R^2 -> 0 + vals = [2 - 2 * (1 - F(1, R * R)) for R in range(4, 40)] + ok &= all(v == F(2, R * R) for v, R in zip(vals, range(4, 40))) + ok &= all(vals[i] > vals[i + 1] for i in range(len(vals) - 1)) and vals[-1] < F(1, 500) + return bool(ok) + + +def evidence_paths(spec): + ep = spec["evidence_paths"] + return list(ep["direct_statement"]["components"]), list(ep["reviewed_corollary"]["components"]) + + +def build(spec, graph, stage): + """Apply the proposal to a copy of the live graph, idempotently: a component the live graph already carries + byte-for-byte is not re-created, an edge already present is not re-added. stage: 'interim' (before step 2: residual + node OPEN_ACTIVE with its evidence attached), 'final' (after step 2: residual PROVED_REVIEWED, both evidence paths + required), 'final-preexisting' (Math-#160 step 1 already created the residual node OPEN_ACTIVE), 'final-direct-only' + and 'final-corollary-only' (the other path's edges supporting: each path alone), 'final-record-unreviewed' (the + record node without its read but still required: the residual must be held). Returns (old, new).""" + old = copy.deepcopy(graph) + if stage == "final-preexisting": + old["nodes"][RES] = {"layer": "D5", "kind": "region", "classification": "OPEN_ACTIVE", "controlling": False, + "fingerprint": FP_RES, "notes": "Math-#160 execution_order step 1"} + new = copy.deepcopy(old) + present = set(installed_state(old, spec)["present"]) + live_by_source = {n.get("source"): nid for nid, n in old["nodes"].items() + if isinstance(n, dict) and n.get("fingerprint") and n.get("source")} + id_map = {} + for c in spec["proposed_graph_nodes"]: + nid = c["id"] + if nid in present: + id_map[nid] = nid # already installed as proposed + continue + if c.get("create_if_absent") and c["source"] in live_by_source: + id_map[nid] = live_by_source[c["source"]] # cross-record node already created by Math-#160 + continue + new["nodes"][nid] = {k: v for k, v in c.items() if k != "id"} + id_map[nid] = nid + t = spec["transitions"][0] + p = t["proposed"] + res = dict(old["nodes"].get(RES) or {}) + res.update({"layer": p["layer"], "kind": "region", + "classification": p["classification"] if stage.startswith("final") else "OPEN_ACTIVE", + "controlling": p["controlling"], "fingerprint": p["fingerprint"], "scope": p["scope"], + "explicit_limits": p["explicit_limits"], "review_disposition": p["review_disposition"], + "review_sources": [r["ref"] for r in p["review_sources"]], + "reading_rule": [id_map.get(x, x) for x in p["reading_rule"]], "notes": p["notes"]}) + new["nodes"][RES] = res + have = {(e["from"], e["to"], e["required"], e["relation"]) for e in new["edges"]} + added = [] + for e in spec["proposed_graph_edges"]: + if e.get("deferred_with"): + continue # the old-node transition presupposes Math-#160 step 3 + key = (e["from"], id_map.get(e["to"], e["to"]), e["required"], e["relation"]) + if key not in have: + added.append({"from": key[0], "to": key[1], "required": key[2], "relation": key[3]}) + have.add(key) + direct, corollary = evidence_paths(spec) + if stage == "final-direct-only": + for e in added: + if e["from"] == RES and e["to"] in corollary: + e["required"] = False + if stage == "final-corollary-only": + for e in added: + if e["from"] == RES and e["to"] in direct: + e["required"] = False + if stage == "final-record-unreviewed" and RECORD_NODE not in present: + new["nodes"][RECORD_NODE]["classification"] = "AUTHOR_SIDE_CANDIDATE" + new["nodes"][RECORD_NODE]["review_basis"] = [] + new["edges"].extend(added) + return old, new + + +def check_transitions(root, spec): + graph, sel = load_live(root) + ok = spec.get("declarative") is True and spec.get("executed") is False + t0, t1 = spec["transitions"] + p = t0["proposed"] + ok &= t0["node"] == RES and t0["kind"] == "region" and p["classification"] == "PROVED_REVIEWED" + ok &= p["controlling"] is False and p["fingerprint"] == FP_RES + ok &= bool(p.get("scope")) and bool(p.get("explicit_limits")) and len(p.get("review_sources", [])) >= 2 + ok &= bool(p.get("notes")) and p.get("review_disposition") == "ACCEPT_AT_EXISTENTIAL_SCOPE" + comps = spec["proposed_graph_nodes"] + cids = [c["id"] for c in comps] + ok &= len(cids) == len(set(cids)) and len({c["source"] for c in comps}) == len(comps) + for c in comps: + ok &= c["kind"] == "reading_rule_component" and c["controlling"] is False + ok &= c["source"] in INVENTORY and c["fingerprint"] == INVENTORY[c["source"]][0] + ok &= bool(c.get("component_role")) and bool(c.get("author_provider")) and len(c.get("review_basis", [])) >= 1 + ok &= c["component_of"] == RES and c["classification"] == "PROVED_REVIEWED" + if c["id"] == PALM_NODE: + ok &= c.get("create_if_absent") is True and "Math-#160" in str(c.get("cross_record")) + # two evidence paths, each sufficient, partitioning the components; the residual requires the union (fail-closed) + direct, corollary = evidence_paths(spec) + ok &= sorted(direct + corollary) == sorted(cids) and not set(direct) & set(corollary) + ok &= RECORD_NODE in corollary and "math.c6r-component.two-scale-law-proof" in direct and len(direct) >= 2 + ok &= sorted(p["reading_rule"]) == sorted(cids) and sorted(t0["required_premises_after"]) == sorted(cids) + req = {(e["from"], e["to"]) for e in spec["proposed_graph_edges"] if e["required"] is True and not e.get("deferred_with")} + ok &= all((RES, cid) in req for cid in cids) + seen = set() + for e in spec["proposed_graph_edges"]: + key = (e["from"], e["to"], e["relation"]) + ok &= key not in seen and type(e["required"]) is bool and bool(e["relation"]) + seen.add(key) + ok &= e["from"] in (RES, WIT) + # the deferred old-node transition + ok &= t1["node"] == WIT and t1.get("deferred") is True and t1["proposed"]["classification"] == "PROVED_REVIEWED" + ok &= sorted(t1["required_premises_after"]) == sorted([RES, AGG]) and t1["proposed"]["controlling"] is False + ok &= AGG not in graph["nodes"] or graph["nodes"][AGG].get("classification") == "PROVED_REVIEWED" + if not ok: + return False, None + st = installed_state(graph, spec) + installed = st["residual"] == "PROVED_REVIEWED" + stages = ("installed",) if installed else ("interim", "final", "final-preexisting", "final-direct-only", + "final-corollary-only", "final-record-unreviewed") + expected_required = {"final-direct-only": len(direct), "final-corollary-only": len(corollary)} + builds = {} + for stage in stages: + old, new = build(spec, graph, "final" if stage == "installed" else stage) + nodes, edges = new["nodes"], new["edges"] + ok &= all(old["nodes"][k] == nodes[k] for k in old["nodes"] if k != RES) # no live node other than the residual changes + ok &= edges[:len(old["edges"])] == old["edges"] + req_after = [e["to"] for e in edges if e["from"] == RES and e["required"] is True] + if stage == "interim": + ok &= nodes[RES]["classification"] == "OPEN_ACTIVE" + else: + ok &= nodes[RES]["classification"] == "PROVED_REVIEWED" + if stage == "installed": + ok &= new == old # the live graph carries the proposal exactly: a no-op + if stage == "final-record-unreviewed": + ok &= nodes[RECORD_NODE]["classification"] == "AUTHOR_SIDE_CANDIDATE" + else: + ok &= nodes[RECORD_NODE]["classification"] == "PROVED_REVIEWED" + ok &= all(nodes[d]["classification"] == "PROVED_REVIEWED" for d in req_after) + ok &= len(req_after) == expected_required.get(stage, len(cids)) + builds[stage] = (old, new) + if not installed: + # the installed state, simulated (Codex 4140125558): the executed graph passes LIVE and re-building it is a no-op + sim = build(spec, graph, "final")[1] + if MUT == "installed-drift": + sim["nodes"]["math.c6r-component.spectral-closure-proof"]["fingerprint"] = "0" * 64 + sim_ok, sim_st = live_ok(sim, sel, spec) + ok &= sim_ok and sim_st["residual"] == "PROVED_REVIEWED" and sim_st["present"] == sorted(cids) + ok &= sim_st["edges_present"] and not sim_st["mismatched"] + o2, n2 = build(spec, sim, "final") + ok &= o2 == n2 + builds["installed-simulated"] = (o2, n2) + return bool(ok), builds + + +def load_hard_gate(root): + hg_spec = importlib.util.spec_from_file_location("hard_gate", root / HARD_GATE) + hg = importlib.util.module_from_spec(hg_spec) + hg_spec.loader.exec_module(hg) + return hg + + +def snapshot(root, graph): + """Exact source snapshot covering every node of a graph, in the shape git_transition_audit.read_snapshot produces, + taken from the working tree: record_only, external_unresolved, blob (bytes and SHA256), tree (sorted file digests), + or missing.""" + out = {} + for nid, n in graph["nodes"].items(): + ref = n.get("source") if isinstance(n, dict) else None + if ref is None: + out[nid] = {"kind": "record_only"} + continue + if ref.startswith(EXTERNAL_PREFIXES): + out[nid] = {"kind": "external_unresolved", "reference": ref} + continue + p = root / ref.rstrip("/") + if p.is_file(): + data = p.read_bytes() + out[nid] = {"kind": "blob", "reference": ref, "bytes": len(data), "sha256": hashlib.sha256(data).hexdigest()} + elif p.is_dir(): + items = [[q.relative_to(p).as_posix(), hashlib.sha256(q.read_bytes()).hexdigest()] + for q in sorted(p.rglob("*")) if q.is_file() and "__pycache__" not in q.parts] + out[nid] = {"kind": "tree", "reference": ref, "files": len(items), + "sha256": hashlib.sha256(json.dumps(items, sort_keys=True).encode()).hexdigest()} + else: + out[nid] = {"kind": "missing", "reference": ref} + return out + + +def check_gate(root, spec, builds): + if builds is None: + return False, {} + hg = load_hard_gate(root) + out = {} + ok = True + comp_ids = [c["id"] for c in spec["proposed_graph_nodes"]] + for stage, (old, new) in builds.items(): + try: + hg.validate_graph_fail_closed(new) + rep_new = hg.closure_report(new) + rep_old = hg.closure_report(old) + old_src, new_src = snapshot(root, old), snapshot(root, new) + if MUT == "snapshot-omitted": + ri = hg.reverse_impact_between(old, new) + else: + ri = hg.reverse_impact_between(old, new, old_sources=old_src, new_sources=new_src) + except Exception: + return False, {} + ok &= ri.get("source_snapshots_supplied") is True and ri.get("promotion_permission") is False + ok &= rep_new.get("gate_ok") is True and not rep_new.get("illegal_controlling") and rep_old.get("gate_ok") is True + ok &= not any(n.get("controlling") for n in new["nodes"].values()) + changed, impacted = set(ri["changed_nodes"]), set(ri["impacted"]) + pre = set(installed_state(old, spec)["present"]) + if stage in ("installed", "installed-simulated"): + ok &= not changed and not impacted # nothing to apply: the proposal is live as declared + else: + ok &= RES in changed and RES in impacted + ok &= all((cid in changed) or (cid not in new["nodes"]) or (cid in pre) for cid in comp_ids) + ok &= WIT not in changed # the deferred transition is not applied + held = {h["node"]: h.get("unsatisfied_required", []) for h in rep_new.get("hold_proposals", [])} + if stage == "interim": + ok &= RES not in held or new["nodes"][RES]["classification"] == "OPEN_ACTIVE" + elif stage == "final-record-unreviewed": + ok &= RES in held and RECORD_NODE in held[RES] # the gate itself holds a residual resting on an unread record + else: + ok &= RES not in held # every required premise PROVED_REVIEWED + # a later source-byte change on any component reaches the residual (and the old node once it depends on it) + wit_depends = any(e["from"] == WIT and e["to"] == RES for e in new["edges"]) + tested = 0 + for cid in comp_ids: + if cid not in new["nodes"]: + continue + drift = copy.deepcopy(new_src) + drift[cid]["sha256"] = "0" * 64 + try: + ri2 = hg.reverse_impact_between(new, new, old_sources=new_src, new_sources=drift) + except Exception: + return False, {} + ok &= set(ri2["changed_nodes"]) == {cid} and RES in ri2["impacted"] + ok &= (not wit_depends) or WIT in ri2["impacted"] + tested += 1 + ok &= tested == sum(1 for cid in comp_ids if cid in new["nodes"]) >= len(comp_ids) - 1 + out[stage] = {"changed_nodes": sorted(changed), "impacted": sorted(impacted), + "residual_classification": new["nodes"][RES]["classification"], + "residual_held": RES in held, "source_snapshots_supplied": True, + "source_drift_reaches_residual": tested, + "old_node_transition": "deferred: presupposes Math-#160 step 3 (aggregate node absent live)"} + return bool(ok), out + + +def check_negatives(src): + rejected = [] + for fault in ("delete", "change", "symlink", "symlink-parent"): + with tempfile.TemporaryDirectory() as tmp: + root = pathlib.Path(tmp) + for path in INVENTORY: + dst = root / path + dst.parent.mkdir(parents=True, exist_ok=True) + shutil.copyfile(src / path, dst) + target = root / SC + if fault == "delete": + target.unlink() + elif fault == "change": + data = bytearray(target.read_bytes()) + data[0] ^= 1 + target.write_bytes(bytes(data)) + elif fault == "symlink": + real = target.with_name("real_" + target.name) + target.rename(real) + os.symlink(real.name, target) + else: + parent = target.parent + real = parent.with_name("real_" + parent.name) + parent.rename(real) + os.symlink(real.name, parent) + rejected.append(not identities_ok(root)) + return all(rejected) + + +def main(): + global MUT + ap = argparse.ArgumentParser() + ap.add_argument("--mutant", choices=MUTANTS) + MUT = ap.parse_args().mutant + root = pathlib.Path(".").resolve() + spec = load_spec(root) + ident = identities_ok(root) + live, live_state = check_live(root, spec) + trans_ok, builds = check_transitions(root, spec) + gate_ok, gate = check_gate(root, spec, builds) + checks = {"IDENTITIES": ident, "VERDICTS": ident and check_verdicts(root), "LIVE": live, + "REVIEWED": ident and check_reviewed(root, spec), "DEDUCTION": check_deduction(), + "TRANSITIONS": trans_ok, "GATE": gate_ok, "NEGATIVES": check_negatives(root)} + passed = all(checks.values()) and len(checks) == 8 + print(json.dumps({"object": "C6-RESIDUAL-CLOSURE-20260930-v1", "checks": checks, "passed": passed, + "inventory_files": len(INVENTORY), "component_nodes": len(spec["proposed_graph_nodes"]), + "live_state": live_state, "gate": gate, + "scope": "identity, verdict-row, live-register (including the installed state), reviewed-text, exact " + "finite bookkeeping of section 3, transition-shape, hard-gate replay with source snapshots in " + "every execution shape, and filesystem-negative checks; the Gaussian limits are the sources' " + "reviewed statements and are not re-proved; nothing is written"}, + indent=2, sort_keys=True)) + return 0 if passed else 1 + + +if __name__ == "__main__": + sys.exit(main())