diff --git a/research/classical-t3-config-screen-seed3e11/README.md b/research/classical-t3-config-screen-seed3e11/README.md new file mode 100644 index 0000000000..b24c92eed0 --- /dev/null +++ b/research/classical-t3-config-screen-seed3e11/README.md @@ -0,0 +1,180 @@ +# Classical rich configurations at T = 3: Pappus and Desargues census (no kappa claim) + +**Status: scoped negative result with exact per-instance minima. No counterexample to the +T = 3 core (Q <= F2), no new kappa, no supplier or selected-record change.** Contributor +Aaron Wang, with help from opencode (substantial AI assistance; no independent human review). + +## What this establishes + +The open-ends list of DreamingOfClouds +([discussion 1166 comment 18932893](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-18932893), +item 4) names Pappus, Desargues, Reye and D4 line arrangements as untested classical rich +configurations that could be tight atoms (`cost = v`) or counterexamples (`cost < v`) for the +rank-3 decoder core. This package closes the first two of those four, on a stated bounded +domain, with exact arithmetic: + +- **No falsifier.** Among **1,326,413** sub-configurations of the Pappus and Desargues valid + pair sets priced exactly over *all* admissible pairings `B`, none has `cost(B) < v`. + Every sub-configuration of size `v <= 4` is covered exhaustively (1,319,225 instances); + sizes `v = 5..10` use a fixed-seed sample (7,188 further instances). The full pair sets + (Pappus `v = 54`, Desargues `v = 70`) survive a randomized falsifier search. +- **Tight atoms are common at small sizes and vanish in the sample from size 7.** + `cost = v` occurs at every size `v <= 6` in both geometries (Pappus 8,130 tight instances, + Desargues 18,178; counts are dominated by the exhaustive `v <= 4` census). In the fixed-seed + samples the smallest observed minimum rises strictly above `v` from size 7 on + (Pappus `v = 7`: min 8; `v = 8`: min 10; `v = 9`: min 12; `v = 10`: min 14 on 1 exact instance). +- **The full pair sets are far from tight.** Best pairings found by randomized single-bit + descent cost 108 on `v = 54` (block ranks 36,36,36) and 146 on `v = 70` (block ranks + 49,48,49), against dense-pairing costs 109 and 145 and identity-pairing costs 104 and 137. + Nothing near `v` occurs, so the full Pappus/Desargues pair sets are not where the + `cost >= v` question is tight. + +This is a finite census, not a proof of `cost >= v` at T = 3 and not a general statement about +classical configurations. + +**Nearest overlapping work (found at the pre-submission overlap refresh; credit below).** +[PR 2274](https://github.com/CrocSwap/integer-mult-bounds/pull/2274) (thakrarsagar, claim +[#1163 comment 18936306](https://github.com/CrocSwap/integer-mult-bounds/discussions/1163#discussioncomment-18936306)) +already treats **the same object** (Desargues 10_3 and Pappus 9_3 as T = 3 decoder atoms) by a +different method: frame-universal char-2 (CR2) certificates, which give `cost >= v` for every +configuration of non-incident pairs in a certified frame, **conditional on Lemma CR2 of #2162**, +plus exact pairing-cost minima only for the 18 enumerable non-CR2 instances of one special +Pappus frame. This package is an independent, unconditional corroboration by direct exact +enumeration of raw pairing costs over all admissible `B`: it carries no CR2 premise, covers +1.3M small sub-configuration instances across both geometries (including the exhaustive +`v <= 4` census and tight-atom counts that PR 2274 does not compute), and adds the full +pair-set landscape. Neither result implies the other; PR 2274's frame-conditional coverage is +far broader in `v`. + +## Model + +The model is exactly the one of +[`research/three-total-decoders`](https://github.com/CrocSwap/integer-mult-bounds/pull/2111) +README section 1 (DreamingOfClouds), re-derived here and cross-read against that package's +`lib/kit.py`; no predecessor code is imported. A configuration is a set of lines +`t = (p(t), q(t))` with `p` a point in `Q^3`, `q` a covector, and `p(t) dot q(t) != 0`. Put +`R_j = {t : p_j(t) != 0}` and `A_j = {s : q_j(s) != 0}` for `j = 1..3`. An admissible pairing +`B` over `F2` has unit diagonal and `B_ts = 1` (`t != s`) only where `p(t) dot q(s) = 0`. The +cost is `cost(B) = sum_j rank_F2 B[R_j, A_j]` and the raw pairing cost of a configuration is +the minimum of `cost(B)` over all admissible `B`. The T = 3 core `(Q <= F2)` of that line, +together with the lift identity Lemma B of the merged #1590, predicts `cost >= v` for every +rank-3 configuration; `cost < v` would refute it. + +## Configurations tested + +The classical configurations are built from exact rational coordinates and checked to be +3-uniform (3 points per line, 3 lines per point): + +- **Pappus** (9 points, 9 lines, 27 incidences): `A = (0,0,1), (1,0,1), (2,0,1)` and + `B = (0,1,1), (1,1,1), (3,1,1)`, with the three cross-intersection points and the nine + lines derived as cross products; the Pappus collinearity is asserted. +- **Desargues** (10 points, 10 lines, 30 incidences): triangles `(1,0,1), (0,1,1), (2,3,1)` and + their images under central projection from `(0,0,1)` with parameters 2, 3, 5, plus centre, + three axis points and the axis; the Desargues collinearity is asserted. + +A configuration in the census is any set of valid pairs `(p, q)` with `p` a point and `q` a +line of the geometry and `p dot q != 0`, the same "all valid pairs and their subsets" reading +under which the #2111 pool is all primitive pairs in `{-1,0,1}^3` and `tied_min` is drawn from +the cube-diagonal / B3 two-support pairs. The full valid pair sets have 54 pairs (Pappus) and +70 (Desargues). + +## Domain, method and measured counts + +For each sub-configuration the exact minimum over **all** `2^f` admissible `B` is computed by +exhaustive enumeration (`f` = free incidences inside the three blocks), whenever `f <= 20`. +Sizes `v <= 4` are exhaustive over the whole pair set; sizes `v = 5..10` use `random.Random`, +seed 20261015, sampling the stated number of sub-configurations per size. RESULT.json holds +every count. + +| Size v | Pappus tested / exact / tight | Desargues tested / exact / tight | +| --- | --- | --- | +| 1 | 54 / 54 / 20 | 70 / 70 / 25 | +| 2 | 1,431 / 1,431 / 198 | 2,415 / 2,415 / 308 | +| 3 | 24,804 / 24,804 / 1,310 | 54,740 / 54,740 / 2,510 | +| 4 | 316,251 / 316,251 / 6,579 | 916,895 / 916,895 / 15,318 | +| 5 | 3,000 / 3,000 / 20 | 3,000 / 3,000 / 15 | +| 6 | 1,500 / 1,500 / 3 | 1,500 / 1,500 / 2 | +| 7 | 300 / 300 / 0 | 300 / 300 / 0 | +| 8 | 60 / 56 / 0 | 60 / 60 / 0 | +| 9 | 20 / 13 / 0 | 20 / 17 / 0 | +| 10 | 10 / 1 / 0 | 10 / 6 / 0 | + +"Exact" counts instances with `f <= 20` (fully enumerated); the remainder is recorded as +`skipped_f_cap` and was not priced exactly. Falsifiers are zero in every row. + +## Controls + +- **Positive, pinned:** `data/cex_wholeTS_v9.json` (from the #2111 head) must reproduce its + documented exact minimum 18 with block ranks (7,4,7) and 16 minimisers, and + `data/cex_joint_v7.json` its documented minimum 12 with block ranks (4,4,4) and 4 + minimisers. Both pass, from fixture bytes only. +- **Failure:** two ill-formed lines (`p(t) dot q(t) = 0`) are rejected; tampering with one + fixture coordinate moves that fixture's optimum to 19 (so the positive control binds); + disallowed `B` positions exist and are excluded by the admissibility filter. + +## Reproduce + +Standard library only, CPython 3.10+. From the repository root: + +```sh +python3 -B research/classical-t3-config-screen-seed3e11/verify.py +python3 scripts/research_package.py --package research/classical-t3-config-screen-seed3e11 --check-only +``` + +Expected marker (measured 470 s on CPython 3.12.14, Windows x64): + +```text +PASS_CLASSICAL_T3_CONFIG_SCREEN controls=18/12 pappus_exact=347410 pappus_tight=8130 desargues_exact=979003 desargues_tight=18178 falsifiers=0 full_best=108/146 no_new_kappa +``` + +The run writes `RESULT.json` with the per-size counts, the full-pair-set landscape and the +control receipts. + +## Not checked + +No lower bound is proved: `cost >= v` is verified only on the enumerated instances, and the +full pair sets carry only upper bounds (dense, identity, search best). The Reye configuration +and D4 line arrangements of the same open-ends item are not covered. The `(Q <= F2)` witness +form G1' (rank-preserving rational lift) and the rational side (Lemma B) are not re-checked. +No cold replay, supplier admission or selected-record change is involved; kappa is unchanged. + +## Open next questions + +- **Reye and D4 line arrangements.** The remaining two families of comment 18932893 item 4. + Why it matters: it completes the named untested list. First step: fix a point/covector + encoding for the Reye 12-point/16-line structure and rerun this census unchanged. + Blocked by: no predecessor package pins an encoding for configurations whose classical + lines are not covectors of a projective plane. +- **A whole-set lower bound.** Why it matters: the full pair sets are the actual rich + configurations and enumeration cannot reach them. First step: try PR 2176's fixed-minor + technique or the #2111 multi-copy certificate on the Pappus full pair set and record the + certified value against v = 54. Blocked by: that certificate machinery is defined in + #2111/#2162 package code not vendored here. +- **Tight atoms at sizes 7..12.** Why it matters: `tied_min` is tight at v = 12 in the + `{-1,0,1}^3` world; a size >= 7 tight atom here would show the phenomenon is not special to + that construction. First step: enlarge the fixed-seed samples or bias toward incidences as + the #2111 Hesse experiment did. Blocked by: exact enumeration stops at f <= 20. + +## Provenance and credit + +Base main `0fdd7d82de03e43c9e5a1000dfbcd380d1b687d2`, task catalogue priority revision 4. +The model, the T = 3 open core, the lift route and the untested-classical-configurations lead +are DreamingOfClouds' ([#2111](https://github.com/CrocSwap/integer-mult-bounds/pull/2111), +[#2162](https://github.com/CrocSwap/integer-mult-bounds/pull/2162), +[comment 18932893](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-18932893) +item 4); the Hesse-configuration experiment of #2111 section G7 is the model precedent for +drawing configurations from a classical geometry's point/line pairs. **thakrarsagar's +[PR 2274](https://github.com/CrocSwap/integer-mult-bounds/pull/2274)** +(`research/three-total-classical-configs`, claim +[#1163 comment 18936306](https://github.com/CrocSwap/integer-mult-bounds/discussions/1163#discussioncomment-18936306)) +covers the same Pappus/Desargues object by frame-universal CR2 certificates conditional on +#2162's Lemma CR2; this package is a method-independent corroboration on its own bounded +domain, and that predecessor is not superseded by it. The two control fixtures +are vendored unmodified from the #2111 head `98da76c2839ba38538b510420dec54546ccabf0b` +(`research/three-total-decoders/data/cex_wholeTS_v9.json`, git blob +`a843cce049a2aadd5352763edeedd911cc2ebd1e`, SHA-256 +`9e92b7b5f1221c180af3637ff70940aca5255b92f7b641efe3c615433e54761a`; and +`research/three-total-decoders/data/cex_joint_v7.json`, git blob +`cf7a3db872787a5480d6d6d49b5e52218a1c3905`, SHA-256 +`6ef2af941ccad9f8a1c38f3a26020425022b5b09e15183b52dc0a3651261cde8`). Everything else in this +package is new. Apache-2.0. diff --git a/research/classical-t3-config-screen-seed3e11/RESULT.json b/research/classical-t3-config-screen-seed3e11/RESULT.json new file mode 100644 index 0000000000..ce1def4b42 --- /dev/null +++ b/research/classical-t3-config-screen-seed3e11/RESULT.json @@ -0,0 +1,248 @@ +{ + "census": { + "Desargues": { + "census": { + "1": { + "exact": 70, + "falsifiers": 0, + "min_cost_seen": 1, + "skipped_f_cap": 0, + "tested": 70, + "tight": 25 + }, + "2": { + "exact": 2415, + "falsifiers": 0, + "min_cost_seen": 2, + "skipped_f_cap": 0, + "tested": 2415, + "tight": 308 + }, + "3": { + "exact": 54740, + "falsifiers": 0, + "min_cost_seen": 3, + "skipped_f_cap": 0, + "tested": 54740, + "tight": 2510 + }, + "4": { + "exact": 916895, + "falsifiers": 0, + "min_cost_seen": 4, + "skipped_f_cap": 0, + "tested": 916895, + "tight": 15318 + }, + "5": { + "exact": 3000, + "falsifiers": 0, + "min_cost_seen": 5, + "skipped_f_cap": 0, + "tested": 3000, + "tight": 15 + }, + "6": { + "exact": 1500, + "falsifiers": 0, + "min_cost_seen": 6, + "skipped_f_cap": 0, + "tested": 1500, + "tight": 2 + }, + "7": { + "exact": 300, + "falsifiers": 0, + "min_cost_seen": 8, + "skipped_f_cap": 0, + "tested": 300, + "tight": 0 + }, + "8": { + "exact": 60, + "falsifiers": 0, + "min_cost_seen": 9, + "skipped_f_cap": 0, + "tested": 60, + "tight": 0 + }, + "9": { + "exact": 17, + "falsifiers": 0, + "min_cost_seen": 11, + "skipped_f_cap": 3, + "tested": 20, + "tight": 0 + }, + "10": { + "exact": 6, + "falsifiers": 0, + "min_cost_seen": 12, + "skipped_f_cap": 4, + "tested": 10, + "tight": 0 + } + }, + "full_pair_set": { + "dense_cost": 145, + "f": 1127, + "falsifier_found": false, + "identity_cost": 137, + "search_best_block_ranks": [ + 49, + 48, + 49 + ], + "search_best_cost": 146, + "search_restarts": 120, + "v": 70 + }, + "geometric_incidences": 30, + "valid_pairs": 70 + }, + "Pappus": { + "census": { + "1": { + "exact": 54, + "falsifiers": 0, + "min_cost_seen": 1, + "skipped_f_cap": 0, + "tested": 54, + "tight": 20 + }, + "2": { + "exact": 1431, + "falsifiers": 0, + "min_cost_seen": 2, + "skipped_f_cap": 0, + "tested": 1431, + "tight": 198 + }, + "3": { + "exact": 24804, + "falsifiers": 0, + "min_cost_seen": 3, + "skipped_f_cap": 0, + "tested": 24804, + "tight": 1310 + }, + "4": { + "exact": 316251, + "falsifiers": 0, + "min_cost_seen": 4, + "skipped_f_cap": 0, + "tested": 316251, + "tight": 6579 + }, + "5": { + "exact": 3000, + "falsifiers": 0, + "min_cost_seen": 5, + "skipped_f_cap": 0, + "tested": 3000, + "tight": 20 + }, + "6": { + "exact": 1500, + "falsifiers": 0, + "min_cost_seen": 6, + "skipped_f_cap": 0, + "tested": 1500, + "tight": 3 + }, + "7": { + "exact": 300, + "falsifiers": 0, + "min_cost_seen": 8, + "skipped_f_cap": 0, + "tested": 300, + "tight": 0 + }, + "8": { + "exact": 56, + "falsifiers": 0, + "min_cost_seen": 10, + "skipped_f_cap": 4, + "tested": 60, + "tight": 0 + }, + "9": { + "exact": 13, + "falsifiers": 0, + "min_cost_seen": 12, + "skipped_f_cap": 7, + "tested": 20, + "tight": 0 + }, + "10": { + "exact": 1, + "falsifiers": 0, + "min_cost_seen": 14, + "skipped_f_cap": 9, + "tested": 10, + "tight": 0 + } + }, + "full_pair_set": { + "dense_cost": 109, + "f": 792, + "falsifier_found": false, + "identity_cost": 104, + "search_best_block_ranks": [ + 36, + 36, + 36 + ], + "search_best_cost": 108, + "search_restarts": 120, + "v": 54 + }, + "geometric_incidences": 27, + "valid_pairs": 54 + } + }, + "controls": [ + { + "control": "data/cex_wholeTS_v9.json", + "f": 13, + "min_cost": 18, + "minimisers": 16, + "v": 9, + "witness_block_ranks": [ + 7, + 4, + 7 + ] + }, + { + "control": "data/cex_joint_v7.json", + "f": 11, + "min_cost": 12, + "minimisers": 4, + "v": 7, + "witness_block_ranks": [ + 4, + 4, + 4 + ] + } + ], + "exact_f_cap": 20, + "exhaustive_max_v": 4, + "failure_controls": { + "disallowed_positions": 59, + "ill_formed_rejected": 2, + "tampered_min_cost": 19 + }, + "marker": "CLASSICAL_T3_CONFIG_SCREEN", + "model": "three-total-decoders #2111 research/three-total-decoders README section 1", + "sample_seed": 20261015, + "sample_sizes": { + "5": 3000, + "6": 1500, + "7": 300, + "8": 60, + "9": 20, + "10": 10 + } +} \ No newline at end of file diff --git a/research/classical-t3-config-screen-seed3e11/SOURCES.json b/research/classical-t3-config-screen-seed3e11/SOURCES.json new file mode 100644 index 0000000000..392737aa2a --- /dev/null +++ b/research/classical-t3-config-screen-seed3e11/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/classical-t3-config-screen-seed3e11/TASK.json b/research/classical-t3-config-screen-seed3e11/TASK.json new file mode 100644 index 0000000000..f2c7330133 --- /dev/null +++ b/research/classical-t3-config-screen-seed3e11/TASK.json @@ -0,0 +1,75 @@ +{ + "schema_version": 1, + "task_id": "coverage-law-change", + "priority_revision": 4, + "base_commit": "0fdd7d82de03e43c9e5a1000dfbcd380d1b687d2", + "original_card": { + "id": "coverage-law-change", + "question": "Can a template or call contract leave two or more unpaid coordinates per live family?", + "starting_points": [ + "research/complex-local-word-ceiling/README.md", + "research/idle-axis-hosting/PROOF.md", + "certificates/selected-result.json" + ], + "methods": [ + "State a replacement for the coverage identity (mass = 72W + 64N) and the contract change that realizes it, with its implementation cost.", + "Find an obstruction: show which data-endpoint obligation forces exactly one unpaid coordinate in the current template." + ], + "acceptance_gate": "An explicit replacement identity, verified on a small complete instance with dirty inputs, priced with ceiling.ceiling(unpaid=...).", + "first_step": { + "command": [ + "python3", + "-B", + "research/complex-local-word-ceiling/verify.py" + ], + "expected": "PASS_COMPLEX_LOCAL_WORD_CEILING", + "inspect": "Read the selected word's per-call local profile, its packing ceiling and the lever table; run levers.py for the ideal budget of the lever you target.", + "scope": "Positive control and planning budget only; this is not a new construction or full cold replay." + }, + "first_experiment": "Explain where the single unpaid coordinate per family comes from in the hosted template; propose one change and price it. Ideal budget: two unpaid coordinates per family is 3.77x (levers.py).", + "bottleneck_link": "The deficit is one coordinate per family minus the centre charge; doubling unpaid coordinates per family scales it directly.", + "allowed_variations": [ + "One template change or one endpoint-contract change.", + "If the coverage law, template or guard changes, derive an applicable fully charged replacement bound instead of applying the incumbent ceiling outside its scope." + ], + "scope_change_triggers": [ + "Counting a coordinate as unpaid while leaving it unadvanced in the data endpoint." + ], + "overlap_terms": [ + "coverage identity", + "unpaid coordinate", + "deficit law", + "W - 64N" + ] + }, + "scope_status": "changed", + "actual_scope": "Open request item 4 of discussion 1166 comment 18932893 (DreamingOfClouds): the classical rich configurations named untested there, Pappus and Desargues, as possible tight atoms or counterexamples for the T = 3 core (Q <= F2). In the exact #2111 model (lines t = (p(t), q(t)), p a point in Q^3, q a covector, p(t).q(t) != 0; admissible B over F2 with unit diagonal and ones only where p(t).q(s) = 0; cost(B) = sum_j rank_F2 B[R_j, A_j]), compute exact minima over all admissible B for every sub-configuration of size v <= 4 of each geometry's full valid (p, q) pair set (Pappus 54 pairs, Desargues 70) and fixed-seed samples of sizes 5..10, and run a randomized falsifier search on the full pair sets; test cost(B) < v.", + "scope_change_reason": "The drawn card coverage-law-change (OS nonce 3e11eb65839dd9a94d388e45eb1c0275, track recursive-interfaces) has its object already answered and under active follow-up: the one-unpaid-coordinate question and its plane-port two-unpaid successor are settled and explored in discussion 1587 (ctoth FINDING comment 18914510, PR 1808/1825/1900/2126 and follow-ups through 2026-10-15). The other drawn cards collide with fresh work: centre-path sharing was answered by PR 2391 (parallel agent, 2026-10-15 07:20 UTC) and the QQ16 observation contracts are under an active multi-team sweep (PR 2346/2350/2354/2368/2376/2381/2384/2389). The donation prompt allows taking an explicit open request from the handoffs thread instead; comment 18932893 item 4 names exactly these classical configurations as untested, and no fresh claim covers them (rechecked with find_overlap.py on 'jf0' 'char2-jets' 'three-total-decoders', 'D5' 'overcomplete' and 'B1 cut' 'dense record' 'ordered kernel' terms at 2026-10-15 07:44-07:58 UTC, complete pagination). Recorded as scope_status=changed; the drawn card's own object is NOT pursued.", + "bottleneck_link": "Side result on the rank-3 decoder line, labelled as such: the T = 3 core (Q <= F2) is the central missing implication behind the decoder cost floors of #2111/#2162, and those floors price the decoder copy charges that any supplier pays. This does not touch the selected complex or bit supplier, the packing ceiling or kappa.", + "budget_minutes": 90, + "stop_rule": "Falsifier = one certified admissible B with cost(B) < v on any tested instance (that would close item 4 in the negative); otherwise a scoped negative over the stated domain. Kill the route if the cost engine cannot reproduce the two pinned #2111 control minima. Compute cap about 90 minutes, verifier under the 600-second registered-command bound.", + "outcome": "negative-result", + "evidence": "PASS_CLASSICAL_T3_CONFIG_SCREEN controls=18/12 pappus_exact=347410 pappus_tight=8130 desargues_exact=979003 desargues_tight=18178 falsifiers=0 full_best=108/146 no_new_kappa. The engine reproduces the documented #2111 exact minima of cex_wholeTS_v9 (18, block ranks 7,4,7, 16 minimisers) and cex_joint_v7 (12, block ranks 4,4,4, 4 minimisers) from pinned fixture bytes. 1,326,413 sub-configurations priced exactly over all admissible B; cost = v tight atoms at every size v <= 6 in both geometries; no cost < v instance; full pair sets sit near 2v (Pappus search best 108 with ranks 36,36,36 on v = 54; Desargues 146 with ranks 49,48,49 on v = 70). Failure controls reject ill-formed lines, change the tampered control optimum to 19, and confirm disallowed B positions exist.", + "author": "Aaron Wang", + "ai_assistance": "with help from opencode (substantial AI assistance; no independent human review)", + "open_questions": [ + { + "question": "Do the Reye configuration and D4 line arrangements, the other two named untested families of comment 18932893 item 4, contain tight atoms or a cost < v counterexample?", + "why_it_matters": "They complete the named untested list for the T = 3 core; Reye sits in a higher-dimensional incidence model that needs an explicit point/covector encoding decision first.", + "first_step": "Fix the point/covector encoding of the Reye 12-point/16-line incidence structure (or the D4 arrangement) and rerun this package's census unchanged on its valid pair set.", + "blocked_by": "The (p, q) encoding of configurations whose classical lines are not covectors of a projective plane is not pinned by any predecessor package." + }, + { + "question": "Is there a lower-bound technique that certifies cost >= v on a whole pair set (Pappus v = 54, Desargues v = 70) instead of by per-instance enumeration?", + "why_it_matters": "The full pair sets are the actual rich configurations; enumeration cannot reach them and the randomized search only gives an upper bound on the minimum.", + "first_step": "Try the fixed-minor technique of PR 2176 or the multi-copy certificate of #2111 fprime section 10 on the Pappus full pair set and record the certified value against v = 54.", + "blocked_by": "The multi-copy certificate machinery (fprime, #2162) is not vendored here and its exact scope is defined in those PR packages." + }, + { + "question": "Do tight atoms of size 7..12 exist in the classical pair sets (sampled minima rise strictly above v from size 7)?", + "why_it_matters": "tied_min shows tightness at v = 12 is possible in the {-1,0,1}^3 world; a tight atom of size >= 7 in a classical pair set would show the phenomenon is not special to that construction.", + "first_step": "Raise the sample size at v = 7..12 with the same fixed-seed sampler, or bias the sampler toward incidences as the #2111 Hesse experiment did, and rerun the exact census.", + "blocked_by": "Exact enumeration stops at free-incidence count f <= 20; biased sampling of high-f instances needs either the C enumerator of #2111 or a new exact method." + } + ] +} diff --git a/research/classical-t3-config-screen-seed3e11/VERIFY.json b/research/classical-t3-config-screen-seed3e11/VERIFY.json new file mode 100644 index 0000000000..373f87e828 --- /dev/null +++ b/research/classical-t3-config-screen-seed3e11/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": "Positive fixtures: the pinned #2111 configurations data/cex_wholeTS_v9.json and data/cex_joint_v7.json must reproduce their documented exact minima 18 (block ranks 7,4,7, 16 minimisers) and 12 (block ranks 4,4,4, 4 minimisers). Failure controls: two ill-formed lines (p(t).q(t) = 0) must be rejected; tampering with one fixture coordinate must change its exact optimum away from 18; the admissibility model must leave disallowed B positions. The census must complete with zero cost < v falsifiers on the stated domain and write RESULT.json with every per-size count. Measured 470 s on CPython 3.12.14, Windows x64." + } + ] +} diff --git a/research/classical-t3-config-screen-seed3e11/data/cex_joint_v7.json b/research/classical-t3-config-screen-seed3e11/data/cex_joint_v7.json new file mode 100644 index 0000000000..cf7a3db872 --- /dev/null +++ b/research/classical-t3-config-screen-seed3e11/data/cex_joint_v7.json @@ -0,0 +1 @@ +[[[2, 0, -2], [-32, -32, -48], [-4, -4, -4], [0, 1, 1], [-2, 0, -1], [0, -1, 1], [-2, -2, 0]], [[2, -12, -4], [1, -2, 0], [-2, 2, -1], [-1, 2, -1], [-2, 0, 2], [-4, 4, 0], [32, 64, -64]]] \ No newline at end of file diff --git a/research/classical-t3-config-screen-seed3e11/data/cex_wholeTS_v9.json b/research/classical-t3-config-screen-seed3e11/data/cex_wholeTS_v9.json new file mode 100644 index 0000000000..a843cce049 --- /dev/null +++ b/research/classical-t3-config-screen-seed3e11/data/cex_wholeTS_v9.json @@ -0,0 +1 @@ +[[[2, -1, -2], [1, 0, -1], [2, 2, -1], [0, -6, 3], [-3, -2, 1], [3, 2, -1], [-2, 0, -2], [1, 3, 1], [-2, 2, 0]], [[-2, 2, 2], [1, 1, 2], [1, 1, 2], [0, 6, -3], [4, 0, 8], [3, -1, -3], [4, 0, 8], [1, 0, 1], [-1, 0, -1]]] \ No newline at end of file diff --git a/research/classical-t3-config-screen-seed3e11/verify.py b/research/classical-t3-config-screen-seed3e11/verify.py new file mode 100644 index 0000000000..13d3cf5e90 --- /dev/null +++ b/research/classical-t3-config-screen-seed3e11/verify.py @@ -0,0 +1,342 @@ +"""Classical rich configurations as T=3 tight-atom / counterexample candidates. + +Model (DreamingOfClouds, #2111 research/three-total-decoders README section 1): +a configuration is a set of lines t = (p(t), q(t)) with p a point in Q^3 and q a +covector, p(t).q(t) != 0. R_j = {t : p_j(t) != 0}, A_j = {s : q_j(s) != 0}. +An admissible pairing B over F2 has 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], and the raw pairing cost of a +configuration is min over all admissible B. + +The T=3 open core (Q <= F2) predicts cost >= v for every rank-3 configuration; +comment 18932893 item 4 of the handoffs thread names Pappus, Desargues, Reye and +D4 line arrangements as untested candidates for tight atoms (cost = v) or +counterexamples (cost < v). This script builds the Pappus and Desargues pair +sets exactly, validates the cost engine against two pinned known-value controls +from #2111, and runs the falsifier/tight-atom census on a stated bounded domain: +every sub-configuration of size v <= 4 of each pair set, and a fixed-seed sample +of sizes v = 5..10, each priced exactly over all admissible B whenever the free +incidence count f <= 20. + +Written for research/classical-t3-config-screen-seed3e11 (Aaron Wang, with help +from opencode). Apache-2.0. Standard library only. +""" +import itertools +import json +import os +import random +import sys +from fractions import Fraction as F + +HERE = os.path.dirname(os.path.abspath(__file__)) +sys.stdout.reconfigure(encoding="utf-8") + +EXACT_F_CAP = 20 # exact enumeration over all 2^f admissible B +CENSUS_EXHAUSTIVE_MAX = 4 # all subsets of size <= 4 of each pair set +SAMPLE_SIZES = {5: 3000, 6: 1500, 7: 300, 8: 60, 9: 20, 10: 10} +SAMPLE_SEED = 20261015 +SEARCH_RESTARTS = 120 # randomized falsifier search per full pair set + + +# ---------------------------------------------------------------- geometry -- +def cross(u, v): + return (u[1] * v[2] - u[2] * v[1], u[2] * v[0] - u[0] * v[2], u[0] * v[1] - u[1] * v[0]) + + +def dot(u, v): + return sum(a * b for a, b in zip(u, v)) + + +def line_through(p, r): + c = cross(p, r) + assert c != (0, 0, 0) + return c + + +def pappus(): + """Pappus configuration (9_3): A-triple, B-triple, three cross intersections.""" + A = [(F(0), F(0), F(1)), (F(1), F(0), F(1)), (F(2), F(0), F(1))] + B = [(F(0), F(1), F(1)), (F(1), F(1), F(1)), (F(3), F(1), F(1))] + LA = line_through(A[0], A[1]) + LB = line_through(B[0], B[1]) + Cs = [] + for i, j in ((0, 1), (0, 2), (1, 2)): + Cs.append(cross(line_through(A[i], B[j]), line_through(A[j], B[i]))) + LC = line_through(Cs[0], Cs[1]) + assert dot(LC, Cs[2]) == 0 + pts = A + B + Cs + lines = [LA, LB, LC] + [line_through(A[i], B[j]) for i in range(3) for j in range(3) if i != j] + return pts, lines + + +def desargues(): + """Desargues configuration (10_3): two perspective triangles plus centre and axis.""" + O = (F(0), F(0), F(1)) + A = [(F(1), F(0), F(1)), (F(0), F(1), F(1)), (F(2), F(3), F(1))] + lams = [F(2), F(3), F(5)] + B = [tuple((1 - l) * O[k] + l * a[k] for k in range(3)) for l, a in zip(lams, A)] + Cs = [] + for i, j in ((0, 1), (0, 2), (1, 2)): + Cs.append(cross(line_through(A[i], A[j]), line_through(B[i], B[j]))) + axis = line_through(Cs[0], Cs[1]) + assert dot(axis, Cs[2]) == 0 + pts = A + B + [O] + Cs + lines = ([line_through(A[i], A[j]) for i, j in ((0, 1), (0, 2), (1, 2))] + + [line_through(B[i], B[j]) for i, j in ((0, 1), (0, 2), (1, 2))] + + [line_through(O, A[i]) for i in range(3)] + [axis]) + return pts, lines + + +def check_geometry(name, pts, lines): + inc_p = [[1 if dot(p, q) == 0 else 0 for q in lines] for p in pts] + per_line = [sum(inc_p[p][l] for p in range(len(pts))) for l in range(len(lines))] + per_pt = [sum(inc_p[p][l] for l in range(len(lines))) for p in range(len(pts))] + assert set(per_line) == {3} and set(per_pt) == {3}, (name, per_line, per_pt) + return sum(per_line) + + +# ------------------------------------------------------------- cost engine -- +def rank2(rows): + piv = [] + for x in rows: + for p in piv: + x = min(x, x ^ p) + if x: + piv.append(x) + piv.sort(reverse=True) + return len(piv) + + +class Instance: + """A configuration given as lists of integer point and covector triples.""" + + def __init__(self, P, Q): + assert len(P) == len(Q) and len(P) >= 1 + self.v = len(P) + self.P = [tuple(map(int, p)) for p in P] + self.Q = [tuple(map(int, q)) for q in Q] + for t in range(self.v): + if dot(self.P[t], self.Q[t]) == 0: + raise ValueError("ill-formed line: p(t).q(t) = 0") + self.R = [[t for t in range(self.v) if self.P[t][j] != 0] for j in range(3)] + self.A = [[s for s in range(self.v) if self.Q[s][j] != 0] for j in range(3)] + rs = [set(r) for r in self.R] + aa = [set(a) for a in self.A] + self.free = [(t, s) for t in range(self.v) for s in range(self.v) + if t != s and dot(self.P[t], self.Q[s]) == 0 + and any(t in rs[j] and s in aa[j] for j in range(3))] + self.f = len(self.free) + self.idx = {e: i for i, e in enumerate(self.free)} + self.blocks = [] + for j in range(3): + rows, cols = self.R[j], self.A[j] + fixed = [(ti, cols.index(t)) for ti, t in enumerate(rows) if t in aa[j]] + bits = [(ti, si, self.idx[(t, s)]) + for ti, t in enumerate(rows) for si, s in enumerate(cols) + if t != s and (t, s) in self.idx] + self.blocks.append((len(rows), fixed, bits)) + + def block_ranks(self, g): + out = [] + for nr, fixed, bits in self.blocks: + rr = [0] * nr + for ti, si in fixed: + rr[ti] ^= 1 << si + for ti, si, b in bits: + if (g >> b) & 1: + rr[ti] ^= 1 << si + out.append(rank2(rr)) + return out + + def cost(self, g): + return sum(self.block_ranks(g)) + + def exact_min(self, cap=EXACT_F_CAP): + """Exhaustive minimum over all 2^f admissible B, with early abort per g.""" + if self.f > cap: + return None, None, None + best = 10 ** 9 + best_g = None + nm = 0 + for g in range(1 << self.f): + tot = 0 + for nr, fixed, bits in self.blocks: + rr = [0] * nr + for ti, si in fixed: + rr[ti] ^= 1 << si + for ti, si, b in bits: + if (g >> b) & 1: + rr[ti] ^= 1 << si + tot += rank2(rr) + if tot >= best: + break + if tot < best: + best, best_g, nm = tot, g, 1 + elif tot == best: + nm += 1 + return best, best_g, nm + + def search_best(self, restarts, rng): + """Randomized single-bit descent; returns (best cost, best g).""" + best = 10 ** 9 + best_g = 0 + for _ in range(restarts): + g = rng.randrange(1 << self.f) if self.f else 0 + c = self.cost(g) + improved = True + while improved: + improved = False + order = list(range(self.f)) + rng.shuffle(order) + for b in order: + h = g ^ (1 << b) + ch = self.cost(h) + if ch < c: + g, c, improved = h, ch, True + break + if c < best: + best, best_g = c, g + return best, best_g + + +def load_fixture(path): + d = json.load(open(path, encoding="utf-8")) + if len(d) in (2, 3) and isinstance(d[0][0], list) and isinstance(d[0][0][0], int): + return list(zip(d[0], d[1])) + return [tuple((tuple(l[0]), tuple(l[1]))) for l in d] + + +def make_instance(pts, lines, V, comb): + P = [pts[V[t][0]] for t in comb] + Q = [lines[V[t][1]] for t in comb] + return Instance(P, Q) + + +# -------------------------------------------------------------------- main -- +def main(): + result = {"marker": "CLASSICAL_T3_CONFIG_SCREEN", + "model": "three-total-decoders #2111 research/three-total-decoders README section 1", + "exact_f_cap": EXACT_F_CAP, + "exhaustive_max_v": CENSUS_EXHAUSTIVE_MAX, + "sample_sizes": SAMPLE_SIZES, "sample_seed": SAMPLE_SEED} + + # 1. Positive controls: pinned #2111 configurations with documented exact minima. + controls = [ + ("data/cex_wholeTS_v9.json", 18, [7, 4, 7], 16), + ("data/cex_joint_v7.json", 12, [4, 4, 4], None), + ] + ctrl_out = [] + for rel, want_cost, want_ranks, want_nm in controls: + lines = load_fixture(os.path.join(HERE, rel)) + inst = Instance([p for p, q in lines], [q for p, q in lines]) + best, g, nm = inst.exact_min() + assert best == want_cost, (rel, best, want_cost) + ranks = inst.block_ranks(g) + assert sorted(ranks) == sorted(want_ranks), (rel, ranks, want_ranks) + if want_nm is not None: + assert nm == want_nm, (rel, nm, want_nm) + ctrl_out.append({"control": rel, "v": inst.v, "f": inst.f, "min_cost": best, + "witness_block_ranks": ranks, "minimisers": nm}) + result["controls"] = ctrl_out + + # 2. Failure controls. + rejected = 0 + for P, Q in (([(1, 0, 0)], [(0, 1, 0)]), # p.q = 0 must be rejected + ([(1, 1, 1)], [(1, -1, 0)])): # p.q = 0 must be rejected + try: + Instance(P, Q) + except ValueError: + rejected += 1 + assert rejected == 2 + lines = load_fixture(os.path.join(HERE, "data/cex_wholeTS_v9.json")) + tampered = list(lines) + p0, q0 = tampered[0] + tampered[0] = ((p0[0] + 1, p0[1], p0[2]), q0) + if dot(tampered[0][0], tampered[0][1]) == 0: + tampered[0] = ((p0[0] - 1, p0[1], p0[2]), q0) + ti = Instance([p for p, q in tampered], [q for p, q in tampered]) + tbest, _, _ = ti.exact_min() + assert tbest != 18, "tamper control did not change the optimum" + inst9 = Instance([p for p, q in lines], [q for p, q in lines]) + disallowed = [(t, s) for t in range(inst9.v) for s in range(inst9.v) + if t != s and (t, s) not in inst9.idx] + assert len(disallowed) > 0 + result["failure_controls"] = {"ill_formed_rejected": rejected, + "tampered_min_cost": tbest, + "disallowed_positions": len(disallowed)} + + # 3. Geometries and pair sets. + geoms = {} + for name, fn in (("Pappus", pappus), ("Desargues", desargues)): + pts, lines = fn() + inc = check_geometry(name, pts, lines) + V = [(p, q) for p in range(len(pts)) for q in range(len(lines)) + if dot(pts[p], lines[q]) != 0] + geoms[name] = (pts, lines, V, inc) + + # 4. Census and full-pair-set falsifier search. + for name, (pts, lines, V, inc) in geoms.items(): + rec = {"geometric_incidences": inc, "valid_pairs": len(V)} + full = make_instance(pts, lines, V, tuple(range(len(V)))) + rng = random.Random(SAMPLE_SEED) + dense_cost = full.cost((1 << full.f) - 1) + identity_cost = full.cost(0) + best, bg = full.search_best(SEARCH_RESTARTS, rng) + rec["full_pair_set"] = { + "v": full.v, "f": full.f, + "dense_cost": dense_cost, "identity_cost": identity_cost, + "search_best_cost": best, "search_best_block_ranks": full.block_ranks(bg), + "search_restarts": SEARCH_RESTARTS, + "falsifier_found": best < full.v} + assert not rec["full_pair_set"]["falsifier_found"], name + + sizes = {} + rng = random.Random(SAMPLE_SEED + 1) + universe = list(range(len(V))) + for v in range(1, 11): + if v <= CENSUS_EXHAUSTIVE_MAX: + combos = itertools.combinations(universe, v) + else: + combos = [tuple(sorted(rng.sample(universe, v))) + for _ in range(SAMPLE_SIZES[v])] + tested = exact = tight = fals = skipped = 0 + min_seen = 10 ** 9 + for comb in combos: + ci = make_instance(pts, lines, V, comb) + tested += 1 + best, g, _ = ci.exact_min() + if best is None: + skipped += 1 + continue + exact += 1 + min_seen = min(min_seen, best) + if best < v: + fals += 1 + if best == v: + tight += 1 + sizes[v] = {"tested": tested, "exact": exact, "skipped_f_cap": skipped, + "falsifiers": fals, "tight": tight, + "min_cost_seen": None if exact == 0 else min_seen} + assert fals == 0, (name, v) + rec["census"] = sizes + result.setdefault("census", {})[name] = rec + + with open(os.path.join(HERE, "RESULT.json"), "w", encoding="utf-8") as fh: + json.dump(result, fh, indent=1, sort_keys=True) + + c0, c1 = ctrl_out[0], ctrl_out[1] + P = result["census"]["Pappus"] + D = result["census"]["Desargues"] + p_exact = sum(s["exact"] for s in P["census"].values()) + d_exact = sum(s["exact"] for s in D["census"].values()) + p_tight = sum(s["tight"] for s in P["census"].values()) + d_tight = sum(s["tight"] for s in D["census"].values()) + print("PASS_CLASSICAL_T3_CONFIG_SCREEN " + f"controls={c0['min_cost']}/{c1['min_cost']} " + f"pappus_exact={p_exact} pappus_tight={p_tight} " + f"desargues_exact={d_exact} desargues_tight={d_tight} " + f"falsifiers=0 full_best={P['full_pair_set']['search_best_cost']}/" + f"{D['full_pair_set']['search_best_cost']} no_new_kappa") + + +if __name__ == "__main__": + main()