diff --git a/research/gl3-order4-register-census/EXPECTED.json b/research/gl3-order4-register-census/EXPECTED.json new file mode 100644 index 0000000000..3595859cb7 --- /dev/null +++ b/research/gl3-order4-register-census/EXPECTED.json @@ -0,0 +1,187 @@ +{ + "address_distance_layers": [ + 1, + 6, + 24, + 51, + 60, + 24, + 2 + ], + "address_group_size": 168, + "claim": "FINITE_MINIMUM_EIGHT_EXACTLY_TWO_REGISTERS", + "controls": [ + "omit-call-0", + "omit-call-1", + "omit-call-2", + "omit-call-3", + "omit-call-4", + "omit-call-5", + "omit-call-6", + "omit-call-7", + "reverse-CNOT-direction", + "reverse-chronology", + "cross-role-dirty-input-leakage", + "natural-image-is-not-formal-equality", + "rank-two-projector-underpricing", + "nonidempotent-paid-generator", + "only-one-role-completed" + ], + "direct_word_chronological": [ + [ + 1, + 0 + ], + [ + 0, + 1 + ], + [ + 2, + 1 + ], + [ + 1, + 2 + ] + ], + "directed_transition_attempts": 559692, + "faithful_regular_basis_columns": 336, + "formal_witness_chronological": [ + [ + 1, + 0, + 1, + 1 + ], + [ + 0, + 1, + 1, + 1 + ], + [ + 2, + 1, + 1, + 1 + ], + [ + 1, + 2, + 1, + 1 + ], + [ + 1, + 0, + 2, + 2 + ], + [ + 0, + 1, + 2, + 2 + ], + [ + 2, + 1, + 2, + 2 + ], + [ + 1, + 2, + 2, + 2 + ] + ], + "independent_full_layer_comparison": true, + "independent_target_meets": 0, + "live_source_hashes_checked": 1, + "natural_distance_layers": [ + 1, + 36, + 816, + 14694, + 225528 + ], + "natural_layer_sha256": [ + "530d743528053cb46bfe9dadf13363b10e1b3581fc4398a932be790cae576bee", + "beca9b337d9692be76bdc89d8c0c4fb30d70b856c7a953ea144eee55996de575", + "57ef9e03c3c2cdabe317eef01ee7ed8079e84e6b3cb2b4b6ac132bd1e92f270a", + "85c7c5429706b2367d48e070c0045aa795165dbcead2345e2373144bd1624858", + "e4150a3f90c70b9629595b43eacf46fcd9041a66e7ba59ba7b31f1222f68e689" + ], + "not_checked": [ + "extra scalar registers", + "physical supplier realization", + "compiler/hosting/precision/tape/analytic transfer", + "Lean proof" + ], + "paid_generator_count": 36, + "positive_fixtures": { + "identity_minimum": 0, + "kernel_group_elements_rows": [ + [ + 1, + 2, + 4 + ], + [ + 2, + 4, + 7 + ], + [ + 4, + 7, + 1 + ], + [ + 7, + 1, + 2 + ] + ], + "single_role_minimum": 4 + }, + "radius_four_size": 241075, + "radius_three_four_target_meets": 0, + "radius_three_size": 15547, + "scalar_idempotents": [ + [ + 1, + 1 + ], + [ + 1, + 3 + ], + [ + 2, + 2 + ], + [ + 2, + 3 + ], + [ + 3, + 1 + ], + [ + 3, + 2 + ] + ], + "schema_version": 1, + "target_displacement_rank": 2, + "target_order": 4, + "target_rows": [ + 2, + 4, + 7 + ] +} diff --git a/research/gl3-order4-register-census/PROOF.md b/research/gl3-order4-register-census/PROOF.md new file mode 100644 index 0000000000..3db705b59e --- /dev/null +++ b/research/gl3-order4-register-census/PROOF.md @@ -0,0 +1,148 @@ +# Exact minimum eight for the fixed order-four target + +This is a computer-assisted finite theorem in an explicitly changed register +model. It is not a theorem about unrestricted integer-multiplication algorithms. + +## 1. Alphabet, target and scalar normalization + +Let `G=GL_3(F2)`, `R=F2[G]`, and + +\[ + h=\begin{pmatrix}0&1&0\\0&0&1\\1&1&1\end{pmatrix}. +\] + +There are exactly two scalar register roles. The target in `M_2(R)` is +`T=diag([h],[h])`; equality of every formal coefficient is required. A free +operation is any `B in GL_2(F2)`, using the identity group label. A paid unit is + +\[ + D_N(g)=I+([g]+1)N,\qquad + g=I+E_{ij},\ i\ne j,\qquad + N=uv^T,\quad u,v\in\mathbb F_2^2,\quad v^Tu=1. +\] + +No address operation is free. There are no extra roles, clean-only input +promises, copies or erasures. Each paid occurrence costs one, including undo. +For each of the three nonzero `u`, exactly two `v` satisfy `v^Tu=1`; these +are precisely the six rank-one binary idempotents. + +Moving scalar basis changes to one end conjugates `N`, preserving the complete +six-projector alphabet. Augmentation `[g] -> 1` maps all paid units and `T` to +`I`. Therefore the remaining scalar matrix must be `I`. Every legal circuit +with `k` paid calls is a product of `k` of the 36 specified units. This argument +is the normalization used in Gareth Davidson's PR #1333, credited here. + +## 2. The natural relaxation is sufficient for exclusion + +The natural representation extends linearly to an algebra homomorphism +`rho: F2[G] -> M_3(F2)`. On the two-register space, reorder coordinates with +address coordinate first. A paid unit becomes + +\[ + \rho_2(D_N(I+E_{ij}))=I_6+E_{ij}\otimes N, + \qquad \rho_2(T)=h\otimes I_2. +\] + +Every such six-dimensional matrix is an involution, since `E_ij^2=0`. +Consequently, if no word of length at most seven reaches `h tensor I_2` in +this matrix alphabet, no formal word of those lengths reaches `T`. +No injectivity of `rho` is needed for this implication. + +In fact `rho` is not injective even when augmented data are retained. Write +`q=[1]+[h]+[h^2]+[h^3]`. Since `h` has order four, `q` is a nonzero formal +element. Direct exact matrix addition gives +`I+h+h^2+h^3=0`, and its augmentation is also zero. Thus replacing an +off-diagonal zero of `T` by `q` preserves its natural image and augmentation +but changes the formal endpoint. This is an explicit checker control, not a +claim that the perturbed endpoint is attainable by a shorter legal word. + +## 3. Complete finite lower-bound certificate + +Breadth-first traversal starts at `I_6`. At each depth, expand **every** state +in the previous new layer by **all 36** generators. Deduplicate only by exact +matrix equality, retaining each state at its shortest distance. By induction, +these are precisely the distance layers; a state seen earlier can use the +same future suffix and therefore need not be re-expanded at a greater depth. +All arithmetic is over `F2`; no floating-point or probabilistic hash comparison +is used for membership or cross-implementation equality. + +The verified layer cardinalities through depth four are + +\[ + (1,36,816,14694,225528), +\] + +and the total directed expansion count is +`36*(1+36+816+14694)=559692`. Let `B_d` be the union of layers through `d` +and `U=h tensor I_2`. The certificate checks + +\[ + \#\{p\in B_3 : pU^{-1}\in B_4\}=0.\tag{1} +\] + +Every word of length at most seven can be split as `U=A B`, with `A` of +length at most four and `B` of length at most three. Taking `p=B` gives +`p U^-1=A^-1 in B_4`, because the generators are involutions. Conversely a +meet gives `U=(pU^-1)^-1 p`, of length at most seven. Thus (1) is a complete +exclusion, not a heuristic search. It includes all shorter and odd lengths. + +The independent implementation enumerates scalar projectors from all 16 +binary 2x2 matrices and uses dense 6x6 row tuples, register-major coordinates +and right multiplication. Its full layer sets equal the primary packed-row +left-product sets after coordinate conversion. Independently, it tests +`U p^-1 in B_4` for every `p in B_3`, computing inverses by binary Gaussian +elimination. This second test also has zero meets. Layer SHA256 values serve +only as deterministic receipts; acceptance compares the actual complete sets. + +## 4. Attained formal upper bound and direct length + +In chronological order, the four address gates are + +\[ + (i,j)=(1,0),(0,1),(2,1),(1,2),\qquad x_i\leftarrow x_i+x_j. +\] + +Their successive row-bitmask matrices are +`(1,2,4) -> (1,3,4) -> (2,3,4) -> (2,3,7) -> (2,4,7)`. +Thus the final address map is `h`. The exact direct Cayley census has distance +layers `1,6,24,51,60,24,2`, totaling +`(8-1)(8-2)(8-4)=168=|GL_3(F2)|`, and places `h` at distance four. +A separate enumeration of all 512 binary matrices, keeping rank three, +agrees on every direct distance. Also `h^4=I`, `h^2!=I` and `rank(h-I)=2`. + +For every scalar idempotent `N` and group labels `a,b`, expansion gives +`D_N(a)D_N(b)=D_N(ab)`. Apply the four chronological gates with `N=E_00`, +then the same four with `N=E_11`. The result is exactly `diag([h],[h])`. +Each role receives four paid calls; the other role is fixed during those +four calls. There are eight total calls, no other roles, no scalar basis +changes and no leftover restoration operation. The identity is in the formal +algebra, so it holds on every module and for arbitrary input values in both roles. + +The coefficient-bitset implementation checks all four formal matrix entries. +A separate set-based implementation acts on all 336 basis vectors of the +faithful left regular module. This representation is faithful because an +algebra element acting on the identity basis element recovers that element; +the register-matrix extension is faithful for the same reason column by column. +Together with Section 3, the minimum is exactly eight. + +## 5. Scope and attribution + +The finite exclusion fixes two scalar registers and the six coordinate-CNOT +labels. It proves neither the same lower bound with extra restored dirty +registers nor an unrestricted direct-sum theorem. If rank-two scalar +projectors were charged one unit, the same four address gates would apply to +both roles in four units; that is a different alphabet and an explicit scope +control. Allowing arbitrary rank-one address maps also changes the problem. + +No rational-address source is reduced modulo two. No physical bit supplier, +all-size compiler, common-label realization, hosting, precision/tape, +analytic transfer, selected cold replay or Lean theorem is established. +The code-disjoint implementations were prepared in the same session, without +an independent human proof review. + +This account's PR #1414 posed the higher-dimensional follow-up to Gareth +Davidson (@bitplane)'s PR #1333. The surrounding abelian register lineage is +credited to eumemic, Ali Romman and David Govea. No predecessor implementation +is imported, and no broad literature-priority claim is made. + +Prepared for commdata2338 (@commdata2338), with substantial OpenAI Codex assistance. diff --git a/research/gl3-order4-register-census/README.md b/research/gl3-order4-register-census/README.md new file mode 100644 index 0000000000..87abf0bff2 --- /dev/null +++ b/research/gl3-order4-register-census/README.md @@ -0,0 +1,139 @@ +# Two order-four GL3 targets need eight coordinate-CNOT calls + +**Finite minimum certificate; no new kappa.** On exactly two arbitrary-input +registers, the formal target `diag([h],[h])` requires exactly **eight** paid +coordinate-CNOT calls, where + +```text +h = [[0,1,0], [0,0,1], [1,1,1]] in GL_3(F2). +``` + +All six directed coordinate CNOTs are allowed, and all scalar `GL_2(F2)` +register mixing is free. The address matrix has order four, +`rank(h-I)=2`, and direct coordinate-CNOT length four. Its coordinate dependency +graph contains the cycle `0 -> 1 -> 2 -> 0`; no address coordinate is a spectator. +This answers one concrete instance of [PR #1414](https://github.com/CrocSwap/integer-mult-bounds/pull/1414)'s +second open question. It does not establish a general direct-sum bound. + +## Model and evidence + +Work in the formal group algebra `R=F2[GL_3(F2)]`. A paid unit is +`I+([g]+1)N`, where `g=I+E_ij`, `i!=j`, and `N=uv^T` is a binary rank-one +idempotent (`v^T u=1`). There are six address labels and six scalar projectors, +hence 36 paid generators. Every occurrence, including an undo, costs one. +Free scalar basis changes normalize away by augmentation. No free address +maps, extra registers, clean allocations, copies or erasures are allowed. +Both role inputs are arbitrary and the complete formal output is prescribed. + +The direct chronological address word is +`(1<-1+0), (0<-0+1), (2<-2+1), (1<-1+2)`. +Execute it first on scalar projector `E_00`, then on `E_11`: eight paid calls, +no additional roles, no scalar basis changes and no omitted restoration bill. +Its full formal coefficients and all **336 columns** of the faithful regular +representation agree with the target. + +For the lower bound, map formal labels to their natural three-dimensional +matrices. This gives an **exclusion-only** six-dimensional matrix relaxation. +Two separately implemented exact traversals agree on every matrix in every +layer through radius four: + +| Distance | 0 | 1 | 2 | 3 | 4 | +| --- | ---: | ---: | ---: | ---: | ---: | +| Distinct natural matrices | 1 | 36 | 816 | 14,694 | 225,528 | + +The radius-three and radius-four balls contain 15,547 and 241,075 matrices. +There are **zero** target meets, excluding every word of length at most seven, +including odd lengths. Each traversal expands 559,692 directed transitions. +No sign/parity argument from the six-element `GL_2(F2)` group is reused. +The direct address census covers all 168 `GL_3(F2)` elements with distance +layers `1,6,24,51,60,24,2`. + +[PROOF.md](PROOF.md) explains normalization, complete finite coverage, +the one-way use of the natural representation and the formal upper bound. +[EXPECTED.json](EXPECTED.json) records exact layer hashes, the witness and +15 semantic/scope controls. A four-term nonzero group-algebra perturbation +has zero natural image and zero augmentation; it demonstrates why a natural +*match* would not certify a formal identity. + +## Reproduce + +Python 3.12 and its standard library suffice. From the repository root: + +```sh +python3 -I -B research/gl3-order4-register-census/verify.py +python3 scripts/research_package.py --package research/gl3-order4-register-census --check-only +python3 scripts/research_package.py --package research/gl3-order4-register-census +``` + +Expected direct output: + +```text +PASS_GL3_ORDER4_REGISTER_CENSUS minimum=8 registers=2 address_group=168 direct_length=4 natural_short_words=0 regular_columns=336 controls=15 no_new_kappa +``` + +The registered hook runs the certificate and seven focused tests. Those tests +check all 1,296 two-generator formal/natural comparisons, all scalar +conjugations, faithful regular rejection, source corruption and receipt +corruption, including the real CLI under optimized Python. `--emit` computes +a fresh receipt on stdout; normal replay reads and compares the entire committed +receipt. It does not regenerate artifacts. Layer hashes encode sorted packed +36-bit row matrices as five little-endian bytes each. + +The independent engine enumerates all 512 candidate address matrices and all +16 scalar matrices, uses dense row tuples in register-major order and right +multiplication. The primary engine uses rank-one factorizations, packed +coordinate-major rows and left multiplication. Entire distance-layer sets +are compared after an explicit index conversion. Each engine also performs +its own target-intersection test, with independently obtained inverse data. +They were written in the same research session; this is implementation +cross-checking, not independent human review. + +## Task, overlap and limitations + +Base `4040a0f46d67b41c36a472a7cd4af791fd4c36cc`; card +`bit-new-register-model`, scope key `7f5f4426ef796683c485`, priority revision 2, +nonce `b4841db8408c803fc7a3fb9693192ecf`. The claim is in +[discussion #1317](https://github.com/CrocSwap/integer-mult-bounds/discussions/1317#discussioncomment-18912727). +[TASK.json](TASK.json) records the scoped question and overlap check. + +This account's PR #1414 (`9e1640094f649ba6db9742796825a8d6c238989b`) treats +order-two swaps in a two-coordinate alphabet. Gareth Davidson's PR #1333 +(`7f25b6d0e1d7e995d4d2840f231d98b1a1a9fec2`) permits all affine rank-one +address operations, giving a different rank-based bill. Concurrent work in +#1317 on a third address coordinate for order-two swaps, and on central +commutators in `UT_3(F2)`, has different targets and alphabets. No pending +implementation is imported or required for replay. + +The result is confined to this target, six-label alphabet and **exactly two +scalar registers**. Additional arbitrary dirty registers are unexamined. +The changed formal nonabelian model does not reduce rational frames modulo two. +Physical/compiler/common-label/hosting, precision/tape and analytic admission +are unrun. There is no selected-supplier cold replay, Lean proof, full +multiplication theorem or exponent improvement. The selected record and +frozen sources are unchanged. + +## Open next questions + +1. **One extra restored dirty scalar register.** This tests whether the + two-role obstruction survives a genuine workspace expansion. First build + the 168-generator nine-dimensional natural relaxation for the same `h` + and seek a short path; certify any positive path formally. Radius-four + growth is the immediate resource blocker, and an empty smaller search + would not settle the question. +2. **A structural lower bound for this target with arbitrary register count.** + This would replace the finite role restriction. Start by identifying an + invariant that assigns at least eight total charges to the two order-four + outputs. The rank floor is only four and the sign-quotient argument + of PR #1414 does not apply here; the present finite census supplies + no universal proof. + +## Credit and license + +Prepared for commdata2338 (@commdata2338), with substantial OpenAI Codex assistance. + +Credit Gareth Davidson (@bitplane), PR #1333, for the restricted-alphabet +question and augmentation normalization; this account's PR #1414 for the +concrete higher-dimensional follow-up; eumemic (PR #288), Ali Romman +(PR #468) and David Govea (PR #720) for the surrounding register-model +lineage. No general rank-method or literature-priority claim is made. +New work is Apache-2.0; all predecessor files and notices remain unchanged. diff --git a/research/gl3-order4-register-census/SOURCES.json b/research/gl3-order4-register-census/SOURCES.json new file mode 100644 index 0000000000..dcb69c1956 --- /dev/null +++ b/research/gl3-order4-register-census/SOURCES.json @@ -0,0 +1,60 @@ +{ + "schema_version": 1, + "base_commit": "4040a0f46d67b41c36a472a7cd4af791fd4c36cc", + "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": 1414, + "head": "9e1640094f649ba6db9742796825a8d6c238989b", + "usage": "context only; no imported implementation or runtime dependency", + "files": [ + { + "path": "research/coordinate-cnot-register-bound/README.md", + "git_blob": "cdcc5a9e7f11ab3dbf7745a175ddcca208c68211", + "sha256": "e1666512fb71cf34c427c69ffb61a18b61e897a7f8f91f87820edf744e85a9fe" + }, + { + "path": "research/coordinate-cnot-register-bound/PROOF.md", + "git_blob": "68fee5b5ccff5329e27300e40dcbd483640dd6b7", + "sha256": "bcee89f92dcce8253bd7eae6e924ddff598c900da81979c6171a412f03d765e1" + } + ] + }, + { + "pr": 1333, + "head": "7f25b6d0e1d7e995d4d2840f231d98b1a1a9fec2", + "usage": "context only; no imported implementation or runtime dependency", + "files": [ + { + "path": "research/binary-affine-register-bound/README.md", + "git_blob": "7b68583becf8be6f3cf666b05b0943e7eb99270c", + "sha256": "7951868efdf35fdb2aacdd302ca825cbde0586a5fae6df23aee78e29f30c332a" + }, + { + "path": "research/binary-affine-register-bound/PROOF.md", + "git_blob": "b1152a39b559f7a058489ec74231488e4f8edd83", + "sha256": "36a33434222798434b0a17476ae5f9bc8a2a3891871c46e77cc50ce2e132206b" + } + ] + } + ] +} diff --git a/research/gl3-order4-register-census/TASK.json b/research/gl3-order4-register-census/TASK.json new file mode 100644 index 0000000000..3fbac6a7bf --- /dev/null +++ b/research/gl3-order4-register-census/TASK.json @@ -0,0 +1,137 @@ +{ + "schema_version": 1, + "task_id": "bit-new-register-model", + "priority_revision": 2, + "base_commit": "4040a0f46d67b41c36a472a7cd4af791fd4c36cc", + "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": "refined", + "actual_scope": "Exact minimum paid coordinate-CNOT cost of diag([h],[h]) in M_2(F2[GL_3(F2)]), h rows (2,4,7), all six coordinate labels, all six binary rank-one idempotents, free scalar GL_2 mixing and exactly two arbitrary-input roles.", + "scope_change_reason": "Take PR1414 second open question in a specified nonabelian three-coordinate alphabet. The order-four strongly connected target has direct length four but displacement rank two. This is outside the abelian rational-address model and is a fixed-role finite result.", + "bottleneck_link": "Tests whether collective register mixing saves paid recursive units in a changed address alphabet. The finite obstruction rejects this specific optimistic eight-call budget reduction; no selected-supplier or exponent improvement follows.", + "budget_minutes": 60, + "stop_rule": "Pin one target, certify its direct length, and exhaust lengths through seven in the two-role model. Stop construction if the exact relaxation excludes a saving; preserve the final quarter for controls and handoff.", + "outcome": "negative-result", + "evidence": "PROOF.md plus EXPECTED.json: all 168 direct address distances; complete equality of two implementations of 241075 natural states through radius 4; zero radius 3/radius 4 target meets; exact eight-call formal witness and 336 faithful regular columns;15 controls and seven focused tests.", + "author": "commdata2338", + "ai_assistance": "Prepared for commdata2338 (@commdata2338), with substantial OpenAI Codex assistance. Both implementations were written in one session; no independent human proof review is claimed.", + "open_questions": [ + { + "question": "Does a third restored dirty scalar register permit fewer than eight calls for the same two h targets?", + "why_it_matters": "Tests whether the obstruction survives a genuine workspace expansion.", + "first_step": "Construct the 168-generator nine-dimensional natural relaxation for diag(h,h,I), seek a short path, and check any candidate in the full formal group algebra.", + "blocked_by": "Radius-four state growth; the present finite certificate fixes exactly two scalar registers." + }, + { + "question": "Can a structural invariant prove the same bound for arbitrary restored dirty-register counts?", + "why_it_matters": "Would turn a fixed-role finite obstruction into a general bound for this target and alphabet.", + "first_step": "Seek a target-specific invariant that charges at least eight units; the basic displacement-rank floor is only four.", + "blocked_by": "The GL2 sign-quotient argument of PR1414 does not apply here, and finite state counts supply no all-register proof." + } + ], + "chooser": { + "nonce": "b4841db8408c803fc7a3fb9693192ecf", + "track": "bit-mechanisms", + "scope_key": "7f5f4426ef796683c485", + "other_suggestion": { + "task_id": "bit-helper-contract", + "scope_key": "bfb61f829a81535adeae", + "reason_passed_over": "PR1194/1311 semantic-D work, PR1420 projected cleanup and this account's PR1306 cover immediate scopes." + } + }, + "refined_scope_key": "GL3F2/six-coordinate-CNOT/order4-rows-2-4-7/two-registers/length<=7", + "question": "Can scalar register mixing beat the direct four-plus-four paid bill for two copies of h?", + "changed_hypothesis": "Nonabelian GL_3(F2) address labels replace abelian rational frames; only six coordinate CNOTs have unit price. No rational frame entries are reduced modulo two.", + "method_domain": "All36 normalized paid generators, all lengths 0..7 by exact radius 3/radius 4 meet-in-the-middle. Natural matrices are used for exclusion only; formal coefficients and the faithful regular action certify the upper witness.", + "optimistic_full_cost_budget": "Eight paid calls, no extra roles, no scalar operations in the attaining word. The lower bound grants every scalar GL_2(F2) operation free. Every undo is included.", + "reproduce": "python3 -I -B research/gl3-order4-register-census/verify.py", + "discussion": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1317#discussioncomment-18912727", + "unchecked_obligations": [ + "extra restored dirty scalar registers", + "other targets and address alphabets", + "physical/compiler/common-label/hosting admission", + "precision/tape and analytic transfer", + "Lean or independent human proof verification", + "selected supplier cold replay" + ], + "overlap": { + "mode": "shared offline snapshot; no novelty certificate", + "queries": [ + "--task bit-new-register-model", + "--task bit-helper-contract", + "GL_3(F2) / GL3 / three-dimensional coordinate / four-call target" + ], + "coverage": { + "discussions": { + "fetched_at": "2026-10-14T01:24:02.227375+00:00", + "complete_pagination": true, + "records": 169 + }, + "open_prs": { + "fetched_at": "2026-10-14T01:23:37.439709+00:00", + "complete_pagination": true, + "records": 776 + } + }, + "distinctions": [ + "PR1414 covers two order-two GL2 coordinate swaps; the present h has order4 and uses three address coordinates.", + "PR1333 allows arbitrary affine rank-one labels; its price rule differs.", + "The concurrent GL3 address-spectator claim in discussion1317 targets order-two swaps with direct bill 6, not this order-four target with bill 8.", + "The active UT3 central-commutator claim has a different group, restricted label set and endpoint." + ], + "final_queries": [ + "order-four / gl3-order4 / two copies of h / four-call target" + ], + "final_coverage": { + "discussions": { + "fetched_at": "2026-10-14T01:24:02.227375+00:00", + "complete_pagination": true, + "records": 169 + }, + "open_prs": { + "fetched_at": "2026-10-14T01:34:09.157196+00:00", + "complete_pagination": true, + "records": 744 + } + }, + "rechecked_heads": { + "1333": "7f25b6d0e1d7e995d4d2840f231d98b1a1a9fec2", + "1414": "9e1640094f649ba6db9742796825a8d6c238989b" + }, + "other_matches": "PR1391 and PR1410 use order-four frames for dirty-echo boundary scheduling, not paid GL3 coordinate-CNOT word length." + } +} diff --git a/research/gl3-order4-register-census/VERIFY.json b/research/gl3-order4-register-census/VERIFY.json new file mode 100644 index 0000000000..c6cf0a5f3c --- /dev/null +++ b/research/gl3-order4-register-census/VERIFY.json @@ -0,0 +1,31 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/bit-three-register-lower-bound/README.md" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 90, + "checks": "Exact 168-element direct distances; independent complete natural layers and target meets; formal upper witness, 336 faithful regular columns and 15 semantic/scope controls." + }, + { + "argv": [ + "{python}", + "-I", + "-B", + "{package}/test_verify.py" + ], + "timeout_seconds": 120, + "checks": "Seven focused semantic and corruption tests, including all 1296 generator-pair comparisons and optimized CLI rejection." + } + ] +} diff --git a/research/gl3-order4-register-census/independent.py b/research/gl3-order4-register-census/independent.py new file mode 100644 index 0000000000..d0604b3f99 --- /dev/null +++ b/research/gl3-order4-register-census/independent.py @@ -0,0 +1,140 @@ +"""Separate dense-row, right-product census and faithful regular action. + +No producer matrix, group, rank, generator or transition routine is imported. +Coordinates are register-major here; verify.py uses coordinate-major packing. +""" +from itertools import product + + +def xor_all(values): + value = 0 + for x in values: + value ^= x + return value + + +def dimension(rows, width): + rows = list(rows) + rank = 0 + for column in range(width): + pivot = next((i for i in range(rank, len(rows)) if rows[i] >> column & 1), None) + if pivot is not None: + rows[rank], rows[pivot] = rows[pivot], rows[rank] + for i in range(len(rows)): + if i != rank and rows[i] >> column & 1: + rows[i] ^= rows[rank] + rank += 1 + return rank + + +def compose(a, b): + return tuple(xor_all(b[j] for j in range(len(b)) if row >> j & 1) for row in a) + + +def address_alphabet(): + answer = [] + for i, j in product(range(3), repeat=2): + if i != j: + rows = [1, 2, 4] + rows[i] |= 1 << j + answer.append(tuple(rows)) + return answer + + +def scalar_projectors(): + return [rows for rows in product(range(4), repeat=2) + if dimension(rows, 2) == 1 and compose(rows, rows) == rows] + + +def canonical(state): + # Canonical index = 2*coordinate+register; native index = 3*register+coordinate. + permutation = [0, 3, 1, 4, 2, 5] + return sum(((state[permutation[i]] >> permutation[j]) & 1) << (6 * i + j) + for i in range(6) for j in range(6)) + + +def inverse(rows): + width = len(rows) + augmented = [row | (1 << (width + i)) for i, row in enumerate(rows)] + for column in range(width): + pivot = next(i for i in range(column, width) if augmented[i] >> column & 1) + augmented[column], augmented[pivot] = augmented[pivot], augmented[column] + for i in range(width): + if i != column and augmented[i] >> column & 1: + augmented[i] ^= augmented[column] + return tuple(row >> width for row in augmented) + + +def census(): + group = {g for g in product(range(8), repeat=3) if dimension(g, 3) == 3} + alphabet = address_alphabet() + identity = (1, 2, 4) + distance = {identity: 0} + frontier = [identity] + while frontier: + following = [] + for state in frontier: + for gate in alphabet: + changed = compose(state, gate) + if changed not in distance: + distance[changed] = distance[state] + 1 + following.append(changed) + frontier = following + if set(distance) != group or len(group) != 168: + raise ValueError("independent GL3 coverage failed") + matrices = [] + for gate in alphabet: + difference = tuple(x ^ y for x, y in zip(gate, identity)) + for projector in scalar_projectors(): + rows = [1 << i for i in range(6)] + for p, q, i in product(range(2), range(2), range(3)): + if projector[p] >> q & 1: + rows[3 * p + i] ^= difference[i] << (3 * q) + matrices.append(tuple(rows)) + if len(set(matrices)) != 36: + raise ValueError("independent generator count failed") + tables = [tuple(xor_all(g[j] for j in range(6) if row >> j & 1) + for row in range(64)) for g in matrices] + root = tuple(1 << i for i in range(6)) + layers = [{root}] + seen = {root} + for _ in range(4): + following = set() + for state in layers[-1]: + for table in tables: + changed = tuple(table[row] for row in state) + if changed not in seen: + following.add(changed) + seen.update(following) + layers.append(following) + # A separate meet test uses T*A^-1, instead of the producer's A*T^-1. + target = (2, 4, 7, 2 << 3, 4 << 3, 7 << 3) + short_ball = set().union(*layers[:4]) + meets = sum(compose(target, inverse(a)) in seen for a in short_ball) + return distance, [{canonical(s) for s in layer} for layer in layers], meets + + +def check_regular(word, target): + """Check all 2*168 basis vectors in the faithful left regular module.""" + group = [g for g in product(range(8), repeat=3) if dimension(g, 3) == 3] + count = 0 + for role, label in product(range(2), group): + state = [set(), set()] + state[role].add(label) + for i, j, u, v in word: + source = set() + for q in range(2): + if v >> q & 1: + source.symmetric_difference_update(state[q]) + gate = [1, 2, 4] + gate[i] ^= 1 << j + delta = source ^ {compose(gate, g) for g in source} + for p in range(2): + if u >> p & 1: + state[p].symmetric_difference_update(delta) + expected = [set(), set()] + expected[role].add(compose(target, label)) + if state != expected: + raise ValueError("faithful regular column differs") + count += 1 + return count diff --git a/research/gl3-order4-register-census/test_verify.py b/research/gl3-order4-register-census/test_verify.py new file mode 100644 index 0000000000..a79ee94599 --- /dev/null +++ b/research/gl3-order4-register-census/test_verify.py @@ -0,0 +1,102 @@ +#!/usr/bin/env python3 +"""Semantic and rejection tests; the registered verifier owns the full census.""" +import copy +import importlib.util +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("gl3_verify", HERE / "verify.py") +v = importlib.util.module_from_spec(spec) +spec.loader.exec_module(v) + + +class SemanticChecks(unittest.TestCase): + @classmethod + def setUpClass(cls): + cls.words = v.direct_census() + cls.formal = v.Formal(cls.words) + cls.witness = tuple((*v.PAIRS[gi], u, u) for u in (1, 2) for gi in cls.words[v.H]) + + def test_every_generator_and_pair_commutes_with_natural_map(self): + for first in v.GENERATORS: + expected_first = v.natural_step(v.I6, first) + self.assertEqual(self.formal.natural(self.formal.word([first])), expected_first) + self.assertEqual(v.natural_step(expected_first, first), v.I6) + for second in v.GENERATORS: + self.assertEqual(self.formal.natural(self.formal.word([first, second])), + v.natural_step(expected_first, second)) + + def test_scalar_conjugation_preserves_complete_alphabet(self): + independent = v.load_independent() + scalars = [(a, b) for a in range(4) for b in range(4) if v.rank((a, b)) == 2] + projectors = {tuple(vv if u >> i & 1 else 0 for i in range(2)) + for u, vv in v.IDEMPOTENTS} + self.assertEqual(projectors, set(independent.scalar_projectors())) + self.assertEqual(len(projectors), 6) + for b in scalars: + inverse = independent.inverse(b) + for n in projectors: + conjugate = v.multiply_rows(b, v.multiply_rows(n, inverse)) + self.assertIn(conjugate, projectors) + + def test_nonfaithful_alias_is_rejected_formally(self): + target = self.formal.target() + powers = [v.I3] + for _ in range(3): + powers.append(v.multiply_rows(v.H, powers[-1])) + alias = list(target) + alias[1] = sum(1 << self.formal.index[g] for g in powers) + self.assertNotEqual(tuple(alias), target) + self.assertEqual(self.formal.natural(tuple(alias)), self.formal.natural(target)) + self.assertEqual(alias[1].bit_count() % 2, 0) # augmentation does not detect it + + def test_regular_engine_rejects_wrong_chronology(self): + independent = v.load_independent() + self.assertEqual(independent.check_regular(self.witness, v.H), 336) + with self.assertRaisesRegex(ValueError, "regular column"): + independent.check_regular(tuple(reversed(self.witness)), v.H) + + def test_receipt_corruption_fails(self): + receipt = json.loads((HERE / "EXPECTED.json").read_text()) + for field in ("radius_three_four_target_meets", "paid_generator_count", "target_order"): + changed = copy.deepcopy(receipt) + changed[field] += 1 + with self.assertRaisesRegex(ValueError, "receipt mismatch"): + v.compare_receipt(receipt, changed) + + def test_source_corruption_fails(self): + with tempfile.TemporaryDirectory(dir=HERE.parent) as tmp: + root = Path(tmp) + package = root / "research" / "gl3-order4-register-census" + package.mkdir(parents=True) + shutil.copy(HERE / "SOURCES.json", package) + pins = json.loads((package / "SOURCES.json").read_text()) + for entry in pins["files"]: + if entry["usage"] == "input": + target = root / entry["path"] + target.parent.mkdir(parents=True, exist_ok=True) + target.write_text("incorrect source bytes\n") + with self.assertRaisesRegex(ValueError, "source SHA256 mismatch"): + v.source_checks(package) + + def test_optimized_cli_rejects_corrupt_receipt(self): + with tempfile.TemporaryDirectory(dir=HERE.parent) as tmp: + path = Path(tmp) / "wrong.json" + receipt = json.loads((HERE / "EXPECTED.json").read_text()) + receipt["claim"] = "FALSE_CLAIM" + path.write_text(json.dumps(receipt)) + run = subprocess.run([sys.executable, "-I", "-O", "-B", str(HERE / "verify.py"), + "--expected", str(path)], capture_output=True, text=True, + timeout=90) + self.assertNotEqual(run.returncode, 0) + self.assertIn("expected receipt mismatch", run.stderr) + + +if __name__ == "__main__": + unittest.main() diff --git a/research/gl3-order4-register-census/verify.py b/research/gl3-order4-register-census/verify.py new file mode 100644 index 0000000000..0b01d4fc3c --- /dev/null +++ b/research/gl3-order4-register-census/verify.py @@ -0,0 +1,365 @@ +#!/usr/bin/env python3 +"""Exact two-role GL3 order-four CNOT certificate. Standard library only.""" +from __future__ import annotations + +import argparse +from collections import Counter, deque +import hashlib +import importlib.util +import json +from pathlib import Path + +HERE = Path(__file__).resolve().parent +I3 = (1, 2, 4) +H = (2, 4, 7) +PAIRS = tuple((i, j) for i in range(3) for j in range(3) if i != j) +IDEMPOTENTS = tuple((u, v) for u in range(1, 4) for v in range(1, 4) + if (u & v).bit_count() % 2) +GENERATORS = tuple((i, j, u, v) for i, j in PAIRS for u, v in IDEMPOTENTS) +I6 = sum(1 << (7 * i) for i in range(6)) + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def rank(rows): + basis = {} + for value in rows: + while value: + pivot = value.bit_length() - 1 + if pivot in basis: + value ^= basis[pivot] + else: + basis[pivot] = value + break + return len(basis) + + +def multiply_rows(a, b): + result = [] + for row in a: + value = 0 + for j in range(len(b)): + if row >> j & 1: + value ^= b[j] + result.append(value) + return tuple(result) + + +def address_gate(i, j): + rows = list(I3) + rows[i] ^= 1 << j + return tuple(rows) + + +def direct_census(): + words = {I3: ()} + queue = deque([I3]) + while queue: + state = queue.popleft() + for gi, (i, j) in enumerate(PAIRS): + changed = list(state) + changed[i] ^= changed[j] + changed = tuple(changed) + if changed not in words: + words[changed] = words[state] + (gi,) + queue.append(changed) + return words + + +def strongly_connected(a): + for start in range(3): + reached = {start} + for _ in range(3): + reached |= {j for i in tuple(reached) for j in range(3) + if i != j and a[i] >> j & 1} + if len(reached) != 3: + return False + return True + + +def order(a): + value = I3 + for k in range(1, 169): + value = multiply_rows(a, value) + if value == I3: + return k + raise ValueError("noninvertible address matrix") + + +def target_matrix(h=H, active=(True, True)): + value = 0 + for i in range(3): + for p in range(2): + row = h[i] if active[p] else I3[i] + expanded = sum(1 << (2 * j + p) for j in range(3) if row >> j & 1) + value |= expanded << (6 * (2 * i + p)) + return value + + +def natural_step(state, generator): + i, j, u, v = generator + source = 0 + if v & 1: + source ^= (state >> (12 * j)) & 63 + if v & 2: + source ^= (state >> (12 * j + 6)) & 63 + if u & 1: + state ^= source << (12 * i) + if u & 2: + state ^= source << (12 * i + 6) + return state + + +def unpack(state): + return tuple((state >> (6 * i)) & 63 for i in range(6)) + + +def pack(rows): + return sum(row << (6 * i) for i, row in enumerate(rows)) + + +def multiply_natural(a, b): + return pack(multiply_rows(unpack(a), unpack(b))) + + +def natural_layers(depth=4, generators=GENERATORS): + seen = {I6} + layers = [{I6}] + attempts = 0 + for _ in range(depth): + following = set() + for state in layers[-1]: + for generator in generators: + attempts += 1 + changed = natural_step(state, generator) + if changed not in seen: + following.add(changed) + seen.update(following) + layers.append(following) + return layers, attempts + + +def state_hash(states): + digest = hashlib.sha256() + for state in sorted(states): + digest.update(state.to_bytes(5, "little")) + return digest.hexdigest() + + +def bounded_meets(layers, target_inverse, left_radius, right_radius): + left = set().union(*layers[:left_radius + 1]) + right = set().union(*layers[:right_radius + 1]) + return sum(multiply_natural(p, target_inverse) in right for p in left) + + +class Formal: + """Four coefficient bitsets in F2[GL3]; never a natural-image oracle.""" + + def __init__(self, group): + self.group = tuple(sorted(group)) + self.index = {g: i for i, g in enumerate(self.group)} + self.one = 1 << self.index[I3] + self.permutations = { + (i, j): tuple(self.index[multiply_rows(address_gate(i, j), g)] + for g in self.group) for i, j in PAIRS + } + + def translate(self, coefficients, pair): + result = 0 + permutation = self.permutations[pair] + while coefficients: + low = coefficients & -coefficients + result ^= 1 << permutation[low.bit_length() - 1] + coefficients ^= low + return result + + def step(self, state, generator): + i, j, u, v = generator + result = list(state) + for column in range(2): + source = 0 + for q in range(2): + if v >> q & 1: + source ^= state[2 * q + column] + delta = source ^ self.translate(source, (i, j)) + for p in range(2): + if u >> p & 1: + result[2 * p + column] ^= delta + return tuple(result) + + def word(self, word, check_alphabet=True): + state = (self.one, 0, 0, self.one) + for generator in word: + if check_alphabet: + require(generator in GENERATORS, "illegal paid generator") + state = self.step(state, generator) + return state + + def target(self, h=H): + label = 1 << self.index[h] + return (label, 0, 0, label) + + def natural(self, state): + rows = [0] * 6 + for p in range(2): + for q in range(2): + coefficient = state[2 * p + q] + for gi, g in enumerate(self.group): + if coefficient >> gi & 1: + for i in range(3): + for j in range(3): + if g[i] >> j & 1: + rows[2 * i + p] ^= 1 << (2 * j + q) + return pack(rows) + + +def source_checks(package=HERE): + pins = json.loads((package / "SOURCES.json").read_text()) + root = package.parents[1] + count = 0 + for entry in pins["files"]: + if entry["usage"] == "input": + actual = hashlib.sha256((root / entry["path"]).read_bytes()).hexdigest() + require(actual == entry["sha256"], "source SHA256 mismatch: " + entry["path"]) + count += 1 + return count + + +def load_independent(): + spec = importlib.util.spec_from_file_location("gl3_independent", HERE / "independent.py") + module = importlib.util.module_from_spec(spec) + spec.loader.exec_module(module) + return module + + +def controls(formal, witness, layers): + passed = [] + target = formal.target() + for i in range(len(witness)): + require(formal.word(witness[:i] + witness[i + 1:]) != target, + "omitted-call control accepted") + passed.append("omit-call-" + str(i)) + changed = list(witness) + i, j, u, v = changed[0] + changed[0] = (j, i, u, v) + require(formal.word(changed) != target, "reversed-CNOT control accepted") + passed.append("reverse-CNOT-direction") + require(formal.word(tuple(reversed(witness))) != target, "inverse-target control accepted") + passed.append("reverse-chronology") + wrong = list(target) + wrong[1] = formal.one + require(formal.natural(tuple(wrong)) != target_matrix(), "cross-role leakage accepted") + passed.append("cross-role-dirty-input-leakage") + powers = [I3] + for _ in range(3): + powers.append(multiply_rows(H, powers[-1])) + kernel = sum(1 << formal.index[g] for g in powers) + wrong = list(target) + wrong[1] ^= kernel + require(tuple(wrong) != target and formal.natural(tuple(wrong)) == target_matrix(), + "nonfaithful-image control failed") + require(kernel.bit_count() == 4, "kernel unexpectedly zero") + passed.append("natural-image-is-not-formal-equality") + widened = (formal.one, 0, 0, formal.one) + for i, j, _, _ in witness[:4]: + widened = formal.step(widened, (i, j, 1, 1)) + widened = formal.step(widened, (i, j, 2, 2)) + require(widened == target, "rank-two-scope control failed") + passed.append("rank-two-projector-underpricing") + invalid = (0, 1, 1, 2) + try: + formal.word([invalid]) + except ValueError: + passed.append("nonidempotent-paid-generator") + else: + raise ValueError("nonidempotent generator accepted") + half = formal.word(witness[:4]) + require(half[0] == target[0] and half[3] != target[3], "second-role control failed") + passed.append("only-one-role-completed") + require(bounded_meets(layers, I6, 0, 0) == 1, "identity positive control failed") + single = target_matrix(active=(True, False)) + single_inverse = target_matrix(multiply_rows(H, multiply_rows(H, H)), (True, False)) + require(bounded_meets(layers, single_inverse, 1, 2) == 0, + "single-role length-three exclusion failed") + require(bounded_meets(layers, single_inverse, 2, 2) > 0, + "single-role length-four positive control failed") + require(formal.natural(half) == single, "single-role formal/natural mismatch") + return passed, {"identity_minimum": 0, "single_role_minimum": 4, + "kernel_group_elements_rows": [list(g) for g in powers]} + + +def certificate(): + inputs = source_checks() + words = direct_census() + require(len(words) == 168, "GL3 coverage mismatch") + require(len(words[H]) == 4 and order(H) == 4, "target length/order mismatch") + require(rank(tuple(a ^ b for a, b in zip(H, I3))) == 2, "rank-gap mismatch") + candidates = sorted(g for g, w in words.items() if len(w) == 4 and order(g) == 4 + and rank(tuple(a ^ b for a, b in zip(g, I3))) == 2 + and strongly_connected(g)) + require(candidates[0] == H, "target selection rule mismatch") + witness = tuple((*PAIRS[gi], u, u) for u in (1, 2) for gi in words[H]) + formal = Formal(words) + require(formal.word(witness) == formal.target(), "formal upper witness failed") + independent = load_independent() + independent_words, independent_layers, independent_meets = independent.census() + require({g: len(w) for g, w in words.items()} == independent_words, + "independent direct distances differ") + layers, attempts = natural_layers() + require(layers == independent_layers, "independent full layer sets differ") + inverse = multiply_rows(H, multiply_rows(H, H)) + meets = bounded_meets(layers, target_matrix(inverse), 3, 4) + require(meets == 0, "short natural word exists: full formal follow-up required") + require(independent_meets == meets, "independent meet test differs") + regular_columns = independent.check_regular(witness, H) + control_names, fixtures = controls(formal, witness, layers) + return { + "schema_version": 1, + "claim": "FINITE_MINIMUM_EIGHT_EXACTLY_TWO_REGISTERS", + "target_rows": list(H), "target_order": 4, "target_displacement_rank": 2, + "address_group_size": len(words), + "address_distance_layers": [Counter(map(len, words.values()))[i] for i in range(7)], + "direct_word_chronological": [list(PAIRS[gi]) for gi in words[H]], + "formal_witness_chronological": [list(g) for g in witness], + "scalar_idempotents": [list(n) for n in IDEMPOTENTS], + "paid_generator_count": len(GENERATORS), + "natural_distance_layers": [len(layer) for layer in layers], + "natural_layer_sha256": [state_hash(layer) for layer in layers], + "directed_transition_attempts": attempts, + "radius_three_size": sum(map(len, layers[:4])), + "radius_four_size": sum(map(len, layers)), + "radius_three_four_target_meets": meets, + "independent_full_layer_comparison": True, + "independent_target_meets": independent_meets, + "faithful_regular_basis_columns": regular_columns, + "positive_fixtures": fixtures, "controls": control_names, + "live_source_hashes_checked": inputs, + "not_checked": ["extra scalar registers", "physical supplier realization", + "compiler/hosting/precision/tape/analytic transfer", "Lean proof"], + } + + +def compare_receipt(actual, expected): + require(actual == expected, "expected receipt mismatch") + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--emit", action="store_true", help="compute JSON without comparing EXPECTED.json") + parser.add_argument("--expected", type=Path, default=HERE / "EXPECTED.json") + args = parser.parse_args() + actual = certificate() + if args.emit: + print(json.dumps(actual, indent=2, sort_keys=True)) + else: + compare_receipt(actual, json.loads(args.expected.read_text())) + print("PASS_GL3_ORDER4_REGISTER_CENSUS minimum=8 registers=2 address_group=168 " + "direct_length=4 natural_short_words=0 regular_columns=336 " + f"controls={len(actual['controls'])} no_new_kappa") + + +if __name__ == "__main__": + main()