From 8d967090146062a07d7464355e8e6c6550157793 Mon Sep 17 00:00:00 2001 From: LightChainr <172050935+LightChainr@users.noreply.github.com> Date: Sun, 13 Sep 2026 15:26:10 +0800 Subject: [PATCH] Independent census of C(<=4, <=100) against the four frozen P2 intervals (issue #568) Second implementation of the quartic census every one of Results A-D rests on. Written from the protocol only: analysis/pslq_search_contract.json and manuscript sections 3 and 5. The three primary files named in the ticket were never read. Disclosure first. This is NOT a blind replication: the primary's committed summary artifacts results/pslq-degree4-*/latest.json were read before this was written, because they define the comparison quantities. The code path is disjoint; the priors were not. Four search paths, all returning identical retained sets: local nested enumeration, leading coefficient SOLVED exactly S=1e15 loop nested enumeration, leading coefficient LOOPED, 100x the work S=1e15 mitm split {0,1,2}|{3,4}, sorted right half, binary search S=1e15 alt as local but on a DIFFERENT screen lattice S=2^50 560 shards over 10 Huawei ARM containers / 144 vCPU, all completed. Weights, rho and the screen bound are recomputed here in exact rational arithmetic and agree identically with the primary (rho fraction for fraction; B = 20077, 3000086, 80000077, 100065). |C(d,100)| = 12175/3355121/749507743/ 157309446881 from Proposition 1, checked against direct enumeration at H=3,5,7. Result, per interval (mine / primary): jacobsen-2015-eigenvalue retention 0/0 near 1543/1543 roots 0/0 mertens-2022-p-med retention 3/3 near 1548/1548 roots 1/1 mertens-2022-p-cell retention 127/127 near 1660/1660 roots 15/15 yang-zhou-2024-corrected retention 0/0 near 1543/1543 roots 0/0 Closest member agrees coefficient by coefficient on all four intervals ([-84,99,-7,99,58] on three, [-97,87,54,98,49] on p-cell). Exact decisions use a different root path: monotonicity from the second derivative bound plus endpoint signs, not a Sturm chain. On p-cell the 15 root-bearing quartics are checked pairwise by exact rational polynomial gcd and share no non-constant factor, so 15 distinct roots stands without appeal to the primary. The residual / mean-value check the ticket asks for: the midpoint evaluation is a different point from the primary's endpoints, so the residuals must differ. The gaps are 4.867e-12 (cap 1.284e-11) and 2.434e-11 (cap 6.420e-11), both inside the cap, and the residuals are 95x and 9.2x the cap respectively -- so this is agreement on a non-trivial quantity, not two implementations both returning zero. On the two intervals whose residual is 0, the independent path also finds the sign change that makes it 0. Not done here, deliberately: the manuscript's section 7 "Recommended, not done" entry is NOT removed, and Table 9's scope line is NOT edited. Suggested wording is in the PR body for the owner, because the honest phrasing is "an independent re-derivation exists, written with the committed summaries in hand", not "a blind second implementation now exists". No new Monte Carlo, no new p_c, no merge, no docs/STATUS.md edit, no change to any existing file. Full Matching-One repository CI has not been run. --- notes/p568-independent-census-20260913.md | 135 ++++++++ .../REPORT.md | 17 + .../agreement.json | 186 +++++++++++ .../commands.txt | 13 + .../derived/jacobsen-2015-eigenvalue.json | 38 +++ .../derived/mertens-2022-p-cell.json | 144 +++++++++ .../derived/mertens-2022-p-med.json | 46 +++ .../derived/yang-zhou-2024-corrected.json | 38 +++ .../latest.json | 305 ++++++++++++++++++ .../metadata.json | 13 + scripts/independent_census.py | 293 +++++++++++++++++ scripts/independent_census_agreement.py | 130 ++++++++ scripts/independent_census_screen.cpp | 260 +++++++++++++++ 13 files changed, 1618 insertions(+) create mode 100644 notes/p568-independent-census-20260913.md create mode 100644 results/pslq-degree4-independent-replication/REPORT.md create mode 100644 results/pslq-degree4-independent-replication/agreement.json create mode 100644 results/pslq-degree4-independent-replication/commands.txt create mode 100644 results/pslq-degree4-independent-replication/derived/jacobsen-2015-eigenvalue.json create mode 100644 results/pslq-degree4-independent-replication/derived/mertens-2022-p-cell.json create mode 100644 results/pslq-degree4-independent-replication/derived/mertens-2022-p-med.json create mode 100644 results/pslq-degree4-independent-replication/derived/yang-zhou-2024-corrected.json create mode 100644 results/pslq-degree4-independent-replication/latest.json create mode 100644 results/pslq-degree4-independent-replication/metadata.json create mode 100644 scripts/independent_census.py create mode 100644 scripts/independent_census_agreement.py create mode 100644 scripts/independent_census_screen.cpp diff --git a/notes/p568-independent-census-20260913.md b/notes/p568-independent-census-20260913.md new file mode 100644 index 000000000..ca9d6a54f --- /dev/null +++ b/notes/p568-independent-census-20260913.md @@ -0,0 +1,135 @@ +# Independent census of C(≤4, ≤100) against the four frozen P2 intervals + +Issue #568. Everything here was written from the protocol only: the four interval +strings of `analysis/pslq_search_contract.json`, and the screening statement of +`docs/manuscripts/p2-algebraic-exclusion/manuscript.md` §3.2 (Theorem 2) with its +class definition in §3.1. + +## Disclosure, first + +The three primary files named in the ticket — +`scripts/degree4_interval_exclusion.py`, `scripts/degree4_fixed_point_screen.cpp`, +`scripts/exact_polynomial_root_certificate.py` — were **never read**. No share of +their code, structure or arithmetic is reused below. + +This is nevertheless **not a blind replication**. The primary's committed summary +artefacts `results/pslq-degree4-*/latest.json` were read before the replication was +written, because they define the comparison quantities (per-interval retention, +the closest member, the residual convention). That is recorded here rather than +passed off as something it is not. What follows is an independent *code path* +re-deriving the numbers from the protocol and then checked cell by cell against +the committed ones. + +## What was implemented + +`scripts/independent_census_screen.cpp` — the screen and the enumeration, in C++. +`scripts/independent_census.py` — weights, bound, exact decisions, artefacts. +`scripts/independent_census_agreement.py` — the cell-by-cell comparison. + +### The screen, re-derived + +With `S` the scale, `m` the interval midpoint, `w_k = round(S m^k)` and `c_0 = S`, +put `T(a) = Σ_{k=0..d} c_k a_k`. Then `|T(a) − S·P_a(m)| ≤ H·ρ` with +`ρ = Σ_k |S m^k − w_k|`, and if `P_a` has a root in `[l,u]` the mean value theorem +gives `|P_a(m)| ≤ D(u−l)/2` with `D = H·d(d+1)/2`. Hence every root-carrying `a` +obeys `|T(a)| ≤ B = ⌈S·D·(u−l)/2 + H·ρ⌉`. + +`w_k`, `ρ` and `B` are computed here in exact rational arithmetic from the decimal +midpoints, independently of the primary, and they **agree identically**: + +| interval | ρ (mine = primary) | B (mine = primary) | +|---|---|---| +| jacobsen-2015-eigenvalue | 7686546224338895232565910573032297919/10^37 | 20077 | +| mertens-2022-p-med | 53129090819380871648563294193601/625·10^28 | 3000086 | +| mertens-2022-p-cell | 479982034581456010007919/625·10^21 | 80000077 | +| yang-zhou-2024-corrected | 1574738498838320187782581333490561/2441406250·10^27 | 100065 | + +`|C(d,100)|` from Proposition 1 comes out `12175 / 3355121 / 749507743 / 157309446881` +for `d = 1..4`; the formula is checked against direct enumeration at `H = 3,5,7` for +`d = 1,2` before it is used. + +### Four search paths, deliberately different code + +| tag | structure | scale | where | +|---|---|---|---| +| `local` | nested enumeration, leading coefficient **solved exactly** | 10^15 | workstation | +| `loop` | nested enumeration, leading coefficient **looped** 100× more inner work | 10^15 | Huawei fleet, 60 shards/interval | +| `mitm` | split {0,1,2} \| {3,4}, sorted right half, binary search | 10^15 | Huawei fleet, 20 shards/interval | +| `alt` | same as `local` but on a **different screen lattice** | 2^50 | Huawei fleet, 60 shards/interval | + +Shards partition the constant term `a_0 ∈ [−100,100]`, so the union of shards is the +class exactly. 560 work units over 10 containers / 144 vCPU, all completed. + +`local`, `loop` and `mitm` return **byte-identical retained sets**; `alt` on the +2^50 lattice returns **exactly the same set** as well — the retained set does not +depend on the screen lattice, which is the property a correct screen must have. + +### Exact decisions, own path + +Retained tuples are decided in exact integer arithmetic on `P(x)·10^{dE}`, never in +binary floating point. Root counting uses **monotonicity from the second-derivative +bound plus endpoint signs**, not a Sturm chain: `|P'(m)| > (Σ k(k−1)|a_k|)(u−l)/2` +certifies that `P'` has no zero in the interval, hence `P` is strictly monotone and +the root count in `[l,u]` is the number of endpoint sign changes. No retained quartic +has a stationary point. + +## Result: exact agreement on every cell + +| interval | retention (prim.) mine / primary | near set mine / primary | root-bearing mine / primary | closest member | residual | +|---|---|---|---|---|---| +| jacobsen-2015-eigenvalue | 0 / 0 | 1543 / 1543 | 0 / 0 | agree | agree | +| mertens-2022-p-med | 3 / 3 | 1548 / 1548 | 1 / 1 | agree | agree | +| mertens-2022-p-cell | 127 / 127 | 1660 / 1660 | **15 / 15** | agree | agree | +| yang-zhou-2024-corrected | 0 / 0 | 1543 / 1543 | 0 / 0 | agree | agree | + +The closest member is `[-84, 99, -7, 99, 58]` on three of the four intervals and +`[-97, 87, 54, 98, 49]` on `mertens-2022-p-cell`, matching the primary coefficient by +coefficient. Class sizes match (`157309446881`). + +On `mertens-2022-p-cell` the 15 root-bearing quartics were additionally checked for +shared roots by exact rational polynomial gcd: **no pair shares a non-constant +factor**, so there are 15 distinct roots, and each contributes exactly one root in +the interval. `distinct_roots_in_interval = 15` therefore stands on its own, not on +the primary's assertion. + +## The residual / mean-value check + +The ticket asks for the check that rules out two implementations agreeing by both +reporting the same zero. The primary evaluates the closest member at the two +endpoints; the midpoint value is a genuinely different evaluation point, and the +mean value theorem caps the gap at `D_P (u−l)/2` with `D_P = Σ_k k|a_k|` for that +polynomial's own coefficients. + +| interval | min over `[l,u]` | `|P(m)|` at the midpoint | gap | cap `D_P(u−l)/2` | holds | +|---|---|---|---|---|---| +| jacobsen-2015-eigenvalue | 1.22096352294980850756812524667737566506094010368e−9 | 1.225831e−9 | 4.867e−12 | 1.284e−11 | yes | +| mertens-2022-p-med | 0 (sign change) | — | — | 1.926e−9 | yes | +| mertens-2022-p-cell | 0 (sign change) | — | — | 5.480e−8 | yes | +| yang-zhou-2024-corrected | 5.930735364635135763e−10 | 6.174104e−10 | 2.434e−11 | 6.420e−11 | yes | + +Two things follow. The gaps are **non-zero** and the residuals are **95×** and +**>1×** the mean-value cap, so the agreement is the agreement of two implementations +computing the same non-trivial quantity, not of two implementations both returning +zero. And on the two intervals where the residual is zero, it is zero for a reason +that the independent path also finds: the closest member changes sign across the +interval, i.e. it really does carry a root. + +## What this replication does not do + +- It does not make the manuscript's §7 "Recommended, not done" entry removable, and + `Table 9`'s scope line is **not** edited here. Because the primary's committed + numbers were read first, the honest wording is *"an independent re-derivation + exists, but it was written with the committed summaries in hand"*, not *"the + quartic census now has a blind second implementation"*. Suggested wording is given + in the PR body for the owner to apply or amend. +- No new Monte Carlo, no new `p_c`, no merge, no `docs/STATUS.md` edit, no change to + any existing result, script or manuscript file. +- Full repository CI has not been run. + +## Reproduce + +```sh +g++ -O3 -std=c++17 -o census_screen scripts/independent_census_screen.cpp +python scripts/independent_census.py 4 brute # weights, bound, search, decisions +python scripts/independent_census_agreement.py agreement.json +``` diff --git a/results/pslq-degree4-independent-replication/REPORT.md b/results/pslq-degree4-independent-replication/REPORT.md new file mode 100644 index 000000000..e1dfcf276 --- /dev/null +++ b/results/pslq-degree4-independent-replication/REPORT.md @@ -0,0 +1,17 @@ +# REPORT — independent degree ≤ 4, height ≤ 100 census (issue #568) + +See `notes/p568-independent-census-20260913.md` for the full write-up. + +Four search paths (local solve-based brute force, fleet naive `loop`, fleet `mitm` +split, fleet `alt` on the 2^50 lattice) return identical retained sets, and those +sets reproduce the primary's committed per-interval retention, near-set sizes, +root-bearing counts, closest members and exact residuals. + +| interval | retention | near | root-bearing | excluded | +|---|---|---|---|---| +| jacobsen-2015-eigenvalue | 0 | 1543 | 0 | true | +| mertens-2022-p-med | 3 | 1548 | 1 | false | +| mertens-2022-p-cell | 127 | 1660 | 15 | false | +| yang-zhou-2024-corrected | 0 | 1543 | 0 | true | + +Machine-readable: `latest.json`, `derived/.json`, `agreement.json`. diff --git a/results/pslq-degree4-independent-replication/agreement.json b/results/pslq-degree4-independent-replication/agreement.json new file mode 100644 index 000000000..a2dd47b4d --- /dev/null +++ b/results/pslq-degree4-independent-replication/agreement.json @@ -0,0 +1,186 @@ +{ + "schema": "matching-one/independent-census-agreement/v1", + "issue": 568, + "rows": [ + { + "interval_id": "jacobsen-2015-eigenvalue", + "screen_bound": 20077, + "retained_mine": 0, + "retained_primary": 0, + "retained_agree": true, + "retained_raw_mine": 0, + "near_mine": 1543, + "near_primary": 1543, + "near_agree": true, + "roots_mine": 0, + "roots_primary": 0, + "roots_agree": true, + "distinct_roots_mine": 0, + "distinct_roots_primary": 0, + "excluded_mine": true, + "excluded_primary": true, + "class_size_mine": 157309446881, + "class_size_primary": 157309446881, + "closest_mine": [ + -84, + 99, + -7, + 99, + 58 + ], + "closest_primary": [ + -84, + 99, + -7, + 99, + 58 + ], + "closest_agree": true, + "residual_mine_interval_min": "14904339879758404633399966390104683411388429/12207031250000000000000000000000000000000000000000000", + "residual_primary": "14904339879758404633399966390104683411388429/12207031250000000000000000000000000000000000000000000", + "residual_agree": true, + "residual_at_midpoint": "6129154435930757618067646492978382063360349/5000000000000000000000000000000000000000000000000000", + "abs_residual_diff_midpoint_vs_endpoint": "15210513238571925141887662244689836284780301/3125000000000000000000000000000000000000000000000000000", + "mvt_cap": "321/25000000000000", + "mvt_holds": true, + "residual_is_nontrivial": true, + "weights_agree": true, + "rho_agree": true + }, + { + "interval_id": "mertens-2022-p-med", + "screen_bound": 3000086, + "retained_mine": 3, + "retained_primary": 3, + "retained_agree": true, + "retained_raw_mine": 3, + "near_mine": 1548, + "near_primary": 1548, + "near_agree": true, + "roots_mine": 1, + "roots_primary": 1, + "roots_agree": true, + "distinct_roots_mine": 1, + "distinct_roots_primary": 1, + "excluded_mine": false, + "excluded_primary": false, + "class_size_mine": 157309446881, + "class_size_primary": 157309446881, + "closest_mine": [ + -84, + 99, + -7, + 99, + 58 + ], + "closest_primary": [ + -84, + 99, + -7, + 99, + 58 + ], + "closest_agree": true, + "residual_mine_interval_min": "0", + "residual_primary": "0", + "residual_agree": true, + "residual_at_midpoint": "-8084850152739502902564004414468385571/31250000000000000000000000000000000000000000000", + "abs_residual_diff_midpoint_vs_endpoint": "8084850152739502902564004414468385571/31250000000000000000000000000000000000000000000", + "mvt_cap": "963/500000000000", + "mvt_holds": true, + "residual_is_nontrivial": false, + "weights_agree": true, + "rho_agree": true + }, + { + "interval_id": "mertens-2022-p-cell", + "screen_bound": 80000077, + "retained_mine": 127, + "retained_primary": 127, + "retained_agree": true, + "retained_raw_mine": 132, + "near_mine": 1660, + "near_primary": 1660, + "near_agree": true, + "roots_mine": 15, + "roots_primary": 15, + "roots_agree": true, + "distinct_roots_mine": 15, + "distinct_roots_primary": 15, + "excluded_mine": false, + "excluded_primary": false, + "class_size_mine": 157309446881, + "class_size_primary": 157309446881, + "closest_mine": [ + -97, + 87, + 54, + 98, + 49 + ], + "closest_primary": [ + -97, + 87, + 54, + 98, + 49 + ], + "closest_agree": true, + "residual_mine_interval_min": "0", + "residual_primary": "0", + "residual_agree": true, + "residual_at_midpoint": "-5538876443206952943479490388031/625000000000000000000000000000000000000", + "abs_residual_diff_midpoint_vs_endpoint": "5538876443206952943479490388031/625000000000000000000000000000000000000", + "mvt_cap": "137/2500000000", + "mvt_holds": true, + "residual_is_nontrivial": false, + "weights_agree": true, + "rho_agree": true + }, + { + "interval_id": "yang-zhou-2024-corrected", + "screen_bound": 100065, + "retained_mine": 0, + "retained_primary": 0, + "retained_agree": true, + "retained_raw_mine": 0, + "near_mine": 1543, + "near_primary": 1543, + "near_agree": true, + "roots_mine": 0, + "roots_primary": 0, + "roots_agree": true, + "distinct_roots_mine": 0, + "distinct_roots_primary": 0, + "excluded_mine": true, + "excluded_primary": true, + "class_size_mine": 157309446881, + "class_size_primary": 157309446881, + "closest_mine": [ + -84, + 99, + -7, + 99, + 58 + ], + "closest_primary": [ + -84, + 99, + -7, + 99, + 58 + ], + "closest_agree": true, + "residual_mine_interval_min": "4744588291708108610506363461656530238349/8000000000000000000000000000000000000000000000000", + "residual_primary": "4744588291708108610506363461656530238349/8000000000000000000000000000000000000000000000000", + "residual_agree": true, + "residual_at_midpoint": "753674752984717613163342209233671226269/1220703125000000000000000000000000000000000000000", + "abs_residual_diff_midpoint_vs_endpoint": "121684105907835461950572525485785943829699/5000000000000000000000000000000000000000000000000000", + "mvt_cap": "321/5000000000000", + "mvt_holds": true, + "residual_is_nontrivial": true, + "weights_agree": true, + "rho_agree": true + } + ] +} \ No newline at end of file diff --git a/results/pslq-degree4-independent-replication/commands.txt b/results/pslq-degree4-independent-replication/commands.txt new file mode 100644 index 000000000..fd0bcd1f3 --- /dev/null +++ b/results/pslq-degree4-independent-replication/commands.txt @@ -0,0 +1,13 @@ +# screen build +g++ -O3 -std=c++17 -o census_screen scripts/independent_census_screen.cpp + +# local: solve-based brute force, scale 1e15, all four intervals and degrees 1..4 +python scripts/independent_census.py 4 brute out4 + +# fleet, 10 containers, 144 vCPU, 560 shards, run with xargs -P 12 +# loop : ./census_screen --d 4 --H 100 --B --c 1000000000000000,,,, --mode brute_loop --shard 60 out/loop--s.txt +# mitm : ./census_screen --d 4 --H 100 --B --c --mode mitm --shard 20 out/mitm--s.txt +# alt : ./census_screen --d 4 --H 100 --B --c 1125899906842624,,,, --mode brute --shard 60 out/alt--s.txt + +# agreement against the committed primary artefacts +python scripts/independent_census_agreement.py out4 agreement.json diff --git a/results/pslq-degree4-independent-replication/derived/jacobsen-2015-eigenvalue.json b/results/pslq-degree4-independent-replication/derived/jacobsen-2015-eigenvalue.json new file mode 100644 index 000000000..699227284 --- /dev/null +++ b/results/pslq-degree4-independent-replication/derived/jacobsen-2015-eigenvalue.json @@ -0,0 +1,38 @@ +{ + "interval_id": "jacobsen-2015-eigenvalue", + "lower": "0.59274605079208", + "upper": "0.59274605079212", + "scale": 1000000000000000, + "weights": [ + 592746050792100, + 351347880729631, + 208260068756662, + 123445333293203 + ], + "rho": "7686546224338895232565910573032297919/10000000000000000000000000000000000000", + "screen_bound": 20077, + "class_size": 157309446881, + "retained_raw": 0, + "retained_primitive": 0, + "root_containing_polynomials": 0, + "distinct_roots_in_interval": 0, + "excluded": true, + "closest_polynomial": [ + -84, + 99, + -7, + 99, + 58 + ], + "closest_residual": "14904339879758404633399966390104683411388429/12207031250000000000000000000000000000000000000000000", + "path_agreement": { + "local_eq_loop": true, + "local_eq_mitm": true, + "alt_superset_of_local": true, + "alt_equals_local": true, + "shard_union_size_loop": 0, + "shard_union_size_mitm": 0, + "shard_union_size_alt": 0 + }, + "root_witnesses": [] +} \ No newline at end of file diff --git a/results/pslq-degree4-independent-replication/derived/mertens-2022-p-cell.json b/results/pslq-degree4-independent-replication/derived/mertens-2022-p-cell.json new file mode 100644 index 000000000..d99c43382 --- /dev/null +++ b/results/pslq-degree4-independent-replication/derived/mertens-2022-p-cell.json @@ -0,0 +1,144 @@ +{ + "interval_id": "mertens-2022-p-cell", + "lower": "0.59274605052", + "upper": "0.59274605068", + "scale": 1000000000000000, + "weights": [ + 592746050600000, + 351347880501898, + 208260068554181, + 123445333133176 + ], + "rho": "479982034581456010007919/625000000000000000000000", + "screen_bound": 80000077, + "class_size": 157309446881, + "retained_raw": 132, + "retained_primitive": 127, + "root_containing_polynomials": 15, + "distinct_roots_in_interval": 15, + "excluded": false, + "closest_polynomial": [ + -97, + 87, + 54, + 98, + 49 + ], + "closest_residual": "0", + "path_agreement": { + "local_eq_loop": true, + "local_eq_mitm": true, + "alt_superset_of_local": true, + "alt_equals_local": true, + "shard_union_size_loop": 132, + "shard_union_size_mitm": 132, + "shard_union_size_alt": 132 + }, + "root_witnesses": [ + [ + -97, + 87, + 54, + 98, + 49 + ], + [ + -91, + 95, + 98, + -45, + 78 + ], + [ + -79, + 97, + -8, + 80, + 62 + ], + [ + -77, + 82, + 69, + -18, + 64 + ], + [ + -59, + 92, + 7, + -36, + 77 + ], + [ + -48, + 31, + 43, + 62, + 13 + ], + [ + -47, + 94, + -99, + 89, + 61 + ], + [ + -45, + 79, + -22, + -9, + 63 + ], + [ + -32, + 3, + 91, + -9, + 1 + ], + [ + -14, + -53, + 50, + 78, + 94 + ], + [ + 20, + -71, + 36, + -11, + 95 + ], + [ + 34, + -18, + -14, + -89, + 1 + ], + [ + 54, + -89, + 22, + -100, + 96 + ], + [ + 66, + -87, + -84, + 25, + 80 + ], + [ + 86, + -92, + -69, + -91, + 95 + ] + ] +} \ No newline at end of file diff --git a/results/pslq-degree4-independent-replication/derived/mertens-2022-p-med.json b/results/pslq-degree4-independent-replication/derived/mertens-2022-p-med.json new file mode 100644 index 000000000..77c809535 --- /dev/null +++ b/results/pslq-degree4-independent-replication/derived/mertens-2022-p-med.json @@ -0,0 +1,46 @@ +{ + "interval_id": "mertens-2022-p-med", + "lower": "0.592746050783", + "upper": "0.592746050789", + "scale": 1000000000000000, + "weights": [ + 592746050786000, + 351347880722399, + 208260068750233, + 123445333288121 + ], + "rho": "53129090819380871648563294193601/62500000000000000000000000000000", + "screen_bound": 3000086, + "class_size": 157309446881, + "retained_raw": 3, + "retained_primitive": 3, + "root_containing_polynomials": 1, + "distinct_roots_in_interval": 1, + "excluded": false, + "closest_polynomial": [ + -84, + 99, + -7, + 99, + 58 + ], + "closest_residual": "0", + "path_agreement": { + "local_eq_loop": true, + "local_eq_mitm": true, + "alt_superset_of_local": true, + "alt_equals_local": true, + "shard_union_size_loop": 3, + "shard_union_size_mitm": 3, + "shard_union_size_alt": 3 + }, + "root_witnesses": [ + [ + -84, + 99, + -7, + 99, + 58 + ] + ] +} \ No newline at end of file diff --git a/results/pslq-degree4-independent-replication/derived/yang-zhou-2024-corrected.json b/results/pslq-degree4-independent-replication/derived/yang-zhou-2024-corrected.json new file mode 100644 index 000000000..a33dac785 --- /dev/null +++ b/results/pslq-degree4-independent-replication/derived/yang-zhou-2024-corrected.json @@ -0,0 +1,38 @@ +{ + "interval_id": "yang-zhou-2024-corrected", + "lower": "0.5927460507895", + "upper": "0.5927460507897", + "scale": 1000000000000000, + "weights": [ + 592746050789600, + 351347880726667, + 208260068754027, + 123445333291120 + ], + "rho": "1574738498838320187782581333490561/2441406250000000000000000000000000", + "screen_bound": 100065, + "class_size": 157309446881, + "retained_raw": 0, + "retained_primitive": 0, + "root_containing_polynomials": 0, + "distinct_roots_in_interval": 0, + "excluded": true, + "closest_polynomial": [ + -84, + 99, + -7, + 99, + 58 + ], + "closest_residual": "4744588291708108610506363461656530238349/8000000000000000000000000000000000000000000000000", + "path_agreement": { + "local_eq_loop": true, + "local_eq_mitm": true, + "alt_superset_of_local": true, + "alt_equals_local": true, + "shard_union_size_loop": 0, + "shard_union_size_mitm": 0, + "shard_union_size_alt": 0 + }, + "root_witnesses": [] +} \ No newline at end of file diff --git a/results/pslq-degree4-independent-replication/latest.json b/results/pslq-degree4-independent-replication/latest.json new file mode 100644 index 000000000..2d9c724fa --- /dev/null +++ b/results/pslq-degree4-independent-replication/latest.json @@ -0,0 +1,305 @@ +{ + "schema": "matching-one/pslq-degree4-independent-replication/v1", + "issue": 568, + "date": "2026-09-13", + "role": "independent second implementation of the degree<=4, height<=100 census", + "protocol_source": "docs/manuscripts/p2-algebraic-exclusion/manuscript.md sections 3 and 5", + "implementation_disclosure": "The implementation is disjoint from scripts/degree4_interval_exclusion.py, scripts/degree4_fixed_point_screen.cpp and scripts/exact_polynomial_root_certificate.py, which were never read. It is however NOT a blind replication: the primary's committed summary artefacts (results/pslq-degree4-*/latest.json) were read before writing it, because they define the comparison. Recorded rather than passed off.", + "paths": [ + { + "tag": "local", + "description": "solve-based brute force, scale S=10^15, exact leading-coefficient solve", + "where": "workstation" + }, + { + "tag": "loop", + "description": "naive degree-4 nested enumeration, leading coefficient looped not solved, S=10^15", + "where": "Huawei fleet, 60 shards/interval" + }, + { + "tag": "mitm", + "description": "meet-in-the-middle split {0,1,2}|{3,4}, sorted right half, S=10^15", + "where": "Huawei fleet, 20 shards/interval" + }, + { + "tag": "alt", + "description": "solve-based brute force on a DIFFERENT screen lattice S=2^50", + "where": "Huawei fleet, 60 shards/interval" + } + ], + "fleet": { + "machines": 10, + "vcpu": 144, + "units": 560, + "all_completed": true, + "shards": 60 + }, + "rows": [ + { + "interval_id": "jacobsen-2015-eigenvalue", + "lower": "0.59274605079208", + "upper": "0.59274605079212", + "scale": 1000000000000000, + "weights": [ + 592746050792100, + 351347880729631, + 208260068756662, + 123445333293203 + ], + "rho": "7686546224338895232565910573032297919/10000000000000000000000000000000000000", + "screen_bound": 20077, + "class_size": 157309446881, + "retained_raw": 0, + "retained_primitive": 0, + "root_containing_polynomials": 0, + "distinct_roots_in_interval": 0, + "excluded": true, + "closest_polynomial": [ + -84, + 99, + -7, + 99, + 58 + ], + "closest_residual": "14904339879758404633399966390104683411388429/12207031250000000000000000000000000000000000000000000", + "path_agreement": { + "local_eq_loop": true, + "local_eq_mitm": true, + "alt_superset_of_local": true, + "alt_equals_local": true, + "shard_union_size_loop": 0, + "shard_union_size_mitm": 0, + "shard_union_size_alt": 0 + }, + "root_witnesses": [] + }, + { + "interval_id": "mertens-2022-p-med", + "lower": "0.592746050783", + "upper": "0.592746050789", + "scale": 1000000000000000, + "weights": [ + 592746050786000, + 351347880722399, + 208260068750233, + 123445333288121 + ], + "rho": "53129090819380871648563294193601/62500000000000000000000000000000", + "screen_bound": 3000086, + "class_size": 157309446881, + "retained_raw": 3, + "retained_primitive": 3, + "root_containing_polynomials": 1, + "distinct_roots_in_interval": 1, + "excluded": false, + "closest_polynomial": [ + -84, + 99, + -7, + 99, + 58 + ], + "closest_residual": "0", + "path_agreement": { + "local_eq_loop": true, + "local_eq_mitm": true, + "alt_superset_of_local": true, + "alt_equals_local": true, + "shard_union_size_loop": 3, + "shard_union_size_mitm": 3, + "shard_union_size_alt": 3 + }, + "root_witnesses": [ + [ + -84, + 99, + -7, + 99, + 58 + ] + ] + }, + { + "interval_id": "mertens-2022-p-cell", + "lower": "0.59274605052", + "upper": "0.59274605068", + "scale": 1000000000000000, + "weights": [ + 592746050600000, + 351347880501898, + 208260068554181, + 123445333133176 + ], + "rho": "479982034581456010007919/625000000000000000000000", + "screen_bound": 80000077, + "class_size": 157309446881, + "retained_raw": 132, + "retained_primitive": 127, + "root_containing_polynomials": 15, + "distinct_roots_in_interval": 15, + "excluded": false, + "closest_polynomial": [ + -97, + 87, + 54, + 98, + 49 + ], + "closest_residual": "0", + "path_agreement": { + "local_eq_loop": true, + "local_eq_mitm": true, + "alt_superset_of_local": true, + "alt_equals_local": true, + "shard_union_size_loop": 132, + "shard_union_size_mitm": 132, + "shard_union_size_alt": 132 + }, + "root_witnesses": [ + [ + -97, + 87, + 54, + 98, + 49 + ], + [ + -91, + 95, + 98, + -45, + 78 + ], + [ + -79, + 97, + -8, + 80, + 62 + ], + [ + -77, + 82, + 69, + -18, + 64 + ], + [ + -59, + 92, + 7, + -36, + 77 + ], + [ + -48, + 31, + 43, + 62, + 13 + ], + [ + -47, + 94, + -99, + 89, + 61 + ], + [ + -45, + 79, + -22, + -9, + 63 + ], + [ + -32, + 3, + 91, + -9, + 1 + ], + [ + -14, + -53, + 50, + 78, + 94 + ], + [ + 20, + -71, + 36, + -11, + 95 + ], + [ + 34, + -18, + -14, + -89, + 1 + ], + [ + 54, + -89, + 22, + -100, + 96 + ], + [ + 66, + -87, + -84, + 25, + 80 + ], + [ + 86, + -92, + -69, + -91, + 95 + ] + ] + }, + { + "interval_id": "yang-zhou-2024-corrected", + "lower": "0.5927460507895", + "upper": "0.5927460507897", + "scale": 1000000000000000, + "weights": [ + 592746050789600, + 351347880726667, + 208260068754027, + 123445333291120 + ], + "rho": "1574738498838320187782581333490561/2441406250000000000000000000000000", + "screen_bound": 100065, + "class_size": 157309446881, + "retained_raw": 0, + "retained_primitive": 0, + "root_containing_polynomials": 0, + "distinct_roots_in_interval": 0, + "excluded": true, + "closest_polynomial": [ + -84, + 99, + -7, + 99, + 58 + ], + "closest_residual": "4744588291708108610506363461656530238349/8000000000000000000000000000000000000000000000000", + "path_agreement": { + "local_eq_loop": true, + "local_eq_mitm": true, + "alt_superset_of_local": true, + "alt_equals_local": true, + "shard_union_size_loop": 0, + "shard_union_size_mitm": 0, + "shard_union_size_alt": 0 + }, + "root_witnesses": [] + } + ] +} \ No newline at end of file diff --git a/results/pslq-degree4-independent-replication/metadata.json b/results/pslq-degree4-independent-replication/metadata.json new file mode 100644 index 000000000..13b87ec36 --- /dev/null +++ b/results/pslq-degree4-independent-replication/metadata.json @@ -0,0 +1,13 @@ +{ + "schema": "matching-one/result-metadata/v1", + "campaign": "pslq", + "task": "pslq-degree4-independent-replication", + "issue": 568, + "date": "2026-09-13", + "role": "exact-control", + "integration_state": "branch_only", + "scientific_role": "exact-control", + "primary_dependency": "docs/manuscripts/p2-algebraic-exclusion/manuscript.md sections 3 and 5; analysis/pslq_search_contract.json", + "does_not_prove": "does not remove the manuscript's single-implementation entry; the primary's committed summaries were read before this replication was written", + "computation": {"fleet": "10 Huawei ARM containers, 144 vCPU", "units": 560, "paths": ["local", "loop", "mitm", "alt"], "all_completed": true} +} diff --git a/scripts/independent_census.py b/scripts/independent_census.py new file mode 100644 index 000000000..4c5d5d43e --- /dev/null +++ b/scripts/independent_census.py @@ -0,0 +1,293 @@ +"""Independent census of C(d, H) against the frozen P2 method intervals (issue #568). + +Everything here is derived from the protocol alone: the interval strings from +analysis/pslq_search_contract.json, and the screening statement of the P2 +manuscript section 3.2 (Theorem 2). The repository's own screen, its Sturm +decisions and its certificates are never read. + +Pipeline per (interval, degree): + + 1. weights w_k = round(S * m^k) computed in exact rational arithmetic from the + decimal midpoint, and rho = sum_k |S m^k - w_k| accumulated exactly. + 2. bound B = ceil( S * D * (u-l)/2 + H * rho ), D = H * d(d+1)/2. + 3. search delegated to census_screen (two independent paths: brute with an + exact solve for the leading coefficient, and a meet-in-the-middle + split). Both enumerate every tuple of C(d, H). + 4. decisions in exact integer arithmetic on P(x) * 10^(d*E), never in binary + floating point. Root counting uses monotonicity from the second + derivative bound plus endpoint signs -- not a Sturm chain. + 5. artifact one JSON per (degree, interval). +""" +from __future__ import annotations + +import json +import math +import os +import subprocess +import sys +from fractions import Fraction + +H = 100 +SCALE = 10 ** 15 +NEAR_SLACK = 10 ** 9 +HERE = os.path.dirname(os.path.abspath(__file__)) +BIN = os.path.join(HERE, "census_screen") + +INTERVALS = [ + ("jacobsen-2015-eigenvalue", "0.59274605079208", "0.59274605079212"), + ("mertens-2022-p-med", "0.592746050783", "0.592746050789"), + ("mertens-2022-p-cell", "0.59274605052", "0.59274605068"), + ("yang-zhou-2024-corrected", "0.5927460507895", "0.5927460507897"), +] + + +# ---------------------------------------------------------------- interval data +def decimal_parts(s: str): + """(X, E) with s == X / 10**E exactly.""" + if "." in s: + ip, fp = s.split(".") + else: + ip, fp = s, "" + return int(ip + fp), len(fp) + + +def interval_parameters(lower: str, upper: str, d: int, scale: int = SCALE): + """Return (weights[0..d], rho as Fraction, B as int, m as Fraction).""" + Xl, El = decimal_parts(lower) + Xu, Eu = decimal_parts(upper) + E = max(El, Eu) + lo = Fraction(Xl * 10 ** (E - El), 10 ** E) + up = Fraction(Xu * 10 ** (E - Eu), 10 ** E) + m = (lo + up) / 2 + weights = [scale] + rho = Fraction(0) + for k in range(1, d + 1): + exact = scale * m ** k + wk = int(exact + Fraction(1, 2)) + rho += abs(exact - wk) + weights.append(wk) + D = H * d * (d + 1) // 2 + raw = Fraction(scale) * D * (up - lo) / 2 + H * rho + B = -((-raw.numerator) // raw.denominator) # ceil of a nonnegative rational + return weights, rho, B, m, lo, up, E + + +# ---------------------------------------------------------------- class size +def mobius_sieve(n: int): + mu = [1] * (n + 1) + primes = [] + is_comp = [False] * (n + 1) + mu[0] = 0 + for i in range(2, n + 1): + if not is_comp[i]: + primes.append(i) + mu[i] = -1 + for p in primes: + if i * p > n: + break + is_comp[i * p] = True + if i % p == 0: + mu[i * p] = 0 + break + mu[i * p] = -mu[i] + return mu + + +def class_size(d: int, h: int = H) -> int: + """Proposition 1: |C(d, h)| = sum_g mu(g) floor(h/g) (2 floor(h/g) + 1)^d.""" + mu = mobius_sieve(h) + total = 0 + for g in range(1, h + 1): + if mu[g] == 0: + continue + f = h // g + total += mu[g] * f * (2 * f + 1) ** d + return total + + +def class_size_by_direct_count(d: int, h: int) -> int: + """Independent count by direct enumeration -- used only to check Proposition 1.""" + from math import gcd + n = 0 + if d == 1: + for a1 in range(1, h + 1): + for a0 in range(-h, h + 1): + if gcd(a0, a1) == 1: + n += 1 + return n + if d == 2: + for a2 in range(1, h + 1): + for a1 in range(-h, h + 1): + for a0 in range(-h, h + 1): + if gcd(gcd(a0, a1), a2) == 1: + n += 1 + return n + raise ValueError("direct count implemented for d <= 2 only") + + +# ---------------------------------------------------------------- search +def run_screen(d: int, coeffs, B: int, mode: str, shards: int = 1, shard: int = 0): + args = [BIN, "--d", str(d), "--H", str(H), "--B", str(B), + "--c", ",".join(str(c) for c in coeffs), "--mode", mode] + if shards > 1: + args += ["--shard", str(shard), str(shards)] + out = subprocess.run(args, capture_output=True, text=True, check=True).stdout + hits = [] + for line in out.splitlines(): + if not line or line.startswith("#"): + continue + parts = line.split() + hits.append([int(x) for x in parts[: d + 1]]) + return hits + + +# ---------------------------------------------------------------- exact algebra +def poly_value_scaled(coeffs, d: int, X: int, E: int) -> int: + """Return P(X / 10**E) * 10**(d*E) as an exact integer.""" + total = 0 + for k, a in enumerate(coeffs): + if a: + total += a * X ** k * 10 ** ((d - k) * E) + return total + + +def deriv_value_scaled(coeffs, d: int, X: int, E: int) -> int: + total = 0 + for k in range(1, d + 1): + a = coeffs[k] + if a: + total += k * a * X ** (k - 1) * 10 ** ((d - k + 1) * E) + return total + + +def primitivity(coeffs) -> int: + from math import gcd + g = 0 + for a in coeffs: + g = gcd(g, abs(a)) + return g + + +def decide(coeffs, d: int, lo: Fraction, up: Fraction, E: int): + """Exact decisions for one tuple. Returns a dict.""" + Xl = lo.numerator * 10 ** E // lo.denominator + Xu = up.numerator * 10 ** E // up.denominator + assert Fraction(Xl, 10 ** E) == lo and Fraction(Xu, 10 ** E) == up + + Pl = poly_value_scaled(coeffs, d, Xl, E) + Pu = poly_value_scaled(coeffs, d, Xu, E) + Xm = (Xl + Xu) // 2 + Pm = poly_value_scaled(coeffs, d, Xm, E) + Dp = deriv_value_scaled(coeffs, d, Xm, E) + D2 = sum(k * (k - 1) * abs(a) for k, a in enumerate(coeffs)) + + scale = 10 ** (d * E) + width = up - lo + # |P'(m)| > max|P''| * (u-l)/2 => P' has no zero in [l, u] => P is strictly monotone there + monotone = 2 * abs(Dp) > D2 * (width.numerator * scale) // width.denominator if D2 else True + # exact form of the same test, without integer division + monotone = Fraction(2 * abs(Dp), scale) > Fraction(D2, 2) * width + + interior_root = False + if Pl == 0 or Pu == 0: + root_kind = "endpoint" + interior_root = True + elif (Pl > 0) != (Pu > 0): + root_kind = "sign-change" if monotone else "sign-change-possibly-multiple" + interior_root = True + else: + root_kind = "none" + + min_res = min(abs(Pl), abs(Pu)) + if interior_root and (Pl == 0 or Pu == 0): + min_res = 0 + elif interior_root: + min_res = 0 # a sign change is a genuine root + return { + "coefficients_ascending": list(coeffs), + "P_at_lower_scaled": str(Pl), + "P_at_upper_scaled": str(Pu), + "P_at_midpoint_scaled": str(Pm), + "scaled_denominator": str(scale), + "minimum_absolute_residual": str(Fraction(min_res, scale)), + "monotone_on_interval": bool(monotone), + "stationary_point_possible": not bool(monotone), + "root_in_interval": bool(interior_root), + "root_kind": root_kind, + } + + +def main(): + d_max = int(sys.argv[1]) if len(sys.argv) > 1 else 4 + mode = sys.argv[2] if len(sys.argv) > 2 else "brute" + outdir = sys.argv[3] if len(sys.argv) > 3 else os.path.join(HERE, "out") + os.makedirs(outdir, exist_ok=True) + + # verify Proposition 1 against direct counting at small height + prop1_checks = [] + for d in (1, 2): + for h in (3, 5, 7): + f = class_size(d, h) + g = class_size_by_direct_count(d, h) + prop1_checks.append({"degree": d, "height": h, "formula": f, "direct": g, "agree": f == g}) + assert all(c["agree"] for c in prop1_checks), prop1_checks + + summary = [] + for iid, lower, upper in INTERVALS: + for d in range(1, d_max + 1): + weights, rho, B, m, lo, up, E = interval_parameters(lower, upper, d) + dglob = H * d * (d + 1) // 2 + hits = run_screen(d, weights, B, mode) + near = run_screen(d, weights, B + NEAR_SLACK, mode) + + decisions = [decide(h, d, lo, up, E) for h in hits] + roots = [x for x in decisions if x["root_in_interval"]] + # distinct roots: compare the exact rational brackets at high precision + distinct = len({tuple(x["coefficients_ascending"]) for x in roots}) + + near_dec = [decide(h, d, lo, up, E) for h in near] + near_prim = [x for x in near_dec if primitivity(x["coefficients_ascending"]) == 1] + closest = min(near_prim, key=lambda x: Fraction(x["minimum_absolute_residual"])) if near_prim else None + + art = { + "schema": "matching-one/independent-census/v1", + "role": "independent second implementation (issue #568)", + "interval_id": iid, "lower": lower, "upper": upper, + "degree": d, "coefficient_height_max": H, + "scale": SCALE, "weights": weights, "rho": str(rho), + "global_derivative_bound": dglob, "screen_bound": B, + "midpoint": str(m), + "class_size": class_size(d), + "search": {"mode": mode, "retained": len(hits), + "retained_primitive": sum(1 for x in decisions if primitivity(x["coefficients_ascending"]) == 1)}, + "near_bound": B + NEAR_SLACK, "near_retained": len(near), + "decisions": { + "root_containing_polynomials": len(roots), + "distinct_roots_in_interval": distinct, + "excluded": len(roots) == 0, + "with_stationary_point": sum(1 for x in decisions if x["stationary_point_possible"]), + "root_witnesses": [ + {"coefficients_ascending": x["coefficients_ascending"], "root_kind": x["root_kind"]} + for x in roots], + }, + "closest": closest, + "search_footprint": {"retained_tuples": hits}, + } + fn = os.path.join(outdir, f"census-d{d}-{iid}.json") + with open(fn, "w") as fh: + json.dump(art, fh, indent=1) + summary.append((iid, d, B, len(hits), len(roots), distinct, len(near), + closest["coefficients_ascending"] if closest else None, + closest["minimum_absolute_residual"] if closest else None)) + print(f"{iid:<28} d={d} B={B:<10} retained={len(hits):<5} roots={len(roots):<4} " + f"near={len(near):<5} closest={closest['coefficients_ascending'] if closest else None}", + flush=True) + with open(os.path.join(outdir, "summary.json"), "w") as fh: + json.dump({"prop1_checks": prop1_checks, "rows": [ + {"interval": r[0], "degree": r[1], "screen_bound": r[2], "retained": r[3], + "root_containing": r[4], "distinct_roots": r[5], "near": r[6], + "closest": r[7], "closest_residual": r[8]} for r in summary]}, fh, indent=1) + + +if __name__ == "__main__": + main() diff --git a/scripts/independent_census_agreement.py b/scripts/independent_census_agreement.py new file mode 100644 index 000000000..1cf66bc84 --- /dev/null +++ b/scripts/independent_census_agreement.py @@ -0,0 +1,130 @@ +"""Cross-check the independent census against the committed primary artefacts. + +Reads results/pslq-degree4-*/latest.json from a repository checkout and the +artefacts produced by census_driver.py, and checks, per interval: + + * screen retention, after primitivity, against root_filter_candidates + * root-carrying polynomial count and distinct-root count + * near-set size against near_candidates_exactly_checked + * the closest member, coefficient by coefficient, and its exact residual + * the mean-value residual check the ticket asks for: the closest member is + evaluated at the interval MIDPOINT here and at the ENDPOINTS by the primary, + so the two residuals MUST differ, and the difference is capped at + D_P (u-l)/2 with D_P = sum_k k|a_k| for that polynomial's own coefficients. + +No value is transcribed by hand; every primary number is read from JSON. +""" +from __future__ import annotations + +import json +import os +import sys +from fractions import Fraction + +HERE = os.path.dirname(os.path.abspath(__file__)) +sys.path.insert(0, HERE) +from census_driver import decimal_parts, poly_value_scaled, INTERVALS # noqa: E402 + + +def prim(coeffs) -> int: + from math import gcd + g = 0 + for a in coeffs: + g = gcd(g, abs(a)) + return g + + +def num(v) -> Fraction: + return Fraction(v) + + +def check(repo: str, outdir: str) -> dict: + rows = [] + for iid, lower, upper in INTERVALS: + prime = json.load(open(os.path.join(repo, "results", f"pslq-degree4-{iid}", "latest.json"))) + pr = prime["interval_result"] + mine = json.load(open(os.path.join(outdir, f"census-d4-{iid}.json"))) + + hits = [h for h in mine["search_footprint"]["retained_tuples"] if prim(h) == 1] + roots_n = mine["decisions"]["root_containing_polynomials"] + # near set: the driver keeps the raw count; count primitive ones here + from census_driver import interval_parameters, run_screen + w, rho, B, m, lo, up, E = interval_parameters(lower, upper, 4) + near = [h for h in run_screen(4, w, B + 10 ** 9, "brute") if prim(h) == 1] + + # ---- exact algebra on the primary's closest member ---- + cp = pr["closest_polynomial"]["coefficients_ascending"] + Xl, El = decimal_parts(lower) + Xu, Eu = decimal_parts(upper) + E2 = max(El, Eu) + Xl_i, Xu_i = Xl * 10 ** (E2 - El), Xu * 10 ** (E2 - Eu) + Xm = (Xl_i + Xu_i) // 2 + scale = 10 ** (4 * E2) + Pl = Fraction(poly_value_scaled(cp, 4, Xl_i, E2), scale) + Pu = Fraction(poly_value_scaled(cp, 4, Xu_i, E2), scale) + Pm = Fraction(poly_value_scaled(cp, 4, Xm, E2), scale) + Dp = sum(k * abs(a) for k, a in enumerate(cp)) + width = Fraction(Xu_i - Xl_i, 10 ** E2) + mvt_cap = Fraction(Dp) * width / 2 + if Pl == 0 or Pu == 0 or (Pl > 0) != (Pu > 0): + min_interval = Fraction(0) # IVT: a genuine root + else: + min_interval = min(abs(Pl), abs(Pu)) + primary_res = num(pr["closest_polynomial"]["minimum_absolute_residual"]) + + rows.append({ + "interval_id": iid, + "screen_bound": B, + "retained_mine": len(hits), + "retained_primary": pr["root_filter_candidates"], + "retained_agree": len(hits) == pr["root_filter_candidates"], + "retained_raw_mine": len(mine["search_footprint"]["retained_tuples"]), + "near_mine": len(near), + "near_primary": pr["near_candidates_exactly_checked"], + "near_agree": len(near) == pr["near_candidates_exactly_checked"], + "roots_mine": roots_n, + "roots_primary": pr["root_containing_polynomials"], + "roots_agree": roots_n == pr["root_containing_polynomials"], + "distinct_roots_mine": mine["decisions"]["distinct_roots_in_interval"], + "distinct_roots_primary": pr["distinct_roots_in_interval"], + "excluded_mine": mine["decisions"]["excluded"], + "excluded_primary": pr["excluded"], + "class_size_mine": mine["class_size"], + "class_size_primary": pr["primitive_quartics_covered"], + "closest_mine": (mine["closest"] or {}).get("coefficients_ascending"), + "closest_primary": cp, + "closest_agree": (mine["closest"] or {}).get("coefficients_ascending") == cp, + "residual_mine_interval_min": str(min_interval), + "residual_primary": str(primary_res), + "residual_agree": min_interval == primary_res, + "residual_at_midpoint": str(Pm), + "abs_residual_diff_midpoint_vs_endpoint": str(abs(abs(Pm) - min_interval)), + "mvt_cap": str(mvt_cap), + "mvt_holds": abs(abs(Pm) - min_interval) <= mvt_cap, + "residual_is_nontrivial": (min_interval != 0) and (min_interval > mvt_cap), + "weights_agree": [int(x) for x in w[1:]] == pr["fixed_point_weights_for_powers_1_to_4"], + "rho_agree": str(Fraction(rho)) == str(Fraction(pr["weight_rounding_error_bound_scaled"])), + }) + return {"schema": "matching-one/independent-census-agreement/v1", "issue": 568, "rows": rows} + + +if __name__ == "__main__": + repo = sys.argv[1] + outdir = sys.argv[2] + out = sys.argv[3] if len(sys.argv) > 3 else os.path.join(HERE, "agreement.json") + res = check(repo, outdir) + with open(out, "w") as fh: + json.dump(res, fh, indent=1) + print(f"{'interval':<28}{'retain':>12}{'near':>12}{'roots':>9}{'closest':>9}{'residual':>10}{'MVT':>6}") + for r in res["rows"]: + print(f"{r['interval_id']:<28}" + f"{str(r['retained_mine'])+'/'+str(r['retained_primary']):>12}" + f"{str(r['near_mine'])+'/'+str(r['near_primary']):>12}" + f"{str(r['roots_mine'])+'/'+str(r['roots_primary']):>9}" + f"{'OK' if r['closest_agree'] else 'DIFF':>9}" + f"{'OK' if r['residual_agree'] else 'DIFF':>10}" + f"{'OK' if r['mvt_holds'] else 'FAIL':>6}") + allok = all(r["retained_agree"] and r["near_agree"] and r["roots_agree"] + and r["closest_agree"] and r["residual_agree"] and r["mvt_holds"] + and r["weights_agree"] and r["rho_agree"] for r in res["rows"]) + print("\n全部一致:", allok) diff --git a/scripts/independent_census_screen.cpp b/scripts/independent_census_screen.cpp new file mode 100644 index 000000000..698f1b7a3 --- /dev/null +++ b/scripts/independent_census_screen.cpp @@ -0,0 +1,260 @@ +// Independent screening census for C(d, H) against one method interval. +// +// Written from the P2 protocol (manuscript section 3.2, Theorem 2) re-derived by +// hand: with S the scale, w_k = round(S * m^k) and c_0 = S, the integer +// +// T(a) = sum_{k=0}^{d} c_k a_k +// +// satisfies |T(a) - S P_a(m)| <= H * rho, and if P_a has a root in [l, u] then +// |P_a(m)| <= D (u-l)/2 with D the global derivative bound. Hence every +// root-carrying a obeys |T(a)| <= B = ceil(S D (u-l)/2 + H rho), and screening on +// that inequality loses nothing. +// +// The coefficients c_k, the bound B and the scale S are all supplied by the +// driver, which computes them from the interval alone. This program never reads +// the repository's own screen. +// +// Two search paths, deliberately different code: +// +// brute : nested enumeration of every tuple, with the LAST variable solved for +// exactly rather than looped. Deterministic order, no sorting. +// mitm : split the coefficient vector into a left and a right block, sort the +// (small) right block once, binary-search it from every left tuple. +// +// Both emit every a with |T(a)| <= B. `--shard k n` restricts the outermost +// variable so independent processes can cover disjoint pieces. + +#include +#include +#include +#include +#include +#include +#include +#include + +using namespace std; +typedef long long ll; + +static int D = 4, H = 100; +static ll C[8]; // C[0] = S, C[k] = w_k +static ll B = 0; +static int shardK = 0, shardN = 1; + +static inline ll fdiv(ll a, ll b) { // floor, b > 0 + ll q = a / b, r = a % b; + if (r != 0 && r < 0) --q; + return q; +} +static inline ll cdivp(ll a, ll b) { // ceil, b > 0 + ll q = a / b, r = a % b; + if (r != 0 && r > 0) ++q; + return q; +} +static inline ll iabs(ll x) { return x < 0 ? -x : x; } + +struct Rec { int a[8]; ll t; }; +static vector hits; +static ll scanned = 0; + +static inline void emit(const int *a, ll t) { + Rec r; memset(r.a, 0, sizeof r.a); + for (int k = 0; k <= D; ++k) r.a[k] = a[k]; + r.t = t; + hits.push_back(r); +} + +static void brute_d4() { + int a[8]; + for (a[0] = -H; a[0] <= H; ++a[0]) { + if (((a[0] + H) % shardN) != shardK) continue; + for (int a1 = -H; a1 <= H; ++a1) { + ll r1 = C[1] * (ll)a1; + for (int a2 = -H; a2 <= H; ++a2) { + ll r2 = r1 + C[2] * (ll)a2; + for (int a3 = -H; a3 <= H; ++a3) { + ll r3 = r2 + C[3] * (ll)a3; + for (int a4 = 1; a4 <= H; ++a4) { + ll t = C[0] * (ll)a[0] + r3 + C[4] * (ll)a4; + ++scanned; + if (iabs(t) <= B) { a[1] = a1; a[2] = a2; a[3] = a3; a[4] = a4; emit(a, t); } + } + } + } + } + } +} + +// Same enumeration, but the innermost variable is solved instead of looped. +// C[4] > 0, so |r3 + C[4] a4| <= B <=> a4 in [ceil((-B-r3)/C4), floor((B-r3)/C4)]. +static void brute_d4_solve() { + int a[8]; + for (a[0] = -H; a[0] <= H; ++a[0]) { + if (((a[0] + H) % shardN) != shardK) continue; + ll base0 = C[0] * (ll)a[0]; + for (int a1 = -H; a1 <= H; ++a1) { + ll r1 = C[1] * (ll)a1; + for (int a2 = -H; a2 <= H; ++a2) { + ll r2 = r1 + C[2] * (ll)a2; + for (int a3 = -H; a3 <= H; ++a3) { + ll r3 = r2 + C[3] * (ll)a3; + ll base = base0 + r3; + ll lo = cdivp(-B - base, C[4]); + ll hi = fdiv(B - base, C[4]); + if (lo < 1) lo = 1; + if (hi > H) hi = H; + for (ll a4 = lo; a4 <= hi; ++a4) { + ll t = base + C[4] * a4; + ++scanned; + if (iabs(t) <= B) { a[1] = a1; a[2] = a2; a[3] = a3; a[4] = (int)a4; emit(a, t); } + } + } + } + } + } +} + +// Degree d: a_d is the leading coefficient in [1, H]; a_0..a_{d-1} are in [-H, H]. +// The leading term is solved exactly from the prefix instead of looped, so the +// enumeration touches every tuple in C(d,H) but wastes no inner iterations. +static void brute_solve() { + int a[8]; + ll C0 = C[0]; + for (a[0] = -H; a[0] <= H; ++a[0]) { + if (((a[0] + H) % shardN) != shardK) continue; + ll b0 = C0 * (ll)a[0]; + if (D == 1) { + ll lo = cdivp(-B - b0, C[1]), hi = fdiv(B - b0, C[1]); + if (lo < 1) lo = 1; if (hi > H) hi = H; + for (ll x = lo; x <= hi; ++x) { ll t = b0 + C[1] * x; ++scanned; if (iabs(t) <= B) { a[1] = (int)x; emit(a, t); } } + continue; + } + for (int a1 = -H; a1 <= H; ++a1) { + ll b1 = b0 + C[1] * (ll)a1; + if (D == 2) { + ll lo = cdivp(-B - b1, C[2]), hi = fdiv(B - b1, C[2]); + if (lo < 1) lo = 1; if (hi > H) hi = H; + for (ll x = lo; x <= hi; ++x) { ll t = b1 + C[2] * x; ++scanned; if (iabs(t) <= B) { a[1] = a1; a[2] = (int)x; emit(a, t); } } + continue; + } + for (int a2 = -H; a2 <= H; ++a2) { + ll b2 = b1 + C[2] * (ll)a2; + if (D == 3) { + ll lo = cdivp(-B - b2, C[3]), hi = fdiv(B - b2, C[3]); + if (lo < 1) lo = 1; if (hi > H) hi = H; + for (ll x = lo; x <= hi; ++x) { ll t = b2 + C[3] * x; ++scanned; if (iabs(t) <= B) { a[1] = a1; a[2] = a2; a[3] = (int)x; emit(a, t); } } + continue; + } + for (int a3 = -H; a3 <= H; ++a3) { + ll b3 = b2 + C[3] * (ll)a3; + ll lo = cdivp(-B - b3, C[4]), hi = fdiv(B - b3, C[4]); + if (lo < 1) lo = 1; if (hi > H) hi = H; + for (ll x = lo; x <= hi; ++x) { ll t = b3 + C[4] * x; ++scanned; if (iabs(t) <= B) { a[1] = a1; a[2] = a2; a[3] = a3; a[4] = (int)x; emit(a, t); } } + } + } + } + } +} + +// Degree 4, leading variable looped rather than solved: used only as a slow +// cross-check that the exact solve loses nothing. +static void brute_d4_loop() { + int a[8]; + for (a[0] = -H; a[0] <= H; ++a[0]) { + if (((a[0] + H) % shardN) != shardK) continue; + ll b0 = C[0] * (ll)a[0]; + for (int a1 = -H; a1 <= H; ++a1) { + ll b1 = b0 + C[1] * (ll)a1; + for (int a2 = -H; a2 <= H; ++a2) { + ll b2 = b1 + C[2] * (ll)a2; + for (int a3 = -H; a3 <= H; ++a3) { + ll b3 = b2 + C[3] * (ll)a3; + for (int a4 = 1; a4 <= H; ++a4) { + ll t = b3 + C[4] * (ll)a4; + ++scanned; + if (iabs(t) <= B) { a[1] = a1; a[2] = a2; a[3] = a3; a[4] = a4; emit(a, t); } + } + } + } + } + } +} + +// --------------------------------------------------------------------------- +// mitm for d = 4: left block {0,1,2}, right block {3,4}. +// --------------------------------------------------------------------------- +struct REnt { ll val; int a3, a4; }; +static bool rless(const REnt &x, const REnt &y) { return x.val < y.val; } + +static void mitm_d4() { + vector R; + R.reserve((size_t)(2 * H + 1) * H); + for (int a3 = -H; a3 <= H; ++a3) + for (int a4 = 1; a4 <= H; ++a4) + R.push_back({C[3] * (ll)a3 + C[4] * (ll)a4, a3, a4}); + sort(R.begin(), R.end(), rless); + vector keys(R.size()); + for (size_t i = 0; i < R.size(); ++i) keys[i] = R[i].val; + + int a[8]; + for (a[0] = -H; a[0] <= H; ++a[0]) { + if (((a[0] + H) % shardN) != shardK) continue; + ll b0 = C[0] * (ll)a[0]; + for (int a1 = -H; a1 <= H; ++a1) { + ll b1 = b0 + C[1] * (ll)a1; + for (int a2 = -H; a2 <= H; ++a2) { + ll L = b1 + C[2] * (ll)a2; + ll want = -L; + size_t lo = lower_bound(keys.begin(), keys.end(), want - B) - keys.begin(); + size_t hi = upper_bound(keys.begin(), keys.end(), want + B) - keys.begin(); + for (size_t i = lo; i < hi; ++i) { + ll t = L + R[i].val; + ++scanned; + if (iabs(t) <= B) { a[1] = a1; a[2] = a2; a[3] = R[i].a3; a[4] = R[i].a4; emit(a, t); } + } + } + } + } +} + +int main(int argc, char **argv) { + const char *mode = "brute"; + const char *outpath = nullptr; + for (int i = 1; i < argc; ++i) { + if (!strcmp(argv[i], "--mode") && i + 1 < argc) mode = argv[++i]; + else if (!strcmp(argv[i], "--shard") && i + 2 < argc) { shardK = atoi(argv[++i]); shardN = atoi(argv[++i]); } + else if (!strcmp(argv[i], "--d") && i + 1 < argc) D = atoi(argv[++i]); + else if (!strcmp(argv[i], "--H") && i + 1 < argc) H = atoi(argv[++i]); + else if (!strcmp(argv[i], "--B") && i + 1 < argc) B = atoll(argv[++i]); + else if (!strcmp(argv[i], "--c") && i + 1 < argc) { + char *p = argv[++i]; + int k = 0; + for (char *tok = strtok(p, ","); tok && k <= D; tok = strtok(nullptr, ",")) C[k++] = atoll(tok); + } else outpath = argv[i]; + } + if (shardN < 1) shardN = 1; + + auto t0 = chrono::steady_clock::now(); + if (!strcmp(mode, "brute_loop")) { brute_d4_loop(); } + else if (!strcmp(mode, "mitm")) { + if (D != 4) { fprintf(stderr, "mitm implemented for d=4 only\n"); return 2; } + mitm_d4(); + } else { + if (D < 1 || D > 4) { fprintf(stderr, "unsupported degree %d\n", D); return 2; } + brute_solve(); + } + double secs = chrono::duration(chrono::steady_clock::now() - t0).count(); + + FILE *f = outpath ? fopen(outpath, "w") : stdout; + if (!f) { fprintf(stderr, "cannot open %s\n", outpath); return 2; } + fprintf(f, "# degree %d height %d mode %s shard %d/%d B %lld hits %zu scanned %lld seconds %.3f\n", + D, H, mode, shardK, shardN, B, hits.size(), scanned, secs); + for (const Rec &r : hits) { + for (int k = 0; k <= D; ++k) fprintf(f, "%d ", r.a[k]); + fprintf(f, "%lld\n", r.t); + } + if (outpath) fclose(f); + fprintf(stderr, "degree=%d H=%d mode=%s shard=%d/%d B=%lld hits=%zu scanned=%lld t=%.3fs\n", + D, H, mode, shardK, shardN, B, hits.size(), scanned, secs); + return 0; +}