diff --git a/research/answered-open-questions-ledger/README.md b/research/answered-open-questions-ledger/README.md new file mode 100644 index 0000000000..64360b75f5 --- /dev/null +++ b/research/answered-open-questions-ledger/README.md @@ -0,0 +1,139 @@ +# Open next questions that merged packages already answer: a ten-row ledger + +**Navigation record. No new mathematical claim and no κ.** Ten open questions +stored in merged research packages are tied to the later merged package whose +README answers them (5 rows), answers them by scope inclusion (2 rows) or +answers only part of them (3 rows). Each row gives the question exactly as +stored in the asking package's `TASK.json`, the answering package, and one to +four quoted README lines. All inputs are pinned to main +`7c49fe32c55de02c2c873655c804b16e4c3fef0a`. The asking packages are frozen, so +the missing cross-references live here instead of in their files. + +| Row | Question stored in | Answered in | Status | +|---|---|---|---| +| L01 | `length9-four-vertex-gap`: arc {0,1,2,3,4}, common far-rim root? | `length9-five-vertex-gap` | answered | +| L02 | `length9-five-vertex-gap`: arc {0,1,2,3,4,5}, common far-rim root? | `length9-six-vertex-gap` | answered | +| L03 | `length9-six-vertex-gap`: arc {0,1,2,3,4,5,6}, common survivor root? | `length9-seven-vertex-gap` | answered | +| L04 | `gaussian-neumann-ten`: smallest integer c with U < c p^2 | `gaussian-neumann-nine` | answered | +| L05 | `precision-blind-composite-rigidity`: even lengths | `weighted-reversal-rescaling` | answered | +| L06 | `paired-plane-rematch-rank34`: minimum fitting rank over all matchings | `paired-plane-frame-packing`, `p112-frame-partition`, `paired-plane-frame-repair` | partial | +| L07 | `triangular-parity-n8`: every n=8 symbol, prefixes at most 3/2 | `triangular-parity-forward-bound` | answered by scope inclusion | +| L08 | `triangular-parity-prefix`: nested splits inside the product of one-level caps | `triangular-parity-forward-bound` | answered by scope inclusion | +| L09 | `diagonal-pair-five-call-collisions`: six-call floor in odd characteristic or F4 | `diagonal-pair-collision-audit` | partial | +| L10 | `connector-gray-growth`: sharp leading constant of N(c)/(c log2 c) | `connector-bounded-depth-cap` | partial | + +[ledger.json](ledger.json) holds the rows. Each row has a `note` that says in +one or two sentences what the answering README settles and what it does not. + +## Statuses + +- `answered` means the answering README states a result for the object the + question names, in its title or first sentences. +- `answered-by-scope-inclusion` means the answering README proves a quantified + statement whose scope includes the asked case, without saying it answers that + question. The inclusion is my reading. The `note` names the definitional step + it relies on: L07 and L08 read the asking package's proper prefixes as the + answering package's forward macro-prefixes, by inspecting the two definitions, + and that step is not proved here. +- `partial` means part of the question, or only its stated first step, is + settled. L06: the stated first step (is 12 the maximum number of disjoint + orthonormal 8-frames?) is answered, but the cited READMEs give a matching with + fitting rank 32 and say they do not claim the optimum over all matchings. + L09: odd characteristic is addressed only for F3 at width two, and the + answering README labels its length-five row local SAT evidence. L10: the + leading constant is fixed at 1/2 only for concatenations of blocks of depth at + most two, and the general constant stays open in [1/2, 1]. + +## Evidence and reproduction + +From the repository root, with CPython 3.12 and the standard library only: + +```sh +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/answered-open-questions-ledger/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -O -W error -B research/answered-open-questions-ledger/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/answered-open-questions-ledger +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/answered-open-questions-ledger --check-source-history +``` + +Any CPython 3.12 installation can replace the displayed interpreter path. Both +direct runs print one line that begins +`PASS_ANSWERED_OPEN_QUESTIONS_LEDGER rows=10 answered=5 scope_inclusion=2 partial=3` +and takes about 0.03 s. The check authenticates the SHA256 of 30 pinned inputs +(19 `TASK.json`, 11 `README.md`), requires each stored question to equal its +`TASK.json` entry and to be unique there, requires each quote to lie inside one +README line, requires that no answering README cites the asking package by a +`research/` or `../` path (that absence is what makes the +cross-reference missing), and rejects eleven mutated copies of a real row: +changed question text, a moved index, a quote absent from the README, a quote +spanning a newline, a quote that is too short, a package answering itself, an +unpinned answering package, an unknown status, an empty answer list, a quote +borrowed from another row, and an answering README that cites the asking +package by path. Checks raise explicit exceptions, so `-O` does not disable +them. + +## What this does and does not establish + +- It establishes that the quoted lines exist in the pinned READMEs and that the + stored questions match the pinned `TASK.json` files. +- It does **not** re-verify any answering result, and it does not decide by + program that a quote answers a question. That reading is mine and is recorded + in each row's status and note. +- The ten rows are chains I met while looking for an open question to take. They + are not a census, and they support no statement about how many other stored + questions are already answered. +- In all ten rows, no answering README cites the asking package by a + `research/` or `../` path; the verifier enforces this on the + pinned READMEs. It does not look at the answering packages' other files, so + a citation there is not excluded. A path-citation index built from READMEs + would therefore not link these pairs. +- In the length-9 chain, the five-vertex package's stop rule says not to start + the six-vertex arc, and its stored question points at that arc. Rows L01 to + L03 record where each next step was taken. I did not check whether the other + asking packages were meant to stop at their stated question. + +## Scope + +`scope-navigation` card, scope refined: the card asks for one navigation repair +or one related family index, and this ledger spans seven small question chains. +No frozen package is edited. The card's first working command, +`python3 -B scripts/research_selected_baseline.py`, printed +`PASS_RESEARCH_BASELINE_BINDINGS_ONLY` at the base commit; that command checks +source bindings only and is not a scientific replay. + +## Open next questions + +The structured list with relevance, first step and blocker is in +[TASK.json](TASK.json). + +1. Which other merged packages store an open question that a later merged + package already answers? First step: for packages whose questions no other + package cites by path, search later PR titles and README first lines for the + named objects, and add a row only when the answering README states the result + in its own words. An automatic match is only a lead. +2. L06: what is the minimum exact fitting rank over all perfect matchings of the + P112 plane ports? The cited READMEs give a rank-32 matching and a floor of 30 + that is stated only for the two-support even-group colouring construction. +3. L09: does the six-call diagonal-pair floor hold over F4, over F5 and at + widths above two? The cited audit settles F3 at width two only. +4. L10: is the general leading constant of N(c)/(c log2 c) above 1/2? Check live + PRs and discussions for a depth-three block construction before choosing it. + +Questions 2 to 4 are pointers to questions other contributors stored. They are +not claimed here. + +## Credit + +This contribution was produced by Nick Petalas. Apache-2.0. + +Every row depends on predecessor work that is cited, not re-verified: +jwr (James Reed) for `length9-four-vertex-gap`, `length9-five-vertex-gap`, +`length9-six-vertex-gap`, `length9-seven-vertex-gap`, `gaussian-neumann-ten`, +`gaussian-neumann-nine`, `triangular-parity-n8` and `triangular-parity-prefix`; +Wentao Li for `precision-blind-composite-rigidity`; Matarener (Mark) for +`paired-plane-rematch-rank34`; Tekalign (tekuuu) for `paired-plane-frame-repair`; +Brian (JoyboyBrian) for `triangular-parity-forward-bound`; JoyboyBrian for +`diagonal-pair-five-call-collisions`; Josie Elliston for +`diagonal-pair-collision-audit` and `connector-bounded-depth-cap`; apoursh for +`connector-gray-growth`; and Nick Petalas for `weighted-reversal-rescaling`, +`paired-plane-frame-packing` and `p112-frame-partition`. Each package's +`README.md` and `TASK.json` retain its own credit line. diff --git a/research/answered-open-questions-ledger/SOURCES.json b/research/answered-open-questions-ledger/SOURCES.json new file mode 100644 index 0000000000..356756a35b --- /dev/null +++ b/research/answered-open-questions-ledger/SOURCES.json @@ -0,0 +1,198 @@ +{ + "schema_version": 1, + "base_commit": "7c49fe32c55de02c2c873655c804b16e4c3fef0a", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "d59b5035e7b4cbaa9d688a1d32dd0d6eb79c466a", + "sha256": "9b8d0eea95b3bf0dfcb7938a732a6439b87a2685dec2a5ab9e525b3b34debbfa" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec", + "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81" + }, + { + "path": "research/connector-bounded-depth-cap/README.md", + "usage": "input", + "git_blob": "0127ee20090453b48024f8a1b279427a6612b0bf", + "sha256": "9e8800a27375b92b77b20cf3594f647a507bf17fd9bff2c4da1be10db2db98fa" + }, + { + "path": "research/connector-bounded-depth-cap/TASK.json", + "usage": "input", + "git_blob": "8bd9ab8d37c6486af6700152b4d8f652dffd6ad0", + "sha256": "d4a7afa712bba008cebd7c54d17766916fd6efec1a0ca7e2d21ea7c86a1cdba0" + }, + { + "path": "research/connector-gray-growth/TASK.json", + "usage": "input", + "git_blob": "21478f695b5d26f6259597fa31cf9d054ee456a2", + "sha256": "ecf631c4ca42f336822de0b12aa97e92330e77712a522e02e25d944c11e5f281" + }, + { + "path": "research/diagonal-pair-collision-audit/README.md", + "usage": "input", + "git_blob": "7b8d36d096438ee17b91de51d7e3e9dc32a9cf06", + "sha256": "5ab441cf115d5e188a01bc5c06b0299732b99d79e7c84f1aab4daa0aaf4c2b78" + }, + { + "path": "research/diagonal-pair-collision-audit/TASK.json", + "usage": "input", + "git_blob": "94bff758ec4ad994f3f451e66b95e8add568114b", + "sha256": "931af1805e1c8deab93f1358373d631eed5c667d089fa2bd78cd628a90bdfe58" + }, + { + "path": "research/diagonal-pair-five-call-collisions/TASK.json", + "usage": "input", + "git_blob": "da30f03b65a5ae3aaf94f1e4098be280a49a13a6", + "sha256": "14cbec29ffc99ab83d46bc3a1180f0167e68bd69a9f6a2d0e54c70097d8f8c8e" + }, + { + "path": "research/gaussian-neumann-nine/README.md", + "usage": "input", + "git_blob": "54a8ce117a233e54e5057fd1edfa378e59527592", + "sha256": "189a0fb9ede1649ffea24ea22605a573366170e172ac563dd001c68d65b966ac" + }, + { + "path": "research/gaussian-neumann-nine/TASK.json", + "usage": "input", + "git_blob": "04fbc1f53346e6ec6071e80ee74f8dc28a6b8b58", + "sha256": "9bdf58a80bc9f80df92e4af60be1ff7821b4ebb7fb4e707d9dc606f88138905a" + }, + { + "path": "research/gaussian-neumann-ten/TASK.json", + "usage": "input", + "git_blob": "b01410a62f5fd085f097b2e0da99558b9772a33d", + "sha256": "f13dbc62b3806a3362a5b7ba4a62e66a2534355d2e4788c419e9ebbd4afc2fc9" + }, + { + "path": "research/length9-five-vertex-gap/README.md", + "usage": "input", + "git_blob": "e1efad786d6efcae365e11809093621621d34d2e", + "sha256": "a00f08a15f9b86923ff43151380244bacea8fd0a1db771d619b0453966d82a83" + }, + { + "path": "research/length9-five-vertex-gap/TASK.json", + "usage": "input", + "git_blob": "82030aa591047048c88607fd3902f4adf74bac00", + "sha256": "62e8ce24434ce64f8a60761239db5904c623f674c671038186fe15ac7f8f8883" + }, + { + "path": "research/length9-four-vertex-gap/TASK.json", + "usage": "input", + "git_blob": "f0a5d863e11d9c7a43fcfb415ac8a31a45905343", + "sha256": "7a053be14725fa2ced586744f04554f16645351a8632bccaa6cc7e36386cc1ed" + }, + { + "path": "research/length9-seven-vertex-gap/README.md", + "usage": "input", + "git_blob": "e71558aafbca16648a57c6fd4726322f063768c0", + "sha256": "96bff830e20fff43990c97bb0d6dab7f9f10440df373ebcabd951d7aa4384f2a" + }, + { + "path": "research/length9-seven-vertex-gap/TASK.json", + "usage": "input", + "git_blob": "dbf1d726ca5a52a5d99b2ef8bd62aea4244b0850", + "sha256": "df5751b7c822b53232a00c6e2ac16959a624272b6aa04867eb539376dec28728" + }, + { + "path": "research/length9-six-vertex-gap/README.md", + "usage": "input", + "git_blob": "244b31647c74fae594cc6fa1e1d9d2f4ad840b9a", + "sha256": "9979f55f13ccf0b3d92d995c68e7121f3ec20fcd4a1f9544ce52dbe736369494" + }, + { + "path": "research/length9-six-vertex-gap/TASK.json", + "usage": "input", + "git_blob": "ad9f129f9c2401f36667e992579348f373ce3615", + "sha256": "8cf851cbdd82c05982fdb502b257fdbd0ddd773f6534d16999975b11bd6e7aff" + }, + { + "path": "research/p112-frame-partition/README.md", + "usage": "input", + "git_blob": "8e8e7fab75ca65f704c1b72ac971d4819ba95fab", + "sha256": "ebb7771c4e517ee22f72918cf7f6d2827fb133003c65f92ce9aa4bb0722a9ef8" + }, + { + "path": "research/p112-frame-partition/TASK.json", + "usage": "input", + "git_blob": "ee0dda27ac6cb9db5fedd31a9c4ee8a440aec7f3", + "sha256": "a2a87aea504bb5d190e0eac9444b453b70d0ab1ad28e59dd697a653151373543" + }, + { + "path": "research/paired-plane-frame-packing/README.md", + "usage": "input", + "git_blob": "a79ef1e4ad48f4a6bb3b11c6cd7e5b9a9d629fb6", + "sha256": "2dde74c4c3922a8cd83f1e2a675361198f1dae883ee94e2779ed3c34f900835c" + }, + { + "path": "research/paired-plane-frame-packing/TASK.json", + "usage": "input", + "git_blob": "3d1264311a3bfe7b24baa1cfe4c4aeb39e476254", + "sha256": "630d3bf12fa09aa1721355b3412bbcbd7737d304cda22208f37a7176a1f12019" + }, + { + "path": "research/paired-plane-frame-repair/README.md", + "usage": "input", + "git_blob": "98015779a08b2dfe2199d34cf00fa2e10d576fb8", + "sha256": "18cab7d6b27d6cbb91efa6d60b4a4c89a15909b2d2169fb54fc17b3abe334771" + }, + { + "path": "research/paired-plane-frame-repair/TASK.json", + "usage": "input", + "git_blob": "c632bb6554938fbe4dd2528f334848832de14af4", + "sha256": "92f813d7dbb8c6000896d774d75fd532d347e96a1aa2c412f240aca3cdc9a0bf" + }, + { + "path": "research/paired-plane-rematch-rank34/TASK.json", + "usage": "input", + "git_blob": "a8ca6cd376f1df59cfac809db6f37e355ebd725f", + "sha256": "fce1710226d0d0da4d1922bc8a6538e6202f85c7419495df4560ea0127dc6643" + }, + { + "path": "research/precision-blind-composite-rigidity/TASK.json", + "usage": "input", + "git_blob": "f12e2ed53749667a1be3af2a2f05fa494fc3ce54", + "sha256": "a7236dac4cf73276bfbb0321a56bdeda225e0cd39a3bae8df947f1e916e5c630" + }, + { + "path": "research/triangular-parity-forward-bound/README.md", + "usage": "input", + "git_blob": "d008710585a897b9b568e74c7b867d8c784e4aa8", + "sha256": "745c2105fc614e6ba453327a37e483b808425a40ce3e2b44e2643b0ea1db3781" + }, + { + "path": "research/triangular-parity-forward-bound/TASK.json", + "usage": "input", + "git_blob": "19b1ffcb4c7fedeaa8179720db43ef0465691f3d", + "sha256": "b4ed309711ad195c5f066625c0abb26c9c624830b64d5a079428ac0dea4fa586" + }, + { + "path": "research/triangular-parity-n8/TASK.json", + "usage": "input", + "git_blob": "d214b1cfe4449510dd1cf4d3a94fafb18a0f466f", + "sha256": "87502efa58b2b5918a76a0ea8c7b877aa7dd825c4402cbd515d9833968e0f265" + }, + { + "path": "research/triangular-parity-prefix/TASK.json", + "usage": "input", + "git_blob": "7d6ca368fca5bc991597d9ef08c756543187e3c6", + "sha256": "6f4099f92d4bfb91d26a683e92b715439d5559ed1b10a540fca2f3bff79e0247" + }, + { + "path": "research/weighted-reversal-rescaling/README.md", + "usage": "input", + "git_blob": "d192032d732526f3fe20b4c59808c531bdc1a8dd", + "sha256": "c455b51a41a4d217390c4286e6b310f0ac7fe802bf624eb83bf5e35868774308" + }, + { + "path": "research/weighted-reversal-rescaling/TASK.json", + "usage": "input", + "git_blob": "7cd7c5da614a272a924312aedf974d53b1598dba", + "sha256": "84ff71dedb70ac86fbf2bb852337c7817fedd2c5c64e602e86b3259537f87717" + } + ] +} diff --git a/research/answered-open-questions-ledger/TASK.json b/research/answered-open-questions-ledger/TASK.json new file mode 100644 index 0000000000..5efa6e811b --- /dev/null +++ b/research/answered-open-questions-ledger/TASK.json @@ -0,0 +1,79 @@ +{ + "schema_version": 1, + "task_id": "scope-navigation", + "priority_revision": 8, + "base_commit": "7c49fe32c55de02c2c873655c804b16e4c3fef0a", + "original_card": { + "id": "scope-navigation", + "question": "Can one misleading historical-current claim or missing research cross-reference be corrected?", + "starting_points": [ + "docs/research/current-status.md", + "docs/research/pr-ledger.md", + "certificates/selected-result.json" + ], + "methods": [ + "Trace one confusing path from onboarding to its authoritative source.", + "Index one tightly related family of obstructions with explicit excluded and open hypotheses." + ], + "acceptance_gate": "Produce evidence-backed navigation, preserve historical records and avoid a duplicate global survey.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_selected_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Resolve the current selected review, separate complex/ordinary BIT/admitted BIT/outer budgets, and compare the card against live handoffs before starting. Historical ceilings require exact source/model equivalence.", + "scope": "Source-binding orientation only; not a scientific replay or all-size proof. Materialize selected inputs if this checkout is sparse." + }, + "first_experiment": "Repair one confusing path or produce a scoped map of one related obstruction family.", + "bottleneck_link": "Clear navigation lowers entry cost for central research; a global survey without a concrete fix is not required.", + "allowed_variations": [ + "One historical-current ambiguity or one bounded family index." + ], + "scope_change_triggers": [ + "Rewriting frozen scientific packages just to change their historical wording." + ], + "overlap_terms": [ + "current status", + "historical checkpoint", + "scope navigation" + ] + }, + "scope_status": "refined", + "actual_scope": "A bounded index of ten open questions stored in merged packages, each tied to the later merged package whose README answers or partly answers it, with exact question text and quoted evidence pinned to one main commit. It re-verifies no mathematical result.", + "scope_change_reason": "The card asks for one navigation repair or one related family index. Frozen packages cannot be edited, so the missing cross-references are collected in one external ledger. It spans seven small question chains rather than one family; each row stands alone.", + "bottleneck_link": "Side result, no bound changes. It supports the overlap step of autoresearch.md: a question stored as open can already be answered by a package that does not cite the asking package by path, so a path-citation or title search can miss the answer.", + "budget_minutes": 60, + "stop_rule": "Stop after the rows whose answering README states the result in its own words. Do not re-verify the cited results, and do not add a row from title similarity alone.", + "outcome": "completed", + "evidence": "verify.py checks 10 rows against 30 SHA256-pinned inputs (19 TASK.json, 11 README), requires each stored question to equal its TASK.json entry and each quote to lie inside one README line, and rejects 11 mutated rows, and requires that no answering README cites the asking package by path. Statuses: 5 answered, 2 answered by scope inclusion, 3 partial.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "Which other merged packages store an open question that a later merged package already answers?", + "why_it_matters": "In all ten rows here no answering README cites the asking package by research path, so a path-citation index and a no-match overlap report both miss the answer. A contributor can spend a session on a closed question.", + "first_step": "Take packages whose questions no other package cites by path, search later PR titles and README first lines for the question's named objects, and add a row only when the answering README states the result in its own words.", + "blocked_by": "Answers are usually cited by PR number or by object name, so each candidate needs a human reading; an automatic match is only a lead." + }, + { + "question": "What is the minimum exact fitting rank over all perfect matchings of the P112 plane ports, given a frame packing number of 13 and a known rank-32 matching (row L06)?", + "why_it_matters": "The cited READMEs give one matching with fitting rank 32 and a floor of 30 that is stated only for the two-support even-group colouring construction. They do not state the minimum over all matchings, and each removed channel lowers the algebraic copy floor of the plane-port decoder.", + "first_step": "Read the frame-partition and frame-repair READMEs for exactly which matchings the floor of 30 covers, then test whether any matching outside that construction needs fewer than 32 scalar queries.", + "blocked_by": "The floor of 30 is stated for the two-support even-group colouring construction, not for every fitting matrix." + }, + { + "question": "Does the six-call diagonal-pair floor hold over F4, over F5, and at widths above two (row L09)?", + "why_it_matters": "The cited audit settles only F3 at width two, and labels its length-five row local SAT evidence.", + "first_step": "Run the audit's SAT encoding on F5 after symmetry reduction, as that package proposes, and state which reductions need their own soundness argument.", + "blocked_by": "Compute cost, and an F4 implementation needs GF(4) arithmetic." + }, + { + "question": "Is the general leading constant of N(c)/(c log2 c) above 1/2 (row L10)?", + "why_it_matters": "The cited README fixes 1/2 only for concatenations of blocks of depth at most two and leaves [1/2, 1] open for the general constant.", + "first_step": "Check live PRs and discussions for a depth-three block construction before choosing this question.", + "blocked_by": "A constant above 1/2 needs blocks of depth at least three, per the cited README." + } + ] +} diff --git a/research/answered-open-questions-ledger/VERIFY.json b/research/answered-open-questions-ledger/VERIFY.json new file mode 100644 index 0000000000..592c664831 --- /dev/null +++ b/research/answered-open-questions-ledger/VERIFY.json @@ -0,0 +1,65 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/connector-bounded-depth-cap/README.md", + "research/connector-bounded-depth-cap/TASK.json", + "research/connector-gray-growth/TASK.json", + "research/diagonal-pair-collision-audit/README.md", + "research/diagonal-pair-collision-audit/TASK.json", + "research/diagonal-pair-five-call-collisions/TASK.json", + "research/gaussian-neumann-nine/README.md", + "research/gaussian-neumann-nine/TASK.json", + "research/gaussian-neumann-ten/TASK.json", + "research/length9-five-vertex-gap/README.md", + "research/length9-five-vertex-gap/TASK.json", + "research/length9-four-vertex-gap/TASK.json", + "research/length9-seven-vertex-gap/README.md", + "research/length9-seven-vertex-gap/TASK.json", + "research/length9-six-vertex-gap/README.md", + "research/length9-six-vertex-gap/TASK.json", + "research/p112-frame-partition/README.md", + "research/p112-frame-partition/TASK.json", + "research/paired-plane-frame-packing/README.md", + "research/paired-plane-frame-packing/TASK.json", + "research/paired-plane-frame-repair/README.md", + "research/paired-plane-frame-repair/TASK.json", + "research/paired-plane-rematch-rank34/TASK.json", + "research/precision-blind-composite-rigidity/TASK.json", + "research/triangular-parity-forward-bound/README.md", + "research/triangular-parity-forward-bound/TASK.json", + "research/triangular-parity-n8/TASK.json", + "research/triangular-parity-prefix/TASK.json", + "research/weighted-reversal-rescaling/README.md", + "research/weighted-reversal-rescaling/TASK.json" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Input SHA256 pins, exact question text, one-line quotes, no path citation of the asking package, status vocabulary and eleven rejecting controls." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "The same checks with assertions disabled; every check raises explicitly." + } + ] +} diff --git a/research/answered-open-questions-ledger/ledger.json b/research/answered-open-questions-ledger/ledger.json new file mode 100644 index 0000000000..826db98750 --- /dev/null +++ b/research/answered-open-questions-ledger/ledger.json @@ -0,0 +1,205 @@ +{ + "schema": "answered-open-questions-ledger/v1", + "rows": [ + { + "id": "L01", + "asking": { + "package": "length9-four-vertex-gap", + "question_index": 1, + "question": "Does the length-9 width-2 arc {0,1,2,3,4} have a positive common far-rim root inside the row-gap bound?" + }, + "answers": [ + { + "package": "length9-five-vertex-gap", + "quote": "# The five-vertex far numerators do not share a positive root" + }, + { + "package": "length9-five-vertex-gap", + "quote": "On the length-9 width-2 arc `{0,1,2,3,4}`, no pivot entry zeros both" + } + ], + "status": "answered", + "note": "The answering README treats the arc named in the question and reports that no pivot entry zeros both far directions at a positive value." + }, + { + "id": "L02", + "asking": { + "package": "length9-five-vertex-gap", + "question_index": 1, + "question": "Does the length-9 width-2 arc {0,1,2,3,4,5} have a positive common far-rim root inside the row-gap bound?" + }, + "answers": [ + { + "package": "length9-six-vertex-gap", + "quote": "# Six-vertex far directions vanish together only below diagonal dominance" + }, + { + "package": "length9-six-vertex-gap", + "quote": "On the length-9 width-2 arc `{0,1,2,3,4,5}`, the path entry from 1 to 2 has" + } + ], + "status": "answered", + "note": "The answering README treats the arc named in the question: no positive far-rim root for the path entry, and common roots only at diagonals below 1/2." + }, + { + "id": "L03", + "asking": { + "package": "length9-six-vertex-gap", + "question_index": 1, + "question": "Does the length-9 width-2 arc {0,1,2,3,4,5,6} have a positive common survivor root inside diagonal dominance?" + }, + "answers": [ + { + "package": "length9-seven-vertex-gap", + "quote": "# Seven-vertex survivor directions vanish together only below dominance" + }, + { + "package": "length9-seven-vertex-gap", + "quote": "On the length-9 width-2 arc `{0,1,2,3,4,5,6}`, the path entry from 1 to 2" + } + ], + "status": "answered", + "note": "The answering README treats the arc named in the question and reports common roots only at diagonals below 1/2." + }, + { + "id": "L04", + "asking": { + "package": "gaussian-neumann-ten", + "question_index": 0, + "question": "What is the smallest integer c such that U < c p^2 for every integer p >= 2?" + }, + "answers": [ + { + "package": "gaussian-neumann-nine", + "quote": "# The smallest integer coefficient on the Neumann ceiling is 9" + } + ], + "status": "answered", + "note": "The answering README states the smallest integer coefficient in its title." + }, + { + "id": "L05", + "asking": { + "package": "precision-blind-composite-rigidity", + "question_index": 1, + "question": "Does the same rigidity classify even lengths, which #4070 handled only for prime powers at n=2?" + }, + "answers": [ + { + "package": "weighted-reversal-rescaling", + "quote": "even-length gap in Wentao Li's [#4095]" + }, + { + "package": "weighted-reversal-rescaling", + "quote": "scales, counting both banks. This holds for every modulus M >= 2, every positive" + } + ], + "status": "answered", + "note": "The answering README states that it answers the even-length gap and that its theorem holds for every modulus M >= 2 and every positive length." + }, + { + "id": "L06", + "asking": { + "package": "paired-plane-rematch-rank34", + "question_index": 0, + "question": "What is the minimum exact fitting rank over all perfect matchings (between 28-type colouring floor and 34)?" + }, + "answers": [ + { + "package": "paired-plane-frame-packing", + "quote": "The literal 112 P112 labels admit **thirteen disjoint orthonormal 8-frames**," + }, + { + "package": "p112-frame-partition", + "quote": "The literal 112 P112 binary labels have **maximum disjoint Gram-I8 packing" + }, + { + "package": "paired-plane-frame-repair", + "quote": "six-groups and three four-groups reduces its **34 scalar queries to 32**." + }, + { + "package": "paired-plane-frame-repair", + "quote": "it supplies no physical decoder, new κ, selected-frontier change, or optimum" + } + ], + "status": "partial", + "note": "The stated first step (is 12 the maximum number of disjoint orthonormal 8-frames?) is answered: thirteen frames are exhibited and the packing number is stated to be exactly 13. For the question itself, the cited READMEs give another matching with fitting rank 32 and say they do not claim the optimum over all matchings, so the minimum over all perfect matchings is not recorded as settled." + }, + { + "id": "L07", + "asking": { + "package": "triangular-parity-n8", + "question_index": 0, + "question": "Does every n=8 symbol with tail l1 at most 1/2 keep every proper prefix at most 3/2?" + }, + "answers": [ + { + "package": "triangular-parity-forward-bound", + "quote": "has **every forward macro-prefix bounded by `1+η` in infinity norm**, provided" + } + ], + "status": "answered-by-scope-inclusion", + "note": "The answering theorem covers every dyadic size and every symbol with tail l1 norm at most eta <= 1, so it includes n = 8 and tail l1 at most 1/2 (bound 3/2). Reading the asking package's per-factor proper prefixes as forward macro-prefixes is done here by inspecting the two definitions; it is not proved in this ledger." + }, + { + "id": "L08", + "asking": { + "package": "triangular-parity-prefix", + "question_index": 0, + "question": "Do nested parity splits keep every proper prefix inside the product of the one-level caps?" + }, + "answers": [ + { + "package": "triangular-parity-forward-bound", + "quote": "has **every forward macro-prefix bounded by `1+η` in infinity norm**, provided" + } + ], + "status": "answered-by-scope-inclusion", + "note": "A cap of 1+eta on every forward macro-prefix is at most a product of two or more one-level caps, since 1+eta >= 1. The reading of proper prefixes as forward macro-prefixes is the same as in L07 and is likewise not proved in this ledger." + }, + { + "id": "L09", + "asking": { + "package": "diagonal-pair-five-call-collisions", + "question_index": 1, + "question": "Does the six-call floor extend to odd characteristic or F4?" + }, + "answers": [ + { + "package": "diagonal-pair-collision-audit", + "quote": "4. **New: the same six-call floor holds over F3 at width two.** Over `F3` there" + }, + { + "package": "diagonal-pair-collision-audit", + "quote": "two. The length-five row is **local SAT evidence**, not a stdlib replay." + } + ], + "status": "partial", + "note": "Odd characteristic is addressed only for F3 at width two, and the answering README labels the length-five row as local SAT evidence rather than a stdlib replay. F4, F5 and larger widths are not claimed there." + }, + { + "id": "L10", + "asking": { + "package": "connector-gray-growth", + "question_index": 0, + "question": "What is the sharp leading constant of N(c)/(c log2 c)?" + }, + "answers": [ + { + "package": "connector-bounded-depth-cap", + "quote": "`(1 + ⌊log₂ c⌋)⌊c/2⌋` lower bound attains this, so **1/2 is the sharp" + }, + { + "package": "connector-bounded-depth-cap", + "quote": "leading constant for depth ≤ 2 block concatenations**." + }, + { + "package": "connector-bounded-depth-cap", + "quote": "The general constant of N(c)/(c log₂ c) stays open in [1/2, 1]. This" + } + ], + "status": "partial", + "note": "The answering README fixes the leading constant at 1/2 for concatenations of blocks of depth at most two and states that the general constant stays open in [1/2, 1]." + } + ] +} diff --git a/research/answered-open-questions-ledger/verify.py b/research/answered-open-questions-ledger/verify.py new file mode 100644 index 0000000000..fe6df2c1d6 --- /dev/null +++ b/research/answered-open-questions-ledger/verify.py @@ -0,0 +1,163 @@ +#!/usr/bin/env python3 +"""Check the answered-open-questions ledger against its pinned sources. + +Every row names an open question stored in one package's TASK.json and one or +more later packages whose README answers it. The check reads only the pinned +input bytes (SHA256 from SOURCES.json), requires each stored question to match +its TASK.json entry exactly, and requires each quote to be a substring of one +README line. Whether a quoted README answers the question is a reading recorded +in the row's status and note; this script does not decide it. + +Standard library only. Explicit exceptions are used, so `python -O` keeps every +check active. Nothing is written. + +Loop bounds are enforced before each loop runs: at most MAX_ROWS rows, at most +MAX_ANSWERS_PER_ROW answers per row, at most MAX_INPUTS pinned inputs and at +most MAX_INPUT_BYTES bytes per input (which bounds the line scans). Memory is +bounded by those limits; Python allocates dynamically, so there is no +preallocation. +""" + +import copy +import hashlib +import json +import re +from pathlib import Path + +PKG = Path(__file__).resolve().parent +ROOT = PKG.parents[1] +STATUSES = ("answered", "answered-by-scope-inclusion", "partial") +MIN_QUOTE = 20 +MAX_ROWS = 100 +MAX_ANSWERS_PER_ROW = 8 +MAX_INPUTS = 200 +MAX_INPUT_BYTES = 1_000_000 + + +class LedgerError(Exception): + """A ledger row or pin failed its check.""" + + +def need(condition, message): + if not condition: + raise LedgerError(message) + + +def load_inputs(): + """Return {path: text} for every live input, after the SHA256 pin check.""" + sources = json.loads((PKG / "SOURCES.json").read_text(encoding="utf-8")) + pins = {row["path"]: row["sha256"] for row in sources["files"] + if row["usage"] == "input"} + need(pins, "SOURCES.json declares no live input") + need(len(pins) <= MAX_INPUTS, "too many pinned inputs") + data = {} + for path, digest in sorted(pins.items()): + raw = (ROOT / path).read_bytes() + need(len(raw) <= MAX_INPUT_BYTES, "pinned input is too large: " + path) + need(hashlib.sha256(raw).hexdigest() == digest, "pin mismatch: " + path) + data[path] = raw.decode("utf-8") + return data + + +def cites_by_path(readme_text, package): + """True if the README names the package as research/ or ../.""" + pattern = r"(?:research/|\.\./)" + re.escape(package) + r"(?![\w-])" + return re.search(pattern, readme_text) is not None + + +def check_row(row, data): + for key in ("id", "asking", "answers", "status", "note"): + need(key in row, "row lacks " + key) + need(row["status"] in STATUSES, "unknown status in " + row["id"]) + need(isinstance(row["note"], str) and row["note"].strip(), "empty note in " + row["id"]) + + asking = row["asking"] + ask_path = "research/%s/TASK.json" % asking["package"] + need(ask_path in data, "asking TASK.json is not a pinned input: " + ask_path) + questions = [q["question"] for q in json.loads(data[ask_path])["open_questions"]] + index = asking["question_index"] + need(isinstance(index, int) and 0 <= index < len(questions), + "question index out of range in " + row["id"]) + need(questions[index] == asking["question"], "question text differs in " + row["id"]) + need(questions.count(asking["question"]) == 1, "question not unique in " + row["id"]) + + need(row["answers"], "no answering package in " + row["id"]) + need(len(row["answers"]) <= MAX_ANSWERS_PER_ROW, "too many answers in " + row["id"]) + for answer in row["answers"]: + package = answer["package"] + need(package != asking["package"], "package answers itself in " + row["id"]) + need("research/%s/TASK.json" % package in data, + "answering package is not pinned: " + package) + path = "research/%s/README.md" % package + need(path in data, "answering README is not a pinned input: " + path) + quote = answer["quote"] + need(isinstance(quote, str) and "\n" not in quote and quote == quote.strip() + and len(quote) >= MIN_QUOTE, "malformed quote in " + row["id"]) + need(any(quote in line for line in data[path].split("\n")), + "quote not found in one line of %s (%s)" % (path, row["id"])) + need(not cites_by_path(data[path], asking["package"]), + "answering README already cites the asking package by path: " + path) + + +def controls(rows, data): + """Each mutated copy of a real row must be rejected with LedgerError.""" + base = rows[0] + other = next(r for r in rows if r["asking"]["package"] != base["asking"]["package"]) + + def mutate(edit): + row = copy.deepcopy(base) + edit(row) + return row + + cases = { + "question text changed": mutate(lambda r: r["asking"].update(question=r["asking"]["question"] + " ")), + "question index moved": mutate(lambda r: r["asking"].update(question_index=0)), + "quote not in README": mutate(lambda r: r["answers"][0].update(quote="a line that no pinned README contains")), + "quote spans a newline": mutate(lambda r: r["answers"][0].update(quote="first line of a quote\nsecond line of it")), + "quote too short": mutate(lambda r: r["answers"][0].update(quote="five-vertex")), + "package answers itself": mutate(lambda r: r["answers"][0].update(package=r["asking"]["package"])), + "answering package unpinned": mutate(lambda r: r["answers"][0].update(package="not-a-pinned-package")), + "unknown status": mutate(lambda r: r.update(status="settled")), + "no answering package": mutate(lambda r: r.update(answers=[])), + "quote taken from another row": mutate(lambda r: r["answers"][0].update(quote=other["answers"][0]["quote"])), + } + cited = dict(data) + path = "research/%s/README.md" % base["answers"][0]["package"] + cited[path] = data[path] + "\nSee ../%s/README.md for the question.\n" % base["asking"]["package"] + attempts = ([(name, row, data) for name, row in cases.items()] + + [("answering README cites the asking package by path", copy.deepcopy(base), cited)]) + for name, row, table in attempts: + try: + check_row(row, table) + except LedgerError: + continue + raise LedgerError("control was accepted: " + name) + return len(attempts) + + +def main(): + ledger_bytes = (PKG / "ledger.json").read_bytes() + ledger = json.loads(ledger_bytes.decode("utf-8")) + need(ledger.get("schema") == "answered-open-questions-ledger/v1", "unknown ledger schema") + rows = ledger["rows"] + need(rows, "empty ledger") + need(len(rows) <= MAX_ROWS, "too many rows") + need(len({r["id"] for r in rows}) == len(rows), "duplicate row id") + need(len({(r["asking"]["package"], r["asking"]["question_index"]) for r in rows}) == len(rows), + "a question appears in two rows") + data = load_inputs() + for row in rows: + check_row(row, data) + n_controls = controls(rows, data) + counts = {s: sum(1 for r in rows if r["status"] == s) for s in STATUSES} + answering = {a["package"] for r in rows for a in r["answers"]} + asking = {r["asking"]["package"] for r in rows} + print("PASS_ANSWERED_OPEN_QUESTIONS_LEDGER rows=%d answered=%d scope_inclusion=%d partial=%d " + "asking_packages=%d answering_packages=%d pinned_inputs=%d controls=%d ledger_sha256=%s" + % (len(rows), counts["answered"], counts["answered-by-scope-inclusion"], counts["partial"], + len(asking), len(answering), len(data), n_controls, + hashlib.sha256(ledger_bytes).hexdigest()[:16])) + + +if __name__ == "__main__": + main()