From 89c3526e4c9fe173f2ec9938377f43e6c21a5f14 Mon Sep 17 00:00:00 2001 From: Claude Date: Fri, 2 Oct 2026 21:32:59 +0000 Subject: [PATCH 1/4] Proof reachability: every frontiers/*/PROOF.md at main 0fda855 (availability only) Continuation of the #163 navigation refresh, picked up in #163 comment 5961771586. Adds docs/integration/2026-10-02-proof-reachability.md: one row per frontiers/*/PROOF.md at the pinned cut 0fda855 (62 rows; 11 already named in PROOF_INDEX.md, 51 reachable from here) with the exact git blob, the introducing pull request and the first-parent integration commit, plus a short record of the #242 -> #243 -> #244 chain with its landing receipts and limits. No verdict, quotation or summary of any review; PROOF_INDEX.md and #163's files are untouched. tools/check_proof_reachability.py (standard library) re-derives every column except the PR column from git at the cut, checks that each PROOF.md appears exactly once, and rejects verdict words in table rows; tests/test_proof_reachability.py adds adverse edits; .github/workflows/proof-reachability.yml runs both in normal and -O modes with full history. Scientific effect: NONE. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01NMeKEismAyeqgdB4sy2NJU --- .github/workflows/proof-reachability.yml | 36 +++++++ .../2026-10-02-proof-reachability.md | 100 ++++++++++++++++++ tests/test_proof_reachability.py | 67 ++++++++++++ tools/check_proof_reachability.py | 98 +++++++++++++++++ 4 files changed, 301 insertions(+) create mode 100644 .github/workflows/proof-reachability.yml create mode 100644 docs/integration/2026-10-02-proof-reachability.md create mode 100644 tests/test_proof_reachability.py create mode 100644 tools/check_proof_reachability.py diff --git a/.github/workflows/proof-reachability.yml b/.github/workflows/proof-reachability.yml new file mode 100644 index 000000000..0119b78fb --- /dev/null +++ b/.github/workflows/proof-reachability.yml @@ -0,0 +1,36 @@ +name: Proof reachability table + +'on': + pull_request: + paths: + - 'docs/integration/2026-10-02-proof-reachability.md' + - 'tools/check_proof_reachability.py' + - 'tests/test_proof_reachability.py' + - '.github/workflows/proof-reachability.yml' + workflow_dispatch: + +permissions: + contents: read + +jobs: + reachability: + runs-on: ubuntu-latest + timeout-minutes: 5 + steps: + - uses: actions/checkout@11d5960a326750d5838078e36cf38b85af677262 + with: + persist-credentials: false + fetch-depth: 0 + - uses: actions/setup-python@a26af69be951a213d495a4c3e4e4022e16d87065 + with: + python-version: '3.11.16' + - name: Re-derive every row from git at the pinned cut, in both interpreter modes + env: + PYTHONDONTWRITEBYTECODE: '1' + run: | + set -euo pipefail + python -B -S tools/check_proof_reachability.py + python -B -O -S tools/check_proof_reachability.py + python -B -S -m unittest -v tests.test_proof_reachability + python -B -O -S -m unittest -v tests.test_proof_reachability + git diff --exit-code diff --git a/docs/integration/2026-10-02-proof-reachability.md b/docs/integration/2026-10-02-proof-reachability.md new file mode 100644 index 000000000..f55d47b9a --- /dev/null +++ b/docs/integration/2026-10-02-proof-reachability.md @@ -0,0 +1,100 @@ +# Proof reachability on `main`: every `frontiers/*/PROOF.md` at one cut + +Cut: `0fda855b8ee0c26d597bb033e0b4cdfb6d07e5e6` (Math- `main`, 2 October 2026; the integration of #246). + +**Scope: source availability only.** This table records where each frontier proof lives at the cut, its exact git blob, the pull request that introduced it, and the first-parent commit on `main` that integrated it. It contains no verdict, grade, summary or quotation of any review. It changes no claim, graph node, STATUS row, register or disposition. A merge, a passing check or a row here is **not** mathematical acceptance. Each packet's own `README.md`, `SOURCES.json` and pull-request conversation carry its status and its review records. + +It continues the navigation refresh of #163, which covers the packets integrated from 26 to 29 September, and it was picked up in #163 comment 5961771586. `PROOF_INDEX.md` is left unchanged; at the cut it names 11 of the 62 proofs below, and the other 51 are reachable from here. + +## How each row is derived + +- **Blob:** `git rev-parse :frontiers//PROOF.md`. +- **Integration commit:** the last line of `git log --first-parent --diff-filter=A -- `, the first-parent commit of `main` that added the path; its committer date is shown. +- **Introduced by:** the pull request that GitHub associates with the commit that first added the path. +- **In `PROOF_INDEX.md`:** whether `PROOF_INDEX.md` at the cut names the packet folder. + +`tools/check_proof_reachability.py` re-derives every column except "Introduced by" from git; that column comes from GitHub's association of commits with pull requests. The checker also verifies that every `frontiers/*/PROOF.md` at the cut appears exactly once, and that no table row carries a verdict word. + +## The table (in order of integration) + +| Packet | `PROOF.md` blob at the cut | Introduced by | Integration commit (date) | In `PROOF_INDEX.md` | +|---|---|---|---|---| +| [`full_price_20260924`](../../frontiers/full_price_20260924/PROOF.md) | `582180e41dca0ad815ad0f18574df42040912149` | [#5](https://github.com/d6g8k5htny-coder/Math-/pull/5) | `a0cd46d22ffe` (2026-09-24) | yes | +| [`price_budget_20260924`](../../frontiers/price_budget_20260924/PROOF.md) | `9b17d179d2408dae9ea497d3c6e5c6538d2c3b8b` | [#4](https://github.com/d6g8k5htny-coder/Math-/pull/4) | `f3a6e5540c21` (2026-09-24) | yes | +| [`remote_window_20260924`](../../frontiers/remote_window_20260924/PROOF.md) | `b383bfcc88ec4ad497dff01fb6640e429ba24a84` | [#6](https://github.com/d6g8k5htny-coder/Math-/pull/6) | `593adcaa89a2` (2026-09-24) | yes | +| [`axial_density_20260925`](../../frontiers/axial_density_20260925/PROOF.md) | `a72418d78fd3c1ec96260dbf19f9a2f3f4ca35ba` | [#21](https://github.com/d6g8k5htny-coder/Math-/pull/21) | `c3cee9bbdeee` (2026-09-25) | yes | +| [`rn_annulus_bridge_20260925`](../../frontiers/rn_annulus_bridge_20260925/PROOF.md) | `6f317515b3d417661f86e2fed09bc7d950899c2b` | [#28](https://github.com/d6g8k5htny-coder/Math-/pull/28) | `f2899d8f4983` (2026-09-25) | yes | +| [`rn_thin_tube_20260925`](../../frontiers/rn_thin_tube_20260925/PROOF.md) | `338d92d1f6be01da01950c853aaecbffa4231c47` | [#22](https://github.com/d6g8k5htny-coder/Math-/pull/22) | `760340e921ac` (2026-09-25) | yes | +| [`rn_mesoscopic_20260925`](../../frontiers/rn_mesoscopic_20260925/PROOF.md) | `0ef068fe7cc17a7c3405536be04a02fc964c2494` | [#7](https://github.com/d6g8k5htny-coder/Math-/pull/7) | `c021278be89b` (2026-09-27) | no | +| [`elder_dimension_lift_20260928`](../../frontiers/elder_dimension_lift_20260928/PROOF.md) | `7303bd791a68a1139251f0f6e403a9f7cc89b006` | [#129](https://github.com/d6g8k5htny-coder/Math-/pull/129) | `e7f8aca41c30` (2026-09-28) | no | +| [`intermediate_window_20260928`](../../frontiers/intermediate_window_20260928/PROOF.md) | `f53a527ce0204fda271f24730b62b4223a5e43ec` | [#107](https://github.com/d6g8k5htny-coder/Math-/pull/107) | `541d4e9daf3f` (2026-09-28) | no | +| [`p15_bipartite_overlap_20260928`](../../frontiers/p15_bipartite_overlap_20260928/PROOF.md) | `8ad826ecb374cc733e3a547bdba0ba63cad10c08` | [#124](https://github.com/d6g8k5htny-coder/Math-/pull/124) | `d39dbbc25c25` (2026-09-28) | no | +| [`p15_tail_load_20260928`](../../frontiers/p15_tail_load_20260928/PROOF.md) | `8187908dfd220cb833b94f82c451ef4c0e45e367` | [#124](https://github.com/d6g8k5htny-coder/Math-/pull/124) | `d39dbbc25c25` (2026-09-28) | no | +| [`remote_collision_20260928`](../../frontiers/remote_collision_20260928/PROOF.md) | `7b48a88e2af54e759e89a8c8219573bb450a65ea` | [#114](https://github.com/d6g8k5htny-coder/Math-/pull/114) | `5a5b97d2c518` (2026-09-28) | yes | +| [`remote_height_decoupling_20260928`](../../frontiers/remote_height_decoupling_20260928/PROOF.md) | `4d7af587db20515955585732d8150d912c89c0e4` | [#124](https://github.com/d6g8k5htny-coder/Math-/pull/124) | `d39dbbc25c25` (2026-09-28) | no | +| [`remote_singleton_law_20260928`](../../frontiers/remote_singleton_law_20260928/PROOF.md) | `2b01956978d7f1d917e929a955f2588263a87426` | [#115](https://github.com/d6g8k5htny-coder/Math-/pull/115) | `4b2aa45b2f99` (2026-09-28) | no | +| [`c6_cluster_law_20260929`](../../frontiers/c6_cluster_law_20260929/PROOF.md) | `ba492c8e62e58bfc055fc8254c790e893d346ba5` | [#159](https://github.com/d6g8k5htny-coder/Math-/pull/159) | `98fdb54954a2` (2026-09-29) | no | +| [`c6_count_cap_boundary_20260929`](../../frontiers/c6_count_cap_boundary_20260929/PROOF.md) | `3d4c28a4ca8784b6c71c13ca804a817a6cb52e6f` | [#146](https://github.com/d6g8k5htny-coder/Math-/pull/146) | `52ed202a094e` (2026-09-29) | no | +| [`c6_factorial_moment_20260929`](../../frontiers/c6_factorial_moment_20260929/PROOF.md) | `f5bd013b7134be9efd246fc9bbb8d18ad5a728bc` | [#140](https://github.com/d6g8k5htny-coder/Math-/pull/140) | `e7d975f446c0` (2026-09-29) | no | +| [`c6_fourier_cutoff_20260929`](../../frontiers/c6_fourier_cutoff_20260929/PROOF.md) | `1d9177a259654df0fb7c558fcb803685e09608d2` | [#148](https://github.com/d6g8k5htny-coder/Math-/pull/148) | `4d062e2a976a` (2026-09-29) | yes | +| [`c6_marked_fourier_20260929`](../../frontiers/c6_marked_fourier_20260929/PROOF.md) | `efb702f601eb0c0a24dad6d125061158158867b9` | [#157](https://github.com/d6g8k5htny-coder/Math-/pull/157) | `2479a7c2bcad` (2026-09-29) | no | +| [`c6_palm_route_20260929`](../../frontiers/c6_palm_route_20260929/PROOF.md) | `89eb8adf08fe7afc2cab9662d3a9875c05ae5cc5` | [#145](https://github.com/d6g8k5htny-coder/Math-/pull/145) | `820d4435c5f1` (2026-09-29) | yes | +| [`c6_rare_cluster_laws_20260929`](../../frontiers/c6_rare_cluster_laws_20260929/PROOF.md) | `2ab625cedfc2e47575c4a7fa4853413418c532da` | [#153](https://github.com/d6g8k5htny-coder/Math-/pull/153) | `190cf2bd4f31` (2026-09-29) | yes | +| [`c6_sharpened_20260929`](../../frontiers/c6_sharpened_20260929/PROOF.md) | `70ba19726a9114bfceae04d021095e6c8eed5026` | [#142](https://github.com/d6g8k5htny-coder/Math-/pull/142) | `bf7c45f5e180` (2026-09-29) | no | +| [`c7_total_bounded_20260929`](../../frontiers/c7_total_bounded_20260929/PROOF.md) | `28748b086ec6761ef467dc67cba475fbdf8b7455` | [#150](https://github.com/d6g8k5htny-coder/Math-/pull/150) | `7f438fca8b7f` (2026-09-29) | no | +| [`c7_zero_gap_limit_20260929`](../../frontiers/c7_zero_gap_limit_20260929/PROOF.md) | `5b6328ea3d6afcbeb731698b3834e536f72d1bcb` | [#155](https://github.com/d6g8k5htny-coder/Math-/pull/155) | `7a1cb09a9d58` (2026-09-29) | no | +| [`cluster_exponential_weight_20260930`](../../frontiers/cluster_exponential_weight_20260930/PROOF.md) | `bf1268b9c18ec05561fd9b14c645ef0b8e530484` | [#164](https://github.com/d6g8k5htny-coder/Math-/pull/164) | `7d0c89a5bb77` (2026-09-29) | no | +| [`d5_dimension_lift_20260929`](../../frontiers/d5_dimension_lift_20260929/PROOF.md) | `9d82c707fdb17d3072a8930f26dabedf59e456fc` | [#141](https://github.com/d6g8k5htny-coder/Math-/pull/141) | `e1ca400b3414` (2026-09-29) | yes | +| [`elder_lower_all_d_20260929`](../../frontiers/elder_lower_all_d_20260929/PROOF.md) | `7f41c9e315be0a7985d4c770a11a2cdf717bd46a` | [#149](https://github.com/d6g8k5htny-coder/Math-/pull/149) | `21244e5ea0b0` (2026-09-29) | no | +| [`local_cluster_tightness_20260929`](../../frontiers/local_cluster_tightness_20260929/PROOF.md) | `adffa6916d0fb57fede0486b5eb3bc6afc127c07` | [#161](https://github.com/d6g8k5htny-coder/Math-/pull/161) | `5c484bfd4b15` (2026-09-29) | no | +| [`planar_cubic_cluster_20260929`](../../frontiers/planar_cubic_cluster_20260929/PROOF.md) | `bb446d08db8a944537a743ad550b88c1c2ad5758` | [#158](https://github.com/d6g8k5htny-coder/Math-/pull/158) | `aa288385af93` (2026-09-29) | no | +| [`remote_inverse_separation_20260928`](../../frontiers/remote_inverse_separation_20260928/PROOF.md) | `1b24d0f6d07f84706a0a8e9b25e111e6eff93a2b` | [#131](https://github.com/d6g8k5htny-coder/Math-/pull/131) | `0b0b281989db` (2026-09-29) | no | +| [`remote_mixed_inverse_20260929`](../../frontiers/remote_mixed_inverse_20260929/PROOF.md) | `975d8211a30be05cb337c81036a0c8de8a9f4264` | [#134](https://github.com/d6g8k5htny-coder/Math-/pull/134) | `5bd924969bb2` (2026-09-29) | no | +| [`sard_g_a2_parameter_20260929`](../../frontiers/sard_g_a2_parameter_20260929/PROOF.md) | `36bbc0c30a451eb8d568717552bb462c0f96685c` | [#139](https://github.com/d6g8k5htny-coder/Math-/pull/139) | `e947ade51def` (2026-09-29) | no | +| [`sard_g_a2_regularity_20260929`](../../frontiers/sard_g_a2_regularity_20260929/PROOF.md) | `8ea2c35375085905986a144c44b522a0b397cee7` | [#139](https://github.com/d6g8k5htny-coder/Math-/pull/139) | `e947ade51def` (2026-09-29) | no | +| [`sard_g_pinned_transfer_20260929`](../../frontiers/sard_g_pinned_transfer_20260929/PROOF.md) | `314e38c6f5f2bd78da79e423f30a341a3d45e22c` | [#139](https://github.com/d6g8k5htny-coder/Math-/pull/139) | `e947ade51def` (2026-09-29) | no | +| [`sard_g_robust_charts_20260929`](../../frontiers/sard_g_robust_charts_20260929/PROOF.md) | `7e2237063a8dd0120e9d5bd15a3caaa32e8495fa` | [#139](https://github.com/d6g8k5htny-coder/Math-/pull/139) | `e947ade51def` (2026-09-29) | no | +| [`side24_periodization_20260929`](../../frontiers/side24_periodization_20260929/PROOF.md) | `1a84f215c53d62918f37517300c350693da62586` | [#144](https://github.com/d6g8k5htny-coder/Math-/pull/144) | `0cd0b821972e` (2026-09-29) | no | +| [`side24_periodization_remainder_20260929`](../../frontiers/side24_periodization_remainder_20260929/PROOF.md) | `0329156897fc59b4bb88ad0228eaaade15f3d687` | [#156](https://github.com/d6g8k5htny-coder/Math-/pull/156) | `8ba851fb2add` (2026-09-29) | no | +| [`spectral_cluster_closure_20260929`](../../frontiers/spectral_cluster_closure_20260929/PROOF.md) | `16c56821b52fd76b0be791622b9c3809eafde75a` | [#162](https://github.com/d6g8k5htny-coder/Math-/pull/162) | `358f2562efbc` (2026-09-29) | no | +| [`unrestricted_selection_difference_20260929`](../../frontiers/unrestricted_selection_difference_20260929/PROOF.md) | `5a55b179a974a90c65d257f3f93765cc6fb30bb8` | [#134](https://github.com/d6g8k5htny-coder/Math-/pull/134) | `5bd924969bb2` (2026-09-29) | no | +| [`extreme_cluster_sampling_20260930`](../../frontiers/extreme_cluster_sampling_20260930/PROOF.md) | `19a6044f2066643b5baab34ce5b6b6efb431e84a` | [#169](https://github.com/d6g8k5htny-coder/Math-/pull/169) | `f430fdecbb1d` (2026-09-30) | no | +| [`fixed_r_inverse_lifetime_20260930`](../../frontiers/fixed_r_inverse_lifetime_20260930/PROOF.md) | `0d4018777d13672c1de1696525512e80b23b7c3c` | [#182](https://github.com/d6g8k5htny-coder/Math-/pull/182) | `2a10ed34e037` (2026-09-30) | no | +| [`lifetime_moment_boundary_20260930`](../../frontiers/lifetime_moment_boundary_20260930/PROOF.md) | `d5ee8abee120a8bec2f6c470e517ff9db4645183` | [#177](https://github.com/d6g8k5htny-coder/Math-/pull/177) | `dda8991f18cb` (2026-09-30) | no | +| [`local_elder_geometry_20260930`](../../frontiers/local_elder_geometry_20260930/PROOF.md) | `ef2aa57959ea9f721bbf2316ce94cf616c1c9113` | [#170](https://github.com/d6g8k5htny-coder/Math-/pull/170) | `fa2e9909d8cc` (2026-09-30) | no | +| [`radial_rate_20260930`](../../frontiers/radial_rate_20260930/PROOF.md) | `65f24b1f9a7b80522a2ee059f5f6877c9f970f0d` | [#176](https://github.com/d6g8k5htny-coder/Math-/pull/176) | `7ca3eb00534d` (2026-09-30) | no | +| [`c2_finite_jet_transfer_20261001`](../../frontiers/c2_finite_jet_transfer_20261001/PROOF.md) | `54cc4a1ae274842bc2c01f9c207549e7b07de7bc` | [#232](https://github.com/d6g8k5htny-coder/Math-/pull/232) | `7fe06b01489a` (2026-10-01) | no | +| [`candidate_third_order_20261001`](../../frontiers/candidate_third_order_20261001/PROOF.md) | `70ca57ef05199e75417d7d57928c1e1c93bf944e` | [#218](https://github.com/d6g8k5htny-coder/Math-/pull/218) | `fb6ee97bc791` (2026-10-01) | no | +| [`concave_fibre_elder_20260930`](../../frontiers/concave_fibre_elder_20260930/PROOF.md) | `923d3236b5291a29bd162937f172190db84dcef5` | [#175](https://github.com/d6g8k5htny-coder/Math-/pull/175) | `eb659bd37d61` (2026-10-01) | no | +| [`cusp_second_order_20261001`](../../frontiers/cusp_second_order_20261001/PROOF.md) | `f6df5a7356a54771b0052e42a864a140709903ad` | [#207](https://github.com/d6g8k5htny-coder/Math-/pull/207) | `566b1a143ec2` (2026-10-01) | no | +| [`elder_partner_extremes_20260930`](../../frontiers/elder_partner_extremes_20260930/PROOF.md) | `91f88e392fb8aa947dac4fc81c2b45f783fa66cd` | [#181](https://github.com/d6g8k5htny-coder/Math-/pull/181) | `443212fb4d84` (2026-10-01) | no | +| [`elder_selected_extremes_20260930`](../../frontiers/elder_selected_extremes_20260930/PROOF.md) | `1310dc11bae684a9889548d1e764e83381b39d57` | [#179](https://github.com/d6g8k5htny-coder/Math-/pull/179) | `6e5f36d7641b` (2026-10-01) | no | +| [`elder_third_order_20261001`](../../frontiers/elder_third_order_20261001/PROOF.md) | `c8767ddecf1041d234f685e95af582073a7be393` | [#220](https://github.com/d6g8k5htny-coder/Math-/pull/220) | `0d797780c2e3` (2026-10-01) | no | +| [`far_elder_rate_20260930`](../../frontiers/far_elder_rate_20260930/PROOF.md) | `072601145601a1021037a2e91bf8826c1c971ecc` | [#187](https://github.com/d6g8k5htny-coder/Math-/pull/187) | `c2f1270d2819` (2026-10-01) | no | +| [`remainder_rate_20260930`](../../frontiers/remainder_rate_20260930/PROOF.md) | `abfb98ae41d66a86d3cb094162db6547d0f29e7e` | [#198](https://github.com/d6g8k5htny-coder/Math-/pull/198) | `124c37d92181` (2026-10-01) | no | +| [`remainder_vanishing_20260930`](../../frontiers/remainder_vanishing_20260930/PROOF.md) | `441152dfc1d8d00cb268cebdb0394212a5bfacdb` | [#191](https://github.com/d6g8k5htny-coder/Math-/pull/191) | `955654747c0e` (2026-10-01) | no | +| [`short_bar_endpoint_law_20261001`](../../frontiers/short_bar_endpoint_law_20261001/PROOF.md) | `0d47dbc1d92863d8c51b918aa47d1fa8b605cfdc` | [#221](https://github.com/d6g8k5htny-coder/Math-/pull/221) | `f166ef52e5ca` (2026-10-01) | no | +| [`third_order_rate_20261001`](../../frontiers/third_order_rate_20261001/PROOF.md) | `110ed33a57902bef11873807e722fde3888b59fb` | [#229](https://github.com/d6g8k5htny-coder/Math-/pull/229) | `6f74f7a77bae` (2026-10-01) | no | +| [`elder_cusp_parity_20261002`](../../frontiers/elder_cusp_parity_20261002/PROOF.md) | `16a1db0658918057ff741df888c13702763d9919` | [#240](https://github.com/d6g8k5htny-coder/Math-/pull/240) | `7636cae5c386` (2026-10-02) | no | +| [`separated_fold_multiplicity_20261002`](../../frontiers/separated_fold_multiplicity_20261002/PROOF.md) | `026cf5237510018d466380683b7679c2de977845` | [#239](https://github.com/d6g8k5htny-coder/Math-/pull/239) | `240a9bfa06af` (2026-10-02) | no | +| [`soft_closed_form_20261002`](../../frontiers/soft_closed_form_20261002/PROOF.md) | `c69f92b1076399fb9f8917bb273e15348b0a497e` | [#244](https://github.com/d6g8k5htny-coder/Math-/pull/244) | `07320089a9c6` (2026-10-02) | no | +| [`soft_fold_limit_20261002`](../../frontiers/soft_fold_limit_20261002/PROOF.md) | `6502cf7ba2edee47761e40308c15b7563b06d1f8` | [#243](https://github.com/d6g8k5htny-coder/Math-/pull/243) | `fa8b0d219e41` (2026-10-02) | no | +| [`soft_rejected_pairs_20261002`](../../frontiers/soft_rejected_pairs_20261002/PROOF.md) | `271412dbc96a29590f5f805258e15c9e335cb430` | [#242](https://github.com/d6g8k5htny-coder/Math-/pull/242) | `54c6759e8434` (2026-10-02) | no | +| [`subpin_collision_20261002`](../../frontiers/subpin_collision_20261002/PROOF.md) | `4d903d0f834fb2077257104cd91822fe253dde8d` | [#245](https://github.com/d6g8k5htny-coder/Math-/pull/245) | `2d8616ef1b45` (2026-10-02) | no | + +Some integration commits brought several packets at once: `d39dbbc` (#124, three packets), `5bd9249` (#134, two packets) and `e947ade` (#139, four packets). + +## The soft fold-scale chain #242 → #243 → #244 (integrated 2 October) + +| Packet | PR | Integration commit | `PROOF.md` blob | Landing receipt on main#229 | +|---|---|---|---|---| +| `soft_rejected_pairs_20261002` | #242 | `54c6759e8434` | `271412dbc96a` | 5959229499 | +| `soft_fold_limit_20261002` | #243 | `fa8b0d219e41` | `6502cf7ba2ed` | 5959530308 | +| `soft_closed_form_20261002` | #244 | `07320089a9c6` | `c69f92b10763` | 5959837508 | + +Limits, stated so that the chain is not over-read: +- **What they concern.** The three packets concern the soft fold-scale model of #242: its rejected set, its fold-scale limit, and its closed form. +- **What they do not establish.** They do not establish the finite-`r` transfer of the model decision to the actual field, which Conjecture 7 needs. +- **Later model-level work.** It lives in issue comments on main#229, not in repository sources, so it is not indexed here. This includes the signed elder margin (5959038812, amended in 5961281898), exact-pin decision stability (5961415030), and the signed-coordinate and level-band bounds (5957815904, 5959878294, 5959920397). +- **Where the status lives.** Review records and status are in each PR's conversation and disposition block. + diff --git a/tests/test_proof_reachability.py b/tests/test_proof_reachability.py new file mode 100644 index 000000000..b4d9061f3 --- /dev/null +++ b/tests/test_proof_reachability.py @@ -0,0 +1,67 @@ +"""Tests for tools/check_proof_reachability.py: the real document passes, and adverse edits fail.""" +import pathlib +import sys +import unittest + +ROOT = pathlib.Path(__file__).resolve().parents[1] +sys.path.insert(0, str(ROOT / 'tools')) +import check_proof_reachability as cpr # noqa: E402 + +DOC = ROOT / 'docs' / 'integration' / '2026-10-02-proof-reachability.md' + + +class RealDocument(unittest.TestCase): + def setUp(self): + self.text = DOC.read_text(encoding='utf-8') + + def test_document_passes(self): + self.assertEqual(cpr.check(self.text), []) + + def test_every_row_parses(self): + cut, rows, lines = cpr.parse(self.text) + self.assertIsNotNone(cut) + self.assertTrue(rows) + self.assertFalse([r for r in rows if 'malformed' in r]) + + +class AdverseEdits(unittest.TestCase): + def setUp(self): + self.text = DOC.read_text(encoding='utf-8') + self.cut, self.rows, self.lines = cpr.parse(self.text) + self.first = self.lines[0] + + def _fails(self, text): + return cpr.check(text) + + def test_wrong_blob_fails(self): + r = self.rows[0] + bad = self.first.replace(r['blob'], ('0' if r['blob'][0] != '0' else '1') + r['blob'][1:]) + self.assertTrue(self._fails(self.text.replace(self.first, bad))) + + def test_dropped_row_fails(self): + self.assertTrue(self._fails(self.text.replace(self.first + '\n', ''))) + + def test_duplicated_row_fails(self): + self.assertTrue(self._fails(self.text.replace(self.first + '\n', self.first + '\n' + self.first + '\n'))) + + def test_wrong_integration_commit_fails(self): + r = self.rows[0] + other = self.rows[-1]['commit'] + self.assertNotEqual(other, r['commit']) + self.assertTrue(self._fails(self.text.replace(self.first, self.first.replace(r['commit'], other)))) + + def test_flipped_index_column_fails(self): + r = self.rows[0] + flipped = self.first[: -len('| %s |' % r['linked'])] + '| %s |' % ('no' if r['linked'] == 'yes' else 'yes') + self.assertTrue(self._fails(self.text.replace(self.first, flipped))) + + def test_verdict_word_fails(self): + self.assertTrue(cpr.verdict_words([self.first + ' ACCEPT'])) + self.assertEqual(cpr.verdict_words([self.first]), []) + + def test_missing_cut_fails(self): + self.assertEqual(cpr.check(self.text.replace('Cut: `', 'Cutoff: `')), ['no cut commit line']) + + +if __name__ == '__main__': + unittest.main() diff --git a/tools/check_proof_reachability.py b/tools/check_proof_reachability.py new file mode 100644 index 000000000..bf87646b0 --- /dev/null +++ b/tools/check_proof_reachability.py @@ -0,0 +1,98 @@ +#!/usr/bin/env python3 +"""Check docs/integration/2026-10-02-proof-reachability.md against git (standard library only). + +The document pins a cut commit. For that cut, every row of its reachability table must name a +frontiers//PROOF.md that exists there, with its exact git blob; the stated integration commit +must be the first-parent commit of the cut's history that added the path; the "linked" column must +agree with PROOF_INDEX.md at the cut; every frontiers/*/PROOF.md at the cut must appear exactly once; +and the table must carry no verdict words. Availability only: nothing here reads or grades a proof. + +Usage: python3 -B -S tools/check_proof_reachability.py [document] (exit 0 iff every check passes) +""" +import re +import subprocess +import sys + +DOC = 'docs/integration/2026-10-02-proof-reachability.md' +CUT_RE = re.compile(r'^Cut: `([0-9a-f]{40})`', re.M) +ROW_RE = re.compile( + r'^\| \[`(?P[A-Za-z0-9_]+)`\]\(\.\./\.\./frontiers/(?P=folder)/PROOF\.md\) ' + r'\| `(?P[0-9a-f]{40})` ' + r'\| \[#(?P\d+)\]\(https://github\.com/d6g8k5htny-coder/Math-/pull/(?P=pr)\) ' + r'\| `(?P[0-9a-f]{12})` \((?P\d{4}-\d{2}-\d{2})\) ' + r'\| (?Pyes|no) \|$') +VERDICT_WORDS = ('ACCEPT', 'AMEND', 'HOLD', 'CONFIRMED', 'VERIFIED', 'PASS', 'REJECT', 'APPROVED', 'FAIL') + + +def git(*args): + return subprocess.run(['git', *args], capture_output=True, text=True, check=True).stdout.strip() + + +def parse(text): + """Return (cut, rows, table_lines) from the document text.""" + m = CUT_RE.search(text) + cut = m.group(1) if m else None + rows, table_lines = [], [] + for line in text.splitlines(): + if line.startswith('| [`'): + table_lines.append(line) + mm = ROW_RE.match(line) + rows.append(mm.groupdict() if mm else {'malformed': line}) + return cut, rows, table_lines + + +def verdict_words(lines): + bad = [] + for line in lines: + for w in VERDICT_WORDS: + if re.search(r'\b' + w + r'\b', line, flags=re.I): + bad.append((w, line[:80])) + return bad + + +def check(text): + failures = [] + cut, rows, table_lines = parse(text) + if cut is None: + return ['no cut commit line'] + for w, line in verdict_words(table_lines): + failures.append('verdict word %s in table row: %s' % (w, line)) + paths = sorted(p for p in git('ls-tree', '-r', '--name-only', cut).splitlines() + if re.fullmatch(r'frontiers/[^/]+/PROOF\.md', p)) + index = git('show', cut + ':PROOF_INDEX.md') + seen = {} + for r in rows: + if 'malformed' in r: + failures.append('malformed row: ' + r['malformed'][:100]) + continue + path = 'frontiers/%s/PROOF.md' % r['folder'] + seen[path] = seen.get(path, 0) + 1 + if path not in paths: + failures.append('not a PROOF.md at the cut: ' + path) + continue + if git('rev-parse', cut + ':' + path) != r['blob']: + failures.append('blob mismatch: ' + path) + added = git('log', cut, '--first-parent', '--diff-filter=A', '--format=%H %cs', '--', path).splitlines() + if not added or not added[-1].startswith(r['commit']) or added[-1].split()[1] != r['date']: + failures.append('integration commit/date mismatch: %s (%s)' % (path, added[-1] if added else 'none')) + linked = ('frontiers/%s/' % r['folder']) in index or r['folder'] in index + if (r['linked'] == 'yes') != linked: + failures.append('PROOF_INDEX linkage mismatch: ' + path) + for p in paths: + if seen.get(p, 0) != 1: + failures.append('appears %d times: %s' % (seen.get(p, 0), p)) + return failures + + +def main(argv): + doc = argv[1] if len(argv) > 1 else DOC + with open(doc, encoding='utf-8') as fh: + failures = check(fh.read()) + for f in failures: + print('FAIL', f) + print('proof-reachability: %s' % ('OK' if not failures else '%d failure(s)' % len(failures))) + return 0 if not failures else 1 + + +if __name__ == '__main__': + sys.exit(main(sys.argv)) From ee087cea7cfa932daf0122aaee8227d1dfbadef4 Mon Sep 17 00:00:00 2001 From: Claude Date: Sat, 3 Oct 2026 13:00:29 +0000 Subject: [PATCH 2/4] #247 v1.1: first-parent integration order; verdict-word scan of both tables Applies the two findings of the Codex review on 89c3526 (r4170055081, r4170055086), as requested in #247 comment 5965742888. The pinned cut 0fda855 and the availability-only scope are unchanged; every row keeps its exact bytes. 1. Order (r4170055081). The 62 inventory rows were sorted by date and folder name, not by integration. They are now ordered by the position of the integration commit in `git rev-list --first-parent --reverse `, with packets that share an integration commit listed alphabetically. The checker re-derives the positions and rejects any out-of-order pair; the original document now fails with 21 order violations. 2. Verdict words (r4170055086). The scan covered only rows beginning with "| [`", so the chain table was never read. It now covers every line of both tables (headers included). The checker also cross-checks the chain table's PR number and commit/blob prefixes against the inventory. Tests: 19 (was 7), including a swapped pair with different commits, a swapped pair sharing a commit, the reversed last four rows, every verdict word in each table in both cases, a header verdict, and wrong chain-table blob, commit and PR. Cut-pinned git queries are cached, so the full gate runs in about 5 s. Scientific effect: NONE. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01NMeKEismAyeqgdB4sy2NJU --- .../2026-10-02-proof-reachability.md | 66 +++++++-------- tests/test_proof_reachability.py | 81 +++++++++++++++++++ tools/check_proof_reachability.py | 54 +++++++++++-- 3 files changed, 164 insertions(+), 37 deletions(-) diff --git a/docs/integration/2026-10-02-proof-reachability.md b/docs/integration/2026-10-02-proof-reachability.md index f55d47b9a..d977d14ce 100644 --- a/docs/integration/2026-10-02-proof-reachability.md +++ b/docs/integration/2026-10-02-proof-reachability.md @@ -13,74 +13,76 @@ It continues the navigation refresh of #163, which covers the packets integrated - **Introduced by:** the pull request that GitHub associates with the commit that first added the path. - **In `PROOF_INDEX.md`:** whether `PROOF_INDEX.md` at the cut names the packet folder. -`tools/check_proof_reachability.py` re-derives every column except "Introduced by" from git; that column comes from GitHub's association of commits with pull requests. The checker also verifies that every `frontiers/*/PROOF.md` at the cut appears exactly once, and that no table row carries a verdict word. +`tools/check_proof_reachability.py` re-derives every column except "Introduced by" from git; that column comes from GitHub's association of commits with pull requests. The checker also verifies that every `frontiers/*/PROOF.md` at the cut appears exactly once; that the rows follow the integration order below; that the commit and blob prefixes in the second table agree with the first; and that no row of either table carries a verdict word. ## The table (in order of integration) +Rows are ordered by the position of their integration commit in `git rev-list --first-parent --reverse `, the order in which `main` received them. Packets integrated by the same commit are listed alphabetically. A committer date can be earlier than a date in an earlier row; the position, not the date, sets the order. + | Packet | `PROOF.md` blob at the cut | Introduced by | Integration commit (date) | In `PROOF_INDEX.md` | |---|---|---|---|---| -| [`full_price_20260924`](../../frontiers/full_price_20260924/PROOF.md) | `582180e41dca0ad815ad0f18574df42040912149` | [#5](https://github.com/d6g8k5htny-coder/Math-/pull/5) | `a0cd46d22ffe` (2026-09-24) | yes | | [`price_budget_20260924`](../../frontiers/price_budget_20260924/PROOF.md) | `9b17d179d2408dae9ea497d3c6e5c6538d2c3b8b` | [#4](https://github.com/d6g8k5htny-coder/Math-/pull/4) | `f3a6e5540c21` (2026-09-24) | yes | +| [`full_price_20260924`](../../frontiers/full_price_20260924/PROOF.md) | `582180e41dca0ad815ad0f18574df42040912149` | [#5](https://github.com/d6g8k5htny-coder/Math-/pull/5) | `a0cd46d22ffe` (2026-09-24) | yes | | [`remote_window_20260924`](../../frontiers/remote_window_20260924/PROOF.md) | `b383bfcc88ec4ad497dff01fb6640e429ba24a84` | [#6](https://github.com/d6g8k5htny-coder/Math-/pull/6) | `593adcaa89a2` (2026-09-24) | yes | | [`axial_density_20260925`](../../frontiers/axial_density_20260925/PROOF.md) | `a72418d78fd3c1ec96260dbf19f9a2f3f4ca35ba` | [#21](https://github.com/d6g8k5htny-coder/Math-/pull/21) | `c3cee9bbdeee` (2026-09-25) | yes | | [`rn_annulus_bridge_20260925`](../../frontiers/rn_annulus_bridge_20260925/PROOF.md) | `6f317515b3d417661f86e2fed09bc7d950899c2b` | [#28](https://github.com/d6g8k5htny-coder/Math-/pull/28) | `f2899d8f4983` (2026-09-25) | yes | | [`rn_thin_tube_20260925`](../../frontiers/rn_thin_tube_20260925/PROOF.md) | `338d92d1f6be01da01950c853aaecbffa4231c47` | [#22](https://github.com/d6g8k5htny-coder/Math-/pull/22) | `760340e921ac` (2026-09-25) | yes | | [`rn_mesoscopic_20260925`](../../frontiers/rn_mesoscopic_20260925/PROOF.md) | `0ef068fe7cc17a7c3405536be04a02fc964c2494` | [#7](https://github.com/d6g8k5htny-coder/Math-/pull/7) | `c021278be89b` (2026-09-27) | no | -| [`elder_dimension_lift_20260928`](../../frontiers/elder_dimension_lift_20260928/PROOF.md) | `7303bd791a68a1139251f0f6e403a9f7cc89b006` | [#129](https://github.com/d6g8k5htny-coder/Math-/pull/129) | `e7f8aca41c30` (2026-09-28) | no | | [`intermediate_window_20260928`](../../frontiers/intermediate_window_20260928/PROOF.md) | `f53a527ce0204fda271f24730b62b4223a5e43ec` | [#107](https://github.com/d6g8k5htny-coder/Math-/pull/107) | `541d4e9daf3f` (2026-09-28) | no | +| [`remote_collision_20260928`](../../frontiers/remote_collision_20260928/PROOF.md) | `7b48a88e2af54e759e89a8c8219573bb450a65ea` | [#114](https://github.com/d6g8k5htny-coder/Math-/pull/114) | `5a5b97d2c518` (2026-09-28) | yes | +| [`remote_singleton_law_20260928`](../../frontiers/remote_singleton_law_20260928/PROOF.md) | `2b01956978d7f1d917e929a955f2588263a87426` | [#115](https://github.com/d6g8k5htny-coder/Math-/pull/115) | `4b2aa45b2f99` (2026-09-28) | no | | [`p15_bipartite_overlap_20260928`](../../frontiers/p15_bipartite_overlap_20260928/PROOF.md) | `8ad826ecb374cc733e3a547bdba0ba63cad10c08` | [#124](https://github.com/d6g8k5htny-coder/Math-/pull/124) | `d39dbbc25c25` (2026-09-28) | no | | [`p15_tail_load_20260928`](../../frontiers/p15_tail_load_20260928/PROOF.md) | `8187908dfd220cb833b94f82c451ef4c0e45e367` | [#124](https://github.com/d6g8k5htny-coder/Math-/pull/124) | `d39dbbc25c25` (2026-09-28) | no | -| [`remote_collision_20260928`](../../frontiers/remote_collision_20260928/PROOF.md) | `7b48a88e2af54e759e89a8c8219573bb450a65ea` | [#114](https://github.com/d6g8k5htny-coder/Math-/pull/114) | `5a5b97d2c518` (2026-09-28) | yes | | [`remote_height_decoupling_20260928`](../../frontiers/remote_height_decoupling_20260928/PROOF.md) | `4d7af587db20515955585732d8150d912c89c0e4` | [#124](https://github.com/d6g8k5htny-coder/Math-/pull/124) | `d39dbbc25c25` (2026-09-28) | no | -| [`remote_singleton_law_20260928`](../../frontiers/remote_singleton_law_20260928/PROOF.md) | `2b01956978d7f1d917e929a955f2588263a87426` | [#115](https://github.com/d6g8k5htny-coder/Math-/pull/115) | `4b2aa45b2f99` (2026-09-28) | no | -| [`c6_cluster_law_20260929`](../../frontiers/c6_cluster_law_20260929/PROOF.md) | `ba492c8e62e58bfc055fc8254c790e893d346ba5` | [#159](https://github.com/d6g8k5htny-coder/Math-/pull/159) | `98fdb54954a2` (2026-09-29) | no | -| [`c6_count_cap_boundary_20260929`](../../frontiers/c6_count_cap_boundary_20260929/PROOF.md) | `3d4c28a4ca8784b6c71c13ca804a817a6cb52e6f` | [#146](https://github.com/d6g8k5htny-coder/Math-/pull/146) | `52ed202a094e` (2026-09-29) | no | -| [`c6_factorial_moment_20260929`](../../frontiers/c6_factorial_moment_20260929/PROOF.md) | `f5bd013b7134be9efd246fc9bbb8d18ad5a728bc` | [#140](https://github.com/d6g8k5htny-coder/Math-/pull/140) | `e7d975f446c0` (2026-09-29) | no | -| [`c6_fourier_cutoff_20260929`](../../frontiers/c6_fourier_cutoff_20260929/PROOF.md) | `1d9177a259654df0fb7c558fcb803685e09608d2` | [#148](https://github.com/d6g8k5htny-coder/Math-/pull/148) | `4d062e2a976a` (2026-09-29) | yes | -| [`c6_marked_fourier_20260929`](../../frontiers/c6_marked_fourier_20260929/PROOF.md) | `efb702f601eb0c0a24dad6d125061158158867b9` | [#157](https://github.com/d6g8k5htny-coder/Math-/pull/157) | `2479a7c2bcad` (2026-09-29) | no | -| [`c6_palm_route_20260929`](../../frontiers/c6_palm_route_20260929/PROOF.md) | `89eb8adf08fe7afc2cab9662d3a9875c05ae5cc5` | [#145](https://github.com/d6g8k5htny-coder/Math-/pull/145) | `820d4435c5f1` (2026-09-29) | yes | -| [`c6_rare_cluster_laws_20260929`](../../frontiers/c6_rare_cluster_laws_20260929/PROOF.md) | `2ab625cedfc2e47575c4a7fa4853413418c532da` | [#153](https://github.com/d6g8k5htny-coder/Math-/pull/153) | `190cf2bd4f31` (2026-09-29) | yes | -| [`c6_sharpened_20260929`](../../frontiers/c6_sharpened_20260929/PROOF.md) | `70ba19726a9114bfceae04d021095e6c8eed5026` | [#142](https://github.com/d6g8k5htny-coder/Math-/pull/142) | `bf7c45f5e180` (2026-09-29) | no | -| [`c7_total_bounded_20260929`](../../frontiers/c7_total_bounded_20260929/PROOF.md) | `28748b086ec6761ef467dc67cba475fbdf8b7455` | [#150](https://github.com/d6g8k5htny-coder/Math-/pull/150) | `7f438fca8b7f` (2026-09-29) | no | -| [`c7_zero_gap_limit_20260929`](../../frontiers/c7_zero_gap_limit_20260929/PROOF.md) | `5b6328ea3d6afcbeb731698b3834e536f72d1bcb` | [#155](https://github.com/d6g8k5htny-coder/Math-/pull/155) | `7a1cb09a9d58` (2026-09-29) | no | -| [`cluster_exponential_weight_20260930`](../../frontiers/cluster_exponential_weight_20260930/PROOF.md) | `bf1268b9c18ec05561fd9b14c645ef0b8e530484` | [#164](https://github.com/d6g8k5htny-coder/Math-/pull/164) | `7d0c89a5bb77` (2026-09-29) | no | -| [`d5_dimension_lift_20260929`](../../frontiers/d5_dimension_lift_20260929/PROOF.md) | `9d82c707fdb17d3072a8930f26dabedf59e456fc` | [#141](https://github.com/d6g8k5htny-coder/Math-/pull/141) | `e1ca400b3414` (2026-09-29) | yes | -| [`elder_lower_all_d_20260929`](../../frontiers/elder_lower_all_d_20260929/PROOF.md) | `7f41c9e315be0a7985d4c770a11a2cdf717bd46a` | [#149](https://github.com/d6g8k5htny-coder/Math-/pull/149) | `21244e5ea0b0` (2026-09-29) | no | -| [`local_cluster_tightness_20260929`](../../frontiers/local_cluster_tightness_20260929/PROOF.md) | `adffa6916d0fb57fede0486b5eb3bc6afc127c07` | [#161](https://github.com/d6g8k5htny-coder/Math-/pull/161) | `5c484bfd4b15` (2026-09-29) | no | -| [`planar_cubic_cluster_20260929`](../../frontiers/planar_cubic_cluster_20260929/PROOF.md) | `bb446d08db8a944537a743ad550b88c1c2ad5758` | [#158](https://github.com/d6g8k5htny-coder/Math-/pull/158) | `aa288385af93` (2026-09-29) | no | +| [`elder_dimension_lift_20260928`](../../frontiers/elder_dimension_lift_20260928/PROOF.md) | `7303bd791a68a1139251f0f6e403a9f7cc89b006` | [#129](https://github.com/d6g8k5htny-coder/Math-/pull/129) | `e7f8aca41c30` (2026-09-28) | no | | [`remote_inverse_separation_20260928`](../../frontiers/remote_inverse_separation_20260928/PROOF.md) | `1b24d0f6d07f84706a0a8e9b25e111e6eff93a2b` | [#131](https://github.com/d6g8k5htny-coder/Math-/pull/131) | `0b0b281989db` (2026-09-29) | no | | [`remote_mixed_inverse_20260929`](../../frontiers/remote_mixed_inverse_20260929/PROOF.md) | `975d8211a30be05cb337c81036a0c8de8a9f4264` | [#134](https://github.com/d6g8k5htny-coder/Math-/pull/134) | `5bd924969bb2` (2026-09-29) | no | +| [`unrestricted_selection_difference_20260929`](../../frontiers/unrestricted_selection_difference_20260929/PROOF.md) | `5a55b179a974a90c65d257f3f93765cc6fb30bb8` | [#134](https://github.com/d6g8k5htny-coder/Math-/pull/134) | `5bd924969bb2` (2026-09-29) | no | | [`sard_g_a2_parameter_20260929`](../../frontiers/sard_g_a2_parameter_20260929/PROOF.md) | `36bbc0c30a451eb8d568717552bb462c0f96685c` | [#139](https://github.com/d6g8k5htny-coder/Math-/pull/139) | `e947ade51def` (2026-09-29) | no | | [`sard_g_a2_regularity_20260929`](../../frontiers/sard_g_a2_regularity_20260929/PROOF.md) | `8ea2c35375085905986a144c44b522a0b397cee7` | [#139](https://github.com/d6g8k5htny-coder/Math-/pull/139) | `e947ade51def` (2026-09-29) | no | | [`sard_g_pinned_transfer_20260929`](../../frontiers/sard_g_pinned_transfer_20260929/PROOF.md) | `314e38c6f5f2bd78da79e423f30a341a3d45e22c` | [#139](https://github.com/d6g8k5htny-coder/Math-/pull/139) | `e947ade51def` (2026-09-29) | no | | [`sard_g_robust_charts_20260929`](../../frontiers/sard_g_robust_charts_20260929/PROOF.md) | `7e2237063a8dd0120e9d5bd15a3caaa32e8495fa` | [#139](https://github.com/d6g8k5htny-coder/Math-/pull/139) | `e947ade51def` (2026-09-29) | no | +| [`c6_factorial_moment_20260929`](../../frontiers/c6_factorial_moment_20260929/PROOF.md) | `f5bd013b7134be9efd246fc9bbb8d18ad5a728bc` | [#140](https://github.com/d6g8k5htny-coder/Math-/pull/140) | `e7d975f446c0` (2026-09-29) | no | +| [`c6_sharpened_20260929`](../../frontiers/c6_sharpened_20260929/PROOF.md) | `70ba19726a9114bfceae04d021095e6c8eed5026` | [#142](https://github.com/d6g8k5htny-coder/Math-/pull/142) | `bf7c45f5e180` (2026-09-29) | no | +| [`c6_count_cap_boundary_20260929`](../../frontiers/c6_count_cap_boundary_20260929/PROOF.md) | `3d4c28a4ca8784b6c71c13ca804a817a6cb52e6f` | [#146](https://github.com/d6g8k5htny-coder/Math-/pull/146) | `52ed202a094e` (2026-09-29) | no | +| [`c6_fourier_cutoff_20260929`](../../frontiers/c6_fourier_cutoff_20260929/PROOF.md) | `1d9177a259654df0fb7c558fcb803685e09608d2` | [#148](https://github.com/d6g8k5htny-coder/Math-/pull/148) | `4d062e2a976a` (2026-09-29) | yes | +| [`d5_dimension_lift_20260929`](../../frontiers/d5_dimension_lift_20260929/PROOF.md) | `9d82c707fdb17d3072a8930f26dabedf59e456fc` | [#141](https://github.com/d6g8k5htny-coder/Math-/pull/141) | `e1ca400b3414` (2026-09-29) | yes | +| [`c6_palm_route_20260929`](../../frontiers/c6_palm_route_20260929/PROOF.md) | `89eb8adf08fe7afc2cab9662d3a9875c05ae5cc5` | [#145](https://github.com/d6g8k5htny-coder/Math-/pull/145) | `820d4435c5f1` (2026-09-29) | yes | +| [`elder_lower_all_d_20260929`](../../frontiers/elder_lower_all_d_20260929/PROOF.md) | `7f41c9e315be0a7985d4c770a11a2cdf717bd46a` | [#149](https://github.com/d6g8k5htny-coder/Math-/pull/149) | `21244e5ea0b0` (2026-09-29) | no | +| [`c7_total_bounded_20260929`](../../frontiers/c7_total_bounded_20260929/PROOF.md) | `28748b086ec6761ef467dc67cba475fbdf8b7455` | [#150](https://github.com/d6g8k5htny-coder/Math-/pull/150) | `7f438fca8b7f` (2026-09-29) | no | | [`side24_periodization_20260929`](../../frontiers/side24_periodization_20260929/PROOF.md) | `1a84f215c53d62918f37517300c350693da62586` | [#144](https://github.com/d6g8k5htny-coder/Math-/pull/144) | `0cd0b821972e` (2026-09-29) | no | +| [`c6_rare_cluster_laws_20260929`](../../frontiers/c6_rare_cluster_laws_20260929/PROOF.md) | `2ab625cedfc2e47575c4a7fa4853413418c532da` | [#153](https://github.com/d6g8k5htny-coder/Math-/pull/153) | `190cf2bd4f31` (2026-09-29) | yes | | [`side24_periodization_remainder_20260929`](../../frontiers/side24_periodization_remainder_20260929/PROOF.md) | `0329156897fc59b4bb88ad0228eaaade15f3d687` | [#156](https://github.com/d6g8k5htny-coder/Math-/pull/156) | `8ba851fb2add` (2026-09-29) | no | +| [`c7_zero_gap_limit_20260929`](../../frontiers/c7_zero_gap_limit_20260929/PROOF.md) | `5b6328ea3d6afcbeb731698b3834e536f72d1bcb` | [#155](https://github.com/d6g8k5htny-coder/Math-/pull/155) | `7a1cb09a9d58` (2026-09-29) | no | +| [`local_cluster_tightness_20260929`](../../frontiers/local_cluster_tightness_20260929/PROOF.md) | `adffa6916d0fb57fede0486b5eb3bc6afc127c07` | [#161](https://github.com/d6g8k5htny-coder/Math-/pull/161) | `5c484bfd4b15` (2026-09-29) | no | +| [`planar_cubic_cluster_20260929`](../../frontiers/planar_cubic_cluster_20260929/PROOF.md) | `bb446d08db8a944537a743ad550b88c1c2ad5758` | [#158](https://github.com/d6g8k5htny-coder/Math-/pull/158) | `aa288385af93` (2026-09-29) | no | +| [`c6_marked_fourier_20260929`](../../frontiers/c6_marked_fourier_20260929/PROOF.md) | `efb702f601eb0c0a24dad6d125061158158867b9` | [#157](https://github.com/d6g8k5htny-coder/Math-/pull/157) | `2479a7c2bcad` (2026-09-29) | no | +| [`c6_cluster_law_20260929`](../../frontiers/c6_cluster_law_20260929/PROOF.md) | `ba492c8e62e58bfc055fc8254c790e893d346ba5` | [#159](https://github.com/d6g8k5htny-coder/Math-/pull/159) | `98fdb54954a2` (2026-09-29) | no | +| [`cluster_exponential_weight_20260930`](../../frontiers/cluster_exponential_weight_20260930/PROOF.md) | `bf1268b9c18ec05561fd9b14c645ef0b8e530484` | [#164](https://github.com/d6g8k5htny-coder/Math-/pull/164) | `7d0c89a5bb77` (2026-09-29) | no | | [`spectral_cluster_closure_20260929`](../../frontiers/spectral_cluster_closure_20260929/PROOF.md) | `16c56821b52fd76b0be791622b9c3809eafde75a` | [#162](https://github.com/d6g8k5htny-coder/Math-/pull/162) | `358f2562efbc` (2026-09-29) | no | -| [`unrestricted_selection_difference_20260929`](../../frontiers/unrestricted_selection_difference_20260929/PROOF.md) | `5a55b179a974a90c65d257f3f93765cc6fb30bb8` | [#134](https://github.com/d6g8k5htny-coder/Math-/pull/134) | `5bd924969bb2` (2026-09-29) | no | +| [`lifetime_moment_boundary_20260930`](../../frontiers/lifetime_moment_boundary_20260930/PROOF.md) | `d5ee8abee120a8bec2f6c470e517ff9db4645183` | [#177](https://github.com/d6g8k5htny-coder/Math-/pull/177) | `dda8991f18cb` (2026-09-30) | no | +| [`radial_rate_20260930`](../../frontiers/radial_rate_20260930/PROOF.md) | `65f24b1f9a7b80522a2ee059f5f6877c9f970f0d` | [#176](https://github.com/d6g8k5htny-coder/Math-/pull/176) | `7ca3eb00534d` (2026-09-30) | no | | [`extreme_cluster_sampling_20260930`](../../frontiers/extreme_cluster_sampling_20260930/PROOF.md) | `19a6044f2066643b5baab34ce5b6b6efb431e84a` | [#169](https://github.com/d6g8k5htny-coder/Math-/pull/169) | `f430fdecbb1d` (2026-09-30) | no | | [`fixed_r_inverse_lifetime_20260930`](../../frontiers/fixed_r_inverse_lifetime_20260930/PROOF.md) | `0d4018777d13672c1de1696525512e80b23b7c3c` | [#182](https://github.com/d6g8k5htny-coder/Math-/pull/182) | `2a10ed34e037` (2026-09-30) | no | -| [`lifetime_moment_boundary_20260930`](../../frontiers/lifetime_moment_boundary_20260930/PROOF.md) | `d5ee8abee120a8bec2f6c470e517ff9db4645183` | [#177](https://github.com/d6g8k5htny-coder/Math-/pull/177) | `dda8991f18cb` (2026-09-30) | no | | [`local_elder_geometry_20260930`](../../frontiers/local_elder_geometry_20260930/PROOF.md) | `ef2aa57959ea9f721bbf2316ce94cf616c1c9113` | [#170](https://github.com/d6g8k5htny-coder/Math-/pull/170) | `fa2e9909d8cc` (2026-09-30) | no | -| [`radial_rate_20260930`](../../frontiers/radial_rate_20260930/PROOF.md) | `65f24b1f9a7b80522a2ee059f5f6877c9f970f0d` | [#176](https://github.com/d6g8k5htny-coder/Math-/pull/176) | `7ca3eb00534d` (2026-09-30) | no | -| [`c2_finite_jet_transfer_20261001`](../../frontiers/c2_finite_jet_transfer_20261001/PROOF.md) | `54cc4a1ae274842bc2c01f9c207549e7b07de7bc` | [#232](https://github.com/d6g8k5htny-coder/Math-/pull/232) | `7fe06b01489a` (2026-10-01) | no | -| [`candidate_third_order_20261001`](../../frontiers/candidate_third_order_20261001/PROOF.md) | `70ca57ef05199e75417d7d57928c1e1c93bf944e` | [#218](https://github.com/d6g8k5htny-coder/Math-/pull/218) | `fb6ee97bc791` (2026-10-01) | no | | [`concave_fibre_elder_20260930`](../../frontiers/concave_fibre_elder_20260930/PROOF.md) | `923d3236b5291a29bd162937f172190db84dcef5` | [#175](https://github.com/d6g8k5htny-coder/Math-/pull/175) | `eb659bd37d61` (2026-10-01) | no | -| [`cusp_second_order_20261001`](../../frontiers/cusp_second_order_20261001/PROOF.md) | `f6df5a7356a54771b0052e42a864a140709903ad` | [#207](https://github.com/d6g8k5htny-coder/Math-/pull/207) | `566b1a143ec2` (2026-10-01) | no | | [`elder_partner_extremes_20260930`](../../frontiers/elder_partner_extremes_20260930/PROOF.md) | `91f88e392fb8aa947dac4fc81c2b45f783fa66cd` | [#181](https://github.com/d6g8k5htny-coder/Math-/pull/181) | `443212fb4d84` (2026-10-01) | no | +| [`remainder_vanishing_20260930`](../../frontiers/remainder_vanishing_20260930/PROOF.md) | `441152dfc1d8d00cb268cebdb0394212a5bfacdb` | [#191](https://github.com/d6g8k5htny-coder/Math-/pull/191) | `955654747c0e` (2026-10-01) | no | | [`elder_selected_extremes_20260930`](../../frontiers/elder_selected_extremes_20260930/PROOF.md) | `1310dc11bae684a9889548d1e764e83381b39d57` | [#179](https://github.com/d6g8k5htny-coder/Math-/pull/179) | `6e5f36d7641b` (2026-10-01) | no | -| [`elder_third_order_20261001`](../../frontiers/elder_third_order_20261001/PROOF.md) | `c8767ddecf1041d234f685e95af582073a7be393` | [#220](https://github.com/d6g8k5htny-coder/Math-/pull/220) | `0d797780c2e3` (2026-10-01) | no | -| [`far_elder_rate_20260930`](../../frontiers/far_elder_rate_20260930/PROOF.md) | `072601145601a1021037a2e91bf8826c1c971ecc` | [#187](https://github.com/d6g8k5htny-coder/Math-/pull/187) | `c2f1270d2819` (2026-10-01) | no | | [`remainder_rate_20260930`](../../frontiers/remainder_rate_20260930/PROOF.md) | `abfb98ae41d66a86d3cb094162db6547d0f29e7e` | [#198](https://github.com/d6g8k5htny-coder/Math-/pull/198) | `124c37d92181` (2026-10-01) | no | -| [`remainder_vanishing_20260930`](../../frontiers/remainder_vanishing_20260930/PROOF.md) | `441152dfc1d8d00cb268cebdb0394212a5bfacdb` | [#191](https://github.com/d6g8k5htny-coder/Math-/pull/191) | `955654747c0e` (2026-10-01) | no | +| [`far_elder_rate_20260930`](../../frontiers/far_elder_rate_20260930/PROOF.md) | `072601145601a1021037a2e91bf8826c1c971ecc` | [#187](https://github.com/d6g8k5htny-coder/Math-/pull/187) | `c2f1270d2819` (2026-10-01) | no | | [`short_bar_endpoint_law_20261001`](../../frontiers/short_bar_endpoint_law_20261001/PROOF.md) | `0d47dbc1d92863d8c51b918aa47d1fa8b605cfdc` | [#221](https://github.com/d6g8k5htny-coder/Math-/pull/221) | `f166ef52e5ca` (2026-10-01) | no | +| [`c2_finite_jet_transfer_20261001`](../../frontiers/c2_finite_jet_transfer_20261001/PROOF.md) | `54cc4a1ae274842bc2c01f9c207549e7b07de7bc` | [#232](https://github.com/d6g8k5htny-coder/Math-/pull/232) | `7fe06b01489a` (2026-10-01) | no | +| [`cusp_second_order_20261001`](../../frontiers/cusp_second_order_20261001/PROOF.md) | `f6df5a7356a54771b0052e42a864a140709903ad` | [#207](https://github.com/d6g8k5htny-coder/Math-/pull/207) | `566b1a143ec2` (2026-10-01) | no | +| [`candidate_third_order_20261001`](../../frontiers/candidate_third_order_20261001/PROOF.md) | `70ca57ef05199e75417d7d57928c1e1c93bf944e` | [#218](https://github.com/d6g8k5htny-coder/Math-/pull/218) | `fb6ee97bc791` (2026-10-01) | no | +| [`elder_third_order_20261001`](../../frontiers/elder_third_order_20261001/PROOF.md) | `c8767ddecf1041d234f685e95af582073a7be393` | [#220](https://github.com/d6g8k5htny-coder/Math-/pull/220) | `0d797780c2e3` (2026-10-01) | no | | [`third_order_rate_20261001`](../../frontiers/third_order_rate_20261001/PROOF.md) | `110ed33a57902bef11873807e722fde3888b59fb` | [#229](https://github.com/d6g8k5htny-coder/Math-/pull/229) | `6f74f7a77bae` (2026-10-01) | no | | [`elder_cusp_parity_20261002`](../../frontiers/elder_cusp_parity_20261002/PROOF.md) | `16a1db0658918057ff741df888c13702763d9919` | [#240](https://github.com/d6g8k5htny-coder/Math-/pull/240) | `7636cae5c386` (2026-10-02) | no | | [`separated_fold_multiplicity_20261002`](../../frontiers/separated_fold_multiplicity_20261002/PROOF.md) | `026cf5237510018d466380683b7679c2de977845` | [#239](https://github.com/d6g8k5htny-coder/Math-/pull/239) | `240a9bfa06af` (2026-10-02) | no | -| [`soft_closed_form_20261002`](../../frontiers/soft_closed_form_20261002/PROOF.md) | `c69f92b1076399fb9f8917bb273e15348b0a497e` | [#244](https://github.com/d6g8k5htny-coder/Math-/pull/244) | `07320089a9c6` (2026-10-02) | no | -| [`soft_fold_limit_20261002`](../../frontiers/soft_fold_limit_20261002/PROOF.md) | `6502cf7ba2edee47761e40308c15b7563b06d1f8` | [#243](https://github.com/d6g8k5htny-coder/Math-/pull/243) | `fa8b0d219e41` (2026-10-02) | no | -| [`soft_rejected_pairs_20261002`](../../frontiers/soft_rejected_pairs_20261002/PROOF.md) | `271412dbc96a29590f5f805258e15c9e335cb430` | [#242](https://github.com/d6g8k5htny-coder/Math-/pull/242) | `54c6759e8434` (2026-10-02) | no | | [`subpin_collision_20261002`](../../frontiers/subpin_collision_20261002/PROOF.md) | `4d903d0f834fb2077257104cd91822fe253dde8d` | [#245](https://github.com/d6g8k5htny-coder/Math-/pull/245) | `2d8616ef1b45` (2026-10-02) | no | +| [`soft_rejected_pairs_20261002`](../../frontiers/soft_rejected_pairs_20261002/PROOF.md) | `271412dbc96a29590f5f805258e15c9e335cb430` | [#242](https://github.com/d6g8k5htny-coder/Math-/pull/242) | `54c6759e8434` (2026-10-02) | no | +| [`soft_fold_limit_20261002`](../../frontiers/soft_fold_limit_20261002/PROOF.md) | `6502cf7ba2edee47761e40308c15b7563b06d1f8` | [#243](https://github.com/d6g8k5htny-coder/Math-/pull/243) | `fa8b0d219e41` (2026-10-02) | no | +| [`soft_closed_form_20261002`](../../frontiers/soft_closed_form_20261002/PROOF.md) | `c69f92b1076399fb9f8917bb273e15348b0a497e` | [#244](https://github.com/d6g8k5htny-coder/Math-/pull/244) | `07320089a9c6` (2026-10-02) | no | Some integration commits brought several packets at once: `d39dbbc` (#124, three packets), `5bd9249` (#134, two packets) and `e947ade` (#139, four packets). diff --git a/tests/test_proof_reachability.py b/tests/test_proof_reachability.py index b4d9061f3..7b746f61d 100644 --- a/tests/test_proof_reachability.py +++ b/tests/test_proof_reachability.py @@ -63,5 +63,86 @@ def test_missing_cut_fails(self): self.assertEqual(cpr.check(self.text.replace('Cut: `', 'Cutoff: `')), ['no cut commit line']) +class IntegrationOrder(unittest.TestCase): + """Finding r4170055081: rows must follow first-parent integration order; any swapped pair fails.""" + + def setUp(self): + self.text = DOC.read_text(encoding='utf-8') + self.cut, self.rows, self.lines = cpr.parse(self.text) + + def _swap(self, i, j): + a, b = self.lines[i], self.lines[j] + return self.text.replace(a + '\n', '\0').replace(b + '\n', a + '\n').replace('\0', b + '\n') + + def test_real_order_has_no_order_failure(self): + self.assertFalse([f for f in cpr.check(self.text) if f.startswith('row order')]) + + def test_swapped_adjacent_rows_with_different_commits_fail(self): + i = next(k for k in range(len(self.rows) - 1) if self.rows[k]['commit'] != self.rows[k + 1]['commit']) + failures = cpr.check(self._swap(i, i + 1)) + self.assertTrue([f for f in failures if f.startswith('row order')], failures) + + def test_swapped_rows_sharing_a_commit_fail(self): + i = next(k for k in range(len(self.rows) - 1) if self.rows[k]['commit'] == self.rows[k + 1]['commit']) + failures = cpr.check(self._swap(i, i + 1)) + self.assertTrue([f for f in failures if f.startswith('row order')], failures) + + def test_last_four_rows_reversed_fail(self): + n = len(self.lines) + text = self._swap(n - 4, n - 1) + failures = cpr.check(text) + self.assertTrue([f for f in failures if f.startswith('row order')], failures) + + +class VerdictWordsBothTables(unittest.TestCase): + """Finding r4170055086: every row of both tables is scanned; a verdict word in either table fails.""" + + def setUp(self): + self.text = DOC.read_text(encoding='utf-8') + self.inventory_row = cpr.parse(self.text)[2][0] + self.chain_row = [l for l in self.text.splitlines() if l.startswith('| `')][0] + + def test_both_tables_are_scanned(self): + scanned = cpr.all_table_lines(self.text) + self.assertIn(self.inventory_row, scanned) + self.assertIn(self.chain_row, scanned) + self.assertEqual(len(cpr.chain_rows(self.text)), 3) + + def test_each_verdict_word_in_each_table_fails(self): + for word in cpr.VERDICT_WORDS: + for row in (self.inventory_row, self.chain_row): + for variant in (word, word.lower()): + bad = row[:-1] + variant + ' |' + failures = cpr.check(self.text.replace(row, bad)) + self.assertTrue([f for f in failures if f.startswith('verdict word')], (word, row[:40])) + + def test_verdict_word_in_a_header_fails(self): + header = '| Packet | PR | Integration commit | `PROOF.md` blob | Landing receipt on main#229 |' + self.assertIn(header, self.text) + failures = cpr.check(self.text.replace(header, header.replace('PR |', 'PR (PASS) |'))) + self.assertTrue([f for f in failures if f.startswith('verdict word')], failures) + + +class ChainTableIdentities(unittest.TestCase): + def setUp(self): + self.text = DOC.read_text(encoding='utf-8') + self.row = [l for l in self.text.splitlines() if l.startswith('| `')][0] + self.chain = cpr.chain_rows(self.text)[0] + + def test_wrong_chain_blob_prefix_fails(self): + b = self.chain['blob'] + bad = self.row.replace(b, ('0' if b[0] != '0' else '1') + b[1:]) + self.assertIn('chain-table identity mismatch: ' + self.chain['folder'], cpr.check(self.text.replace(self.row, bad))) + + def test_wrong_chain_commit_prefix_fails(self): + c = self.chain['commit'] + bad = self.row.replace(c, ('0' if c[0] != '0' else '1') + c[1:]) + self.assertIn('chain-table identity mismatch: ' + self.chain['folder'], cpr.check(self.text.replace(self.row, bad))) + + def test_wrong_chain_pr_fails(self): + bad = self.row.replace('| #%s |' % self.chain['pr'], '| #%d |' % (int(self.chain['pr']) + 1)) + self.assertIn('chain-table identity mismatch: ' + self.chain['folder'], cpr.check(self.text.replace(self.row, bad))) + + if __name__ == '__main__': unittest.main() diff --git a/tools/check_proof_reachability.py b/tools/check_proof_reachability.py index bf87646b0..f0ccd03ec 100644 --- a/tools/check_proof_reachability.py +++ b/tools/check_proof_reachability.py @@ -5,10 +5,14 @@ frontiers//PROOF.md that exists there, with its exact git blob; the stated integration commit must be the first-parent commit of the cut's history that added the path; the "linked" column must agree with PROOF_INDEX.md at the cut; every frontiers/*/PROOF.md at the cut must appear exactly once; -and the table must carry no verdict words. Availability only: nothing here reads or grades a proof. +the rows must follow first-parent integration order (position in `git rev-list --first-parent --reverse +`, ties by folder name); the commit and blob prefixes of the second (chain) table must agree with +the first; and no line of either table may carry a verdict word. Availability only: nothing here reads +or grades a proof. Usage: python3 -B -S tools/check_proof_reachability.py [document] (exit 0 iff every check passes) """ +import functools import re import subprocess import sys @@ -21,15 +25,20 @@ r'\| \[#(?P\d+)\]\(https://github\.com/d6g8k5htny-coder/Math-/pull/(?P=pr)\) ' r'\| `(?P[0-9a-f]{12})` \((?P\d{4}-\d{2}-\d{2})\) ' r'\| (?Pyes|no) \|$') +CHAIN_RE = re.compile( + r'^\| `(?P[A-Za-z0-9_]+)` \| #(?P\d+) \| `(?P[0-9a-f]{12})` ' + r'\| `(?P[0-9a-f]{12})` \| (?P\d+) \|$') VERDICT_WORDS = ('ACCEPT', 'AMEND', 'HOLD', 'CONFIRMED', 'VERIFIED', 'PASS', 'REJECT', 'APPROVED', 'FAIL') +@functools.lru_cache(maxsize=None) def git(*args): + """Every query names the pinned cut, so its answer cannot change within a run; cache it.""" return subprocess.run(['git', *args], capture_output=True, text=True, check=True).stdout.strip() def parse(text): - """Return (cut, rows, table_lines) from the document text.""" + """Return (cut, rows, table_lines) from the document text (inventory rows only).""" m = CUT_RE.search(text) cut = m.group(1) if m else None rows, table_lines = [], [] @@ -41,6 +50,21 @@ def parse(text): return cut, rows, table_lines +def all_table_lines(text): + """Every line of every Markdown table in the document: headers, separators and data rows.""" + return [line for line in text.splitlines() if line.startswith('|')] + + +def chain_rows(text): + """Data rows of the second (chain) table: lines of the form | `folder` | #PR | ...""" + out = [] + for line in text.splitlines(): + if line.startswith('| `'): + mm = CHAIN_RE.match(line) + out.append(mm.groupdict() if mm else {'malformed': line}) + return out + + def verdict_words(lines): bad = [] for line in lines: @@ -55,12 +79,13 @@ def check(text): cut, rows, table_lines = parse(text) if cut is None: return ['no cut commit line'] - for w, line in verdict_words(table_lines): + for w, line in verdict_words(all_table_lines(text)): failures.append('verdict word %s in table row: %s' % (w, line)) paths = sorted(p for p in git('ls-tree', '-r', '--name-only', cut).splitlines() if re.fullmatch(r'frontiers/[^/]+/PROOF\.md', p)) index = git('show', cut + ':PROOF_INDEX.md') - seen = {} + position = {h: i for i, h in enumerate(git('rev-list', '--first-parent', '--reverse', cut).splitlines())} + seen, keys, computed = {}, [], {} for r in rows: if 'malformed' in r: failures.append('malformed row: ' + r['malformed'][:100]) @@ -70,17 +95,36 @@ def check(text): if path not in paths: failures.append('not a PROOF.md at the cut: ' + path) continue - if git('rev-parse', cut + ':' + path) != r['blob']: + blob = git('rev-parse', cut + ':' + path) + if blob != r['blob']: failures.append('blob mismatch: ' + path) added = git('log', cut, '--first-parent', '--diff-filter=A', '--format=%H %cs', '--', path).splitlines() if not added or not added[-1].startswith(r['commit']) or added[-1].split()[1] != r['date']: failures.append('integration commit/date mismatch: %s (%s)' % (path, added[-1] if added else 'none')) + if added: + commit = added[-1].split()[0] + keys.append((position[commit], r['folder'])) + computed[r['folder']] = (r['pr'], commit, blob) linked = ('frontiers/%s/' % r['folder']) in index or r['folder'] in index if (r['linked'] == 'yes') != linked: failures.append('PROOF_INDEX linkage mismatch: ' + path) for p in paths: if seen.get(p, 0) != 1: failures.append('appears %d times: %s' % (seen.get(p, 0), p)) + for a, b in zip(keys, keys[1:]): + if a > b: + failures.append('row order: %s (first-parent position %d) is listed before %s (position %d)' + % (a[1], a[0], b[1], b[0])) + for c in chain_rows(text): + if 'malformed' in c: + failures.append('malformed chain-table row: ' + c['malformed'][:100]) + continue + if c['folder'] not in computed: + failures.append('chain-table packet not in the inventory: ' + c['folder']) + continue + pr, commit, blob = computed[c['folder']] + if c['pr'] != pr or not commit.startswith(c['commit']) or not blob.startswith(c['blob']): + failures.append('chain-table identity mismatch: ' + c['folder']) return failures From 3de6e032a992130e4d15d31e4e3975df6e0627f7 Mon Sep 17 00:00:00 2001 From: Dylan Roy <249851642+d6g8k5htny-coder@users.noreply.github.com> Date: Sat, 3 Oct 2026 18:22:47 -0700 Subject: [PATCH 3/4] Reconcile dated proof navigation with the post-C126 source cut Preserve the original 62-row document byte for byte; add six one-level paths and fourteen separately counted nested proof routes at bbe85e2. Check full blob/SHA-256 identities, immutable links, counts, omissions and copy exclusion. Append a navigation-only link to PROOF_INDEX. No proof or scientific-status change. Authored assistance by OpenAI/Codex under Dylan Roy's explicit authorization; original Anthropic/Claude authorship retained. Separate nonauthor delta review required. --- PROOF_INDEX.md | 4 + .../2026-10-02-proof-reachability.md | 70 ++++++++++++++++ tests/test_proof_reachability.py | 45 +++++++++++ tools/check_proof_reachability.py | 80 ++++++++++++++++++- 4 files changed, 198 insertions(+), 1 deletion(-) diff --git a/PROOF_INDEX.md b/PROOF_INDEX.md index 030447a11..7c7e1b0d6 100644 --- a/PROOF_INDEX.md +++ b/PROOF_INDEX.md @@ -51,3 +51,7 @@ The shared [public inventory](https://github.com/d6g8k5htny-coder/main/tree/main ## Repository rule A reviewed/closed theorem or lemma must have its full proof or immutable byte-bound mirror in this repository plus the exact review/certificate. An open theorem with a complete candidate proof must link it here. An open item without a complete proof must link the strongest partial derivation and state the missing proof explicitly. Superseded/refuted work stays available. Tests and hashes are evidence, not substitutes for analytic proof. A navigation refresh records source availability and existing review scope; any change to [claims/LANDING_CLAIMS.json](claims/LANDING_CLAIMS.json) or the D0-D7 graph requires its own source-bound reconciliation through the existing validators. + +## Later frontier proof paths + +[Frontier proof reachability and the post-C126 supplement](docs/integration/2026-10-02-proof-reachability.md) retain the original 2 October inventory and add a separately pinned 3 October cut, including routes to the nested soft-layer and A4 records. These are dated availability inventories, not new verdicts or a count of distinct theorems. diff --git a/docs/integration/2026-10-02-proof-reachability.md b/docs/integration/2026-10-02-proof-reachability.md index d977d14ce..c5dd02757 100644 --- a/docs/integration/2026-10-02-proof-reachability.md +++ b/docs/integration/2026-10-02-proof-reachability.md @@ -100,3 +100,73 @@ Limits, stated so that the chain is not over-read: - **Later model-level work.** It lives in issue comments on main#229, not in repository sources, so it is not indexed here. This includes the signed elder margin (5959038812, amended in 5961281898), exact-pin decision stability (5961415030), and the signed-coordinate and level-band bounds (5957815904, 5959878294, 5959920397). - **Where the status lives.** Review records and status are in each PR's conversation and disposition block. + +## Post-C126 supplement — 3 October 2026 + +Post-C126 cut: `bbe85e270f2c8b747f2d5d9477c86e86e323fe15`. + +The original document above, including its 62-row inventory and statements about +then-available sources, is preserved byte for byte from #247 v1.1 (`ee087cea`). +This supplement records availability at the later cut where #261 incorporated +C124. It does not update the mathematical scope of any historical statement. +The [69-packet historical record](https://github.com/d6g8k5htny-coder/Math-/blob/4ff4f1dacd8ab4f22c8e5307fb5eba69cbacf2ba/docs/integration/2026-09-29-navigation-refresh.md) +and the [proof availability index](../../PROOF_INDEX.md) are separate reading routes. + +One-level inventory: 68 paths; 62 retained; 6 added; 0 removed. + +The rule is exactly `frontiers//PROOF.md`. All 62 retained proof +blobs are unchanged between the two cuts. Nested files, `sources/` copies, +coefficient packets, files with other names, and issue-only payloads are outside +this count. A path count is not a count of distinct theorems or accepted results. +Rows below pin the later commit in their links and record the full Git blob and +SHA-256 of each proof. Their order is lexical by path, not integration order. + +### Six additional one-level proof paths + +| Source path at the later cut | Git blob | SHA-256 | +|---|---|---| +| [source: `frontiers/cusp_torus_transfer_20261001/PROOF.md`](https://github.com/d6g8k5htny-coder/Math-/blob/bbe85e270f2c8b747f2d5d9477c86e86e323fe15/frontiers/cusp_torus_transfer_20261001/PROOF.md) | `de3d85fdcf65487adc982bae7318246c1b8f016c` | `6b818bdc34c6908505c6b2ad65584f740254a8525ddc8a45197d560386243bb0` | +| [source: `frontiers/moving_remote_collision_20261003/PROOF.md`](https://github.com/d6g8k5htny-coder/Math-/blob/bbe85e270f2c8b747f2d5d9477c86e86e323fe15/frontiers/moving_remote_collision_20261003/PROOF.md) | `596782786a200412a58169440b45d4f5bb36aadf` | `d94f8f2f7e809da37465729d3eca5f9793bce5fc5410d9f83e61db259ddf73df` | +| [source: `frontiers/ordinary_short_bar_occurrence_20261001/PROOF.md`](https://github.com/d6g8k5htny-coder/Math-/blob/bbe85e270f2c8b747f2d5d9477c86e86e323fe15/frontiers/ordinary_short_bar_occurrence_20261001/PROOF.md) | `69ff20a6c514629373f3ad12eb2db2a2596777d6` | `16d2c5f6c1fe45dd6ce8f6b69455db4908b8e6319e57d58c4ad7c9d1881bdd4d` | +| [source: `frontiers/replacement_bar_occurrence_20261001/PROOF.md`](https://github.com/d6g8k5htny-coder/Math-/blob/bbe85e270f2c8b747f2d5d9477c86e86e323fe15/frontiers/replacement_bar_occurrence_20261001/PROOF.md) | `724258d33408f754ffc21848196e1fdd80c8bf6a` | `b49f2ea5975dc05270f51fea4a3574093f726258cdab94888742507c2caa275f` | +| [source: `frontiers/strict_unique_replacement_coefficient_20261003/PROOF.md`](https://github.com/d6g8k5htny-coder/Math-/blob/bbe85e270f2c8b747f2d5d9477c86e86e323fe15/frontiers/strict_unique_replacement_coefficient_20261003/PROOF.md) | `eff422d197fcc1ff41c155c783bfeca101330a20` | `2b8949f7be425861275db49563c9dc81fee20d7118e5c6703f25f9d40e4f4188` | +| [source: `frontiers/unique_replacement_bar_intensity_20261001/PROOF.md`](https://github.com/d6g8k5htny-coder/Math-/blob/bbe85e270f2c8b747f2d5d9477c86e86e323fe15/frontiers/unique_replacement_bar_intensity_20261001/PROOF.md) | `9c79a672f5d81e04972032b2f1faf185f4664fa5` | `ba1901cbb4bac037befb21d648172ac3ba04aa370f5377a2919c0da988572552` | + +### Nested records, counted separately + +Nested inventory: 14 proof paths in the two named collections below. + +The [soft-layer collection README](https://github.com/d6g8k5htny-coder/Math-/blob/bbe85e270f2c8b747f2d5d9477c86e86e323fe15/frontiers/planar_soft_layer_chain_20261003/README.md) +routes to C91–C99, C101–C103 and C124, their full reviews, source crosswalk and +checkers. The [A4 collection README](https://github.com/d6g8k5htny-coder/Math-/blob/bbe85e270f2c8b747f2d5d9477c86e86e323fe15/frontiers/planar_rejected_endpoint_margin_20261003/README.md) +routes to A4, its full review and exposure correction. These 13 plus 1 proof +records are not added to the 68 one-level paths. C100 and C104 are outside the +soft-layer collection. Copied dependencies elsewhere in `sources/` are not +new entries in either inventory. The linked proof statements and reviews govern; +this route adds no review verdict or extension to small-gap/global-bar claims. + +| Nested source path at the later cut | Git blob | SHA-256 | +|---|---|---| +| [source: `frontiers/planar_rejected_endpoint_margin_20261003/A4/PROOF.md`](https://github.com/d6g8k5htny-coder/Math-/blob/bbe85e270f2c8b747f2d5d9477c86e86e323fe15/frontiers/planar_rejected_endpoint_margin_20261003/A4/PROOF.md) | `f1a71b2a0db6fc43636583af6c9f471d6c040488` | `acd172c5f8626aa3b7be5ac691786eefa6d6f243a32909502dfdbd79c8066a7c` | +| [source: `frontiers/planar_soft_layer_chain_20261003/C101/PROOF.md`](https://github.com/d6g8k5htny-coder/Math-/blob/bbe85e270f2c8b747f2d5d9477c86e86e323fe15/frontiers/planar_soft_layer_chain_20261003/C101/PROOF.md) | `6dcbdf68db9d10014f1a1fe09104e3397480d229` | `300d0d18abb74332e593e389485c817a3c0ea7c31345194e3cfdd4039ac3b5c4` | +| [source: `frontiers/planar_soft_layer_chain_20261003/C102/PROOF.md`](https://github.com/d6g8k5htny-coder/Math-/blob/bbe85e270f2c8b747f2d5d9477c86e86e323fe15/frontiers/planar_soft_layer_chain_20261003/C102/PROOF.md) | `0e35fe954fedf144baa647103d303efcd4ffab7e` | `1a89b365bec20e353b84d5ac17b1acbe9179d48e4e4137e04d3c7e40ad207628` | +| [source: `frontiers/planar_soft_layer_chain_20261003/C103/PROOF.md`](https://github.com/d6g8k5htny-coder/Math-/blob/bbe85e270f2c8b747f2d5d9477c86e86e323fe15/frontiers/planar_soft_layer_chain_20261003/C103/PROOF.md) | `b9920348bef731b1fcaaa9e5aa6cadaed77ec837` | `652e66f8645eb1a34c28a85900b05405d424bb0e282b86a7d5597f10b8f9c8e3` | +| [source: `frontiers/planar_soft_layer_chain_20261003/C124/PROOF.md`](https://github.com/d6g8k5htny-coder/Math-/blob/bbe85e270f2c8b747f2d5d9477c86e86e323fe15/frontiers/planar_soft_layer_chain_20261003/C124/PROOF.md) | `d99cec53ecabfe3fb9d4a1e4a085cd026134fd5c` | `90148657397dcce31e8039afa9015c022f74b2ed0d41e75f2f2339074a8a520f` | +| [source: `frontiers/planar_soft_layer_chain_20261003/C91/PROOF.md`](https://github.com/d6g8k5htny-coder/Math-/blob/bbe85e270f2c8b747f2d5d9477c86e86e323fe15/frontiers/planar_soft_layer_chain_20261003/C91/PROOF.md) | `92c9c4797081d884080622c276c6c7fe6c843533` | `74a9ee276c3647276deb544c6d83e3cf21f708f55f9009fa4db5cc49c9d0e9aa` | +| [source: `frontiers/planar_soft_layer_chain_20261003/C92/PROOF.md`](https://github.com/d6g8k5htny-coder/Math-/blob/bbe85e270f2c8b747f2d5d9477c86e86e323fe15/frontiers/planar_soft_layer_chain_20261003/C92/PROOF.md) | `4f6598a15dd9a64b26b5b8c6904ec4be45152409` | `6fa4c3d6d1e8c3d8590c865802d5df061ad5b17652ddc7fd7bf5c5e8b8de084a` | +| [source: `frontiers/planar_soft_layer_chain_20261003/C93/PROOF.md`](https://github.com/d6g8k5htny-coder/Math-/blob/bbe85e270f2c8b747f2d5d9477c86e86e323fe15/frontiers/planar_soft_layer_chain_20261003/C93/PROOF.md) | `204fd6f3d3a1bb04945dc3e1556bd1ee8e7af35e` | `f25f86cc66ae335b4832ea53670646815567ec7854fa0386f8c57f6939e0af1c` | +| [source: `frontiers/planar_soft_layer_chain_20261003/C94/PROOF.md`](https://github.com/d6g8k5htny-coder/Math-/blob/bbe85e270f2c8b747f2d5d9477c86e86e323fe15/frontiers/planar_soft_layer_chain_20261003/C94/PROOF.md) | `a9f2695b4b2c45a3fa059ee3e2f889647374bffa` | `0fe4fa2028f8ddbbf5a79df3879bcbd3789f19409fb44ad739caeabedff1af3c` | +| [source: `frontiers/planar_soft_layer_chain_20261003/C95/PROOF.md`](https://github.com/d6g8k5htny-coder/Math-/blob/bbe85e270f2c8b747f2d5d9477c86e86e323fe15/frontiers/planar_soft_layer_chain_20261003/C95/PROOF.md) | `25faf41278c5b0f52603fbca8287b4b0c047b5da` | `c0d9ee72352fafe91f96a8b6187c978f09ee3c187d5f4c7c2462c0187750d2e1` | +| [source: `frontiers/planar_soft_layer_chain_20261003/C96/PROOF.md`](https://github.com/d6g8k5htny-coder/Math-/blob/bbe85e270f2c8b747f2d5d9477c86e86e323fe15/frontiers/planar_soft_layer_chain_20261003/C96/PROOF.md) | `93e3734279f024a7d253076a7d93712def5779ab` | `0758b5de8f4d9e4658ca3c6cf3e52c23d8e12f77999e9c3668ef0bedb15a05f5` | +| [source: `frontiers/planar_soft_layer_chain_20261003/C97/PROOF.md`](https://github.com/d6g8k5htny-coder/Math-/blob/bbe85e270f2c8b747f2d5d9477c86e86e323fe15/frontiers/planar_soft_layer_chain_20261003/C97/PROOF.md) | `49e304440987e19ec4c1a407271093d2fc879f0a` | `acf83958e6ea650d83bf811b2beacc03b553637dc4a3160012567c7f0a300a57` | +| [source: `frontiers/planar_soft_layer_chain_20261003/C98/PROOF.md`](https://github.com/d6g8k5htny-coder/Math-/blob/bbe85e270f2c8b747f2d5d9477c86e86e323fe15/frontiers/planar_soft_layer_chain_20261003/C98/PROOF.md) | `ae0def45e3109f13b917f85b5d617f582cc5d0e2` | `3ca1622197bf22cf71ab64f2938ecc0b022ed09487b691d50ae8d2ad1f46d198` | +| [source: `frontiers/planar_soft_layer_chain_20261003/C99/PROOF.md`](https://github.com/d6g8k5htny-coder/Math-/blob/bbe85e270f2c8b747f2d5d9477c86e86e323fe15/frontiers/planar_soft_layer_chain_20261003/C99/PROOF.md) | `f8a68df60da33d59fac617267f5ab66f94fb856d` | `55eb6c33105190da4194e63d90ceeb40f3434b14b92803700ab840df67e9295e` | + +This is a bounded dated inventory, not an exhaustive index of every proof format +or later repository addition. The checker verifies the retained prefix, the two +cut relationship, exact one-level delta, unchanged retained blobs, the named +nested inventory, and every listed byte identity and immutable link. + +Supplement author: OpenAI/Codex, assisting the original Anthropic/Claude proposal +under Dylan Roy's explicit authorization. Scientific effect: NONE. + diff --git a/tests/test_proof_reachability.py b/tests/test_proof_reachability.py index 7b746f61d..d4d6eac1f 100644 --- a/tests/test_proof_reachability.py +++ b/tests/test_proof_reachability.py @@ -144,5 +144,50 @@ def test_wrong_chain_pr_fails(self): self.assertIn('chain-table identity mismatch: ' + self.chain['folder'], cpr.check(self.text.replace(self.row, bad))) +class PostC126Inventory(unittest.TestCase): + """Reject stale counts, missing nested routes, mutable pins and copied sources.""" + + def setUp(self): + self.text = DOC.read_text(encoding='utf-8') + self.rows = [line for line in self.text.splitlines() if line.startswith('| [source:')] + + def test_real_supplement_passes(self): + self.assertEqual(cpr.check(self.text), []) + + def test_missing_or_duplicate_supplement_fails(self): + original, supplement = self.text.split('') + self.assertTrue(cpr.check(original)) + self.assertTrue(cpr.check(self.text + '' + supplement)) + + def test_wrong_count_fails(self): + self.assertTrue(cpr.check(self.text.replace('One-level inventory: 68 paths', 'One-level inventory: 82 paths'))) + + def test_dropped_added_proof_fails(self): + self.assertTrue(cpr.check(self.text.replace(self.rows[0] + '\n', ''))) + + def test_dropped_nested_proof_fails(self): + row = next(row for row in self.rows if '/C124/PROOF.md' in row) + self.assertTrue(cpr.check(self.text.replace(row + '\n', ''))) + + def test_duplicate_source_fails(self): + self.assertTrue(cpr.check(self.text.replace(self.rows[0], self.rows[0] + '\n' + self.rows[0]))) + + def test_wrong_hash_or_mutable_url_fails(self): + row = self.rows[0] + digest = row.split('`')[-2] + failures = cpr.check(self.text.replace(row, row.replace(digest, '0' * 64))) + self.assertTrue(any(f.startswith('post-cut source identity mismatch:') for f in failures)) + bad = row.replace('/blob/bbe85e270f2c8b747f2d5d9477c86e86e323fe15/', '/blob/main/') + self.assertIn('malformed post-cut source row', cpr.check(self.text.replace(row, bad))) + + def test_copied_source_substitution_fails(self): + row = next(row for row in self.rows if 'frontiers/replacement_bar_occurrence_20261001/PROOF.md' in row) + bad = row.replace('replacement_bar_occurrence_20261001/PROOF.md', 'replacement_bar_occurrence_20261001/sources/c50/PROOF.md') + self.assertTrue(cpr.check(self.text.replace(row, bad))) + + def test_historical_prose_edit_fails(self): + self.assertTrue(cpr.check(self.text.replace('other 51 are reachable', 'other 99 are reachable'))) + + if __name__ == '__main__': unittest.main() diff --git a/tools/check_proof_reachability.py b/tools/check_proof_reachability.py index f0ccd03ec..5790c35c0 100644 --- a/tools/check_proof_reachability.py +++ b/tools/check_proof_reachability.py @@ -8,11 +8,14 @@ the rows must follow first-parent integration order (position in `git rev-list --first-parent --reverse `, ties by folder name); the commit and blob prefixes of the second (chain) table must agree with the first; and no line of either table may carry a verdict word. Availability only: nothing here reads -or grades a proof. +or grades a proof. The additive post-C126 supplement also preserves the historical +document bytes and checks its separately pinned one-level delta, named nested +collections, full proof identities and immutable links. Usage: python3 -B -S tools/check_proof_reachability.py [document] (exit 0 iff every check passes) """ import functools +import hashlib import re import subprocess import sys @@ -29,6 +32,13 @@ r'^\| `(?P[A-Za-z0-9_]+)` \| #(?P\d+) \| `(?P[0-9a-f]{12})` ' r'\| `(?P[0-9a-f]{12})` \| (?P\d+) \|$') VERDICT_WORDS = ('ACCEPT', 'AMEND', 'HOLD', 'CONFIRMED', 'VERIFIED', 'PASS', 'REJECT', 'APPROVED', 'FAIL') +POST_START = '' +POST_END = '' +HISTORICAL_HEAD = 'ee087cea7cfa932daf0122aaee8227d1dfbadef4' +POST_ROW = re.compile( + r'^\| \[source: `(?Pfrontiers/[A-Za-z0-9_/]+/PROOF\.md)`\]' + r'\(https://github\.com/d6g8k5htny-coder/Math-/blob/(?P[0-9a-f]{40})/(?P=path)\) ' + r'\| `(?P[0-9a-f]{40})` \| `(?P[0-9a-f]{64})` \|$') @functools.lru_cache(maxsize=None) @@ -74,6 +84,73 @@ def verdict_words(lines): return bad +@functools.lru_cache(maxsize=None) +def source_bytes(cut, path): + """Retain every byte, including terminal newlines, for identity checks.""" + return subprocess.run(['git', 'show', cut + ':' + path], + capture_output=True, check=True).stdout + + +def check_post_cut(text, old_cut): + """Check the additive later-cut inventory without replacing the historical cut.""" + if text.count(POST_START) != 1 or text.count(POST_END) != 1: + return ['post-cut supplement must occur exactly once'] + original, rest = text.split(POST_START) + supplement, tail = rest.split(POST_END) + failures = [] + if tail.strip(): + failures.append('unexpected content after post-cut supplement') + if original.encode('utf-8') != source_bytes(HISTORICAL_HEAD, DOC): + failures.append('historical document changed') + cuts = re.findall(r'^Post-C126 cut: `([0-9a-f]{40})`\.$', supplement, re.M) + if len(cuts) != 1: + return failures + ['post-cut commit must occur exactly once'] + cut = cuts[0] + try: + if git('merge-base', old_cut, cut) != old_cut: + return failures + ['post-cut does not descend from historical cut'] + old_paths = set(git('ls-tree', '-r', '--name-only', old_cut).splitlines()) + new_paths = set(git('ls-tree', '-r', '--name-only', cut).splitlines()) + except subprocess.CalledProcessError: + return failures + ['post-cut commit unavailable'] + old_one = {p for p in old_paths if re.fullmatch(r'frontiers/[^/]+/PROOF\.md', p)} + new_one = {p for p in new_paths if re.fullmatch(r'frontiers/[^/]+/PROOF\.md', p)} + added, retained, removed = new_one - old_one, new_one & old_one, old_one - new_one + nested = {p for p in new_paths if re.fullmatch( + r'frontiers/(planar_soft_layer_chain_20261003/C\d+|' + r'planar_rejected_endpoint_margin_20261003/A4)/PROOF\.md', p)} + counts = 'One-level inventory: %d paths; %d retained; %d added; %d removed.' % ( + len(new_one), len(retained), len(added), len(removed)) + nested_count = 'Nested inventory: %d proof paths in the two named collections below.' % len(nested) + if supplement.splitlines().count(counts) != 1 or supplement.splitlines().count(nested_count) != 1: + failures.append('post-cut inventory count mismatch') + for path in retained: + if git('rev-parse', old_cut + ':' + path) != git('rev-parse', cut + ':' + path): + failures.append('retained proof changed: ' + path) + seen = [] + for line in supplement.splitlines(): + if not line.startswith('| [source:'): + continue + match = POST_ROW.fullmatch(line) + if not match: + failures.append('malformed post-cut source row') + continue + row = match.groupdict() + path = row['path'] + seen.append(path) + if path not in added | nested: + failures.append('unexpected post-cut source: ' + path) + continue + if (row['cut'] != cut or row['blob'] != git('rev-parse', cut + ':' + path) + or row['sha256'] != hashlib.sha256(source_bytes(cut, path)).hexdigest()): + failures.append('post-cut source identity mismatch: ' + path) + if len(seen) != len(set(seen)) or set(seen) != added | nested: + failures.append('post-cut source membership mismatch') + if seen != sorted(added) + sorted(nested): + failures.append('post-cut source order mismatch') + return failures + + def check(text): failures = [] cut, rows, table_lines = parse(text) @@ -125,6 +202,7 @@ def check(text): pr, commit, blob = computed[c['folder']] if c['pr'] != pr or not commit.startswith(c['commit']) or not blob.startswith(c['blob']): failures.append('chain-table identity mismatch: ' + c['folder']) + failures.extend(check_post_cut(text, cut)) return failures From a7f7b319f875b6b6da19b70ebc79eb7d7cb32961 Mon Sep 17 00:00:00 2001 From: Dylan Roy <249851642+d6g8k5htny-coder@users.noreply.github.com> Date: Sat, 3 Oct 2026 19:33:03 -0700 Subject: [PATCH 4/4] Preserve raw newlines at proof reachability CLI boundary Repair A1 from review5403796683 without changing authentic navigation or proof bytes. Add real-file CLI regressions in normal and optimized Python. Actual author: OpenAI/Codex /root/repair_navigation_byte_guard, delegated by Dylan Roy. Scientific effect: NONE. --- tests/test_proof_reachability.py | 29 +++++++++++++++++++++++++++++ tools/check_proof_reachability.py | 3 ++- 2 files changed, 31 insertions(+), 1 deletion(-) diff --git a/tests/test_proof_reachability.py b/tests/test_proof_reachability.py index d4d6eac1f..8d75e1591 100644 --- a/tests/test_proof_reachability.py +++ b/tests/test_proof_reachability.py @@ -1,6 +1,8 @@ """Tests for tools/check_proof_reachability.py: the real document passes, and adverse edits fail.""" import pathlib +import subprocess import sys +import tempfile import unittest ROOT = pathlib.Path(__file__).resolve().parents[1] @@ -10,6 +12,33 @@ DOC = ROOT / 'docs' / 'integration' / '2026-10-02-proof-reachability.md' +class CommandLineBytes(unittest.TestCase): + """A1: exercise actual file bytes across the CLI's input boundary in both modes.""" + + def _run_document(self, source, expected_code, expected_line): + with tempfile.TemporaryDirectory() as directory: + document = pathlib.Path(directory) / 'reachability.md' + document.write_bytes(source) + for mode in ([], ['-O']): + with self.subTest(mode=mode): + result = subprocess.run( + [sys.executable, '-B', '-S', *mode, + str(ROOT / 'tools' / 'check_proof_reachability.py'), str(document)], + cwd=ROOT, capture_output=True, text=True, timeout=30) + self.assertEqual(result.returncode, expected_code, result.stdout + result.stderr) + self.assertIn(expected_line, result.stdout.splitlines()) + self.assertEqual(result.stderr, '') + + def test_authentic_file_bytes_pass(self): + self._run_document(DOC.read_bytes(), 0, 'proof-reachability: OK') + + def test_historical_crlf_mutation_fails(self): + source = DOC.read_bytes() + mutant = source.replace(b'\n', b'\r\n', 1) + self.assertNotEqual(mutant, source) + self._run_document(mutant, 1, 'FAIL historical document changed') + + class RealDocument(unittest.TestCase): def setUp(self): self.text = DOC.read_text(encoding='utf-8') diff --git a/tools/check_proof_reachability.py b/tools/check_proof_reachability.py index 5790c35c0..662d698fe 100644 --- a/tools/check_proof_reachability.py +++ b/tools/check_proof_reachability.py @@ -208,7 +208,8 @@ def check(text): def main(argv): doc = argv[1] if len(argv) > 1 else DOC - with open(doc, encoding='utf-8') as fh: + # Preserve CR/LF bytes for the historical-prefix identity check. + with open(doc, encoding='utf-8', newline='') as fh: failures = check(fh.read()) for f in failures: print('FAIL', f)