From f46783ec06f184612e7859f575cbdad2ea722a4f Mon Sep 17 00:00:00 2001 From: josecarlosgonzalezroque-design Date: Thu, 15 Oct 2026 19:21:28 -0600 Subject: [PATCH] research: independently audit five-b UT4 gap coverage --- research/ut4-five-b-coverage-audit/README.md | 214 ++++++++++++++++++ .../ut4-five-b-coverage-audit/RESULT.json | 162 +++++++++++++ .../ut4-five-b-coverage-audit/SOURCES.json | 54 +++++ research/ut4-five-b-coverage-audit/TASK.json | 79 +++++++ .../ut4-five-b-coverage-audit/VERIFY.json | 21 ++ .../compare_reference.py | 87 +++++++ research/ut4-five-b-coverage-audit/gaps.py | 106 +++++++++ .../ut4-five-b-coverage-audit/profiles.py | 110 +++++++++ research/ut4-five-b-coverage-audit/verify.py | 157 +++++++++++++ 9 files changed, 990 insertions(+) create mode 100644 research/ut4-five-b-coverage-audit/README.md create mode 100644 research/ut4-five-b-coverage-audit/RESULT.json create mode 100644 research/ut4-five-b-coverage-audit/SOURCES.json create mode 100644 research/ut4-five-b-coverage-audit/TASK.json create mode 100644 research/ut4-five-b-coverage-audit/VERIFY.json create mode 100644 research/ut4-five-b-coverage-audit/compare_reference.py create mode 100644 research/ut4-five-b-coverage-audit/gaps.py create mode 100644 research/ut4-five-b-coverage-audit/profiles.py create mode 100644 research/ut4-five-b-coverage-audit/verify.py diff --git a/research/ut4-five-b-coverage-audit/README.md b/research/ut4-five-b-coverage-audit/README.md new file mode 100644 index 0000000000..71db275a48 --- /dev/null +++ b/research/ut4-five-b-coverage-audit/README.md @@ -0,0 +1,214 @@ +# Independent coverage audit of the five-b UT4 census + +**Result:** the three-call single-label gap cap and four-call combined gap cap +used in [PR #2828](https://github.com/CrocSwap/integer-mult-bounds/pull/2828) +are sufficient for its opposite-orientation `(5,5,5)` cases, including calls +whose active projection is zero. A separate implementation reconstructs the +same **5,664 active profile pairs** and every bounded three-role gap table. + +This supplies an explicit coverage argument for the truncations in +`build_gap_dirty`, `get_dirty_profs`, and `build_joint_dp` at reference head +`8a1000c09819b43ca9a8f2929788af4af40dab70`. It complements the author's full +exclusion and planted controls. It is a finite coverage/operator audit, not +another proof of the full arbitrary-workspace lower bound or a new kappa claim. + +## Precise scope + +Use the reference's quotient + +``` +Q = F2 / (A^2, B^2, C^2, AC-CA, degree >= 4). +``` + +There are two active roles `H` and one dirty role `K`. Every paid coupling is a +nonzero rank-one binary matrix `xy^T`; nilpotent and idempotent couplings are +both allowed. All five `b` couplings lie in `H x H`. In Case I, `a` may have a +dirty component in `x`, and `c` in `y`; Case II reverses these orientations. +There are 21 legal couplings for each outer label in each orientation, +including three with zero `H x H` projection. + +The target is the quotient image of `diag([z],[uz],I_K)`, where +`z=I+E14` and `u=I+E13` in `UT4(F2)`. On `H`, it has coefficient `I_2` at +`1, ABC, ACB, BAC, CBA`, coefficient `S=diag(0,1)` at `AB, BA, ABA, BAB`, +and zero at the other basis elements. The reference's reduction from arbitrary +finite dirty workspaces to these orientations is **inherited**, not proved here. + +Only `AC, ACB, BAC` can receive an interior dirty contraction in the active +block. Thus the other fourteen coefficient equations constrain the active +prefix profiles without knowing the dirty components or intra-gap order. +Indeed, a dirty contraction requires consecutive selected labels `c,a` in +Case I or `a,c` in Case II. After `CA=AC`, the only surviving basis monomials +containing that adjacent pair are `AC, ACB, BAC`; `ACA=CAC=0` and all degrees +at least four vanish. + +## Coverage argument + +Write `B_1,...,B_5` for the middle couplings. There are nine nonzero rank-one +`2 x 2` matrices. Their sum must be zero: enumerate the first four and set the +fifth to their XOR, rejecting a zero or rank-two fifth matrix. This gives all +3,600 middle sequences. + +For either outer label, let `P_j` be its active prefix sum before `B_j`, +and set `P_0=P_6=0`. Its six gap increments and rank sum are + +``` +S_i = P_(i+1) + P_i, i = 0,...,5, +rho(P) = sum_i rank(S_i). +``` + +Each projected paid call has rank at most one, so five calls necessarily give +`rho(P)<=5`. This is only used as a necessary condition; zero projected calls +are allowed. No parity or nonzero-active-call assumption is imposed. + +Put `L_j=sum_(ij) B_i`. The side equations are + +``` +sum_j P_j B_j = T, +sum_j B_j P_j = T, +sum_j P_j B_j P_j = T, +sum_j (L_j P_j B_j + B_j P_j R_j) = T, +``` + +where `T=S` for `a` and `T=0` for `c`. For `a` these are `AB, BA, ABA, BAB`; +for `c` they are `CB, BC, CBC, BCB`. The remaining cross equations are + +``` +sum_j P^a_j B_j P^c_j = I_2, +sum_j P^c_j B_j P^a_j = I_2. +``` + +`profiles.py` enumerates all sixteen possible matrices at each of the five +prefix positions. A 2+3 meet-in-the-middle join matches the four side equations +and then checks the six gap ranks. This differs from the reference's split at +the middle prefix and packed multiplicity counters. The cross join represents +`B_j=x_j y_j^T` through the five columns `P_j x_j` and rows `y_j^T P_j`. +The identity cross-products require both associated row/column pairs to have +rank two, which justifies dropping singular keys. Exhausting these joins gives: + +| Quantity | Count | +|---|---:| +| Middle sequences | 3,600 | +| `a` profiles passing side equations and `rho<=5` | 236,224 | +| `c` profiles passing side equations and `rho<=5` | 2,899,368 | +| Compatible transport-key pairs | 288 | +| Compatible active profile pairs | 5,664 | + +These counts include multiplicity over middle sequences. The final profile +triples are unique. A direct expansion over all subsequences of degrees 1–3 +checks all fourteen retained coefficient equations for every final pair. + +For a fixed pair, let `r^a_i=rank(S^a_i)` and similarly for `c`. If gap `i` +contains `k^a_i` calls, every other gap needs at least its increment rank, hence + +``` +k^a_i <= 5 - sum_(h != i) r^a_h =: U^a_i, +k^c_i <= 5 - sum_(h != i) r^c_h =: U^c_i. +``` + +This remains true for pure-dirty calls. The complete profile enumeration gives + +``` +max_(pair,i) U^a_i = max_(pair,i) U^c_i = 3, +max_(pair,i) (U^a_i + U^c_i) = 4. +``` + +Equivalently, for every compatible pair and every gap, the combined rank demand +in the other five gaps is at least six. Therefore each label needs at most +three calls in a gap, and the combined total is at most four. **The reference's +truncations cover every word satisfying the necessary active equations.** The +bound is on a relaxation; attaining one of these upper bounds does not establish +the existence of a complete realizing word. + +The `(rho_a,rho_c)` histogram is `(4,4):152`, `(4,5):760`, `(5,4):792`, +`(5,5):3960`. [RESULT.json](RESULT.json) records the full gap-cap histogram. + +## Independent operator check + +`gaps.py` builds the 21 couplings directly as `3 x 3` outer products. Within +an `a/c` gap only `1,A,C,AC` survive. A dynamic program retains the full +three-role `A` and `C` coefficients and multiplies them **before** projecting +the `AC` coefficient onto `H`. It never uses the reference's packed dirty +correction formulas. A separate literal enumeration supplies the single-label +tables, including the flag recording whether any dirty component was used. + +For each orientation the joint table has **81,935 states**, representing +**2,798,629 words** over all `0<=k_a,k_c<=3`, `k_a+k_c<=4`, including the empty +word. Every count pair is checked against +`binomial(k_a+k_c,k_a) * 21^(k_a+k_c)`. + +The optional comparison matched every table entry and multiplicity via canonical +SHA256 digests, and matched the entire sorted active-profile set, not just its +cardinality. Its profile-set digest is +`e19ab0445cd473806fb8e7e3d09b9a2911b65a4a02302720f3a7fe49e3be4961`. +The reference's differently defined digest also includes per-profile word counts; +it should not be compared directly to this digest. + +Controls reject a changed middle coupling and gap caps of two/three that the +rank certificate cannot justify. A positive fixture uses `e_1 e_K^T` followed +by `e_K e_1^T`: both active projections vanish, while their product has active +coefficient `E11`. Reversing the order or multiplying only active projections +gives zero. Both orientations' gap tables must contain this fixture. + +## Reproduce and evidence limits + +From the repository root, using Python 3.12 and only its standard library: + +```sh +python3.12 -B scripts/research_package.py --package research/ut4-five-b-coverage-audit --check-only +python3.12 -B scripts/research_package.py --package research/ut4-five-b-coverage-audit +``` + +The second command rebuilds the result and checks the committed receipt; it +does not rewrite it. Measured generation time was 74.8 seconds on Python +3.12.14/Windows, with a 300-second replay limit. To explicitly regenerate the +receipt, run `verify.py --write-result`. The independent replay makes no network +requests and imports no predecessor code. + +To repeat the comparison, export the files listed under `audited_reference` +in [SOURCES.json](SOURCES.json) from the +[pinned reference tree](https://github.com/steph4n-gh/integer-mult-bounds/tree/8a1000c09819b43ca9a8f2929788af4af40dab70), +retaining their repository-relative paths beneath `REFERENCE_ROOT`, then run: + +```sh +python3.12 -B research/ut4-five-b-coverage-audit/compare_reference.py REFERENCE_ROOT +``` + +The adapter checks all source hashes before importing the reference. It observes +the reference's profile enumeration and also checks that every original census +output remains equal to its frozen receipt. Comparison took 9.2 seconds. The +author's original `verify.py` and `controls.py` were separately replayed and +passed; those reruns are **not independent implementations**. + +This package does not independently reconstruct the dirty-prefix filters, the +final whole-word `AC/ACB/BAC` rejection, the other count splits, or the inherited +all-workspace compression and group-to-quotient proof. It does not establish a +native multiplication supplier. Only the selected-result binding/arithmetic +baseline was run, not the full selected supplier cold replay. No selected result +or predecessor file is changed. + +Scientific inputs are pinned to main `b5e86d8104338796ce3cdf71666b6dbe72ec17fa`; +the submission refresh is recorded in [TASK.json](TASK.json). The original card +was `bit-new-register-model`, refined to a deliberately complementary audit of +pending work. Live PR searches were available; complete Discussion pagination +and authenticated Discussion posting were not. No advance reservation was posted. + +## Open next questions + +Independently reconstruct the remaining dirty-prefix equations and the final +three-coefficient rejection for all fifteen-call five-`b` splits. This would +test the remaining computational implication in #2828. Start from its then-current +pinned head and reuse these profile/gap digests, with a separate bounded audit. +No computational blocker is known; the inherited workspace-compression proof +still needs separate review. The structured handoff is in [TASK.json](TASK.json). + +## Credit + +The complete fifteen-call exclusion belongs to steph4n-gh's PR #2828. Its +predecessors include Gareth Davidson / bitplane (#2027, #2314, #2343), Nick +Petalas (#2175), ToikY (#1662, #1680), CinnaDavis / 1337isnot1337 (#1541), and +Aaron Wang / navinor's profile method (#1690). This package adds the separate +coverage certificate and operator comparison; it vendors none of their code. + +Prepared for josecarlosgonzalezroque-design with substantial OpenAI Codex +assistance in analysis, implementation, verification and writing. No independent +human review or subagents. New work is Apache-2.0. diff --git a/research/ut4-five-b-coverage-audit/RESULT.json b/research/ut4-five-b-coverage-audit/RESULT.json new file mode 100644 index 0000000000..a7fef33286 --- /dev/null +++ b/research/ut4-five-b-coverage-audit/RESULT.json @@ -0,0 +1,162 @@ +{ + "schema_version": 1, + "scope": "five-b opposite-orientation active profiles and bounded gap operators", + "statistics": { + "middles": 3600, + "c_pass": 2899368, + "a_pass": 236224, + "key_pairs": 288, + "profile_pairs": 5664 + }, + "profile_set_sha256": "e19ab0445cd473806fb8e7e3d09b9a2911b65a4a02302720f3a7fe49e3be4961", + "rank_sum_histogram": [ + [ + 4, + 4, + 152 + ], + [ + 4, + 5, + 760 + ], + [ + 5, + 4, + 792 + ], + [ + 5, + 5, + 3960 + ] + ], + "gap_cap_histogram": [ + [ + 1, + 1, + 2, + 320 + ], + [ + 1, + 2, + 2, + 216 + ], + [ + 1, + 2, + 3, + 664 + ], + [ + 1, + 3, + 3, + 56 + ], + [ + 1, + 3, + 4, + 88 + ], + [ + 2, + 1, + 2, + 224 + ], + [ + 2, + 1, + 3, + 544 + ], + [ + 2, + 2, + 2, + 544 + ], + [ + 2, + 2, + 3, + 1728 + ], + [ + 2, + 2, + 4, + 272 + ], + [ + 2, + 3, + 3, + 224 + ], + [ + 2, + 3, + 4, + 208 + ], + [ + 3, + 1, + 3, + 64 + ], + [ + 3, + 1, + 4, + 64 + ], + [ + 3, + 2, + 3, + 192 + ], + [ + 3, + 2, + 4, + 192 + ], + [ + 3, + 3, + 4, + 64 + ] + ], + "gap_tables": { + "I": { + "a_single_sha256": "1e4217998ef1b0bb8aca2fc235829d04945752b4bb85694482499c05bf4dcd86", + "c_single_sha256": "98591d5f597e2abe5231ed6068968e07e5b614bb52ab8ed1a0a60637b1098f5e", + "joint_sha256": "4738bd011fe1b517afdb674bd12037c4027148adeb95199b90a3b19100dd60c3", + "joint_states": 81935, + "joint_words": 2798629 + }, + "II": { + "a_single_sha256": "98591d5f597e2abe5231ed6068968e07e5b614bb52ab8ed1a0a60637b1098f5e", + "c_single_sha256": "1e4217998ef1b0bb8aca2fc235829d04945752b4bb85694482499c05bf4dcd86", + "joint_sha256": "1b077d3ce2efad520a23ce9064907fbeaaec294d96e584a21164f29fc6a92b0d", + "joint_states": 81935, + "joint_words": 2798629 + } + }, + "controls": { + "literal_profile_checks": 5664, + "changed_middle_rejected": true, + "unsupported_single_cap_2_rejected": true, + "unsupported_joint_cap_3_rejected": true, + "pure_dirty_and_order_controls": true, + "gap_multiplicities_match_closed_form": true + } +} diff --git a/research/ut4-five-b-coverage-audit/SOURCES.json b/research/ut4-five-b-coverage-audit/SOURCES.json new file mode 100644 index 0000000000..dc437af994 --- /dev/null +++ b/research/ut4-five-b-coverage-audit/SOURCES.json @@ -0,0 +1,54 @@ +{ + "schema_version": 1, + "base_commit": "b5e86d8104338796ce3cdf71666b6dbe72ec17fa", + "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/register-pairing-compression/README.md", + "usage": "input", + "git_blob": "d80d0cb3a3f8955ddd5d6ea706c408d78344ca90", + "sha256": "4fc3611c00deb4166863c3ebf4483958d42cb02e95fa4aa8313e4af8d8043b5d" + }, + { + "path": "research/ut4-mixed-weighted-boundary/PROOF.md", + "usage": "input", + "git_blob": "d5ba9d06c0bb4e8553da56d504eb8d5f2ee0e1bd", + "sha256": "580fce5e5e460fd00afa8fa0231395859fdf5cf0998df9d21471b40a996665ef" + } + ], + "audited_reference": { + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/2828", + "repository": "steph4n-gh/integer-mult-bounds", + "head": "8a1000c09819b43ca9a8f2929788af4af40dab70", + "usage": "Optional comparison only; no reference imports or downloads in the independent replay.", + "sha256": { + "research/ut4-fifteen-call-five-b/PROOF.md": "9e74a9b46b930f90333653a53d3a079cb21a2147f52a7ba046123178a1e3fc04", + "research/ut4-fifteen-call-five-b/README.md": "2ff908bb4206e6081eec062891af35b2b142a7f013fdf6a639657feb8990bd8a", + "research/ut4-fifteen-call-five-b/RESULT.json": "c8e1f41842931ddf2cf82c638053dd26a6ee1562825cf1a5708243c3a2cec8eb", + "research/ut4-fifteen-call-five-b/SOURCES.json": "531f7359c703f524a43cadf3bddb935040a3072ec67ad63d4c00f08df92d2ade", + "research/ut4-fifteen-call-five-b/TASK.json": "4d69ca3e3c6094180b85364cbb466c8ea09253d02106a2d3a7bb58fdb9221065", + "research/ut4-fifteen-call-five-b/VERIFY.json": "97e0b4009abc2daedb62f125e8db3e1fe31bd5a1d6727284907917324fb27f2d", + "research/ut4-fifteen-call-five-b/census.py": "a20eeb35aee5dff8788e798d68a237c9c1adf6fdcb35626c34be2b3af058d972", + "research/ut4-fifteen-call-five-b/controls.py": "475910cacdcce5df971b7432ef067040a78e7a14313ee1070981ba33855ced42", + "research/ut4-fifteen-call-five-b/vendor/predecessor.py": "b7f8167aaf1fd41de03255d7b7048b82e527f2c9252b3245d5648e5d89afb342", + "research/ut4-fifteen-call-five-b/verify.py": "1046309e51965c56d3d2b665a9dea49de107c3922474d7e22ff33bea17b642c1", + "research/register-pairing-compression/PROOF.md": "f9c3c3f1363787ed0c92a65abba065d5debcb1e526a439cd3c82ad48d24f27bd", + "research/register-pairing-compression/RESULT.json": "151121844b1ada7462e0442ec1c5003c735c8e19bc1e1fdc1c1238ec950312dd", + "research/ut4-mixed-root-tariffs/PROOF.md": "c0def58338a69a57ac95f1d32a744993aa07656c46eba88a99354b276917bd8e", + "research/ut4-mixed-weighted-boundary/PROOF.md": "580fce5e5e460fd00afa8fa0231395859fdf5cf0998df9d21471b40a996665ef", + "research/ut4-mixed-weighted-boundary/RESULT.json": "631aaf146da1351246729984e8f7426125a1f91c68af99843e91b880e2f75e0f", + "research/ut4-one-slack-workspace/PROOF.md": "a9e2c7e6f6841b0f9a53c65861c2e212c2bc126923d9e41f5723c530389e96cf" + } + } +} diff --git a/research/ut4-five-b-coverage-audit/TASK.json b/research/ut4-five-b-coverage-audit/TASK.json new file mode 100644 index 0000000000..c9c3b8bcd2 --- /dev/null +++ b/research/ut4-five-b-coverage-audit/TASK.json @@ -0,0 +1,79 @@ +{ + "schema_version": 1, + "task_id": "bit-new-register-model", + "priority_revision": 5, + "base_commit": "b5e86d8104338796ce3cdf71666b6dbe72ec17fa", + "original_card": { + "id": "bit-new-register-model", + "question": "Can an explicitly larger or nonabelian register model escape the scoped three-register obstruction?", + "starting_points": [ + "docs/research/research-family-status.md", + "research/bit-three-register-lower-bound/README.md", + "certificates/selected-result.json", + "research/bit-gl3-mixed-targets-length10/README.md", + "docs/research/community-efficient1000-review.md" + ], + "methods": [ + "Construct the smallest exact identity in a newly specified legal operation alphabet.", + "Derive a target-specific relaxation bound for that same explicit alphabet." + ], + "acceptance_gate": "Name the changed hypothesis, all counted roles and a uniform identity; finite column tests alone do not certify it. 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", + "scripts/research_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Read Model section 1 of the three-register bound and identify the exact excluded free operations.", + "scope": "Positive control / source-bound orientation only; this is not a new construction or full cold replay." + }, + "first_experiment": "First compare the alphabet, role count and length with the fully replayed #1974 census and #2027 mixed-root tariff. Identify a changed premise and a legal native implementation; then price one smallest completed instance before searching larger words.", + "bottleneck_link": "A small-width completed saving changes the bit primitive; a finite-address identity alone is insufficient.", + "allowed_variations": [ + "Choose a fixed larger register count or a specified nonabelian operation family." + ], + "scope_change_triggers": [ + "Remaining inside the already-excluded three-register abelian model.", + "Repeating the two-register GL3 census or a covered three-register length without changing a hypothesis; a formal group-algebra word without native conversion is a partial result." + ], + "overlap_terms": [ + "three-register", + "nonabelian", + "group algebra" + ] + }, + "scope_status": "changed", + "actual_scope": "Independent coverage and bounded-gap operator audit of PR2828 at 8a1000c09819b43ca9a8f2929788af4af40dab70: reconstruct all 5664 (5,5,5) active profile pairs, justify the single-label 3-call and joint 4-call gap caps even with pure-dirty calls, and compare all bounded three-role gap operator tables.", + "scope_change_reason": "The live PR2828 already proposes the new UT4 bound requested by PR2314/2343; independently checking its new finite coverage adds value without repeating the construction search.", + "bottleneck_link": "Audit the acceptance of a nonabelian bit-mechanism obstruction; no native supplier or new kappa is claimed.", + "budget_minutes": 60, + "stop_rule": "One bounded audit within this 60-minute session. Return an exact discrepancy or independently reproducible coverage evidence; do not extend to new word lengths.", + "outcome": "completed", + "evidence": "RESULT.json records a separate 2+3 meet-in-the-middle enumeration, all-profile literal quotient checks, gap-cap histograms and dense 3x3 operator-table digests. compare_reference.py matched the exact profile set and every gap table against the pinned PR2828 source; its full census was also replayed without changing its outputs. See README for the precise conditional scope and unrun obligations.", + "author": "josecarlosgonzalezroque-design", + "ai_assistance": "Substantial OpenAI Codex assistance in analysis, code, verification and writing; no subagents or independent human review.", + "open_questions": [ + { + "question": "Can a separate checker reconstruct the remaining dirty-profile constraints and final AC/ACB/BAC rejection for all 15-call five-b splits?", + "why_it_matters": "This audit establishes profile and gap-table coverage but does not independently certify the entire all-workspace exclusion in PR2828.", + "first_step": "Pin the then-current PR2828 head, reuse the exact active-profile/gap-table digests here, and independently enumerate homogeneous dirty prefixes and the final three quotient coefficients.", + "blocked_by": "No computational blocker is known; a separate bounded audit and the inherited workspace-compression premises are required." + } + ], + "selection_seed": "8ba89d68e89ff103bcb9f7385f01f450", + "claim_status": "No advance Discussion claim was posted; no authenticated Discussion-posting tool is available. Completed finding prepared for a focused contribution PR.", + "overlap": { + "helper": "find_overlap.py --task bit-new-register-model; 2139 local records; gh unavailable, so no remote snapshot", + "remote": "Live GitHub API searches of open PR bodies and targeted PR2828 searches; board start/handoff/current-list pages read; Discussion pagination incomplete. PR2828 is the audit object, PR2314/2343 are predecessors. No novelty guarantee.", + "submission_refresh": "2026-10-16T01:17:54Z helper refresh: 2194 local records, 207 possible matches; no remote snapshot because gh is unavailable. Canonical main refreshed again at 01:18:45Z. Live API search for PRs mentioning 2828 returned only PR2828, still at its pinned head. Discussion pagination remains incomplete; no uniqueness guarantee." + }, + "freshness": { + "checked_utc": "2026-10-16T01:18:45Z", + "canonical_main": "23ef28cbeb7a3e2e985be22cab6832424bd98cf6", + "priority_revision": 5, + "decision": "Continue and rebase the isolated contribution. Guidance, catalogue, selected record, family status and both live proof inputs remain unchanged from the scientific base. The last upstream batch adds no changed ut4/five-b package. The registered replay passed on 808e0e98 in 71.954 seconds; its runner and all audit inputs are unchanged in 23ef28cb.", + "reference_pr_head": "8a1000c09819b43ca9a8f2929788af4af40dab70", + "reference_pr_status": "open, unmerged" + } +} diff --git a/research/ut4-five-b-coverage-audit/VERIFY.json b/research/ut4-five-b-coverage-audit/VERIFY.json new file mode 100644 index 0000000000..4f5a51d6dd --- /dev/null +++ b/research/ut4-five-b-coverage-audit/VERIFY.json @@ -0,0 +1,21 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/register-pairing-compression/README.md", + "research/ut4-mixed-weighted-boundary/PROOF.md" + ], + "commands": [ + { + "argv": [ + "{python}", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 300, + "checks": "Independent 5664-profile reconstruction, 3/4 gap caps, literal quotient controls and dense three-role gap tables; no reference imports." + } + ] +} diff --git a/research/ut4-five-b-coverage-audit/compare_reference.py b/research/ut4-five-b-coverage-audit/compare_reference.py new file mode 100644 index 0000000000..a106bb2774 --- /dev/null +++ b/research/ut4-five-b-coverage-audit/compare_reference.py @@ -0,0 +1,87 @@ +#!/usr/bin/env python3 +# SPDX-License-Identifier: Apache-2.0 +"""Optional comparison with a local, hash-pinned checkout of PR #2828. + +The independent verifier never imports the reference. This adapter executes it +only after checking every external file recorded in SOURCES.json. +""" +import argparse +from hashlib import sha256 +import importlib.util +import json +from pathlib import Path + +import gaps as G +import profiles as P +from verify import HERE, profile_digest, require + + +def import_file(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 run(root): + source = json.loads((HERE / 'SOURCES.json').read_text(encoding='utf-8'))['audited_reference'] + for name, expected in source['sha256'].items(): + require(sha256((root / name).read_bytes()).hexdigest() == expected, + 'reference source mismatch: ' + name) + directory = root / 'research/ut4-fifteen-call-five-b' + census = import_file('pinned_five_b_reference', directory / 'census.py') + predecessor, _ = census.load() + independent = json.loads((HERE / 'RESULT.json').read_text(encoding='utf-8')) + + tables = census.build_three_role_tables(predecessor, tuple(P.RANK)) + for case, (_, _, at, ct, joint) in tables.items(): + def single_rows(table): + return sorted([k, s, w, used, count] + for k, values in table.items() for s, terms in values.items() + for w, used, count in terms) + joint_rows = sorted([*state, q, count] + for state, terms in joint.items() for q, count in terms) + actual = { + 'a_single_sha256': sha256(G.canonical(single_rows(at))).hexdigest(), + 'c_single_sha256': sha256(G.canonical(single_rows(ct))).hexdigest(), + 'joint_sha256': sha256(G.canonical(joint_rows)).hexdigest(), + 'joint_states': len(joint_rows), + 'joint_words': sum(row[-1] for row in joint_rows), + } + require(actual == independent['gap_tables'][case], 'gap table mismatch: ' + case) + + # Observe every original active-profile pair, without replacing its search. + # Other splits are also visited: retain the rank<=5 subdomain and deduplicate. + observed = set() + original = census.eval_base_2role + + def observe(predecessor, middle, a_gaps, c_gaps): + def prefix(increments): + result, running = [], 0 + for value in increments[:5]: + running ^= value + result.append(running) + return tuple(result) + if sum(P.RANK[x] for x in a_gaps) <= 5 and sum(P.RANK[x] for x in c_gaps) <= 5: + observed.add((tuple(middle), prefix(a_gaps), prefix(c_gaps))) + return original(predecessor, middle, a_gaps, c_gaps) + + census.eval_base_2role = observe + replay = census.run(predecessor) + expected = json.loads((directory / 'RESULT.json').read_text(encoding='utf-8')) + # The adapter must not change any field returned by the original census. + for field, value in json.loads(json.dumps(replay)).items(): + require(value == expected[field], 'reference census drift: ' + field) + require(len(observed) == 5664, 'reference profile-set size') + require(profile_digest(observed) == independent['profile_set_sha256'], + 'reference profile-set mismatch') + for field, value in independent['statistics'].items(): + require(value == replay['domains']['5,5,5'][field], 'reference count: ' + field) + print('PASS_PINNED_PR2828_COMPARISON profile_set=' + profile_digest(observed) + + ' orientations=2 gap_words_each=2798629') + + +if __name__ == '__main__': + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument('reference_root', type=Path, help='root of an exact PR2828 checkout/export') + run(parser.parse_args().reference_root.resolve()) diff --git a/research/ut4-five-b-coverage-audit/gaps.py b/research/ut4-five-b-coverage-audit/gaps.py new file mode 100644 index 0000000000..25ddbe0d72 --- /dev/null +++ b/research/ut4-five-b-coverage-audit/gaps.py @@ -0,0 +1,106 @@ +# SPDX-License-Identifier: Apache-2.0 +"""Literal three-by-three matrix audit of #2828's bounded gap tables. + +No packed active/dirty correction formula or predecessor implementation is used. +""" +from collections import Counter +from functools import lru_cache +from hashlib import sha256 +from itertools import product +import json + + +def canonical(value): + return json.dumps(value, sort_keys=True, separators=(',', ':')).encode() + + +def outer(x, y, n=3): + return sum(((x >> i) & 1) * ((y >> j) & 1) << (n*i+j) + for i in range(n) for j in range(n)) + + +@lru_cache(maxsize=None) +def mm(a, b): + return sum((sum(((a >> (3*i+k)) & 1) * ((b >> (3*k+j)) & 1) + for k in range(3)) % 2) << (3*i+j) + for i in range(3) for j in range(3)) + + +def active(mask): + return sum(((mask >> (3*i+j)) & 1) << (2*i+j) + for i in range(2) for j in range(2)) + + +def dirty(mask, orientation): + if orientation == 'column': # x has a dirty component: bottom-left row. + return (mask >> 6) & 3 + return ((mask >> 2) & 1) | (((mask >> 5) & 1) << 2) + + +def alphabet(orientation): + xs, ys = (range(1, 8), range(1, 4)) if orientation == 'column' else (range(1, 4), range(1, 8)) + return tuple(sorted(outer(x,y) for x,y in product(xs,ys))) + + +def single_table(choices, orientation): + result = [] + for k in range(4): + counts = Counter() + for word in product(choices, repeat=k): + s = 0 + used = 0 + for n in word: + s ^= n + used |= bool(dirty(n, orientation)) + counts[active(s), dirty(s, orientation), used] += 1 + result.extend([k, *state, count] for state, count in sorted(counts.items())) + return result + + +def joint_table(a_choices, c_choices, a_orientation, c_orientation): + # A^2=C^2=ACA=CAC=0. Thus only 1, A, C, AC survive within a gap. + # Retain full 3x3 A/C coefficients; compute products before taking HH. + tables = {(0,0): {(0,0,0): 1}} + rows = [[0,0,0,0,0,0,0,1]] + for total in range(1,5): + for ka in range(total+1): + kc = total-ka + if max(ka,kc)>3: + continue + counts = Counter() + for letter, choices, previous in ( + ('a', a_choices, (ka-1,kc)), ('c', c_choices, (ka,kc-1))): + for (a,c,q), count in tables.get(previous,{}).items(): + for n in choices: + if letter == 'a': + state = (a^n,c,q^active(mm(c,n))) + else: + state = (a,c^n,q^active(mm(a,n))) + counts[state] += count + tables[ka,kc] = counts + rows.extend([ka,kc,active(a),dirty(a,a_orientation),active(c),dirty(c,c_orientation),q,count] + for (a,c,q),count in counts.items()) + return sorted(rows) + + +def run(): + result={} + for case, ao, co in (('I','column','row'),('II','row','column')): + aa, cc = alphabet(ao), alphabet(co) + at,ct=single_table(aa,ao),single_table(cc,co) + joint=joint_table(aa,cc,ao,co) + result[case]={ + 'a_single_sha256':sha256(canonical(at)).hexdigest(), + 'c_single_sha256':sha256(canonical(ct)).hexdigest(), + 'joint_sha256':sha256(canonical(joint)).hexdigest(), + 'joint_states':len(joint), + 'joint_words':sum(row[-1] for row in joint), + } + return result + + +if __name__=='__main__': + import time + start=time.perf_counter() + print(json.dumps(run(),indent=2)) + print('seconds',time.perf_counter()-start) diff --git a/research/ut4-five-b-coverage-audit/profiles.py b/research/ut4-five-b-coverage-audit/profiles.py new file mode 100644 index 0000000000..571f9107cb --- /dev/null +++ b/research/ut4-five-b-coverage-audit/profiles.py @@ -0,0 +1,110 @@ +# SPDX-License-Identifier: Apache-2.0 +"""Independent 5-b active-profile and gap-cap audit; standard library only. + +The profile method is due to Aaron Wang (#1690). Equations and the 5,664-pair +reference count are from steph4n-gh's #2828, building on Petalas and Davidson. +This implementation uses a separate 2+3 join, with no predecessor imports. +""" +from collections import defaultdict, Counter +from itertools import product + + +def mm(a, b, n=2): + return sum((sum(((a >> (n*i+k)) & 1) * ((b >> (n*k+j)) & 1) + for k in range(n)) % 2) << (n*i+j) + for i in range(n) for j in range(n)) + + +M = [[mm(a,b) for b in range(16)] for a in range(16)] +XY = {sum(((x >> i) & 1) * ((y >> j) & 1) << (2*i+j) + for i in range(2) for j in range(2)): (x,y) + for x in range(1,4) for y in range(1,4)} +RANK = [0 if a == 0 else 1 if a in XY else 2 for a in range(16)] +COUPLINGS = sorted(XY) + + +def gaps(p): + return tuple(x ^ y for x,y in zip((0,)+p, p+(0,))) + + +def key(middle,p): + result=[0,0,0,0] + for j,(b,a) in enumerate(zip(middle,p)): + x,y=XY[b] + for i in range(2): + u=sum(((a >> (2*i+k)) & 1)*((x>>k)&1) for k in range(2))%2 + v=sum(((y >> k)&1)*((a>>(2*k+i))&1) for k in range(2))%2 + result[i]|=u<5: + continue + for wanted, dest, stat in ((0x8888,aa,'a_pass'),(0,cc,'c_pass')): + for p0,p1,head in left.get(value^wanted,()): + if head+RANK[p1^p2]+tail<=5: + stats[stat]+=1 + p=(p0,p1,p2,p3,p4) + k=key(mid,p) + if k[0] and k[1] and k[0]!=k[1] and k[2] and k[3] and k[2]!=k[3]: + dest[k].append(p) + # Join by the two row equations, without the candidate's packed key routine. + crows=defaultdict(list) + for ck in cc: + crows[ck[2:]].append(ck) + for ak,ap in aa.items(): + row0=[v for v in range(32) if (dot(ak[0],v),dot(ak[1],v))==(1,0)] + row1=[v for v in range(32) if (dot(ak[0],v),dot(ak[1],v))==(0,1)] + for w0,w1 in product(row0,row1): + for ck in crows.get((w0,w1),()): + if (dot(ck[0],ak[2]),dot(ck[0],ak[3]),dot(ck[1],ak[2]),dot(ck[1],ak[3]))!=(1,0,0,1): + continue + stats['key_pairs']+=1 + for a,c in product(sorted(ap),sorted(cc[ck])): + stats['profile_pairs']+=1 + ra=tuple(RANK[s] for s in gaps(a)) + rc=tuple(RANK[s] for s in gaps(c)) + rank_pairs[sum(ra),sum(rc)]+=1 + # Zero projected calls allowed. Every other gap needs at least its rank. + ca=tuple(5-(sum(ra)-v) for v in ra) + ccaps=tuple(5-(sum(rc)-v) for v in rc) + caps[max(ca),max(ccaps),max(x+y for x,y in zip(ca,ccaps))]+=1 + pairs.append((mid,a,c)) + if progress and stats['middles']%900==0: + print('independent middle',stats['middles'],flush=True) + return dict(stats), sorted(pairs), rank_pairs, caps diff --git a/research/ut4-five-b-coverage-audit/verify.py b/research/ut4-five-b-coverage-audit/verify.py new file mode 100644 index 0000000000..4518a788b8 --- /dev/null +++ b/research/ut4-five-b-coverage-audit/verify.py @@ -0,0 +1,157 @@ +#!/usr/bin/env python3 +# SPDX-License-Identifier: Apache-2.0 +"""Reconstruct the finite coverage audit; this is not a full #2828 proof replay.""" +import argparse +from collections import Counter +from hashlib import sha256 +from itertools import combinations +import json +from pathlib import Path +import time + +import gaps as G +import profiles as P + +HERE = Path(__file__).resolve().parent +TARGET = {'': 9, 'ab': 8, 'ba': 8, 'aba': 8, 'bab': 8, + 'abc': 9, 'cba': 9} +NONADJACENT = ('', 'a', 'b', 'c', 'ab', 'ba', 'bc', 'cb', + 'aba', 'abc', 'bab', 'bcb', 'cba', 'cbc') + + +def require(ok, message): + if not ok: + raise ValueError(message) + + +def profile_digest(pairs): + # Sorted numeric triples [middle, a-prefix, c-prefix], compact JSON + LF. + h = sha256() + for row in sorted(pairs): + h.update(G.canonical(row) + b'\n') + return h.hexdigest() + + +def reduced(word): + while 'ca' in word: + word = word.replace('ca', 'ac') + return None if any(x == y for x, y in zip(word, word[1:])) else word + + +# One A and C increment in each of the six gaps, separated by five B calls. +# Intra-gap ordering only affects AC, ACB, BAC, which are deliberately omitted. +LABELS = 'acbacbacbacbacbac' +TERMS = [(indices, reduced(''.join(LABELS[i] for i in indices))) + for degree in (1, 2, 3) + for indices in combinations(range(len(LABELS)), degree)] +TERMS = [(indices, name) for indices, name in TERMS if name in NONADJACENT] + + +def literal_profile_coefficients(middle, a, c): + word = [] + for i, (sa, sc) in enumerate(zip(P.gaps(a), P.gaps(c))): + word.extend((sa, sc)) + if i < 5: + word.append(middle[i]) + result = {'': 9} + for indices, name in TERMS: + value = 9 + for i in indices: + value = P.M[value][word[i]] + result[name] = result.get(name, 0) ^ value + return {name: result.get(name, 0) for name in NONADJACENT} + + +def check_profile(row): + actual = literal_profile_coefficients(*row) + require(actual == {name: TARGET.get(name, 0) for name in NONADJACENT}, + 'nonadjacent quotient equations') + + +def check_caps(caps, single=3, joint=4): + require(all(a <= single and c <= single and ac <= joint + for a, c, ac in caps), 'gap cap is not justified by the rank bounds') + + +def rejects(action): + try: + action() + except ValueError: + return + raise ValueError('negative control was not rejected') + + +def controls(pairs, caps): + # Full literal subsequence expansion is independent of the side/key join. + for row in pairs: + check_profile(row) + middle, a, c = pairs[0] + altered = (middle[0] ^ 1,) + middle[1:] + rejects(lambda: check_profile((altered, a, c))) + rejects(lambda: check_caps(caps, single=2)) + rejects(lambda: check_caps(caps, joint=3)) + + # Pure-dirty couplings have zero HH projection but a nonzero cross product. + # This detects the incorrect active-projection simplification. + enter, leave = G.outer(1, 4), G.outer(4, 1) + require(G.active(enter) == G.active(leave) == 0, 'pure-dirty fixture') + require(G.active(G.mm(enter, leave)) == 1, 'ordered dirty contraction') + require(G.active(G.mm(leave, enter)) == 0, 'reverse dirty contraction') + require(P.M[G.active(enter)][G.active(leave)] != 1, 'projection mutation control') + for ao, co in (('column', 'row'), ('row', 'column')): + aa, cc = G.alphabet(ao), G.alphabet(co) + require(len(aa) == len(set(aa)) == len(cc) == len(set(cc)) == 21, + 'complete rank-one orientation alphabet') + require(sum(G.active(n) == 0 for n in aa) == 3 and + sum(G.active(n) == 0 for n in cc) == 3, 'pure-dirty alphabet coverage') + # Explicit two-letter word must occur in the general gap table. + a_n, c_n = (leave, enter) if ao == 'column' else (enter, leave) + positive = [1, 1, 0, G.dirty(a_n, ao), 0, G.dirty(c_n, co), 1] + rows = G.joint_table(aa, cc, ao, co) + require(any(row[:-1] == positive for row in rows), 'dirty gap positive fixture') + totals = Counter() + for row in rows: + totals[tuple(row[:2])] += row[-1] + from math import comb + require(set(totals) == {(ka, kc) for ka in range(4) for kc in range(4) + if ka+kc <= 4}, 'gap count-pair domain') + require(all(count == comb(ka+kc, ka) * 21**(ka+kc) + for (ka, kc), count in totals.items()), 'gap multiplicity coverage') + return {'literal_profile_checks': len(pairs), 'changed_middle_rejected': True, + 'unsupported_single_cap_2_rejected': True, + 'unsupported_joint_cap_3_rejected': True, + 'pure_dirty_and_order_controls': True, + 'gap_multiplicities_match_closed_form': True} + + +def run(): + stats, pairs, ranks, caps = P.enumerate_profiles(progress=True) + require(len(pairs) == len(set(pairs)) == 5664, 'distinct profile-pair count') + check_caps(caps) + checked = controls(pairs, caps) + return { + 'schema_version': 1, + 'scope': 'five-b opposite-orientation active profiles and bounded gap operators', + 'statistics': stats, + 'profile_set_sha256': profile_digest(pairs), + 'rank_sum_histogram': [[*key, count] for key, count in sorted(ranks.items())], + 'gap_cap_histogram': [[*key, count] for key, count in sorted(caps.items())], + 'gap_tables': G.run(), + 'controls': checked, + } + + +if __name__ == '__main__': + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument('--write-result', action='store_true', help='explicitly regenerate RESULT.json') + args = parser.parse_args() + start = time.perf_counter() + result = run() + if args.write_result: + (HERE / 'RESULT.json').write_text(json.dumps(result, indent=2) + '\n', encoding='utf-8') + else: + require(result == json.loads((HERE / 'RESULT.json').read_text(encoding='utf-8')), + 'audit receipt mismatch') + print('PASS_UT4_FIVE_B_COVERAGE_AUDIT profiles=5664 single_gap_cap=3 joint_gap_cap=4' + ' profile_set=' + result['profile_set_sha256'] + + ' seconds=' + str(round(time.perf_counter()-start, 3)))