diff --git a/research/ut3-two-targets-any-registers/EXPECTED.json b/research/ut3-two-targets-any-registers/EXPECTED.json new file mode 100644 index 0000000000..4cc3d353d2 --- /dev/null +++ b/research/ut3-two-targets-any-registers/EXPECTED.json @@ -0,0 +1,198 @@ +{ + "schema_version": 1, + "status": "PASS_UT3_ANY_REGISTERS", + "written_theorem": "minimum 4w for every finite r>=w>=1 with all nonzero rank-one scalar couplings; eight at w=2", + "finite_evidence": { + "group_products": 64, + "algebra_associativity_triples": 32768, + "idempotent_determinants": 154, + "expanded_paid_involutions": 566, + "nilpotent_scalar_couplings": 129, + "symbolic_two_occurrence_patterns": 84, + "concrete_two_occurrence_words": 70236, + "faithful_witness_columns": [ + 16, + 24, + 32, + 64, + 128 + ], + "conjugated_witness_columns": 40, + "general_witnesses": [ + [ + 1, + 1, + 4 + ], + [ + 2, + 1, + 4 + ], + [ + 2, + 2, + 8 + ], + [ + 3, + 1, + 4 + ], + [ + 3, + 2, + 8 + ], + [ + 3, + 3, + 12 + ], + [ + 4, + 1, + 4 + ], + [ + 4, + 2, + 8 + ], + [ + 4, + 3, + 12 + ], + [ + 4, + 4, + 16 + ], + [ + 8, + 1, + 4 + ], + [ + 8, + 2, + 8 + ], + [ + 8, + 3, + 12 + ], + [ + 8, + 4, + 16 + ], + [ + 8, + 5, + 20 + ], + [ + 8, + 6, + 24 + ], + [ + 8, + 7, + 28 + ], + [ + 8, + 8, + 32 + ], + [ + 16, + 1, + 4 + ], + [ + 16, + 2, + 8 + ], + [ + 16, + 3, + 12 + ], + [ + 16, + 4, + 16 + ], + [ + 16, + 5, + 20 + ], + [ + 16, + 6, + 24 + ], + [ + 16, + 7, + 28 + ], + [ + 16, + 8, + 32 + ], + [ + 16, + 9, + 36 + ], + [ + 16, + 10, + 40 + ], + [ + 16, + 11, + 44 + ], + [ + 16, + 12, + 48 + ], + [ + 16, + 13, + 52 + ], + [ + 16, + 14, + 56 + ], + [ + 16, + 15, + 60 + ], + [ + 16, + 16, + 64 + ] + ], + "zero_product_rank_pairs": 7129, + "controls": 48 + }, + "acceptance_limit": "Finite checks corroborate README proof; quotient equality never admits a formal word.", + "new_kappa": false +} diff --git a/research/ut3-two-targets-any-registers/README.md b/research/ut3-two-targets-any-registers/README.md new file mode 100644 index 0000000000..3fc4f569a2 --- /dev/null +++ b/research/ut3-two-targets-any-registers/README.md @@ -0,0 +1,210 @@ +# Nilpotent rank-one couplings do not lower the central UT3 call bill + +**Scoped extension and independent check; no new kappa.** Central UT3 targets +still cost exactly `4w` calls if the paid alphabet admits **every nonzero +rank-one scalar coupling**, including nilpotent matrices as well as +idempotents. This holds for every finite `r>=w>=1` with all extra registers +arbitrary dirty and restored. A degree-two quotient proves the bound. + +This answers the arbitrary-register handoff in juper997's +[PR1478](https://github.com/CrocSwap/integer-mult-bounds/pull/1478), pinned at +`b30fdba48f3db70e3589ba740b0782b56ec0ba2e`. That package proves the two-target +minimum for `r=2,3`. woklerx's +[PR1443](https://github.com/CrocSwap/integer-mult-bounds/pull/1443), pinned at +`965ff75aabb16cdd0978f4bf9222bcdedf514021`, independently proves the two-register +case. Those minima and direct words are predecessor results. + +Steph4n-gh's concurrent +[PR1573](https://github.com/CrocSwap/integer-mult-bounds/pull/1573), head +`0b8c5a69297c794f2de22c04494c83e41300ae36`, which already proves `4w` for +every finite workspace and target count in the **idempotent** alphabet. +That shared conclusion is corroboration. The precise extension here removes +`v^T u=1`, permitting nilpotent paid couplings `v^T u=0` at the same optimistic +unit price. Every expanded call is reversible; the lower bound survives. +The proof uses one quotient retaining both mixed coefficients, instead of +the predecessor's natural representation and generator-swapped companion. + +## Exact model and complete bill + +Let `G=UT_3(F2)`, with triples `(u,v,z)` for entries `01,12,02` and product + +`(u,v,z)(U,V,Z)=(u+U,v+V,z+Z+uV)`. + +Set `a=I+E01`, `b=I+E12`, `c=abab=I+E02`. The group has eight elements; `a,b` +are involutions and `c` is a nonidentity central involution. Work in the full +formal group algebra `R=F2[G]`. For any finite `r>=w>=1`, a paid factor is + +`D_N(g)=I+([g]+1)N`, where `g` is **only a or b**, +`N=u v^T` is any nonzero binary rank-one matrix; `v^T u` may be zero or one. + +At trace one, `N^2=N` is the predecessor's idempotent type. At trace zero, +`N^2=0` is the added nilpotent type. For example, `N=E01` adds +`([g]+1)` times register 1 into register 0, with both inputs dirty. Each such +coupling is optimistically priced at one paid call. Its full formal inverse +is itself: `([g]+1)^2=0`, hence `D_N(g)^2=I` without an idempotence assumption. + +The required endpoint is `T=diag([c],...,[c],1,...,1)`, with exactly `w` central +targets. Equality means every formal coefficient agrees on every register, +including the `r-w` restored dirty roles. There is no free address map, clean +allocation, COPY, ERASE, higher-rank paid factor, or free inverse. +Scalar `GL_r(F2)` maps are free **in this optimistic screening model**. + +Move all scalar maps to one end by conjugating the scalar couplings. Every +paid factor augments to `I` under `[g]->1`, and the target also augments to `I`, +so the final scalar map is `I`. Rank survives conjugation. The expanded +alphabet already includes every nonzero rank-one matrix, so it covers all +these conjugates. This retains Gareth Davidson's PR1333 normalization; it +does not assume a nilpotent matrix is conjugate to an idempotent. + +The attaining bill is four calls `(a,b,a,b)` on each data coordinate. It uses +`w` data roles, zero extra workspace, `4w` paid calls, no scalar preparation, +and no uncharged undo. Appending identity roles gives every `r>=w` boundary. + +## Dimension-independent proof + +Use the associative algebra + +`A=F2/(X^2,Y^2, all monomials of length >=3)`. + +Its basis is `1,X,Y,XY,YX`. The group map `a->1+X`, `b->1+Y` is valid: +both images square to one, and their product has fourth power one. +The presentation `a^2=b^2=(ab)^4=1` is the eight-element dihedral group +isomorphic to `UT_3(F2)`. Alternatively the explicit map on triples is + +`(u,v,z) -> 1+uX+vY+zXY+(z+uv)YX`; + +substitution in the displayed group law verifies multiplication directly. +In particular, `c->1+XY+YX`. Extend linearly to `R->A`. This quotient is used +only for a necessary lower-bound condition, never for formal acceptance. + +Let `Q=diag(1,...,1,0,...,0)` have rank `w`. The target's quotient image is +`I+(XY+YX)Q`; its `X` and `Y` coefficients vanish, while both mixed +coefficients equal `Q`. + +There are `p` a-labeled factors. Write their scalar matrices, in chronological +order, as `N_i=u_i v_i^T`. Let `U=(u_1 ... u_p)` and `V=(v_1 ... v_p)`. +The coefficient of `X` in the product is + +`sum_i N_i = U V^T = 0`. + +Every `XY` term chooses an a factor first and a b factor later. Therefore its +coefficient is `sum_i N_i S_i`, where `S_i` is the sum of the b projectors +after a occurrence `i`. Its column space lies in the column space of `U`. +Every `YX` term is `sum_i R_i N_i`, with `R_i` the sum of b projectors before +that occurrence. Its row space lies in the row space of `V^T`. No term of +length three or more survives, and `X^2=Y^2=0`; no commutation of scalar +matrices is used. Since both mixed coefficients are `Q`, + +`rank(U)>=w` and `rank(V^T)>=w`. + +But `UV^T=0` gives `image(V^T) subset kernel(U)` inside `F2^p`, so + +`rank(U)+rank(V^T)<=p`. + +Hence **p>=2w**. For the `q` b-labeled factors, the same argument exchanges +`X,Y`: the `Y` coefficient is zero, the `YX` column space comes from their +left vectors, and the `XY` row space comes from their right vectors. +Thus **q>=2w**. Every legal word has at least `p+q>=4w` paid calls. +The direct formal word above attains `4w`, proving the theorem. + +The lower-bound argument uses rank one, not idempotence, for the scalar +matrices. The direct upper construction uses idempotents, which remain in +the expanded alphabet. Neither determinant parity nor a bound on the number +of restored roles is needed. In fact the predecessor's parity shortcut no +longer applies to every paid call: for nilpotent `N`, `det(I+tN)=1` in +`F2[t]/t^2`, whereas idempotent calls contribute `1+t`. + +## Exact executable evidence + +[verify.py](verify.py) corroborates the proof with standard-library F2 arithmetic: + +- All 64 group products verify the quotient homomorphism; all 32,768 triples + of quotient elements verify associativity. +- All 154 rank-one idempotents on 2, 3 and 4 registers verify the separate-label + determinant formula by a direct Leibniz calculation. This is an additional + control inherited from the parity approach, not a required proof step. +- All 283 rank-one matrices at those dimensions (9,49,225) check the expanded + alphabet; all 566 a/b paid factors square to identity in the full formal + algebra and the faithful regular representation. The 129 added nilpotent + scalar matrices have determinant one in the dual-number quotient. +- All 70,236 two-a-occurrence words with up to three b calls on two registers + check the mixed-coefficient factorization and rank bound. The independent + symbolic subsequence expansion checks all 84 two-occurrence label patterns + through length eight. These bounded tests do not establish the uniform proof. +- All 7,129 zero-product pairs among binary `2-by-p` and `p-by-2` matrices, + `p=1..4`, verify the rank inequality without a paid-projector assumption. +- The full formal `4w` witness and a separate faithful regular replay agree + for every `w=1..r` at `r=1,2,3,4,8,16` (34 fixtures). The coefficient-span + bounds are checked on every witness. A five-register scalar-conjugated + fixture exercises dirty workspace and the changed output basis. +- Forty omitted-call controls reject; eight further controls distinguish + rank-two paid calls, the enlarged central-label alphabet, a nonfaithful + quotient kernel, a wrong scalar boundary, and un-restored dirty workspace. + In particular, allowing `c` itself as a primitive attains two targets in two + calls, and allowing rank-two projectors attains them in four. The restricted + alphabet and rank charge are essential. + +All 324 ordered two-factor products over the expanded two-register alphabet +also agree between formal, quotient and faithful regular replay in the tests. +The formal and regular engines use different address multiplication: triples +versus literal 3-by-3 binary matrices. They share ordinary F2 matrix arithmetic +and were written in one session. This is not independent human proof review. +[EXPECTED.json](EXPECTED.json) records counts; `--emit` prints a fresh receipt +without modifying the source. Acceptance is type-sensitive and read-only. +Exact executed environments, commands and the resolved temporary-directory +limitation are recorded in [VALIDATION.md](VALIDATION.md). + +## Reproduce and limits + +From the repository root, Python 3.10+ and the standard library: + +```sh +python3 -I -B research/ut3-two-targets-any-registers/verify.py +python3 -I -O -B research/ut3-two-targets-any-registers/verify.py +python3 -I -B research/ut3-two-targets-any-registers/test_verify.py +python3 scripts/research_package.py --package research/ut3-two-targets-any-registers --check-only +python3.12 scripts/research_package.py --package research/ut3-two-targets-any-registers +``` + +Expected checker: `PASS_UT3_ANY_REGISTERS minimum=4w ... two_targets=8 ... no_new_kappa`. +[TASK.json](TASK.json) records the selection, refinement, sources, overlap and +stop rule; [SOURCES.json](SOURCES.json) pins exact base inputs and predecessor +heads. The initial main is `680967accfd4311f3241dc154e1f434869747b43`. +Coordination is in [Discussion1569](https://github.com/CrocSwap/integer-mult-bounds/discussions/1569). + +This changes the rational abelian starting model to a specified nonabelian +binary group and restricted paid alphabet. It does not reduce rational frame +entries modulo two or establish a rational-frame identity. Other targets, +groups, alphabets and primitive prices are outside the theorem. +Selected-source binding orientation passed. Full selected-supplier cold replay, +physical/compiler and common-label realization, ownership/hosting, +precision/tape, outer analytic transfer, Lean formalization and independent +human proof review are not supplied. No new supplier or multiplication +exponent is claimed. + +## Open next questions + +Which additional paid address primitive could escape the `4w` obstruction at +a favorable **complete** price? This matters because more dirty workspace +alone cannot help in the declared alphabet. A first step is to state an +expanded alphabet and map it into the same quotient, then charge its mixed +coefficients and explicit formal realization before searching. A cheaply +declared central label makes the optimistic bill smaller, but its actual +physical implementation and compatibility with the retained bit interface +remain the blocker. No physical escape or broader group lower bound is implied. + +## Credit and license + +Credit steph4n-gh's concurrent PR1573 for the all-register/all-target +idempotent result, shared zero-sum rank proof, and separate-label bounds; +juper997's PR1478 for the fixed-register UT3 result and explicit +arbitrary-register handoff; woklerx's PR1443 for the two-register dihedral +certificate; Gareth Davidson (@bitplane), PR1333, for the nonabelian affine +direction, scalar normalization and rank-method context; and eumemic (PR288), +Ali Romman (PR468) and David Govea (PR720) for the retained register-model and +rank-method lineage. No predecessor code is imported and no literature-priority +claim is made for rank-nullity or group-algebra methods. + +Prepared by **Arham Tahir with substantial OpenAI Codex assistance** in +reasoning, implementation, validation and writing. No subagents were used. +New work is Apache-2.0; predecessor files and notices are unchanged. diff --git a/research/ut3-two-targets-any-registers/SOURCES.json b/research/ut3-two-targets-any-registers/SOURCES.json new file mode 100644 index 0000000000..7283b00685 --- /dev/null +++ b/research/ut3-two-targets-any-registers/SOURCES.json @@ -0,0 +1,71 @@ +{ + "schema_version": 1, + "base_commit": "680967accfd4311f3241dc154e1f434869747b43", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "ae6a99f28aa468649eb66a361e764d769363bf11", + "sha256": "10b9e340fd8e354a37a0c4813c90e5de1dd42044b5f6aca4a3fc5a42b685fa32" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "c05fafaa25ba95b2d5af86b1800427198e3d20eb", + "sha256": "89b5928bc92c81e2647b6d702a7ad85a6795b8f44e2eb267b2ff3145d8f2b2ce" + }, + { + "path": "research/bit-three-register-lower-bound/README.md", + "usage": "input", + "git_blob": "25e41c370c101a33a6deb978de08b03ed7539b79", + "sha256": "c12b33ef388deece0cbf891505a2ce2c0779a0c3a6cf1f0f7f7039bab59cbebd" + } + ], + "contextual_predecessors": [ + { + "pr": 1478, + "head": "b30fdba48f3db70e3589ba740b0782b56ec0ba2e", + "path": "research/ut3-commutator-register-bound/README.md", + "git_blob": "26af5fcb949eb68e6a43001fe1debd2d465b0504", + "sha256": "6a8c399bfc765050ee80a20ec83251cfcf435b90ad528a6f4ae4f7f770991e59", + "url": "https://github.com/CrocSwap/integer-mult-bounds/blob/b30fdba48f3db70e3589ba740b0782b56ec0ba2e/research/ut3-commutator-register-bound/README.md", + "usage": "Context/attribution only; not imported or executed." + }, + { + "pr": 1443, + "head": "965ff75aabb16cdd0978f4bf9222bcdedf514021", + "path": "research/bit-dihedral-commutator/README.md", + "git_blob": "b7619a5d56f32daf7f48d6cc3a0e260c5a333510", + "sha256": "4f3f9df6d6d96a26ccb0fcd2ef947cce5d53b0d992da22e866f1e025be4c0492", + "url": "https://github.com/CrocSwap/integer-mult-bounds/blob/965ff75aabb16cdd0978f4bf9222bcdedf514021/research/bit-dihedral-commutator/README.md", + "usage": "Context/attribution only; not imported or executed." + }, + { + "pr": 1573, + "head": "0b8c5a69297c794f2de22c04494c83e41300ae36", + "path": "research/ut3-commutator-all-registers/README.md", + "git_blob": "4a6a4ee9d995818348b3b853a95500dcce81228d", + "sha256": "fdd5405da1c0535a407013f2a4628a07dae4957fd9fb776cd14f05315d1aa26b", + "url": "https://github.com/CrocSwap/integer-mult-bounds/blob/0b8c5a69297c794f2de22c04494c83e41300ae36/research/ut3-commutator-all-registers/README.md", + "usage": "Context/independent predecessor replay only; not imported by this package." + }, + { + "pr": 1573, + "head": "0b8c5a69297c794f2de22c04494c83e41300ae36", + "path": "research/ut3-commutator-all-registers/independent.py", + "git_blob": "b92331ac2952716e38a44203e1328af5336e91b6", + "sha256": "a5ea48c528cbbb07ad8fbc2f6a0244ac6def9a7e7fcc382a3d846fa785e3449a", + "url": "https://github.com/CrocSwap/integer-mult-bounds/blob/0b8c5a69297c794f2de22c04494c83e41300ae36/research/ut3-commutator-all-registers/independent.py", + "usage": "Context/independent predecessor replay only; not imported by this package." + }, + { + "pr": 1573, + "head": "0b8c5a69297c794f2de22c04494c83e41300ae36", + "path": "research/ut3-commutator-all-registers/verify.py", + "git_blob": "a359dabf83c3a5ad12b6c078ae6a1e558624805b", + "sha256": "b229d8c04747a661144fda9f510a7abd3ae0b0b2f989b7fd51dd9e23e46cb5ba", + "url": "https://github.com/CrocSwap/integer-mult-bounds/blob/0b8c5a69297c794f2de22c04494c83e41300ae36/research/ut3-commutator-all-registers/verify.py", + "usage": "Context/independent predecessor replay only; not imported by this package." + } + ] +} diff --git a/research/ut3-two-targets-any-registers/TASK.json b/research/ut3-two-targets-any-registers/TASK.json new file mode 100644 index 0000000000..27392cf0dc --- /dev/null +++ b/research/ut3-two-targets-any-registers/TASK.json @@ -0,0 +1,145 @@ +{ + "schema_version": 1, + "task_id": "bit-new-register-model", + "priority_revision": 2, + "base_commit": "680967accfd4311f3241dc154e1f434869747b43", + "original_card": { + "id": "bit-new-register-model", + "question": "Can an explicitly larger or nonabelian register model escape the scoped three-register obstruction?", + "starting_points": [ + "research/bit-three-register-lower-bound/README.md", + "certificates/selected-result.json" + ], + "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.", + "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": "Write a complete operation alphabet outside one named premise and price a baseline before searching identities.", + "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." + ], + "overlap_terms": [ + "three-register", + "nonabelian", + "group algebra" + ] + }, + "scope_status": "changed", + "actual_scope": "Exact minimum 4w central UT3(F2) calls for every finite r>=w>=1 when paid a/b couplings include ALL nonzero binary rank-one scalar matrices, both idempotent and nilpotent; every extra register dirty and restored, free scalar mixing.", + "scope_change_reason": "Final overlap found concurrent PR1573 with the same all-register 4w idempotent theorem. That theorem is corroboration, with explicit credit. This bounded complementary extension removes the scalar-idempotence hypothesis, allowing nilpotent rank-one paid couplings at an optimistic unit price. Their full formal inverses and rank proof are supplied; the parity shortcut is explicitly invalid in this expanded alphabet.", + "bottleneck_link": "Screens an actual alphabet extension as well as extra dirty workspace: even granting every rank-one nilpotent address coupling at unit price cannot lower the complete direct 4w call bill for central targets. No physical bit-supplier admission is claimed.", + "budget_minutes": 60, + "stop_rule": "One 60-minute session. Prove or falsify the all-register coefficient argument; check the quotient homomorphism exhaustively and formal attaining witnesses, then stop without a larger census.", + "outcome": "negative-result", + "evidence": "README written extension and independent degree-two quotient; 566 complete formal/faithful expanded-call involutions, 70236 mixed-coefficient cases, 34 attaining 4w fixtures, 48 semantic/model controls and four focused tests.", + "author": "Arham Tahir", + "ai_assistance": "Substantial OpenAI Codex assistance in reasoning, code, verification and writing; no subagents or independent human proof review.", + "open_questions": [ + { + "question": "Which additional paid address primitive can escape 4w at a favorable complete price?", + "why_it_matters": "Extra restored workspace and nilpotent rank-one scalar coupling alone cannot lower this model bill.", + "first_step": "State a larger address-label alphabet, compute its quotient images, and price its full formal implementation before searching.", + "blocked_by": "Physical realization and retained bit-interface compatibility; declaring the central address label cheap is not an implementation." + } + ], + "chooser_nonce": "02e3f35bb37f8e361f7fe7e0c9239d58", + "scope_key": "UT3F2/a-b/all-rank-one-scalar-couplings-including-nilpotents/all-central-target-counts/arbitrary-restored-registers/degree-two-quotient", + "selected_method": "Construct the smallest exact identity in a newly specified legal operation alphabet; refined to the card's target-specific relaxation method after the known eight-call direct word.", + "optimistic_budget": { + "paid_calls": "4w (eight at w=2)", + "data_roles": "w", + "dirty_extras": "any finite r-w", + "scalar_mixing": "free in screening model", + "nilpotent_couplings": "optimistic unit price per a/b factor", + "required_improvement": "fewer than 4w calls; excluded by the written proof" + }, + "predecessors": [ + { + "pr": 1478, + "head": "b30fdba48f3db70e3589ba740b0782b56ec0ba2e", + "credit": "juper997; fixed r=2,3 minimum and explicit arbitrary-r handoff" + }, + { + "pr": 1443, + "head": "965ff75aabb16cdd0978f4bf9222bcdedf514021", + "credit": "woklerx; exact two-register dihedral minimum" + }, + { + "pr": 1333, + "head": "7f25b6d0e1d7e995d4d2840f231d98b1a1a9fec2", + "credit": "Gareth Davidson; model and free-scalar augmentation normalization" + }, + { + "pr": 1573, + "head": "0b8c5a69297c794f2de22c04494c83e41300ae36", + "credit": "steph4n-gh; concurrent 4w theorem for all registers and target counts with idempotent scalar couplings, shared zero-sum rank argument" + } + ], + "discussion": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1569", + "entry_overlap": { + "open_prs": { + "fetched_at": "2026-10-14T03:03:14.893167+00:00", + "complete_pagination": true, + "records": 721 + }, + "discussions": { + "fetched_at": "2026-10-14T03:03:49.010423+00:00", + "complete_pagination": true, + "records": 221 + } + }, + "changed_hypothesis": "Remove v^T u=1 from the scalar paid alphabet; retain nonzero rank one, g in {a,b}, formal endpoint, and restored dirty roles.", + "predecessor_replay": { + "pr": 1573, + "head": "0b8c5a69297c794f2de22c04494c83e41300ae36", + "python": "3.12.14", + "command": "python3.12 -I -O -B verify.py (isolated four-file source export)", + "result": "PASS_UT3_ALL_REGISTERS; no predecessor code imported by the new package" + }, + "final_overlap": { + "searched_at": "2026-10-14T03:29:52.679885+00:00", + "terms": [ + "UT3", + "UT_3", + "dihedral commutator", + "nilpotent", + "nonidempotent" + ], + "coverage": { + "open_prs": { + "fetched_at": "2026-10-14T03:28:55.916592+00:00", + "complete_pagination": true, + "records": 725 + }, + "discussions": { + "fetched_at": "2026-10-14T03:29:29.144585+00:00", + "complete_pagination": true, + "records": 229 + } + }, + "warnings": [], + "limits": "Remote PR scope is open PRs including drafts. Closed work is searched through local READMEs, TASK metadata and ledger only. No code diffs or arbitrary package files are searched. Recheck relevant heads before submission.", + "decision": "PR1573 old-alphabet 4w theorem is independently corroborated and credited. Submit only the explicit extension to all rank-one scalar couplings including nilpotents, with separate quotient evidence; no priority claim for the shared theorem.", + "rechecked_heads": { + "1478": "b30fdba48f3db70e3589ba740b0782b56ec0ba2e", + "1443": "965ff75aabb16cdd0978f4bf9222bcdedf514021", + "1333": "7f25b6d0e1d7e995d4d2840f231d98b1a1a9fec2", + "1573": "0b8c5a69297c794f2de22c04494c83e41300ae36" + } + } +} diff --git a/research/ut3-two-targets-any-registers/VALIDATION.md b/research/ut3-two-targets-any-registers/VALIDATION.md new file mode 100644 index 0000000000..bf45442f0c --- /dev/null +++ b/research/ut3-two-targets-any-registers/VALIDATION.md @@ -0,0 +1,54 @@ +# Local validation + +Research base: `680967accfd4311f3241dc154e1f434869747b43` (current main when +the session started). New work is confined to this package. The selected +record, upstream inputs and frozen predecessor packages are unchanged. + +On Windows, CPython **3.12.14** (bundled runtime), these final-scope commands passed: + +```sh +python3.12 -I -B scripts/research_package.py --package research/ut3-two-targets-any-registers +``` + +The registered hook runs the isolated optimized verifier, then all four tests. +It reports `PASS_UT3_ANY_REGISTERS ... minimum=4w ... controls=48`, four passing +tests, and `PASS_REGISTERED_RESEARCH_PACKAGE ... outcome=negative-result`. +The counts in `EXPECTED.json` include the expanded nilpotent alphabet. + +An additional **CPython 3.14.6** isolated optimized replay passed: + +```sh +python3.14 -I -O -B research/ut3-two-targets-any-registers/verify.py +``` + +Tests make a temporary minimal source export in a path containing spaces. +The export's optimized replay leaves every source/receipt byte unchanged. +Three actual receipt corruptions (boolean replacing integer schema, omitted +fixture and an underpriced fixture) and actual source drift all reject, +without overwriting the evidence. The tests also check 324 two-factor words +over the expanded paid alphabet, including noncommuting scalar couplings. + +The first test attempt failed because this Windows execution sandbox denied +its default temporary directory. Setting `TEMP` and `TMP` to an existing +directory inside the authorized workspace resolved that environment problem. +No verifier or proof change was made to bypass it. The final registered replay +used that environment; the temporary exports were cleaned up by the tests. + +Independent predecessor check: PR1573 at +`0b8c5a69297c794f2de22c04494c83e41300ae36` was exported into a separate directory +with its `README.md`, `verify.py`, `independent.py` and `CERTIFICATE.json`. +Its command `python3.12 -I -O -B verify.py` passed as +`PASS_UT3_ALL_REGISTERS`. Exact canonical source Git blobs and SHA256 hashes are +in `SOURCES.json`; this package imports none of that code. The shared theorem +is credited as corroboration, and the submission removes scalar idempotence. + +The prescribed source-bound `scripts/research_baseline.py` orientation passed. +`scripts/verify_selected_result.py` passed for the full selected source +inventory, exact kappa and proof supplements. `git diff --cached --check` +passed. The metadata/provenance checks run as part of the registered replay. + +Not run or established: selected-supplier cold circuit replay, hosted CI, +physical/compiler/common-label admission, ownership/hosting, precision/tape, +outer analytic transfer, Lean formalization or independent human proof review. +The arbitrary-register theorem is the written rank proof, not an extrapolation +from these finite checks. No new kappa is claimed. diff --git a/research/ut3-two-targets-any-registers/VERIFY.json b/research/ut3-two-targets-any-registers/VERIFY.json new file mode 100644 index 0000000000..82ad6e4146 --- /dev/null +++ b/research/ut3-two-targets-any-registers/VERIFY.json @@ -0,0 +1,32 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/bit-three-register-lower-bound/README.md" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-O", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Exact quotient algebra and rank controls; every rank-one scalar coupling at r=2,3,4, including 129 nilpotents, with 566 full formal/faithful involutions; 70236 mixed-coefficient cases, attaining 4w witnesses and 48 controls. Corroborates README proof." + }, + { + "argv": [ + "{python}", + "-I", + "-B", + "{package}/test_verify.py" + ], + "timeout_seconds": 120, + "checks": "All 324 two-factor formal/quotient/regular comparisons in the expanded alphabet, noncommuting order, nilpotent versus idempotent hypotheses, optimized isolated relocation and real source/type-sensitive receipt corruption rejection." + } + ] +} diff --git a/research/ut3-two-targets-any-registers/test_verify.py b/research/ut3-two-targets-any-registers/test_verify.py new file mode 100644 index 0000000000..3eb4576472 --- /dev/null +++ b/research/ut3-two-targets-any-registers/test_verify.py @@ -0,0 +1,101 @@ +"""Mathematical and artifact failure controls, Apache-2.0; Codex assistance.""" +import hashlib +import importlib.util +import itertools +import json +from pathlib import Path +import shutil +import subprocess +import sys +import tempfile +import unittest + +HERE = Path(__file__).resolve().parent +spec = importlib.util.spec_from_file_location('ut3_checker', HERE / 'verify.py') +checker = importlib.util.module_from_spec(spec) +spec.loader.exec_module(checker) + + +class VerifyTests(unittest.TestCase): + def test_noncommuting_mixed_coefficients(self): + n, m = (1, 0), (1, 1) + xy = checker.qword([(1, n), (2, m)], 2) + yx = checker.qword([(2, m), (1, n)], 2) + self.assertEqual(xy[3], checker.mm(n, m)) + self.assertEqual(yx[4], checker.mm(m, n)) + self.assertNotEqual(xy[3], yx[4]) + self.assertEqual(xy[4], checker.zero(2)) + self.assertEqual(yx[3], checker.zero(2)) + + def test_all_two_factor_formal_images(self): + generators = [(g, n) for g in (1, 2) for n in checker.rank_one_matrices(2)] + for word in itertools.product(generators, repeat=2): + formal = checker.formal_word(word, 2) + self.assertEqual(checker.qword(word, 2), checker.quotient_formal(formal, 2)) + self.assertEqual(checker.regular_word(word, 2), checker.regular_formal(formal, 2)) + + def test_proof_hypotheses_are_needed(self): + # Without the zero linear boundary, the zero-product span inequality + # would be false: one outer product has two active spans but one call. + u, vt = (1, 0), (1,) + self.assertNotEqual(checker.mm(u, vt), checker.zero(2)) + self.assertGreater(checker.rank(u) + checker.rank(vt), 1) + # One central target has legal rank-one mixed coefficients at four calls. + word = checker.direct(4, 1) + self.assertEqual(checker.rank(checker.qword(word, 4)[3]), 1) + self.assertEqual(checker.formal_word(word, 4), checker.target(4, 1)) + nilpotent = (2, 0) + checker.validate_paid(nilpotent) + self.assertEqual(checker.mm(nilpotent, nilpotent), checker.zero(2)) + self.assertEqual(checker.determinant_dual(nilpotent), 1) + with self.assertRaisesRegex(ValueError, 'idempotent'): + checker.validate_projector(nilpotent) + + def test_isolated_optimized_replay_and_real_corruptions(self): + source_root = HERE.parents[1] + source = 'research/bit-three-register-lower-bound/README.md' + with tempfile.TemporaryDirectory(prefix='UT3 proof with spaces ') as directory: + root = Path(directory) + package = root / 'research' / HERE.name + shutil.copytree(HERE, package, ignore=shutil.ignore_patterns('__pycache__')) + input_path = root / source + input_path.parent.mkdir(parents=True) + input_path.write_bytes((source_root / source).read_bytes()) + files = [p for p in root.rglob('*') if p.is_file()] + before = {p.relative_to(root).as_posix(): hashlib.sha256(p.read_bytes()).hexdigest() for p in files} + + def replay(): + return subprocess.run([sys.executable, '-I', '-O', '-B', str(package / 'verify.py')], + cwd=root, capture_output=True, text=True, timeout=30) + + result = replay() + self.assertEqual(result.returncode, 0, result.stderr) + self.assertIn('minimum=4w', result.stdout) + after = {p.relative_to(root).as_posix(): hashlib.sha256(p.read_bytes()).hexdigest() + for p in root.rglob('*') if p.is_file()} + self.assertEqual(before, after) + receipt_path = package / 'EXPECTED.json' + original = receipt_path.read_bytes() + for change in ('bool', 'omitted-fixture', 'underpriced'): + receipt = json.loads(original) + if change == 'bool': + receipt['schema_version'] = True + elif change == 'omitted-fixture': + receipt['finite_evidence']['general_witnesses'].pop() + else: + receipt['finite_evidence']['general_witnesses'][0][2] = 3 + receipt_path.write_text(json.dumps(receipt), encoding='utf-8') + broken = replay() + self.assertNotEqual(broken.returncode, 0) + self.assertIn('receipt mismatch', broken.stderr) + self.assertEqual(json.loads(receipt_path.read_text()), receipt) + receipt_path.write_bytes(original) + input_path.write_bytes(input_path.read_bytes() + b'\ncorrupted input\n') + broken = replay() + self.assertNotEqual(broken.returncode, 0) + self.assertIn('source pin', broken.stderr) + self.assertEqual(receipt_path.read_bytes(), original) + + +if __name__ == '__main__': + unittest.main() diff --git a/research/ut3-two-targets-any-registers/verify.py b/research/ut3-two-targets-any-registers/verify.py new file mode 100644 index 0000000000..43d29a4aff --- /dev/null +++ b/research/ut3-two-targets-any-registers/verify.py @@ -0,0 +1,409 @@ +"""Exact controls for the written arbitrary-register UT3 bound. Apache-2.0. + +Finite checks corroborate README.md; they do not enumerate all register counts +or certify formal equality from a quotient. Substantial OpenAI Codex assistance. +""" +import argparse +import hashlib +import itertools +import json +from pathlib import Path + +HERE = Path(__file__).resolve().parent +BASIS = ('', 'x', 'y', 'xy', 'yx') + + +def need(condition, message): + if not condition: + raise ValueError(message) + + +def qmul(left, right): + out = 0 + for i, a in enumerate(BASIS): + if left >> i & 1: + for j, b in enumerate(BASIS): + if right >> j & 1: + word = a + b + if word in BASIS: + out ^= 1 << BASIS.index(word) + return out + + +def group_mul(g, h): + """UT3 triples encoded x+2y+4z; multiplication is noncommutative.""" + return g ^ h ^ (((g & 1) * ((h >> 1) & 1)) << 2) + + +def image(g): + x, y, z = g & 1, (g >> 1) & 1, (g >> 2) & 1 + return 1 | (x << 1) | (y << 2) | (z << 3) | ((z ^ (x * y)) << 4) + + +def eye(r): + return tuple(1 << i for i in range(r)) + + +def zero(r): + return (0,) * r + + +def add(a, b): + return tuple(x ^ y for x, y in zip(a, b)) + + +def mm(a, b): + rows = [] + for row in a: + result = 0 + while row: + bit = row & -row + result ^= b[bit.bit_length() - 1] + row ^= bit + rows.append(result) + return tuple(rows) + + +def rank(a): + pivots = {} + for row in a: + while row: + pivot = row.bit_length() - 1 + if pivot not in pivots: + pivots[pivot] = row + break + row ^= pivots[pivot] + return len(pivots) + + +def outer(u, v, r): + return tuple(v if u >> i & 1 else 0 for i in range(r)) + + +def projectors(r): + return [outer(u, v, r) for u in range(1, 1 << r) + for v in range(1, 1 << r) if (u & v).bit_count() % 2] + + +def rank_one_matrices(r): + return [outer(u, v, r) for u in range(1, 1 << r) for v in range(1, 1 << r)] + + +def validate_paid(n): + need(rank(n) == 1, 'not a rank-one paid coupling') + + +def validate_projector(n): + need(rank(n) == 1 and mm(n, n) == n, 'not a rank-one idempotent') + + +def qword(word, r): + """Matrix product in quotient coefficients; order matches written product.""" + out = [eye(r), *[zero(r) for _ in range(4)]] + for g, n in word: + label = 1 if g == 1 else 2 + need(g in (1, 2), 'restricted alphabet') + nxt = list(out) + for i in range(5): + monomial = BASIS[i] + BASIS[label] + if monomial in BASIS: + j = BASIS.index(monomial) + nxt[j] = add(nxt[j], mm(out[i], n)) + out = nxt + return tuple(out) + + +def formal_word(word, r): + """Full eight-coefficient group-algebra product, not quotient admission.""" + out = {0: eye(r)} + for g, n in word: + nxt = dict(out) + for h, coefficient in out.items(): + term = mm(coefficient, n) + for label in (h, group_mul(h, g)): + nxt[label] = add(nxt.get(label, zero(r)), term) + out = {g: n for g, n in nxt.items() if any(n)} + return out + + +def quotient_formal(formal, r): + out = [zero(r) for _ in range(5)] + for g, matrix in formal.items(): + for i in range(5): + if image(g) >> i & 1: + out[i] = add(out[i], matrix) + return tuple(out) + + +def regular_word(word, r): + """Separate F2 replay in a faithful regular representation. + + Construct literal 3x3 address matrices instead of using group_mul/image, + then form 8r-dimensional right-regular operators and multiply row masks. + """ + addresses = [(1 | ((g & 1) << 1) | (((g >> 2) & 1) << 2), + 2 | (((g >> 1) & 1) << 2), 4) for g in range(8)] + out = eye(8 * r) + for g, n in word: + permutation = [addresses.index(mm(h, addresses[g])) for h in addresses] + rows = [] + for i in range(r): + for h in range(8): + row = 1 << (8 * i + h) + for j in range(r): + if n[i] >> j & 1: + row ^= (1 << (8 * j + h)) ^ (1 << (8 * j + permutation[h])) + rows.append(row) + out = mm(out, tuple(rows)) + return out + + +def regular_formal(formal, r): + addresses = [(1 | ((g & 1) << 1) | (((g >> 2) & 1) << 2), + 2 | (((g >> 1) & 1) << 2), 4) for g in range(8)] + rows = [0] * (8 * r) + for g, n in formal.items(): + for h in range(8): + destination = addresses.index(mm(addresses[h], addresses[g])) + for i in range(r): + for j in range(r): + if n[i] >> j & 1: + rows[8 * i + h] ^= 1 << (8 * j + destination) + return tuple(rows) + + +def determinant_dual(n): + """Leibniz determinant of I+tN over F2[t]/t^2, without rank-one shortcut.""" + r = len(n) + out = 0 + for permutation in itertools.permutations(range(r)): + term = 1 + for i, j in enumerate(permutation): + value = int(i == j) | (((n[i] >> j) & 1) << 1) + term = ((term & 1) * (value & 1)) | ( + (((term & 1) * (value >> 1)) ^ ((term >> 1) * (value & 1))) << 1) + out ^= term + return out + + +def target(r, w=2): + q = tuple(1 << i if i < w else 0 for i in range(r)) + return {0: add(eye(r), q), 4: q} if r > w else {4: q} + + +def direct(r, w=2): + return [(g, outer(1 << i, 1 << i, r)) + for i in range(w) for g in (1, 2, 1, 2)] + + +def coefficient_rank_check(word, r): + """Check both scalar-span bounds used in the proof, without inferring equality.""" + coefficients = qword(word, r) + for label, linear, column_mixed, row_mixed in ((1, 1, 3, 4), (2, 2, 4, 3)): + factors = [n for g, n in word if g == label] + vectors = [] + for n in factors: + v = next((row for row in n if row), 0) + need(v != 0 and all(row in (0, v) for row in n), 'rank-one factorization') + u = sum(1 << i for i, row in enumerate(n) if row) + vectors.append((u, v)) + u_matrix = tuple(sum(((u >> i) & 1) << j for j, (u, v) in enumerate(vectors)) + for i in range(r)) + vt_matrix = tuple(v for u, v in vectors) + need(mm(u_matrix, vt_matrix) == coefficients[linear], 'linear coefficient UV^T') + need(rank(coefficients[column_mixed]) <= rank(u_matrix), 'mixed column span') + need(rank(coefficients[row_mixed]) <= rank(vt_matrix), 'mixed row span') + if not any(coefficients[linear]): + need(rank(u_matrix) + rank(vt_matrix) <= len(factors), 'zero-product rank inequality') + + +def zero_product_controls(): + """All binary 2-by-p / p-by-2 pairs, p=1..4; no paid-word assumption.""" + checked = 0 + for p in range(1, 5): + for packed_u in range(1 << (2 * p)): + u = (packed_u & ((1 << p) - 1), packed_u >> p) + for packed_v in range(1 << (2 * p)): + vt = tuple((packed_v >> (2 * i)) & 3 for i in range(p)) + if mm(u, vt) == zero(2): + need(rank(u) + rank(vt) <= p, 'independent rectangular rank control') + checked += 1 + return checked + + +def symbolic_patterns(): + """Expand by selecting at most two nonconstant factors, independently. + + B symbols are chronological and both x symbols are N. These bounded + patterns corroborate the written all-length coefficient formula. + """ + patterns = 0 + for k in range(2, 9): + for first, second in itertools.combinations(range(k), 2): + labels = ['y'] * k + labels[first] = labels[second] = 'x' + names = [('N',) if t == 'x' else (f'B{i}',) for i, t in enumerate(labels)] + coefficients = {'x': set(), 'xy': set(), 'yx': set()} + for i in range(k): + if labels[i] == 'x': + coefficients['x'].symmetric_difference_update([names[i]]) + for j in range(i + 1, k): + monomial = labels[i] + labels[j] + if monomial in ('xy', 'yx'): + coefficients[monomial].symmetric_difference_update([names[i] + names[j]]) + middle = [f'B{i}' for i in range(first + 1, second)] + need(not coefficients['x'], 'linear coefficient must vanish') + need(coefficients['xy'] == {('N', b) for b in middle}, 'left factorization') + need(coefficients['yx'] == {(b, 'N') for b in middle}, 'right factorization') + patterns += 1 + return patterns + + +def run_checks(): + for a, b in itertools.product(range(8), repeat=2): + need(image(group_mul(a, b)) == qmul(image(a), image(b)), 'quotient homomorphism') + for a, b, c in itertools.product(range(32), repeat=3): + need(qmul(qmul(a, b), c) == qmul(a, qmul(b, c)), 'quotient associativity') + need(image(4) == 1 | 8 | 16, 'central target has both mixed coefficients') + + count = 0 + for r in (2, 3, 4): + ns = projectors(r) + need(len(ns) == ((1 << r) - 1) * (1 << (r - 1)), 'complete outer-product count') + for n in ns: + validate_projector(n) + need(determinant_dual(n) == 3, 'separate-label determinant parity') + count += 1 + + expanded_generators, nilpotent_count = 0, 0 + for r in (2, 3, 4): + matrices = rank_one_matrices(r) + need(len(matrices) == ((1 << r) - 1) ** 2, 'complete rank-one alphabet') + need(len(set(matrices)) == len(matrices), 'unique outer products over F2') + for n in matrices: + validate_paid(n) + if mm(n, n) == zero(r): + need(determinant_dual(n) == 1, 'nilpotent coupling has no parity contribution') + nilpotent_count += 1 + else: + need(mm(n, n) == n, 'rank-one trace dichotomy') + for g in (1, 2): + need(formal_word([(g, n), (g, n)], r) == {0: eye(r)}, 'every expanded paid call is involutory') + need(regular_word([(g, n), (g, n)], r) == eye(8 * r), 'faithful expanded involution') + expanded_generators += 1 + + concrete = 0 + ns = rank_one_matrices(2) + for bcount in range(4): + for first, second in itertools.combinations(range(bcount + 2), 2): + for n in ns: + for bs in itertools.product(ns, repeat=bcount): + word, at, middle = [], 0, zero(2) + for i in range(bcount + 2): + if i in (first, second): + word.append((1, n)) + else: + word.append((2, bs[at])) + if first < i < second: + middle = add(middle, bs[at]) + at += 1 + out = qword(word, 2) + need(out[1] == zero(2), 'two equal a linear coefficient') + need(out[3] == mm(n, middle) and out[4] == mm(middle, n), 'mixed coefficient law') + need(rank(out[3]) <= 1 and rank(out[4]) <= 1, 'rank-one obstruction') + concrete += 1 + + witness_counts, controls = [], 0 + for r in (2, 3, 4, 8, 16): + word, wanted = direct(r), target(r) + formal = formal_word(word, r) + need(formal == wanted, 'complete dirty boundary of eight-call witness') + need(qword(word, r) == quotient_formal(formal, r), 'formal/quotient compatibility') + need(regular_word(word, r) == regular_formal(wanted, r), 'faithful regular witness') + for i in range(8): + need(formal_word(word[:i] + word[i + 1:], r) != wanted, 'omitted paid call') + controls += 1 + need(formal_word(direct(r, 1), r) == target(r, 1), 'rank-one target legitimately costs four') + witness_counts.append(r * 8) + + general_witnesses = [] + for r in (1, 2, 3, 4, 8, 16): + for w in range(1, r + 1): + word, wanted = direct(r, w), target(r, w) + need(formal_word(word, r) == wanted, '4w complete formal witness') + need(regular_word(word, r) == regular_formal(wanted, r), '4w faithful boundary') + coefficient_rank_check(word, r) + general_witnesses.append([r, w, 4 * w]) + + r = 5 + scalar = list(eye(r)) + scalar[0] ^= scalar[4] + scalar = tuple(scalar) + word = [(g, mm(mm(scalar, n), scalar)) for g, n in direct(r)] + conjugated = {g: mm(mm(scalar, n), scalar) for g, n in target(r).items()} + need(formal_word(word, r) == conjugated, 'arbitrary dirty scalar conjugation') + need(regular_word(word, r) == regular_formal(conjugated, r), 'conjugated faithful boundary') + coefficient_rank_check(word, r) + need(formal_word(word, r) != target(r), 'nontrivial scalar/output boundary detected') + controls += 1 + + for n in (zero(2), eye(2)): + try: + validate_paid(n) + except ValueError: + controls += 1 + else: + raise ValueError('invalid paid primitive admitted') + need(formal_word([(g, eye(2)) for g in (1, 2, 1, 2)], 2) == target(2), + 'rank-two primitives destroy the eight-unit bound') + controls += 1 + expanded = [(4, outer(1 << i, 1 << i, 3)) for i in range(2)] + need(formal_word(expanded, 3) == target(3), 'central-label primitive destroys the bound') + controls += 1 + kernel = {g: (1,) for g in range(8)} + need(quotient_formal(kernel, 1) == (zero(1),) * 5, 'nonfaithful quotient kernel') + need(any(regular_formal(kernel, 1)), 'formal nonzero kernel survives faithful replay') + controls += 1 + need(formal_word(direct(3) + [(1, outer(4, 4, 3))], 3) != target(3), 'dirty extra must be restored') + controls += 1 + validate_paid((2, 0)) + need(determinant_dual((2, 0)) == 1, 'legal nilpotent coupling defeats idempotent parity shortcut') + controls += 1 + + return {'schema_version': 1, 'status': 'PASS_UT3_ANY_REGISTERS', + 'written_theorem': 'minimum 4w for every finite r>=w>=1 with all nonzero rank-one scalar couplings; eight at w=2', + 'finite_evidence': {'group_products': 64, 'algebra_associativity_triples': 32768, + 'idempotent_determinants': count, 'expanded_paid_involutions': expanded_generators, + 'nilpotent_scalar_couplings': nilpotent_count, + 'symbolic_two_occurrence_patterns': symbolic_patterns(), + 'concrete_two_occurrence_words': concrete, 'faithful_witness_columns': witness_counts, + 'conjugated_witness_columns': 40, 'general_witnesses': general_witnesses, + 'zero_product_rank_pairs': zero_product_controls(), 'controls': controls}, + 'acceptance_limit': 'Finite checks corroborate README proof; quotient equality never admits a formal word.', + 'new_kappa': False} + + +def check_pins(): + root = HERE.parents[1] + for source in json.loads((HERE / 'SOURCES.json').read_text(encoding='utf-8'))['files']: + if source['usage'] == 'input': + need(hashlib.sha256((root / source['path']).read_bytes()).hexdigest() == source['sha256'], 'source pin') + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument('--emit', action='store_true', help='print fresh receipt without writing files') + args = parser.parse_args() + check_pins() + receipt = run_checks() + if args.emit: + print(json.dumps(receipt, indent=2)) + else: + expected = json.loads((HERE / 'EXPECTED.json').read_text(encoding='utf-8')) + need(json.dumps(receipt, sort_keys=True) == json.dumps(expected, sort_keys=True), 'receipt mismatch') + print(receipt['status'], 'minimum=4w registers=any-finite-r>=w>=1 two_targets=8', + 'controls=' + str(receipt['finite_evidence']['controls']), 'no_new_kappa') + + +if __name__ == '__main__': + main()