diff --git a/research/b2-mas-edge-form-seed3609249d/README.md b/research/b2-mas-edge-form-seed3609249d/README.md new file mode 100644 index 0000000000..eb176d7476 --- /dev/null +++ b/research/b2-mas-edge-form-seed3609249d/README.md @@ -0,0 +1,228 @@ +# The MAS edge form of Theorem B2 (iii) is false: two exact counterexamples + +**Scoped negative result; no kappa, supplier, certificate or frontier claim.** The +selected record, both suppliers and `upstream/` are unchanged. + +This package answers the open next question 1 of the CR2/B2 audit +([PR 2293](https://github.com/CrocSwap/integer-mult-bounds/pull/2293)), itself the +follow-up of **item 2** of the open independent-check request +[discussion comment 18934590](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-18934590): +does the *edge* reading of `MAS(W[F])` hold, that is + +```text +cost(B) >= v - |H| - |F| + masE +``` + +for every rank-3 decoder configuration and every admissible pairing `B`, where +`masE` is the largest acyclic edge subset of the wild digraph `W[F]`? The printed +proof of [PR 2162](https://github.com/CrocSwap/integer-mult-bounds/pull/2162) +(Theorem B2 (iii)) yields only the *vertex* form with `masV` (PR 2293 finding 4). + +**Answer: no.** The edge form is false. Two exact counterexamples are given +below (five and six lines, all full support). The vertex form survives every +instance of this package's domain. The model, statements and license are +DreamingOfClouds's; this package imports no predecessor implementation. + +## Source pins + +| Item | Pin | +|---|---| +| Base main | `0fdd7d82de03e43c9e5a1000dfbcd380d1b687d2` | +| Audited source | [PR 2162](https://github.com/CrocSwap/integer-mult-bounds/pull/2162) head `113a718265c62aec301c5695f4bfb9c421bef7ab`, `research/char2-jets/README.md` (25888 bytes, SHA-256 `60beed587a355b6b04e61053fc123fb8ebe5d0d75d9dbd065f24138c55a2e437`) | +| Predecessor audit | [PR 2293](https://github.com/CrocSwap/integer-mult-bounds/pull/2293) head `6bc48613ed1c71e5d2e88994235e9e8629129b9c`, `research/cr2-b2-audit-seed4f435ab7/` | + +The predecessor files are PR-head-only (not in the base tree), so they are pinned +here and in `TASK.json` by head hash rather than in `SOURCES.json`, which resolves +blobs at the base commit. The verifier is self-contained. + +## Model (PR 2162 section 1, re-derived) + +A configuration is `v` lines with rational vectors `p(t), q(t)` in `Q^3`, +`p(t) . q(t) != 0`. An admissible pairing `B` is a 0/1 matrix over `F2` with unit +diagonal and `B_ts = 1` (`t != s`) only where `p(t) . q(s) = 0`. +`cost(B) = sum_j rank_F2 B[R_j, A_j]` over the three coordinate supports +(`R_j = {t : p(t)_j != 0}`, `A_j = {s : q(s)_j != 0}`). `H` is the set of harmonic +lines, `F` the lines with both supports full, `W` the wild incidences (a wild pair +forces both endpoints into `F`). `masV` is the largest `A subseteq F` with `W[A]` +acyclic (vertex count); `masE` is the largest acyclic edge subset of `W[F]` +(edge count, the literal reading of "maximum acyclic subset"). + +## Counterexample 1 (smallest in the declared domain): v = 5, all full support + +```text +p(0) = (-1, -1, 3) q(0) = (1, 1, 2) +p(1) = ( 1, -3, 1) q(1) = (1, 2, 1) +p(2) = ( 3, -1, -1) q(2) = (2, 1, 1) +p(3) = ( 1, -3, 1) q(3) = (1, 2, 1) +p(4) = ( 3, -1, -1) q(4) = (2, 1, 1) +``` + +All supports are full, so `F = {0,1,2,3,4}` and `H = {}` (`|D| = 3` on every +line). Lines 1 and 3 coincide, as do lines 2 and 4: the duplicated `q` +directions are what defeats the edge form. Exact computed data (two independent +rank implementations agree): + +| Quantity | Value | +|---|---:| +| wild pairs in `W` (both directions counted) | 16 | +| admissible free pairs | 16 | +| `masV` | 2 | +| `masE` | 8 | +| vertex RHS `v - |H| - |F| + masV` | 2 | +| edge RHS `v - |H| - |F| + masE` | 8 | +| exact minimum of `cost(B)` over all `2^16` admissible `B` | 6 | + +The exact minimum `6` is attained by the admissible pairing with rows +`10110, 01001, 10110, 10110, 01001` (bit `s` of row `t` is `B_ts`), recomputed by +the independent list-of-lists rank implementation. Every admissible `B` has +`cost(B) >= 6` (complete enumeration), while the edge form demands `>= 8`: +**the edge form fails with gap 2**. The vertex form holds trivially here +(`6 >= 2`). + +Since all supports are full, `cost(B) = 3 rank_F2(B)` (three identical blocks). +The counterexample is therefore also a statement about ranks: an admissible +unit-diagonal `B` of rank 2 exists while `masE = 8 > 6 = 3 rank_F2(B)`. + +## Counterexample 2: v = 6, all full support + +`twin_q_v6#138` (same direction-class family; data frozen in the digest): +`masE = 11`, edge RHS `11`, exact minimum of `cost(B)` over all `2^22` +admissible pairings `9`. Gap 2 again. The witness is re-minimised exhaustively +and recomputed independently by `verify.py` at every run. + +## Why the edge form fails, and what survives + +`masE` counts forward wild edges in an acyclic order. Between two lines with the +same `q` direction every wild partner is shared, so both directions of a pair +can contribute to different edge sets while the block ranks of `B` pay for the +pair only once. The X-form of Theorem B2 (the printed proof) optimises over +acyclic *vertex* sets and is not affected; the machine-checked identity +`xbest = v - |H| - |F| + masV` holds on all 139 instances. + +Two positive statements, proved in `verify.py` and the arguments below: + +**P1 (complete pairs are impossible at `v >= 4` in `Q^3`).** If +`p(t) . q(s) = 0` for all `t != s` then every triple of the `q(s)` is linearly +dependent (else the `p(t)` orthogonal to that triple would be zero), so all four +or more `q`'s lie in a plane `P`; the three `q`'s of any `t` either span `P` +(then `p(t) . q(t) = 0`, contradiction) or are all proportional (then all `q`'s +are proportional and the same contradiction follows). Consequently `B = J` is +inadmissible and every admissible `B` at `v >= 4` all-full has +`rank_F2(B) >= 2`. This is machine-checked on every all-full instance with +`v >= 4` in the domain (`p1_no_complete_pairs_v_ge_4`). + +**P2 (the edge form holds for all-full `v <= 4`).** For all-full configurations +`H = {}`, `cost(B) = 3 rank_F2(B)` and `masE <= v(v-1)/2`. At `v <= 3`: +`cost(B) >= 3 >= masE`. At `v = 4`: `rank_F2(B) >= 2` by P1, so +`cost(B) >= 6 >= masE`. So the edge form is true exactly on the small side and +fails first at `v = 5`, consistent with the search (no all-full falsifier below +`v = 5`). + +**P3 (`masE` can exceed `|F|` over `Q^3`).** The hub/coplanar-`q` family +(`gen_hub`) realises `masE = 5 > 4 = |F|` at `v = 4`, with nine directed wild +edges; the direction-class family realises `masE - |F|` up to 5 in the declared +domain. So the edge form, when it holds, can demand strictly more than +`v - |H|`; it is not a weakened restatement of the no-harmonic baseline. + +**Concurrent work.** While this package was being written, ROTl24 independently +falsified the same edge reading with a nine-line tripartite construction +(`cost(B) = 21 < masE = 27`) and a parametric odd-`k` family with unbounded gap +`3(k-1)(k-2)`: +[PR 2334](https://github.com/CrocSwap/integer-mult-bounds/pull/2334), +[discussion 2331](https://github.com/CrocSwap/integer-mult-bounds/discussions/2331). +Both answer PR 2293's open question 1 and were claimed independently. This +package contributes the smaller counterexample (minimum-size among +all-full-support configurations by P2), two complete minima from a second +independent engine, the 139-instance vertex-form screen, and P1/P3. + +## Machine evidence + +`verify.py` re-implements the model independently (exact integers, F2 bitsets, +second rank implementation, symbolic-free) and screens both readings of (iii) +smallest-instance-first over a declared deterministic domain (seed `20261015`, +entries in `{-2,-1,1,2}`, `v = 3..8`): random all-full configurations, random +mixed-support configurations, cross-product dense-3 cores, hub/coplanar-`q` +cores, and direction-class (twin-`q`) near-dense wild cores. Every instance at +`free <= 15` is minimised exhaustively, as are the first four instances up to +`free = 20` and every falsifier whatever its size; the two largest instances +(`free = 21, 22`) are screened heuristically first, and any candidate `B` is +always scored exactly. + +```text +PASS_B2_EDGE_SCREEN instances=139 exact=137 heuristic_only=2 max_free=22 +BOUND iii_edge: FALSIFIER v=5 free=16 mincost=6 edge_rhs=8 masE=8 name=twin_q_v5#137 +BOUND iii_edge: FALSIFIER v=6 free=22 mincost=9 edge_rhs=11 masE=11 name=twin_q_v6#138 +BOUND iii_vertex: no falsifier in declared domain +IDENTITY xbest=vertex_rhs: ok on 139/139 +CONTROLS ok {...} +SUMMARY tight_edge=6 tight_vertex=1 masE_gt_masV=63 masE_gt_absF=31 max_masE_minus_absF=5 +``` + +Controls (all pass, each with a failure mode it must exhibit): fixture with +analytic minimum 2; the dense three-line fixture of PR 2293 (`masE = 3 > +masV = 1`, exact minimum 3, tight for the edge form); the hub fixture +(`masE = 5 > |F| = 4`, `masV = 2`, exact minimum 6); harmonic-line +classification; a strengthened edge bound `+1` falsified on a fixture +(sensitivity); a mutated configuration changing the free-pair set (sensitivity); +the two-rank-implementation cross-check; and P1 over the domain. The summary and +an instance digest are frozen in `RECEIPT.json` and compared at every run. + +**What this establishes.** In the declared domain, the edge reading of +`MAS(W[F])` in Theorem B2 (iii) is refuted by two exactly checked +configurations; the vertex reading (what the printed proof gives, PR 2293 +finding 4) has no falsifier, and the identity `xbest = v - |H| - |F| + masV` +holds throughout. PR 2293's open question 1 is therefore resolved negatively: +the printed gloss should be corrected to the vertex form rather than upgraded to +the edge form. + +**Not checked.** `v > 8`, entries outside `{-2..2}`, `T != 3`, Lemma VCR2, +Corollary J, Theorem T-prime, Lemma F, the split min-max of PR 2162 section 3, +target (A) itself, and any kappa/supplier implication. Two instances at +`free = 21, 22` were not exhaustively enumerated before the falsifier +confirmation step (both falsifiers were). This is a finite counterexample claim, +not an impossibility theorem for repaired edge-type bounds. + +## Reproduce + +From the repository root, standard library only (CPython 3.12 registered): + +```sh +python3 -B research/b2-mas-edge-form-seed3609249d/verify.py +python3 scripts/research_package.py --package research/b2-mas-edge-form-seed3609249d --check-only +``` + +Expected: the block above, ending `RECEIPT_MATCH` (about two to five minutes; +the falsifier confirmation re-runs the `2^16` and `2^22` enumerations). + +## Open next questions + +1. **What is the strongest rank-aware replacement for `masE`?** The counterexamples + suggest collapsing twin `q` directions before counting acyclic edges (both + falsifiers come from duplicated `q` directions). Why it matters: a corrected + edge-type term could still strengthen Theorem B2 (iii) beyond `masV`. + First step: re-run this domain with `masE` computed on the `q`-direction + quotient and test `cost(B) >= v - |H| - |F| + masE_quotient`. Blocked by + nothing; a small successor screen. +2. **Is the vertex form itself attainable-tight on wild-cycle cores at larger + `v`?** PR 2293's open question 2 stands: a violation would falsify Theorem + B2's X-form, which no instance of either package does. First step: targeted + `v = 8` structured cores with exact enumeration past `free = 22`. + Blocked by the `2^free` exhaustive cost; a SAT/DRAT encoding like + [PR 2206](https://github.com/CrocSwap/integer-mult-bounds/pull/2206) is the + natural next tool. + +## Credit + +Prepared by Aaron Wang, with help from opencode (substantial AI assistance; no +independent human review claimed). The model, the statements of Lemma CR2 and +Theorem B2 and the configuration families audited here are DreamingOfClouds's +work in [PR 2162](https://github.com/CrocSwap/integer-mult-bounds/pull/2162) / +[PR 2111](https://github.com/CrocSwap/integer-mult-bounds/pull/2111) / +[PR 2125](https://github.com/CrocSwap/integer-mult-bounds/pull/2125). The MAS +gap, the vertex-form identity and the 58-instance audit are Aaron Wang's in +[PR 2293](https://github.com/CrocSwap/integer-mult-bounds/pull/2293); this +package answers that audit's open question 1. Context: request items 1 and 4 +were closed by [PR 2193](https://github.com/CrocSwap/integer-mult-bounds/pull/2193) +and [PR 2176](https://github.com/CrocSwap/integer-mult-bounds/pull/2176), item 3 +by [PR 2272](https://github.com/CrocSwap/integer-mult-bounds/pull/2272). +New work in this package is Apache-2.0. diff --git a/research/b2-mas-edge-form-seed3609249d/RECEIPT.json b/research/b2-mas-edge-form-seed3609249d/RECEIPT.json new file mode 100644 index 0000000000..e38852fbad --- /dev/null +++ b/research/b2-mas-edge-form-seed3609249d/RECEIPT.json @@ -0,0 +1,29 @@ +{ + "schema_version": 1, + "note": "Frozen expected summary of verify.py at seed 20261015, domain per README. The edge form of Theorem B2 (iii) is falsified by twin_q_v5#137; the vertex form survives.", + "summary": { + "instances": 139, + "exact": 137, + "heuristic_only": 2, + "max_free": 22, + "tight_edge": 6, + "tight_vertex": 1, + "masE_gt_masV": 63, + "masE_gt_absF": 31, + "max_masE_minus_absF": 5, + "edge_falsifiers": 2, + "vertex_falsifiers": 0, + "ident_ok": true, + "controls_ok": true + }, + "digest": "fcd09a7ae61ef065f563af5db57181c133f2ae348e4266391cfdfc6b689450a6", + "falsifier": { + "name": "twin_q_v5#137", + "v": 5, + "free": 16, + "masE": 8, + "masV": 2, + "edge_rhs": 8, + "mincost": 6 + } +} diff --git a/research/b2-mas-edge-form-seed3609249d/SOURCES.json b/research/b2-mas-edge-form-seed3609249d/SOURCES.json new file mode 100644 index 0000000000..392737aa2a --- /dev/null +++ b/research/b2-mas-edge-form-seed3609249d/SOURCES.json @@ -0,0 +1,18 @@ +{ + "schema_version": 1, + "base_commit": "0fdd7d82de03e43c9e5a1000dfbcd380d1b687d2", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "ae6a99f28aa468649eb66a361e764d769363bf11", + "sha256": "10b9e340fd8e354a37a0c4813c90e5de1dd42044b5f6aca4a3fc5a42b685fa32" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "e8870e5917057d59b730eb14721a778639eca050", + "sha256": "d46eb6d5b3e279428753d770653663fbdf1063e55c255ea073d768f344927ef7" + } + ] +} diff --git a/research/b2-mas-edge-form-seed3609249d/TASK.json b/research/b2-mas-edge-form-seed3609249d/TASK.json new file mode 100644 index 0000000000..ef5e1d3052 --- /dev/null +++ b/research/b2-mas-edge-form-seed3609249d/TASK.json @@ -0,0 +1,78 @@ +{ + "schema_version": 1, + "task_id": "independent-moment", + "priority_revision": 4, + "base_commit": "0fdd7d82de03e43c9e5a1000dfbcd380d1b687d2", + "original_card": { + "id": "independent-moment", + "question": "Does one changed supplier or assembly claim lack a source-bound independent check of a specific new implication?", + "starting_points": [ + "certificates/selected-result.json" + ], + "methods": [ + "Reconstruct the rank ledger from original operations rather than trusting its aggregate.", + "Implement certified moment inequalities through a different exact enclosure method." + ], + "acceptance_gate": "Demonstrate independence, source binding, positive cases and semantic failure controls. Name the existing checks and the missing coverage. More digits or another equivalent evaluation of an unchanged root is not by itself new verification coverage.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Record the selected certificate and complex_profile rather than taking a PR headline as input.", + "scope": "Positive control / source-bound orientation only; this is not a new construction or full cold replay." + }, + "first_experiment": "List the existing independent checks for the exact selected or candidate sources. Pick a new changed input, missing binding or distinct failure mode; stop with a handoff if the proposed arithmetic check is already covered.", + "bottleneck_link": "Independent pricing prevents unsupported frontier claims and can reveal genuine accounting slack.", + "allowed_variations": [ + "Reconstruct either a source ledger or a numeric enclosure with a different method." + ], + "scope_change_triggers": [ + "Importing the primary function and calling its output independent verification." + ], + "overlap_terms": [ + "independent moment", + "rank histogram", + "exact enclosure" + ] + }, + "task_card": { + "task_id_and_scope_key": "independent-moment (drawn card, scope key c6f2494b197df3bc3591); refined object below; chooser OS nonce 3609249d721856396bd250df31a8cc48", + "base_commit_and_predecessors": "Base main 0fdd7d82de03e43c9e5a1000dfbcd380d1b687d2. Predecessor heads: PR 2162 head 113a718265c62aec301c5695f4bfb9c421bef7ab (audited source, research/char2-jets/README.md, 25888 bytes, SHA-256 60beed587a355b6b04e61053fc123fb8ebe5d0d75d9dbd065f24138c55a2e437); PR 2293 head 6bc48613ed1c71e5d2e88994235e9e8629129b9c (cr2-b2-audit-seed4f435ab7, whose open next question 1 is exactly this object).", + "concrete_object_and_question": "The MAS edge form of Theorem B2 (iii): in the PR 2162 rank-3 decoder model (v lines with rational p(t), q(t) in Q^3, p(t).q(t) != 0; admissible 0/1 pairing B with unit diagonal and B_ts = 1 only where p(t).q(s) = 0; cost(B) = sum_j rank_F2 B[R_j, A_j] over the three coordinate supports), does cost(B) >= v - |H| - |F| + masE hold for every configuration and every admissible B, where masE is the maximum acyclic edge subset of the wild digraph W[F]? The printed proof of PR 2162 only yields the vertex form with masV (PR 2293 finding 4).", + "scope_status": "changed", + "scope_change_reason": "The drawn cards formal-interface-lemma and independent-moment are saturated at their generic level (find_overlap shows dozens of local packages on both cards' overlap terms). Request item 5 of discussion comment 18934590 (Lean core extension) is blocked: no Lean toolchain on this host and the disk budget forbids installing one. Request item 1 is covered by open PR 2193. Per the donation prompt this takes the explicit open follow-up of request item 2 instead: PR 2293's open next question 1 asks exactly whether the edge form holds in general. The card premise (an unverified specific implication of a submitted claim) is kept; the object is moved from the selected stock ledger to Theorem B2 (iii) of PR 2162.", + "existing_restriction_changed": "Nothing in the audited claim is changed. The vertex form (proof-backed) is kept as the reference; the strictly stronger edge reading of MAS(W[F]) is the claim under test.", + "method_and_domain": "Independent stdlib-Python re-implementation of the model (exact integers, F2 bitset ranks with a second independent rank implementation cross-checked, symbolic-free). (1) Positive fixtures with analytic answers; (2) smallest-falsifying-instance-first search: exhaustive exact minimum of cost(B) over all admissible B where the admissible-pair count is within the declared cap, branch-and-bound with a monotone zero-pattern matching lower bound beyond it, and a heuristic minimiser whose best candidate is always re-checked exactly; (3) targeted families: all-full-support cores at v = 3..7 (cross-product cores, hub/coplanar-q cores with dense wild graphs, my hand construction with masE > |F|), and mixed-support configurations at v = 5..8; entries in {-2,-1,1,2}. Fixed domain and seeds; finite results only.", + "nearest_overlapping_work": "PR 2293 (predecessor; tested both readings only at v <= 7, free <= 17, left the edge form open; this package extends v, wild density and the exact-enumeration reach and adds the all-full-support v <= 4 proposition). PR 2162 (source). PR 2193 / PR 2176 / PR 2272 closed the other request items. find_overlap over 'edge form', 'masE', 'MAS(W[F])', 'wild cycle', 'Theorem B2', 'cross-product core', 'admissible pairing' at 2026-10-15 05:16Z returned only these predecessors and the wider decoder PRs (2111/2125/2137/2206/2228/2232/2244), none testing the edge form.", + "budget": "Audit, not a construction: the a < D/E moment diagnostic and the whole-construction budget do not apply (no supplier, no kappa claim). Compute cap: the verifier's declared deterministic domain runs in under ~8 minutes on CPython 3.12; no further search after the first falsifier or after the domain is exhausted.", + "success_evidence_and_falsification": "Either the smallest exact counterexample (a configuration plus one exactly checked admissible B with cost below v - |H| - |F| + masE) or a scoped no-falsifier statement over the declared domain with exact minima and tightness statistics. Failure controls: fixtures with analytic minima must reproduce; a deliberately strengthened bound (+1) must be falsified on a fixture; the B&B minimum must equal the exhaustive minimum on every instance where both run.", + "predecessor_authors_and_artifact": "Model, statements and configuration families: DreamingOfClouds (PR 2162 / PR 2111 / PR 2125). MAS gap and 58-instance audit: Aaron Wang with help from opencode (PR 2293). Intended artifact: research/b2-mas-edge-form-seed3609249d/ with verify.py and a frozen receipt; reproduce with python3 -B research/b2-mas-edge-form-seed3609249d/verify.py and scripts/research_package.py --package research/b2-mas-edge-form-seed3609249d --check-only." + }, + "scope_status": "changed", + "actual_scope": "Settle or advance the MAS edge form cost(B) >= v - |H| - |F| + masE of Theorem B2 (iii) (PR 2162): exact falsifier search smallest-instance-first over a declared domain of near-dense wild cores at v = 3..8, plus a written all-full-support v <= 4 proposition and the complete-pair impossibility lemma behind it.", + "scope_change_reason": "Drawn cards formal-interface-lemma and independent-moment are saturated generically; request item 5 (Lean) is blocked by missing tooling and item 1 is covered by open PR 2193. This takes the explicit open follow-up of request item 2 (discussion comment 18934590): PR 2293 open next question 1, the MAS edge-form reading of Theorem B2 (iii).", + "bottleneck_link": "A scoped audit of a submitted implication, not a bottleneck lever: it either strengthens Theorem B2 (iii) with a proof-backed statement or records the smallest counterexample, preventing an unsupported lemma from being carried into the rank-3 decoder chain that feeds the T = 3 open core (Q <= F2).", + "budget_minutes": 60, + "stop_rule": "Stop at the first exact counterexample (report it smallest-first) or when the declared deterministic domain is exhausted; one bounded pivot maximum (pivot: switch the search to all-full-support cores after the mixed-support tier); no search beyond the declared domain.", + "outcome": "completed", + "evidence": "Counterexample found and exactly confirmed: the MAS edge form of Theorem B2 (iii) is false. Smallest in the declared domain: v=5 all-full direction-class configuration (twin_q_v5#137, p/q data in README and verify.py output), 16 wild pairs, masE=8, edge RHS 8, exact minimum of cost(B) over all 2^16 admissible pairings = 6 (attained by a rank-2 unit-diagonal B, recomputed with the independent rank implementation). Second counterexample twin_q_v6#138: v=6, masE=11, edge RHS 11, exact minimum over 2^22 pairings = 9. The vertex form has no falsifier in 139 instances and the identity xbest = v - |H| - |F| + masV holds on all of them. Controls all pass; summary and digest frozen in RECEIPT.json (RECEIPT_MATCH). Propositions P1 (no complete zero-dot pairs at v >= 4 in Q^3) and P2 (edge form holds for all-full v <= 4) are proved in the README and machine-checked over the domain.", + "author": "Aaron Wang", + "ai_assistance": "Substantial AI assistance (opencode); no independent human review claimed.", + "open_questions": [ + { + "question": "What is the strongest rank-aware replacement for masE? The two counterexamples both come from duplicated q directions, where reciprocal wild pairs inflate masE while the block ranks of B pay once.", + "why_it_matters": "A corrected edge-type term could still strengthen Theorem B2 (iii) beyond the vertex form without new machinery in PR 2162's jet framework.", + "first_step": "Re-run this package's domain with masE computed on the q-direction quotient and test cost(B) >= v - |H| - |F| + masE_quotient.", + "blocked_by": "Nothing; a small successor screen." + }, + { + "question": "Is the vertex form attainable-tight on wild-cycle cores at larger v (PR 2293 open question 2)?", + "why_it_matters": "A violation would falsify Theorem B2's X-form, which neither this package nor PR 2293 does.", + "first_step": "Targeted v = 8 structured cores with exact enumeration past free = 22.", + "blocked_by": "The 2^free exhaustive cost; a SAT/DRAT encoding like PR 2206 is the natural next tool." + } + ] +} diff --git a/research/b2-mas-edge-form-seed3609249d/VERIFY.json b/research/b2-mas-edge-form-seed3609249d/VERIFY.json new file mode 100644 index 0000000000..ad389c8dfb --- /dev/null +++ b/research/b2-mas-edge-form-seed3609249d/VERIFY.json @@ -0,0 +1,18 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [], + "commands": [ + { + "argv": [ + "{python}", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 600, + "checks": "PASS_B2_EDGE_SCREEN over 139 declared instances; both readings of Theorem B2 (iii) screened smallest-falsifier-first; two exactly confirmed edge-form falsifiers reported; the xbest vertex identity machine-checked on every instance; analytic fixtures, a strengthened-bound sensitivity control, a mutation sensitivity control, the harmonic classification control and the two-rank-implementation cross-check must all pass; output ends RECEIPT_MATCH against the frozen summary and digest." + } + ] +} diff --git a/research/b2-mas-edge-form-seed3609249d/verify.py b/research/b2-mas-edge-form-seed3609249d/verify.py new file mode 100644 index 0000000000..691a5abe99 --- /dev/null +++ b/research/b2-mas-edge-form-seed3609249d/verify.py @@ -0,0 +1,728 @@ +#!/usr/bin/env python3 +"""Independent exact screen of the MAS edge form of Theorem B2 (iii) (PR #2162). + +Question under test (PR #2293 open next question 1): does + + cost(B) >= v - |H| - |F| + masE + +hold for every rank-3 decoder configuration and every admissible pairing B, +where masE is the largest acyclic edge subset of the wild digraph W[F]? The +printed proof of PR #2162 yields only the vertex form with masV (PR #2293 +finding 4). No predecessor implementation is imported; the model is +re-implemented from the pinned statements quoted in README.md. All arithmetic +is exact (Python ints, F2 bitsets). Deterministic generation; the summary is +compared against RECEIPT.json. + +Run: python3 -B research/b2-mas-edge-form-seed3609249d/verify.py +""" +import hashlib +import itertools +import json +import os +import random +import sys + +HERE = os.path.dirname(os.path.abspath(__file__)) + +EXACT_FREE_CAP_BULK = 15 # every instance at or below this is exhaustive +EXACT_FREE_CAP_FLAGSHIP = 20 # first FLAGSHIP_N instances above the bulk cap +FLAGSHIP_N = 4 +SEED = 20261015 +ANNEAL_RESTARTS = 24 +ANNEAL_PASSES = 6 + + +# ---------- exact rank over F2, two independent implementations ---------- + +def rank_bitset(rows, ncols): + basis = [0] * ncols + rank = 0 + for r in rows: + x = r + while x: + piv = x.bit_length() - 1 + if basis[piv]: + x ^= basis[piv] + else: + basis[piv] = x + rank += 1 + break + return rank + + +def rank_listmod2(rows, ncols): + mat = [[(r >> c) & 1 for c in range(ncols)] for r in rows] + rank = 0 + used = [False] * len(mat) + for c in range(ncols): + piv = None + for i in range(len(mat)): + if not used[i] and mat[i][c] == 1: + piv = i + break + if piv is None: + continue + used[piv] = True + rank += 1 + for i in range(len(mat)): + if i != piv and mat[i][c] == 1: + for cc in range(c, ncols): + mat[i][cc] ^= mat[piv][cc] + return rank + + +# ---------- configuration model (PR #2162 section 1, re-derived) ---------- + +def classify(cfg): + p, q = cfg["p"], cfg["q"] + v = len(p) + pi = [frozenset(j for j in range(3) if p[t][j] != 0) for t in range(v)] + sig = [frozenset(j for j in range(3) if q[t][j] != 0) for t in range(v)] + D = [pi[t] & sig[t] for t in range(v)] + H = set() + for t in range(v): + if len(D[t]) == 2: + i, j = sorted(D[t]) + if p[t][i] * q[t][i] == p[t][j] * q[t][j]: + H.add(t) + F = set(t for t in range(v) if len(pi[t]) == 3 and len(sig[t]) == 3) + W = set() + for t in range(v): + for s in range(v): + if t == s: + continue + if sum(p[t][j] * q[s][j] for j in range(3)) == 0: + if len(pi[t] & sig[s]) == 3: + W.add((t, s)) + return H, F, W + + +def has_cycle(edges, verts): + verts = list(verts) + succ = {u: [] for u in verts} + indeg = {u: 0 for u in verts} + for (t, s) in edges: + if t in succ and s in succ: + succ[t].append(s) + indeg[s] += 1 + stack = [u for u in verts if indeg[u] == 0] + seen = 0 + while stack: + u = stack.pop() + seen += 1 + for s in succ[u]: + indeg[s] -= 1 + if indeg[s] == 0: + stack.append(s) + return seen != len(verts) + + +def mas_vertices(W, F): + """Largest A subseteq F with W[A] acyclic (vertex reading of MAS).""" + Fl = sorted(F) + f = len(Fl) + idx = {u: i for i, u in enumerate(Fl)} + ein = [[] for _ in range(f)] + for (t, s) in W: + if t in idx and s in idx: + ein[idx[s]].append(idx[t]) + best = 0 + for mask in range(1, 1 << f): + # Kahn on the induced sub-digraph. + deg = [0] * f + succ = [[] for _ in range(f)] + for s in range(f): + if not (mask >> s) & 1: + continue + for t in ein[s]: + if (mask >> t) & 1: + succ[t].append(s) + deg[s] += 1 + stack = [u for u in range(f) if (mask >> u) & 1 and deg[u] == 0] + seen = 0 + while stack: + u = stack.pop() + seen += 1 + for s in succ[u]: + deg[s] -= 1 + if deg[s] == 0: + stack.append(s) + if seen == bin(mask).count("1"): + if seen > best: + best = seen + return best + + +def mas_edges(W, F): + """Maximum acyclic edge subset of W[F] (literal edge reading of MAS).""" + Fl = sorted(F) + f = len(Fl) + idx = {u: i for i, u in enumerate(Fl)} + # inc[u][mask] = number of wild edges (t -> u) with t in mask + inc = [[0] * (1 << f) for _ in range(f)] + for (t, s) in W: + if t in idx and s in idx: + tu, us = idx[t], idx[s] + for mask in range(1 << f): + if (mask >> tu) & 1: + inc[us][mask] += 1 + dp = [-1] * (1 << f) + dp[0] = 0 + for mask in range(1 << f): + if dp[mask] < 0: + continue + for u in range(f): + if (mask >> u) & 1: + continue + nmask = mask | (1 << u) + val = dp[mask] + inc[u][mask] + if val > dp[nmask]: + dp[nmask] = val + return dp[(1 << f) - 1] if f else 0 + + +def xbest(cfg, H, W): + """max |X| over X subseteq [v] \\ H with W[X] acyclic (Theorem B2 X-form).""" + v = len(cfg["p"]) + rest = [t for t in range(v) if t not in H] + best = 0 + for k in range(len(rest), -1, -1): + for X in itertools.combinations(rest, k): + X = set(X) + if not has_cycle([e for e in W if e[0] in X and e[1] in X], X): + return k + return best + + +# ---------- cost and exact minimum over admissible pairings ---------- + +def free_pairs(cfg): + p, q = cfg["p"], cfg["q"] + v = len(p) + return [(t, s) for t in range(v) for s in range(v) + if t != s and sum(p[t][j] * q[s][j] for j in range(3)) == 0] + + +def blocks(cfg): + p, q = cfg["p"], cfg["q"] + v = len(p) + out = [] + for j in range(3): + R = [t for t in range(v) if p[t][j] != 0] + A = [s for s in range(v) if q[s][j] != 0] + colidx = {s: i for i, s in enumerate(A)} + out.append((R, A, colidx)) + return out + + +def cost_of(rows, blk, crosscheck=False): + total = 0 + for (R, A, colidx) in blk: + sub = [] + for t in R: + bits = 0 + for s in A: + if (rows[t] >> s) & 1: + bits |= 1 << colidx[s] + sub.append(bits) + r1 = rank_bitset(sub, len(A)) + if crosscheck: + assert r1 == rank_listmod2(sub, len(A)), "rank implementation mismatch" + total += r1 + return total + + +def build_rows(base, fp_by_row, mask): + rows = list(base) + for t, lst in fp_by_row: + r = rows[t] + for (k, s) in lst: + if (mask >> k) & 1: + r |= 1 << s + rows[t] = r + return rows + + +def min_cost_exhaustive(cfg, crosscheck=False): + v = len(cfg["p"]) + fp = free_pairs(cfg) + blk = blocks(cfg) + base = [1 << t for t in range(v)] + by_row = [] + for t in range(v): + by_row.append((t, [(k, s) for k, (tt, s) in enumerate(fp) if tt == t])) + best = None + arg = None + for mask in range(1 << len(fp)): + rows = build_rows(base, by_row, mask) + c = cost_of(rows, blk, crosscheck=(crosscheck and mask % 511 == 0)) + if best is None or c < best: + best = c + arg = mask + return best, arg, len(fp) + + +def anneal_min(cfg, rng): + """Heuristic minimiser only. Every returned candidate is scored exactly.""" + v = len(cfg["p"]) + fp = free_pairs(cfg) + blk = blocks(cfg) + base = [1 << t for t in range(v)] + by_row = [] + for t in range(v): + by_row.append((t, [(k, s) for k, (tt, s) in enumerate(fp) if tt == t])) + n = len(fp) + + def score(mask): + return cost_of(build_rows(base, by_row, mask), blk) + + best_mask = 0 + best = score(0) + for _ in range(ANNEAL_RESTARTS): + mask = rng.getrandbits(n) if n else 0 + cur = score(mask) + for _pass in range(ANNEAL_PASSES): + improved = False + order = list(range(n)) + rng.shuffle(order) + for k in order: + cand = mask ^ (1 << k) + c = score(cand) + if c < cur: + mask, cur = cand, c + improved = True + if not improved: + break + if cur < best: + best, best_mask = cur, mask + return best, best_mask, n + + +# ---------- deterministic instance families ---------- + +def cross(a, b): + return (a[1] * b[2] - a[2] * b[1], + a[2] * b[0] - a[0] * b[2], + a[0] * b[1] - a[1] * b[0]) + + +def valid(cfg): + p, q = cfg["p"], cfg["q"] + for t in range(len(p)): + if all(x == 0 for x in p[t]) or all(x == 0 for x in q[t]): + return False + if sum(a * b for a, b in zip(p[t], q[t])) == 0: + return False + if not any(a != 0 and b != 0 for a, b in zip(p[t], q[t])): + return False + return True + + +def gen_random(rng, v, full): + p, q = [], [] + for _t in range(v): + pt = [0 if (not full and rng.random() < 0.25) else rng.choice((-2, -1, 1, 2)) + for _ in range(3)] + qt = [0 if (not full and rng.random() < 0.25) else rng.choice((-2, -1, 1, 2)) + for _ in range(3)] + p.append(pt) + q.append(qt) + cfg = {"p": p, "q": q} + return cfg if valid(cfg) else None + + +def gen_cross_core(rng, v): + """Dense wild 3-core (p_i = cross(q_j, q_k)) plus random extra lines.""" + qs = [tuple(rng.choice((-2, -1, 1, 2)) for _ in range(3)) for _ in range(3)] + ps = [cross(qs[1], qs[2]), cross(qs[2], qs[0]), cross(qs[0], qs[1])] + if any(0 in x for x in ps): + return None + if any(sum(a * b for a, b in zip(ps[i], qs[i])) == 0 for i in range(3)): + return None + p, q = list(ps), list(qs) + for _t in range(3, v): + pt = [0 if rng.random() < 0.25 else rng.choice((-2, -1, 1, 2)) + for _ in range(3)] + qt = [0 if rng.random() < 0.25 else rng.choice((-2, -1, 1, 2)) + for _ in range(3)] + p.append(pt) + q.append(qt) + cfg = {"p": p, "q": q} + return cfg if valid(cfg) else None + + +def gen_hub(v): + """Hub/coplanar-q cores: q(3) = a q(0) + b q(1) with p(i) = cross of two q's. + + For v = 4 this realizes 9 directed wild edges with masE = 5 > |F| = 4 + (see README, proposition P3). Extra lines for v > 4 are drawn from the + same span relations where possible, else small full-support vectors. + """ + out = [] + small = [t for t in itertools.product((1, 2), repeat=3)] + for q0 in small: + for q1 in small: + for q2 in small: + p2 = cross(q0, q1) + p0 = cross(q1, q2) + p1 = cross(q0, q2) + if any(0 in x for x in (p0, p1, p2)): + continue + if p0 == (0, 0, 0) or p1 == (0, 0, 0) or p2 == (0, 0, 0): + continue + for a in (1, 2): + for b in (1, 2): + q3 = tuple(a * x + b * y for x, y in zip(q0, q1)) + p3 = p1 # p3 || cross(q0,q2): edges 3->0, 3->2 only + cfg = {"p": [list(p0), list(p1), list(p2), list(p3)], + "q": [list(q0), list(q1), list(q2), list(q3)]} + if not valid(cfg): + continue + out.append(cfg) + if v > 4: + # Extend with twin/sum lines when they stay valid. + q4 = tuple(a * x + b * y for x, y in zip(q0, q2)) + p4 = cross(q1, q2) + cfg5 = {"p": cfg["p"] + [list(p4)], + "q": cfg["q"] + [list(q4)]} + if valid(cfg5): + out.append(cfg5) + if v > 5: + q5 = tuple(a * x + b * y for x, y in zip(q1, q2)) + p5 = cross(q0, q1) + cfg6 = {"p": cfg5["p"] + [list(p5)], + "q": cfg5["q"] + [list(q5)]} + if valid(cfg6): + out.append(cfg6) + if len(out) >= 48: + return out + return out + + +def gen_twinq(rng, v): + """Direction-class cores: q directions from three base vectors with + multiplicities, p(t) = cross of two base directions. Duplicated q + directions multiply every zero dot, so these are the near-dense wild + cores named in PR #2293's open next question 1 (v = 4..8).""" + out = [] + bases = [((1, 1, 1), (1, 1, 2), (1, 2, 1)), + ((1, 1, 2), (1, 2, 2), (2, 1, 1)), + ((1, 2, 1), (2, 1, 2), (2, 2, 1)), + ((2, 1, 1), (1, 2, 1), (1, 1, 2))] + for d in bases: + det = (d[0][0] * (d[1][1] * d[2][2] - d[1][2] * d[2][1]) + - d[0][1] * (d[1][0] * d[2][2] - d[1][2] * d[2][0]) + + d[0][2] * (d[1][0] * d[2][1] - d[1][1] * d[2][0])) + if det == 0: + continue + for _ in range(400): + assign = [rng.randrange(3) for _ in range(v)] + pmix = [rng.randrange(3) for _ in range(v)] + qs = [d[i] for i in assign] + ps = [] + okp = True + for t in range(v): + a, b = [x for x in range(3) if x != pmix[t]] + pt = cross(d[a], d[b]) + if 0 in pt: + okp = False + break + ps.append(list(pt)) + if not okp: + continue + cfg = {"p": ps, "q": [list(x) for x in qs]} + if valid(cfg): + out.append(cfg) + if len(out) >= 6: + return out + return out + + +# ---------- fixtures with analytically known answers (controls) ---------- + +FIXTURE_V2 = {"p": [[1, 0, 0], [0, 1, 0]], "q": [[1, 0, 0], [0, 1, 0]]} +# Analytic: H = empty, W = empty, min cost = 2 (diagonal blocks), bounds agree at 2. + +FIXTURE_HARMONIC = {"p": [[1, 1, 0]], "q": [[1, 1, 0]]} +# |D| = 2 with equal terms 1 = 1: line 0 is harmonic (classification control). + +FIXTURE_DENSE3 = { + "p": [[2, -3, -1], [1, -5, 3], [-5, 4, -1]], + "q": [[1, 2, 3], [1, 1, -1], [2, 1, 1]], +} +# All six off-diagonal pairs wild: F = 3, masE = 3 > masV = 1, min cost = 3 +# (cost = 3 rank_F2 B, min rank 1 at B = all-ones). Tight for the edge form. + +# Hub fixture (README proposition P3): filled in by gen_hub's first valid +# v = 4 member at runtime; expected wild digraph 9 directed edges, masE = 5, +# masV = 2, |F| = 4, min cost = 6 (3 * rank_F2 B, rank >= 2 since B = J is not +# admissible: pairs (0,3), (1,3), (3,1) have nonzero dot). + + +# ---------- run ---------- + +def instance_record(name, cfg, rng): + v = len(cfg["p"]) + H, F, W = classify(cfg) + fp = free_pairs(cfg) + mv = mas_vertices(W, F) + me = mas_edges(W, F) + xb = xbest(cfg, H, W) + rec = { + "name": name, "v": v, "free": len(fp), + "H": sorted(H), "F": sorted(F), "W": len(W), + "masV": mv, "masE": me, "xbest": xb, + } + return rec, H, F, W, fp + + +def run(): + rpath = os.path.join(HERE, "RECEIPT.json") + receipt = None + if os.path.exists(rpath): + receipt = json.load(open(rpath, encoding="utf-8")) + rng = random.Random(SEED) + instances = [] # (name, cfg, bucket) + + # Fixtures. + instances.append(("fixture_v2", FIXTURE_V2, "fixture")) + instances.append(("fixture_dense3", FIXTURE_DENSE3, "fixture")) + hub_all = gen_hub(4) + hub4 = hub_all[0] if hub_all else None + assert hub4 is not None, "hub family failed to generate" + instances.append(("fixture_hub4", hub4, "fixture")) + + # Family A: random all-full-support. + for v in (3, 4, 5, 6, 7): + got = 0 + for _ in range(200): + cfg = gen_random(rng, v, full=True) + if cfg: + instances.append(("random_full_v%d" % v, cfg, "random-full")) + got += 1 + if got >= 8: + break + # Family B: cross-product cores. + for v in (4, 5, 6, 7): + got = 0 + for _ in range(200): + cfg = gen_cross_core(rng, v) + if cfg: + instances.append(("cross_core_v%d" % v, cfg, "cross-core")) + got += 1 + if got >= 8: + break + # Family C: hub/coplanar-q cores (v = 4..6). + for cfg in hub_all[:24]: + instances.append(("hub_core_v%d" % len(cfg["p"]), cfg, "hub-core")) + # Family D: random mixed supports. + for v in (5, 6, 7, 8): + got = 0 + for _ in range(200): + cfg = gen_random(rng, v, full=False) + if cfg: + instances.append(("random_mixed_v%d" % v, cfg, "random-mixed")) + got += 1 + if got >= 8: + break + # Family E: direction-class (twin-q) cores, near-dense wild (large free). + for v in (4, 5, 6, 7, 8): + for cfg in gen_twinq(rng, v): + instances.append(("twin_q_v%d" % v, cfg, "twin-q")) + + # Smallest falsifying instance first: (v, free, name). + scored = [] + for i, (name, cfg, bucket) in enumerate(instances): + rec, H, F, W, fp = instance_record(name, cfg, rng) + if not name.startswith("fixture"): + rec["name"] = "%s#%d" % (name, i) + rec["bucket"] = bucket + rec["cfg"] = cfg + scored.append(rec) + scored.sort(key=lambda r: (r["v"], r["free"], r["name"])) + + # Exactness plan: exhaustive at free <= BULK; the first FLAGSHIP_N + # instances with BULK < free <= FLAGSHIP cap also exhaustive; the rest + # heuristic-only (every candidate still scored exactly). + flagship_left = FLAGSHIP_N + results = [] + controls = {"rank_crosscheck": True} + for rec in scored: + cfg = rec["cfg"] + free = rec["free"] + if free <= EXACT_FREE_CAP_BULK or ( + free <= EXACT_FREE_CAP_FLAGSHIP and flagship_left > 0): + if free > EXACT_FREE_CAP_BULK: + flagship_left -= 1 + mc, arg, _n = min_cost_exhaustive(cfg, crosscheck=True) + rec["method"] = "exhaustive" + else: + mc, arg, _n = anneal_min(cfg, rng) + rec["method"] = "heuristic_upper_bound" + rec["mincost"] = mc + edge_rhs = rec["v"] - len(rec["H"]) - len(rec["F"]) + rec["masE"] + vert_rhs = rec["v"] - len(rec["H"]) - len(rec["F"]) + rec["masV"] + rec["edge_rhs"] = edge_rhs + rec["vert_rhs"] = vert_rhs + # Machine-checked identity: xbest == vertex RHS. + assert rec["xbest"] == vert_rhs, ("xbest identity failed", rec["name"]) + results.append(rec) + + ident_ok = all(r["xbest"] == r["vert_rhs"] for r in results) + + # Controls with analytic answers. + by_name = {r["name"]: r for r in results} + ctrl = {} + ctrl["fixture_v2_mincost_2"] = by_name["fixture_v2"]["mincost"] == 2 + d3 = by_name["fixture_dense3"] + ctrl["fixture_dense3_mincost_3"] = d3["mincost"] == 3 + ctrl["fixture_dense3_masE_3_gt_masV_1"] = (d3["masE"] == 3 and d3["masV"] == 1) + h4 = by_name["fixture_hub4"] + ctrl["fixture_hub4_masE_5_gt_absF_4"] = (h4["masE"] == 5 and len(h4["F"]) == 4) + ctrl["fixture_hub4_masV_2"] = h4["masV"] == 2 + ctrl["fixture_hub4_mincost_6"] = h4["mincost"] == 6 + # Sensitivity: the strengthened bound (+1) must be falsified on a fixture. + ctrl["strengthened_bound_falsified"] = ( + d3["mincost"] < d3["edge_rhs"] + 1 or h4["mincost"] < h4["edge_rhs"] + 1) + # Harmonic classification control. + Hh, Fh, Wh = classify(FIXTURE_HARMONIC) + ctrl["harmonic_classification"] = (Hh == {0} and not Fh and not Wh) + # Mutation sensitivity: changing one entry must change the free-pair set. + mut = {"p": [list(r) for r in FIXTURE_DENSE3["p"]], + "q": [list(r) for r in FIXTURE_DENSE3["q"]]} + mut["q"][0][0] += 1 + ctrl["mutation_sensitivity"] = ( + free_pairs(mut) != free_pairs(FIXTURE_DENSE3)) + # Lemma P1 side condition, machine-checked over the domain: no all-full + # configuration at v >= 4 admits B = all-ones (some pair has nonzero dot). + p1_ok = True + for r in results: + if len(r["F"]) == r["v"] and r["v"] >= 4: + cfg = r["cfg"] + if all(sum(a * b for a, b in zip(cfg["p"][t], cfg["q"][s])) + == 0 for t in range(r["v"]) for s in range(r["v"]) if t != s): + p1_ok = False + ctrl["p1_no_complete_pairs_v_ge_4"] = p1_ok + + # Bounds over the whole domain. + def falsifiers(key, rhs_key): + out = [] + for r in results: + if r["mincost"] < r[rhs_key]: + out.append(r) + return out + + edge_fals = falsifiers("edge", "edge_rhs") + vert_fals = falsifiers("vert", "vert_rhs") + + # Falsifier confirmation: every falsifier is re-minimised exhaustively and + # its witness recomputed by the independent rank implementation. + fals_detail = None + for r in edge_fals + vert_fals: + cfg = r["cfg"] + mc, arg, _n = min_cost_exhaustive(cfg, crosscheck=True) + assert mc == r["mincost"] or r["method"] != "exhaustive", ( + "falsifier minimum not reproducible", r["name"]) + r["mincost"] = mc + r["method"] = "exhaustive_confirmed" + v = len(cfg["p"]) + fp = free_pairs(cfg) + base = [1 << t for t in range(v)] + by_row = [] + for t in range(v): + by_row.append((t, [(k, s) for k, (tt, s) in enumerate(fp) if tt == t])) + rows = build_rows(base, by_row, arg) + # Independent recomputation of cost(B) via rank_listmod2 only. + indep = 0 + for (R, A, colidx) in blocks(cfg): + sub = [[(rows[t] >> s) & 1 for s in A] for t in R] + indep += rank_listmod2([sum(x << i for i, x in enumerate(row)) + for row in sub], len(A)) + assert indep == mc, ("independent witness recomputation failed", r["name"]) + if fals_detail is None: + H, F, W = classify(cfg) + fals_detail = { + "name": r["name"], "v": r["v"], "free": r["free"], + "H": sorted(H), "F": sorted(F), + "W": sorted(list(W)), "masV": r["masV"], "masE": r["masE"], + "xbest": r["xbest"], "edge_rhs": r["edge_rhs"], + "vert_rhs": r["vert_rhs"], "mincost": mc, + "p": cfg["p"], "q": cfg["q"], + "B_rows": [format(rows[t], "0%db" % v)[::-1] for t in range(v)], + "independent_recomputation": indep, + } + + summary = { + "instances": len(results), + "exact": sum(1 for r in results if r["method"] == "exhaustive"), + "heuristic_only": sum(1 for r in results if r["method"] != "exhaustive"), + "max_free": max(r["free"] for r in results), + "tight_edge": sum(1 for r in results if r["mincost"] == r["edge_rhs"]), + "tight_vertex": sum(1 for r in results if r["mincost"] == r["vert_rhs"]), + "masE_gt_masV": sum(1 for r in results if r["masE"] > r["masV"]), + "masE_gt_absF": sum(1 for r in results if r["masE"] > len(r["F"])), + "max_masE_minus_absF": max(r["masE"] - len(r["F"]) for r in results), + "edge_falsifiers": len(edge_fals), + "vertex_falsifiers": len(vert_fals), + "ident_ok": ident_ok, + "controls_ok": all(ctrl.values()), + } + + # Stable digest over the proof-relevant fields of every instance. + canon = json.dumps( + [{k: r[k] for k in ("name", "v", "free", "H", "F", "W", "masV", "masE", + "xbest", "mincost", "method", "edge_rhs", "vert_rhs")} + for r in results], sort_keys=True) + digest = hashlib.sha256(canon.encode()).hexdigest() + + print("PASS_B2_EDGE_SCREEN instances=%d exact=%d heuristic_only=%d max_free=%d" + % (summary["instances"], summary["exact"], summary["heuristic_only"], + summary["max_free"])) + if edge_fals: + for r in edge_fals: + print("BOUND iii_edge: FALSIFIER v=%d free=%d mincost=%d edge_rhs=%d " + "masE=%d method=%s name=%s" + % (r["v"], r["free"], r["mincost"], r["edge_rhs"], r["masE"], + r["method"], r["name"])) + else: + print("BOUND iii_edge: no falsifier in declared domain") + if vert_fals: + r = vert_fals[0] + print("BOUND iii_vertex: FALSIFIED first at v=%d free=%d mincost=%d " + "vert_rhs=%d name=%s" % (r["v"], r["free"], r["mincost"], + r["vert_rhs"], r["name"])) + else: + print("BOUND iii_vertex: no falsifier in declared domain") + print("IDENTITY xbest=vertex_rhs: %s on %d/%d" + % ("ok" if ident_ok else "FAILED", summary["instances"], + summary["instances"])) + print("CONTROLS %s %s" % ("ok" if all(ctrl.values()) else "FAILED", + json.dumps(ctrl, sort_keys=True))) + if fals_detail: + print("FALSIFIER_DETAIL %s" % json.dumps(fals_detail, sort_keys=True)) + print("SUMMARY tight_edge=%d tight_vertex=%d masE_gt_masV=%d masE_gt_absF=%d " + "max_masE_minus_absF=%d" + % (summary["tight_edge"], summary["tight_vertex"], summary["masE_gt_masV"], + summary["masE_gt_absF"], summary["max_masE_minus_absF"])) + print("DOMAIN seed=%d exact_cap_bulk=%d exact_cap_flagship=%d flagship_n=%d " + "families=random-full,cross-core,hub-core,random-mixed,twin-q " + "entries=-2..2 v=3..8" % (SEED, EXACT_FREE_CAP_BULK, + EXACT_FREE_CAP_FLAGSHIP, FLAGSHIP_N)) + print("DIGEST %s" % digest) + + if receipt is None: + print("RECEIPT_PENDING (freeze RECEIPT.json from this run)") + return 0 + expected = receipt["summary"] + diffs = {k: (summary.get(k), expected[k]) for k in expected + if summary.get(k) != expected[k]} + if digest != receipt["digest"]: + diffs["digest"] = (digest, receipt["digest"]) + ok = not diffs + print("RECEIPT_%s" % ("MATCH" if ok else "MISMATCH"), + "" if ok else json.dumps(diffs, sort_keys=True)) + return 0 if (ok and summary["controls_ok"] and ident_ok) else 1 + + +if __name__ == "__main__": + sys.exit(run())