diff --git a/research/six-trio-complete-profile-audit/README.md b/research/six-trio-complete-profile-audit/README.md new file mode 100644 index 0000000000..4e8881771b --- /dev/null +++ b/research/six-trio-complete-profile-audit/README.md @@ -0,0 +1,156 @@ +# Complete the six-source one-TRIO census domain + +This resolves the profile omission identified in the maintainer review of +[PR2134](https://github.com/CrocSwap/integer-mult-bounds/pull/2134), head +388a63c83cf24c3355be9798bde5a381188dadb3. The full legal domain contains five +singleton-count profiles and 5,675,670 canonical words, rather than the two +profiles and 2,342,340 words accepted by its filter. Two enumeration methods +agree on every per-profile histogram. The claimed maximum survives: 61 of 63 +nonzero masks, attained by 88 canonical words. The best completed unit-call +bill remains 144, versus the credited 142-call singleton incumbent. + +This repairs the existing finite result's completeness. It does not claim its +witness, cost formula or maximum as a new construction, or extend the search +to more calls or another alphabet. + +## Exact domain and complete profile proof + +Retain six read-only sources, one arbitrary dirty connector, arbitrary dirty +output targets, thirteen singleton source calls, and one atomic TRIO toggling +three distinct sources. Readouts observe the connector at call boundaries; +their targets are unread until completion. Each complete call restores private +scratch and preserves other rows. The schedule must work for arbitrary +compatible linear maps and inputs over F2. The combined TRIO remains a changed +alphabet assumption; its native realization and extra costs are not free. + +Let c_j be singleton multiplicities. Every source must have even total count +at least two. Hence every c_j>=1 (zero cannot become two with one TRIO), their +sum is 13, and exactly three are odd. The unique restoring TRIO acts on those +odd labels. Conversely these conditions suffice: odd positive counts become +even and at least two; already-even counts are at least two. + +The total sorted profiles are (2,2,2,2,4,4) and (2,2,2,2,2,6). Subtract one from +*any three distinct positions*, rather than one selected choice in each profile: + +| Sorted singleton counts | Canonical words | Maximum nonzero coverage | Old filter | +| --- | ---: | ---: | --- | +| 1,1,1,2,2,6 | 180180 | 45 | omitted | +| 1,1,1,2,4,4 | 450450 | 50 | omitted | +| 1,1,2,2,2,5 | 540540 | 54 | retained | +| 1,1,2,2,3,4 | 2702700 | 58 | omitted | +| 1,2,2,2,3,3 | 1801800 | 61 | retained | + +Independently enumerate positive nondecreasing six-tuples summing 13 and keep +exactly three odd entries. This yields the same five profiles exhaustively, +since each entry lies between 1 and 8. The review's omitted example with counts +(1,1,1,2,2,6) passes the complete predicate and fails the pinned predecessor's +actual `analyze_word`. That source remains unchanged and receives credit for +its valid subdomain. + +## Why the TRIO can be last + +The valid invariance is **cyclic rotation of the closed path**, not arbitrary +commutation of adjacent calls. Let the 14 edge masks have XOR sum 0, with prefix +vertices q_0=0,...,q_14=q_0. Rotate the edge sequence to start just after its +unique TRIO. Every new boundary vertex is an old q_i XOR the new starting +vertex, so all pair differences are unchanged. The TRIO is now last. The +duplicate closing vertex adds no new difference, making q_0 through q_13 +the complete boundary set. Repeated vertices are allowed. + +Source-label permutations preserve coverage too. Thus the census covers every +TRIO placement. Controls check all 14 rotations of the witness and exhibit an +adjacent commuting swap that changes its coverage set; the stronger arbitrary- +commutation assertion is unnecessary and is not used. + +## Two complete enumerations + +The Python primary fixes each sorted multiplicity profile, labels coordinates +by their total counts, and orders equal-count labels by first occurrence. It +enumerates multiset permutations under only that equal-count symmetry. Every +source-relabeling orbit has exactly one representative. For profile c its +independent combinatorial count is + + 13! / (product_j c_j! * product_v multiplicity(v)!). + +The program checks this count for each profile. It stores occupied prefixes +in a 64-bit mask; adding vertex q contributes that set translated by XOR q, +implemented by exact bit-block swaps. This differs from the predecessor's +list-based incremental calculation and the native direct-pair calculation. + +The C++ cross-check enumerates all 9,321,312 restricted-growth words on six +labels. It admits a leaf solely when exactly three counts are odd, recomputes +all pair differences from its 14 prefixes, and records a separate histogram +per profile. Every histogram matches Python. Neither acceptance predicate uses +the old two-profile list. Summing the new rows belonging to that old list +reproduces every bin of its recorded histogram, including maximum 61 and 88 +maximizers. The finite exclusion depends on these completed exhaustive runs; +it is not inferred from a sampled subset or receipt alone. + +## Completed bill and limits + +An arbitrary dirty connector requires an even number of readouts for each +active output. Paired readouts realize precisely prefix differences. At most 61 +of 63 masks are paired, so at least two outputs need four or more readouts: +the total is at least 61*2+2*4=130. The credited witness repairs its missing +masks 11 and 40 with four readouts each, attaining 130. Adding 14 source calls +gives 144. The retained full-cover singleton word uses 126 readouts and 142 calls. + +The attaining witness has the incumbent's source-map multiplicity multiset. +With common dispatch/frame price f, readout price g, and all incremental TRIO +expenses rho, its difference is -2f+4g+rho, or 2+rho at unit prices. No native +TRIO implementation, free workspace, favorable nonuniform tariff, hosted +invoice, selected supplier or new kappa follows. Additional TRIO calls, +different readouts and different restoration rules are outside this theorem. + +The two algorithms share model-assisted development. Their different symmetry +quotients and coverage calculations are computational cross-checks, not +independent human authorship or formal-kernel verification. + +## Reproduce + +Python 3.12+, standard library only (about 17 seconds locally): + +```sh +python3 -I -O -B research/six-trio-complete-profile-audit/verify.py +python3 scripts/research_package.py --package research/six-trio-complete-profile-audit +``` + +Separate C++17 full census: + +```sh +g++ -O3 -std=c++17 research/six-trio-complete-profile-audit/independent.cpp -o trio-independent +./trio-independent +``` + +Its JSON `profiles` must equal RESULT.json's `profiles`. Registered replay +recomputes the complete Python census; it does not compile C++. Default replay +is read-only and compares the complete typed receipt. --write creates a new +file exclusively. Actual runs are in VALIDATION.md. + +## Provenance and stopping decision + +Start b5ea56e0, priority 5; picker 1f7ab218c17758bb2e23f41aac1faadd drew +bit-mechanisms. Baseline and R439 helper-star orientation passed first. +The changed scope repairs a current review blocker instead of extending the +closed scalar/helper censuses. TASK.json links the canonical claim. Current +model sources and unchanged predecessor bytes have exact Git/SHA256 pins. +No original author's branch, frozen source or selected frontier is changed. + +Family decision: finish this completeness repair and stop. Boundary and call +bill are explicit; native TRIO, scratch, hosting, precision/tape and whole- +supplier costs remain unknown. This changes whether the existing finite claim +has evidence for its stated domain, without justifying a construction campaign. + +Credit 1337isnot1337 for PR2134's witness and subdomain census, the maintainer +review for the omission finding, Ross Richardson's connector boundary and the +retained six-source authors. The C++ cross-check follows the predecessor's +RGS/direct-difference approach; Python's multiplicity-first enumerator is +separately written here. Prepared by ywz65 with substantial OpenAI Codex +assistance in proof, code, validation and writing. Apache-2.0; notices retained. + +## Open next questions + +Can the original PR incorporate this complete domain and replace its arbitrary- +commutation sentence with the closed-path rotation proof? Compare all five +histograms and the old subdomain before updating its claim. This closes the +stated finite blocker; no additional larger census is proposed here. diff --git a/research/six-trio-complete-profile-audit/RESULT.json b/research/six-trio-complete-profile-audit/RESULT.json new file mode 100644 index 0000000000..01a7a55107 --- /dev/null +++ b/research/six-trio-complete-profile-audit/RESULT.json @@ -0,0 +1,301 @@ +{ + "added_eligible": 3333330, + "at_maximum": 88, + "completed_unit_calls": 144, + "eligible": 5675670, + "incumbent_unit_calls": 142, + "maximum": 61, + "maximum_witness": { + "closing_trio_mask": 21, + "covered_nonzero_masks": 61, + "four_readout_indices_for_missing_masks": { + "11": [ + 0, + 1, + 7, + 13 + ], + "40": [ + 0, + 1, + 4, + 9 + ] + }, + "missing_masks": [ + 11, + 40 + ], + "prefixes": [ + 0, + 1, + 3, + 2, + 6, + 14, + 15, + 31, + 63, + 47, + 45, + 37, + 53, + 21 + ], + "singleton_counts": [ + 3, + 2, + 1, + 2, + 3, + 2 + ], + "singleton_word": [ + 0, + 1, + 0, + 2, + 3, + 0, + 4, + 5, + 4, + 1, + 3, + 4, + 5 + ], + "total_source_map_counts": [ + 4, + 2, + 2, + 2, + 4, + 2 + ] + }, + "minimum_output_readouts": 130, + "noninvariant_adjacent_swap": 0, + "old_eligible": 2342340, + "omitted_example": [ + 0, + 1, + 2, + 3, + 3, + 4, + 4, + 5, + 5, + 5, + 5, + 5, + 5 + ], + "profiles": [ + { + "counts": [ + 1, + 1, + 1, + 2, + 2, + 6 + ], + "histogram": { + "21": 312, + "25": 3874, + "28": 11708, + "30": 13556, + "31": 6294, + "32": 14364, + "34": 25724, + "35": 14148, + "36": 12996, + "37": 14996, + "38": 12480, + "39": 14016, + "40": 4632, + "41": 13584, + "42": 5940, + "43": 8640, + "44": 1512, + "45": 1404 + } + }, + { + "counts": [ + 1, + 1, + 1, + 2, + 4, + 4 + ], + "histogram": { + "21": 416, + "25": 5302, + "28": 15824, + "30": 17438, + "31": 9356, + "32": 30492, + "34": 61140, + "35": 18696, + "36": 29664, + "37": 35448, + "38": 39648, + "39": 35292, + "40": 23868, + "41": 40032, + "42": 18486, + "43": 27336, + "44": 4704, + "45": 20556, + "46": 5400, + "47": 5520, + "48": 3168, + "49": 2592, + "50": 72 + } + }, + { + "counts": [ + 1, + 1, + 2, + 2, + 2, + 5 + ], + "histogram": { + "21": 624, + "25": 7878, + "28": 21576, + "30": 22893, + "31": 10677, + "32": 32064, + "34": 56724, + "35": 23916, + "36": 26061, + "37": 39921, + "38": 39060, + "39": 37116, + "40": 19020, + "41": 46494, + "42": 21393, + "43": 38946, + "44": 5022, + "45": 33693, + "46": 10062, + "47": 19740, + "48": 7872, + "49": 8784, + "50": 4368, + "51": 3438, + "52": 1950, + "53": 1092, + "54": 156 + } + }, + { + "counts": [ + 1, + 1, + 2, + 2, + 3, + 4 + ], + "histogram": { + "21": 1794, + "25": 23889, + "28": 63456, + "30": 81483, + "31": 32862, + "32": 134970, + "34": 254295, + "35": 86154, + "36": 121761, + "37": 182160, + "38": 175704, + "39": 179745, + "40": 128892, + "41": 240819, + "42": 142827, + "43": 208752, + "44": 39312, + "45": 197649, + "46": 49026, + "47": 105396, + "48": 75276, + "49": 60702, + "50": 35274, + "51": 34962, + "52": 20748, + "53": 13848, + "54": 5208, + "55": 2808, + "56": 1920, + "57": 684, + "58": 324 + } + }, + { + "counts": [ + 1, + 2, + 2, + 2, + 3, + 3 + ], + "histogram": { + "21": 1040, + "25": 12662, + "28": 33596, + "30": 41396, + "31": 15274, + "32": 75314, + "34": 127568, + "35": 46640, + "36": 59224, + "37": 113458, + "38": 96380, + "39": 96330, + "40": 81636, + "41": 154168, + "42": 77204, + "43": 143602, + "44": 13596, + "45": 144758, + "46": 47928, + "47": 85308, + "48": 93680, + "49": 58894, + "50": 42768, + "51": 51392, + "52": 29728, + "53": 23052, + "54": 17624, + "55": 9736, + "56": 4284, + "57": 2548, + "58": 660, + "59": 176, + "60": 88, + "61": 88 + } + } + ], + "rejected_controls": [ + "old actual predicate rejects legal omitted profile", + "one odd count cannot close with a distinct-label TRIO", + "missing source", + "out-of-alphabet source" + ], + "rotation_checks": 14, + "schema_version": 1, + "scope": "complete one-TRIO domain repair; no new supplier or kappa", + "status": "PASS_COMPLETE_SIX_TRIO_PROFILES", + "xor_translation_basis_checks": 4096 +} diff --git a/research/six-trio-complete-profile-audit/SOURCES.json b/research/six-trio-complete-profile-audit/SOURCES.json new file mode 100644 index 0000000000..8361a7fbb6 --- /dev/null +++ b/research/six-trio-complete-profile-audit/SOURCES.json @@ -0,0 +1,56 @@ +{ + "schema_version": 1, + "base_commit": "b5ea56e0a5ac4552166253b1fa4be0753bb38c30", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "ae6a99f28aa468649eb66a361e764d769363bf11", + "sha256": "10b9e340fd8e354a37a0c4813c90e5de1dd42044b5f6aca4a3fc5a42b685fa32" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "889b95d936746df124872133ae1e7cc339adcb92", + "sha256": "7d185cd8c2af35988d638d969748ad7b670f902606444dbfc748e4402c340df6" + }, + { + "path": "research/universal-connector-boundary/README.md", + "usage": "input", + "git_blob": "d277f7c5830b1f2bc42e1ff41ab86e7d7564929f", + "sha256": "23415f7829ab8d80a783142f10f7d31abbce84579362769984680af3df954476" + }, + { + "path": "research/universal-connector-six-source/README.md", + "usage": "input", + "git_blob": "c7123c3cfd7545deb6af607800df0d15c6e8c0d2", + "sha256": "ea9cca56d1547dcd984f5f99f6c6243c9417a7ede08f68782c7a6616aa6eb563" + } + ], + "vendored_files": [ + { + "path": "research/six-trio-complete-profile-audit/vendor/pr2134/search.py", + "usage": "input", + "source_commit": "388a63c83cf24c3355be9798bde5a381188dadb3", + "source_path": "research/six-source-trio-path-seed87a169/search.py", + "git_blob": "c16f1f1189d459fef1d53908e1681fab387c50ae", + "sha256": "23f033cd3679f503d1444fd75fd0083b5cd07af3f6596944019ce354e6bc4ee9" + }, + { + "path": "research/six-trio-complete-profile-audit/vendor/pr2134/README.md", + "usage": "input", + "source_commit": "388a63c83cf24c3355be9798bde5a381188dadb3", + "source_path": "research/six-source-trio-path-seed87a169/README.md", + "git_blob": "7c01fdc4df8e696d4e104dfb1a10e1f966ccbaaa", + "sha256": "ce544208ccc043b31bb79d25cdc02eca3d56b0f9eb054ca5eff58cb5b9e59ae9" + }, + { + "path": "research/six-trio-complete-profile-audit/vendor/pr2134/CERTIFICATE.json", + "usage": "input", + "source_commit": "388a63c83cf24c3355be9798bde5a381188dadb3", + "source_path": "research/six-source-trio-path-seed87a169/CERTIFICATE.json", + "git_blob": "c9a64690c7e22fb93f81695472d90b966e3c136c", + "sha256": "93a467e13e93a313698ea8762ae9ca90b7c50bbc852bf25f4d2b21d82d76cb99" + } + ] +} diff --git a/research/six-trio-complete-profile-audit/TASK.json b/research/six-trio-complete-profile-audit/TASK.json new file mode 100644 index 0000000000..158cf13476 --- /dev/null +++ b/research/six-trio-complete-profile-audit/TASK.json @@ -0,0 +1,85 @@ +{ + "schema_version": 1, + "task_id": "bit-helper-contract", + "priority_revision": 5, + "base_commit": "b5ea56e0a5ac4552166253b1fa4be0753bb38c30", + "original_card": { + "id": "bit-helper-contract", + "question": "Can one precisely specified helper-mixing word satisfy a replacement for the inherited H2/K interface?", + "starting_points": [ + "docs/research/research-family-status.md", + "research/r439-bsection-stars-seed01/README.md", + "research/r439-copy-path-sharing-barrier/README.md" + ], + "methods": [ + "Derive a replacement interface lemma and price its implementation.", + "Seek an exact dirty-input or chronological-cut counterexample to the proposed replacement." + ], + "acceptance_gate": "A full boundary contract and paid profile; unchanged scalar counts alone are insufficient. A scoped local result may be retained without a complete supplier. Expanding it into further construction rounds requires the family-level budget and obligation gate in research-family-status.md; an optimistic passing relaxation alone is not acceptance.", + "first_step": { + "command": [ + "python3", + "-B", + "research/r439-bsection-stars-seed01/verify.py" + ], + "expected": "PASS_R439_BSECTION_STARS", + "inspect": "Compare the two false H2/K flags with the unchanged paid profile in its README.", + "scope": "Positive control / source-bound orientation only; this is not a new construction or full cold replay." + }, + "first_experiment": "Write one replacement H2/K implication for a single helper-star operation, then try to falsify it on dirty inputs.", + "bottleneck_link": "A legitimate replacement could admit a cheaper bit circuit; scalar savings alone do not alter the selected moment.", + "allowed_variations": [ + "Choose one helper-star or quartet instance; narrow to one boundary implication." + ], + "scope_change_triggers": [ + "Changing only source count or scalar addition count without an interface argument." + ], + "overlap_terms": [ + "H2_D_frame0_targets_from_helpers", + "K_equals_D", + "helper-star" + ] + }, + "scope_status": "changed", + "actual_scope": "Complete the omitted legal multiplicity domain in PR2134 and justify reducing every TRIO placement by closed-path rotation.", + "scope_change_reason": "The current maintainer review identifies this precise unresolved completeness blocker. Existing helper scalar censuses were already covered; this repairs a finite claim instead of extending their search.", + "bottleneck_link": "Scoped bit connector alphabet evidence only: it decides whether a pending finite 14-call exclusion covers its stated domain. Native TRIO and whole-supplier costs remain unproved.", + "budget_minutes": 60, + "stop_rule": "Stop when the complete profile derivation and two independent full histograms agree, the old subdomain is retained, and the completed bill is checked. Do not enlarge the alphabet or call budget.", + "outcome": "completed", + "evidence": "README.md, census.py, independent.cpp, verify.py and RESULT.json; exact predecessor inputs in SOURCES.json.", + "author": "ywz65", + "ai_assistance": "Substantial OpenAI Codex assistance in proof, implementation, validation and writing.", + "open_questions": [ + { + "question": "Can PR2134 incorporate the complete domain and replace arbitrary commutation with closed-path rotation?", + "why_it_matters": "Its current public full-domain statement exceeds the old two-profile filter.", + "first_step": "Compare all five histograms, retained subdomain and the rotation proof before updating its claim.", + "blocked_by": "Maintainer or original-author integration; no larger census needed." + } + ], + "picker_nonce": "1f7ab218c17758bb2e23f41aac1faadd", + "canonical_thread": "https://github.com/CrocSwap/integer-mult-bounds/pull/2134#issuecomment-6198385003", + "first_steps": [ + "Selected baseline passed.", + "R439 helper-star orientation passed after redirecting TEMP/TMP into the writable workspace." + ], + "family_decision": { + "boundary": "six read-only sources; arbitrary dirty connector/outputs; thirteen singleton calls and one distinct-label TRIO; boundary readouts; full restoration", + "proved": "complete five-profile domain; cyclic rotation reduction; computational maximum61; attained130 readouts and144 total unit calls", + "upper_bounded": "no whole-supplier budget is claimed", + "unknown": "native TRIO, scratch, hosting, precision/tape and complete supplier costs", + "consumer": "No downstream consumer may treat the atomic TRIO or its incremental expenses as free.", + "stop": "Resolve this present review blocker and stop; no further construction campaign justified." + }, + "overlap": { + "open_prs": "Complete 793-open-PR snapshot 2026-10-15T17:45:16.848802Z; title/body and local notes, not every diff.", + "discussions": "Complete cached snapshot 2026-10-15T15:22:22.047084Z; later Discussion changes not covered.", + "targeted": "PR2134 exact head and comments checked with REST before claim; only maintainer omission review, no author repair." + }, + "upstream_checkpoint": { + "commit": "6bd33bc0b87a01e9c9d8b1c01576f3ddbcaee850", + "priority_revision": 5, + "decision": "Continue on exact b5ea scientific/start base. Guidance, selected record and pinned inputs unchanged. New incorporated 12-call/11-singleton TRIO census PR2146 is distinct from this 14-call domain repair. Target PR2134 remains at388a63 with only maintainer review and our claim." + } +} diff --git a/research/six-trio-complete-profile-audit/VALIDATION.md b/research/six-trio-complete-profile-audit/VALIDATION.md new file mode 100644 index 0000000000..007fb1064a --- /dev/null +++ b/research/six-trio-complete-profile-audit/VALIDATION.md @@ -0,0 +1,35 @@ +# Validation record + +Local runs on Windows, October 15, 2026: + +- Python 3.12.14 registered optimized replay passed. It recomputed all + 5,675,670 multiplicity representatives, exact per-profile cardinalities, + every old-subdomain histogram bin, and the model/witness controls. +- GCC 16.2, `-O3 -std=c++17`, compiled `independent.cpp`. The full RGS run + visited 9,321,312 complete six-label words and admitted 5,675,670. All five + histograms exactly matched the Python receipt. Maximum 61; 88 maximizers. +- Python 3.14.5, `-I -O -B`, replayed a Git-free export containing this package + and only the two declared external inputs. Default replay changed no bytes. +- Altered receipt fields `schema_version=true` and `maximum=61.0` were rejected. + Equivalent JSON whitespace/key ordering was accepted. An altered external + model source and altered vendored predecessor code were rejected by their + hashes before execution. Existing output-file overwrite and unknown CLI + flags were rejected. All exported files matched their original hashes after + restoration. + +The Python enumeration uses a different quotient and coverage update from the +C++ RGS/direct-pair calculation. Both were developed with model assistance; +this is computational cross-validation, not independent human or formal-kernel +verification. The generic replay runs Python only; C++ was a separate local +cross-check. CI, native TRIO admission, selected cold replay, whole-supplier +cost and a new exponent are not claimed. + +Prepublication canonical main was +`6bd33bc0b87a01e9c9d8b1c01576f3ddbcaee850`; its guidance and selected record +match the exact starting base `b5ea56e0`. Relevant newly incorporated PR2146 +uses eleven singletons and one TRIO (twelve calls), a distinct domain. A +complete 793-open-PR title/body snapshot at 17:45:16 UTC and cached complete +Discussion snapshot at 15:22:22 UTC were searched. Later Discussion changes +and all code diffs are outside that search coverage. Targeted REST checks +confirmed PR2134 still has head `388a63c8` with no repair beyond the maintained +review and this investigation's claim. diff --git a/research/six-trio-complete-profile-audit/VERIFY.json b/research/six-trio-complete-profile-audit/VERIFY.json new file mode 100644 index 0000000000..e087120c4b --- /dev/null +++ b/research/six-trio-complete-profile-audit/VERIFY.json @@ -0,0 +1,23 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/universal-connector-boundary/README.md", + "research/universal-connector-six-source/README.md" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-O", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 180, + "checks": "Full5,675,670-word multiplicity census, exact old subdomain, profile count proof, all14 witness rotations, actual omitted-profile rejection, four-readout repairs and typed receipt." + } + ] +} diff --git a/research/six-trio-complete-profile-audit/census.py b/research/six-trio-complete-profile-audit/census.py new file mode 100644 index 0000000000..41822725ac --- /dev/null +++ b/research/six-trio-complete-profile-audit/census.py @@ -0,0 +1,62 @@ +"""Multiplicity-first complete census, separately written by ywz65/Codex. + +Apache-2.0. Does not import a predecessor enumerator. +""" +from collections import Counter +from itertools import combinations_with_replacement +from math import factorial, prod + +MASKS = (0x5555555555555555, 0x3333333333333333, 0x0f0f0f0f0f0f0f0f, + 0x00ff00ff00ff00ff, 0x0000ffff0000ffff, 0x00000000ffffffff) +TRANSLATIONS = [[(1 << bit, MASKS[bit]) for bit in range(6) if delta & (1 << bit)] + for delta in range(64)] + + +def translate(occupied, delta): + for step, mask in TRANSLATIONS[delta]: + occupied = ((occupied & mask) << step) | ((occupied >> step) & mask) + return occupied + + +def profiles(): + return [p for p in combinations_with_replacement(range(1, 9), 6) + if sum(p) == 13 and sum(c % 2 for c in p) == 3] + + +def profile_size(profile): + return factorial(13) // (prod(factorial(c) for c in profile) + * prod(factorial(m) for m in Counter(profile).values())) + + +def enumerate_profiles(): + result = [] + for profile in profiles(): + remaining = list(profile) + histogram = Counter() + previous_equal = [i-1 if i and profile[i] == profile[i-1] else -1 for i in range(6)] + + def visit(depth, state, occupied, cover): + if depth == 13: + histogram[(cover & ~1).bit_count()] += 1 + return + for label in range(6): + if not remaining[label]: + continue + previous = previous_equal[label] + if (previous >= 0 and remaining[label] == profile[label] + and remaining[previous] == profile[previous]): + continue + remaining[label] -= 1 + new_state = state ^ (1 << label) + translated = occupied + for step, mask in TRANSLATIONS[new_state]: + translated = ((translated & mask) << step) | ((translated >> step) & mask) + visit(depth + 1, new_state, occupied | (1 << new_state), cover | translated) + remaining[label] += 1 + + visit(0, 0, 1, 0) + if sum(histogram.values()) != profile_size(profile): + raise ValueError("multiplicity quotient count differs from combinatorial count") + result.append({"counts": list(profile), + "histogram": {str(k): v for k, v in sorted(histogram.items())}}) + return result diff --git a/research/six-trio-complete-profile-audit/independent.cpp b/research/six-trio-complete-profile-audit/independent.cpp new file mode 100644 index 0000000000..546984e93e --- /dev/null +++ b/research/six-trio-complete-profile-audit/independent.cpp @@ -0,0 +1,33 @@ +// Complete-domain RGS/direct-difference cross-check. ywz65/Codex, Apache-2.0. +// Credits PR2134 (1337isnot1337) for the predecessor RGS approach and witness. +#include +#include +#include +#include +#include +#include +using A=std::array; +std::array word{},best{}; +A counts{}; +std::map> hist; +uint64_t complete=0,eligible=0; int maximum=-1; +void visit(int depth,int used){ + if(depth==13){ + if(used!=6)return; ++complete; + int odd=0;for(int c:counts)odd+=c%2; + if(odd!=3)return; ++eligible; + std::array p{}; + for(int i=0;i<13;++i)p[i+1]=p[i]^(1<maximum){maximum=n;best=word;} + return; + } + for(int label=0;label<=std::min(used,5);++label){word[depth]=label;++counts[label];visit(depth+1,std::max(used,label+1));--counts[label];} +} +int main(){visit(0,0);std::cout<<"{\"complete\":"< next_label or (label == next_label and next_label >= 6): + raise ValueError("word is not a restricted-growth string") + if label == next_label: + next_label += 1 + seen.add(label) + counts[label] += 1 + state ^= 1 << label + prefixes.append(state) + if len(seen) != 6 or tuple(sorted(counts)) not in PROFILES: + raise ValueError("word is outside the two charged source-map profiles") + trio = state + if trio.bit_count() != 3: + raise ValueError("closing TRIO must toggle exactly three odd-count labels") + return counts, trio, prefixes, differences(prefixes) + + +def four_readout_representations(prefixes, target): + # Return lexicographically first four distinct boundary indices whose + # prefix values XOR to target. The path certificate has distinct states. + for a in range(len(prefixes)): + for b in range(a + 1, len(prefixes)): + for c in range(b + 1, len(prefixes)): + for d in range(c + 1, len(prefixes)): + if prefixes[a] ^ prefixes[b] ^ prefixes[c] ^ prefixes[d] == target: + return [a, b, c, d] + return None + + +def singleton_positive_control(): + # The incumbent six-source word from universal-connector-six-source. + word = [0, 1, 0, 2, 0, 1, 0, 2, 3, 4, 3, 5, 3, 4, 3, 5] + prefixes = [0] + state = 0 + for label in word: + state ^= 1 << label + prefixes.append(state) + if state != 0 or differences(prefixes) != (1 << 64) - 2: + raise ValueError("positive control failed to cover all 63 nonzero masks") + return word, prefixes + + +def enumerate_class(): + histogram = Counter() + nodes = complete = eligible = 0 + record_hash = hashlib.sha256() + best_size = -1 + best_word = best_prefixes = best_counts = best_trio = None + counts = [0] * 6 + word = [0] * N + prefixes = [0] + + def visit(depth, used, cover): + nonlocal nodes, complete, eligible + nonlocal best_size, best_word, best_prefixes, best_counts, best_trio + nodes += 1 + if depth == N: + if used != 6: + return + complete += 1 + profile = tuple(sorted(counts)) + if profile not in PROFILES: + return + eligible += 1 + size = (cover & ~1).bit_count() + histogram[size] += 1 + # Fixed-width records make the full exact census auditable. + record_hash.update(bytes(word)) + record_hash.update(cover.to_bytes(8, "big")) + if size > best_size: + best_size = size + best_word = word.copy() + best_prefixes = prefixes.copy() + best_counts = counts.copy() + best_trio = prefixes[-1] + return + + for label in range(min(used + 1, 6)): + word[depth] = label + counts[label] += 1 + new_state = prefixes[-1] ^ (1 << label) + new_cover = cover + for old_state in prefixes: + new_cover |= 1 << (new_state ^ old_state) + prefixes.append(new_state) + visit(depth + 1, max(used, label + 1), new_cover) + prefixes.pop() + counts[label] -= 1 + + visit(0, 0, 0) + if sum(histogram.values()) != eligible or best_size != max(histogram): + raise ValueError("internal enumeration accounting failure") + covered = differences(best_prefixes) + missing = [mask for mask in range(1, 64) if not (covered >> mask & 1)] + reps = {str(mask): four_readout_representations(best_prefixes, mask) for mask in missing} + singleton_word, singleton_prefixes = singleton_positive_control() + return { + "schema": "six-source-single-trio-path-census-v1", + "domain": { + "sources": 6, + "singleton_calls": 13, + "trio_calls": 1, + "trio_position": "last, by commuting source updates", + "canonicalization": "restricted-growth strings over six labels", + "allowed_sorted_singleton_count_profiles": [list(x) for x in sorted(PROFILES)], + "prefixes_tested": "p0 through p13; p14=p0 after closing TRIO", + "coverage_rule": "pairwise XOR differences of p0..p13", + "repeated_prefixes_allowed": True, + }, + "enumeration": { + "rgs_nodes_including_root": nodes, + "complete_six_label_words": complete, + "words_in_allowed_profiles": eligible, + "records_sha256": record_hash.hexdigest(), + "histogram_nonzero_pair_masks": {str(k): histogram[k] for k in sorted(histogram)}, + "maximum_coverage": best_size, + "number_at_maximum": histogram[best_size], + }, + "maximum_witness": { + "singleton_word": best_word, + "singleton_counts": best_counts, + "closing_trio_mask": best_trio, + "total_source_map_counts": [best_counts[j] + ((best_trio >> j) & 1) for j in range(6)], + "prefixes": best_prefixes, + "covered_nonzero_masks": best_size, + "missing_masks": missing, + "four_readout_indices_for_missing_masks": reps, + }, + "positive_control": { + "incumbent_singleton_word": singleton_word, + "prefixes": singleton_prefixes, + "nonzero_masks_covered": 63, + "root_calls": 142, + }, + "cost": { + "incumbent": {"source_map_applications": 16, "source_calls": 16, "output_readouts": 126, "root_calls": 142}, + "best_one_trio_with_four_readout_repairs": {"source_map_applications": 16, "source_calls": 14, "output_readouts": 130, "root_calls": 144}, + "delta_formula": "-2*f + 4*g + rho; f=source-call frame/dispatch cost, g=one output readout cost, rho=all additional TRIO-specific expense", + "unit_call_delta": 2, + "scope_note": "The source-map multiplicity multiset matches the incumbent's (2,2,2,2,4,4); at unit call prices the completed one-TRIO path loses by 2 before rho.", + }, + } + + +def main(): + if len(sys.argv) != 2 or sys.argv[1] not in ("--write", "--check"): + print("usage: search.py --write|--check", file=sys.stderr) + return 2 + result = enumerate_class() + path = HERE / "CERTIFICATE.json" + encoded = json.dumps(result, indent=2, sort_keys=True) + "\n" + if sys.argv[1] == "--write": + path.write_text(encoded, encoding="utf-8") + elif not path.is_file() or path.read_text(encoding="utf-8") != encoded: + print("FAIL_CERTIFICATE_MISMATCH", file=sys.stderr) + return 1 + print("PASS_SINGLE_TRIO_CENSUS nodes=%d eligible=%d max=%d/%d at_max=%d" % ( + result["enumeration"]["rgs_nodes_including_root"], + result["enumeration"]["words_in_allowed_profiles"], + result["enumeration"]["maximum_coverage"], 63, + result["enumeration"]["number_at_maximum"])) + return 0 + + +if __name__ == "__main__": + raise SystemExit(main()) diff --git a/research/six-trio-complete-profile-audit/verify.py b/research/six-trio-complete-profile-audit/verify.py new file mode 100644 index 0000000000..0a871baeb8 --- /dev/null +++ b/research/six-trio-complete-profile-audit/verify.py @@ -0,0 +1,170 @@ +#!/usr/bin/env python3 +"""Replay the complete domain repair. ywz65/Codex; Apache-2.0.""" +import argparse +from collections import Counter +from hashlib import sha256 +import importlib.util +from itertools import combinations +import json +from pathlib import Path + +PACKAGE = Path(__file__).resolve().parent +ROOT = PACKAGE.parents[1] + + +def require(ok, message): + if not ok: + raise ValueError(message) + + +def load_module(name, path): + spec = importlib.util.spec_from_file_location(name, path) + module = importlib.util.module_from_spec(spec) + spec.loader.exec_module(module) + return module + + +def pairs(rows): + result = {} + for key, value in rows: + require(key not in result, "duplicate JSON key") + result[key] = value + return result + + +def read_json(path): + return json.loads(path.read_text(encoding="utf-8"), object_pairs_hook=pairs) + + +def same(a, b): + if type(a) is not type(b): + return False + if isinstance(a, dict): + return a.keys() == b.keys() and all(same(a[k], b[k]) for k in a) + if isinstance(a, list): + return len(a) == len(b) and all(same(x, y) for x, y in zip(a, b)) + return a == b + + +def prefix_masks(edges): + result = [0] + for edge in edges: + result.append(result[-1] ^ edge) + return result + + +def differences(vertices): + return {a ^ b for a in vertices for b in vertices} - {0} + + +def admissible(word): + require(len(word) == 13 and all(type(x) is int and 0 <= x < 6 for x in word), "word alphabet/length") + counts = [word.count(j) for j in range(6)] + require(all(counts) and sum(c % 2 for c in counts) == 3, "complete parity domain") + return counts + + +def build_result(): + manifest = read_json(PACKAGE / "SOURCES.json") + for row in manifest["files"] + manifest["vendored_files"]: + if row["usage"] == "input": + require(sha256((ROOT / row["path"]).read_bytes()).hexdigest() == row["sha256"], + "source hash: " + row["path"]) + census = load_module("complete_trio_census", PACKAGE / "census.py") + old = load_module("old_trio_census", PACKAGE / "vendor/pr2134/search.py") + prior = read_json(PACKAGE / "vendor/pr2134/CERTIFICATE.json") + # A separate total-profile subtraction derivation of the full singleton set. + derived = set() + for total in ((2, 2, 2, 2, 4, 4), (2, 2, 2, 2, 2, 6)): + for trio in combinations(range(6), 3): + derived.add(tuple(sorted(c - (j in trio) for j, c in enumerate(total)))) + require(derived == set(census.profiles()) and len(derived) == 5, "complete profile derivations") + for delta in range(64): + for state in range(64): + require(census.translate(1 << state, delta) == 1 << (state ^ delta), "XOR bit translation") + rows = census.enumerate_profiles() + histogram = Counter() + old_histogram = Counter() + for row in rows: + histogram.update({int(k): v for k, v in row["histogram"].items()}) + if tuple(row["counts"]) in old.PROFILES: + old_histogram.update(row["histogram"]) + require(dict(old_histogram) == prior["enumeration"]["histogram_nonzero_pair_masks"], "entire old-subdomain histogram") + require(sum(histogram.values()) == 5675670 and max(histogram) == 61 and histogram[61] == 88, + "complete census result") + require(sum(old_histogram.values()) == 2342340, "retained subdomain count") + + controls = [] + def rejects(name, fn): + try: + fn() + except ValueError: + controls.append(name) + else: + raise ValueError("control did not reject: " + name) + + omitted = [0, 1, 2, 3, 3, 4, 4] + [5]*6 + require(admissible(omitted) == [1, 1, 1, 2, 2, 6], "review counterexample") + rejects("old actual predicate rejects legal omitted profile", lambda: old.analyze_word(omitted)) + rejects("one odd count cannot close with a distinct-label TRIO", + lambda: admissible([0, 1, 1, 2, 2, 3, 3, 4, 4, 5, 5, 5, 5])) + rejects("missing source", lambda: admissible([0]*13)) + rejects("out-of-alphabet source", lambda: admissible([0]*12+[6])) + + witness = prior["maximum_witness"] + word = witness["singleton_word"] + counts = admissible(word) + trio = sum((c % 2) << j for j, c in enumerate(counts)) + edges = [1 << label for label in word] + [trio] + vertices = prefix_masks(edges) + require(vertices[-1] == 0 and trio.bit_count() == 3, "restored closing TRIO") + cover = differences(vertices) + require(len(cover) == 61 and sorted(set(range(1, 64))-cover) == [11, 40], "retained maximizing witness") + for cut in range(14): + rotated = prefix_masks(edges[cut:] + edges[:cut]) + require(set(rotated) == {v ^ vertices[cut] for v in vertices}, "cyclic vertex translation") + require(differences(rotated) == cover, "all TRIO placements") + changed = None + for i in range(12): + swapped = edges[:] + swapped[i], swapped[i+1] = swapped[i+1], swapped[i] + if differences(prefix_masks(swapped)) != cover: + changed = i + break + require(changed is not None, "arbitrary commutation must not stand in for rotation") + for target in (11, 40): + indices = witness["four_readout_indices_for_missing_masks"][str(target)] + require(len(indices) == 4 and len(set(indices)) == 4, "four distinct readouts") + mask = 0 + for i in indices: + mask ^= vertices[i] + require(mask == target, "four-readout repair") + baseline = prior["positive_control"]["incumbent_singleton_word"] + require(len(baseline) == 16 and len(differences(prefix_masks([1 << x for x in baseline]))) == 63, + "incumbent full-cover positive control") + return {"schema_version": 1, "status": "PASS_COMPLETE_SIX_TRIO_PROFILES", + "profiles": rows, "eligible": sum(histogram.values()), "maximum": 61, "at_maximum": 88, + "old_eligible": sum(old_histogram.values()), "added_eligible": 3333330, + "omitted_example": omitted, "maximum_witness": witness, + "rotation_checks": 14, "xor_translation_basis_checks": 4096, + "noninvariant_adjacent_swap": changed, "rejected_controls": controls, + "minimum_output_readouts": 130, "completed_unit_calls": 144, "incumbent_unit_calls": 142, + "scope": "complete one-TRIO domain repair; no new supplier or kappa"} + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--write", type=Path) + args = parser.parse_args() + result = build_result() + if args.write: + with args.write.open("x", encoding="utf-8", newline="\n") as stream: + json.dump(result, stream, indent=2, sort_keys=True) + stream.write("\n") + else: + require(same(result, read_json(PACKAGE / "RESULT.json")), "complete typed receipt mismatch") + print(result["status"] + " eligible=5675670 max=61 at_max=88 calls=144") + + +if __name__ == "__main__": + main()