From 5938ce3e91bbb8b5c2227af7976d444b2fbac7d4 Mon Sep 17 00:00:00 2001 From: Adam Gall Date: Wed, 14 Oct 2026 10:31:38 -0400 Subject: [PATCH] Prove sharp even finite-dihedral tariffs with dirty workspace --- research/finite-dihedral-cut-bound/README.md | 286 ++++++++++ .../finite-dihedral-cut-bound/RECEIPT.json | 49 ++ .../finite-dihedral-cut-bound/SELECTION.json | 60 ++ .../finite-dihedral-cut-bound/SOURCES.json | 30 + research/finite-dihedral-cut-bound/TASK.json | 79 +++ .../finite-dihedral-cut-bound/VALIDATION.json | 50 ++ .../finite-dihedral-cut-bound/VERIFY.json | 23 + research/finite-dihedral-cut-bound/verify.py | 535 ++++++++++++++++++ 8 files changed, 1112 insertions(+) create mode 100644 research/finite-dihedral-cut-bound/README.md create mode 100644 research/finite-dihedral-cut-bound/RECEIPT.json create mode 100644 research/finite-dihedral-cut-bound/SELECTION.json create mode 100644 research/finite-dihedral-cut-bound/SOURCES.json create mode 100644 research/finite-dihedral-cut-bound/TASK.json create mode 100644 research/finite-dihedral-cut-bound/VALIDATION.json create mode 100644 research/finite-dihedral-cut-bound/VERIFY.json create mode 100755 research/finite-dihedral-cut-bound/verify.py diff --git a/research/finite-dihedral-cut-bound/README.md b/research/finite-dihedral-cut-bound/README.md new file mode 100644 index 0000000000..7ef17c9f10 --- /dev/null +++ b/research/finite-dihedral-cut-bound/README.md @@ -0,0 +1,286 @@ +# Even finite dihedral groups: sharp reflection tariffs from address cuts + +**Scoped all-register theorem; no new kappa.** Put +`G = D_{2n} = `, where the rotation period +`n=2m` is even, and set `y=r^-1 x`, so `r=xy`. For any finite number +`R>=W` of arbitrary-input scalar registers, the complete formal endpoint + +``` +diag([r^k_1 x^e_1], ..., [r^k_W x^e_W], 1, ..., 1) +``` + +in `M_R(F2[G])` has the exact separate paid-call bills + +``` +A = sum_i d_n(k_i+e_i) x calls +B = sum_i d_n(k_i) y calls, +d_n(t) = min(t mod n, n-(t mod n)), e_i in {0,1}. +``` + +Both minima are attained **simultaneously**. Thus any nonnegative per-letter +prices `alpha,beta` give the sharp total `alpha*A+beta*B`. No scalar mixing, +interleaving, or extra restored dirty workspace can lower that bill. +For example, the D16 central pair costs 8 x calls and 8 y calls for **every** +workspace count, not just the two-register census of PR1821. + +This answers the finite-torsion question left explicitly open by +[PR1911](https://github.com/CrocSwap/integer-mult-bounds/pull/1911). +Its infinite-dihedral Laurent-degree proof does not descend through `r^n=1`. +The new proof uses two finite permutation representations and a cut rank, +which does survive that relation. It is not an enlarged finite word search. +D8 central targets with arbitrary workspace were already settled by PR1573; +that overlapping special case is credited, not claimed anew. + +## Exact model and fully paid boundary + +The only paid address labels are x and y. A unit call is +`D_N(g)=I+([g]+1)N`, with `N=u v^T` over F2 and `v^T u=1`. +All binary rank-one idempotents are allowed, not only coordinate projectors. +Free scalar `GL_R(F2)` changes may occur anywhere. They do not change address +coordinates. There are no other free address maps, resets, erasures, COPYs or +clean inputs. Every input, including every workspace input, is arbitrary; +the full boundary restores each spectator and has no residual couplings. +Every paid preparation/restoration call is counted. + +This replaces the rational abelian address group in the retained three-register +model by an explicitly nonabelian finite group (abelian only at the degenerate +boundary n=2). It does not reduce rational frame entries modulo two. Scalar +mixing is granted free as an **optimistic relaxation**, not asserted free in a +physical supplier. No physical compiler, hosting, frame, precision/tape or +analytic bridge is provided. Those adoption obligations remain unestablished. + +## Uniform lower-bound proof + +### 1. A subadditive crossing rank + +Split a finite vector space into address halves H and K, including all scalar +roles in each half. For any linear operator M, let `q(M)=rank_F2 M[H,K]`. +Block multiplication gives + +``` +(AB)[H,K] = A[H,H] B[H,K] + A[H,K] B[K,K], +q(AB) <= q(A)+q(B). +``` + +No invertibility is needed for this inequality. A scalar register map acts +independently at each address, so its crossing block is zero. Invertible scalar +changes, even interleaved, therefore contribute zero to the bound. + +### 2. Two different valid representations, including n=2 mod 4 + +For **each** integer c, represent G on addresses `a in Z/nZ` by + +``` +rho_c(r)(a) = a+1, +rho_c(x)(a) = c-a, +rho_c(y)(a) = c-1-a. +``` + +Both reflections square to the identity; their product x after y is `a+1`; +that translation has order n; and x conjugates it to its inverse. These are +therefore representations of the actual finite presentation. Extend them +linearly to F2[G] and entrywise to register matrices. + +Use the balanced interval `H={0,...,m-1}`, `K={m,...,2m-1}`. For an interval +translated by t on this 2m-cycle, + +``` +| (H+t) intersect K | = d_n(t). (1) +``` + +For residues `0<=t<=m` precisely t points cross; replace t by `n-t` for the +other half of the residues. This proves (1) for all integers, not by sampling. + +Take two representations: + +* `c=m`: y preserves H, while x sends H to H+1. Thus y has no crossing + entries and x has exactly one entry in each directed crossing block. +* `c=m-1`: x preserves H, while y sends H to H-1. Thus x has no crossing + entries and y has exactly one. + +The reflection offset **must change between the representations**. In +particular this handles n=6,10,...: we do not assume the fixed-point-free +reflection `a -> -a-1` preserves an odd-cardinality half. The verifier includes +n=2,6,10 and rejects that incorrect fixed-offset shortcut. + +For arbitrary N, the crossing block of a represented paid factor is +`N tensor E`, where E is the indicated address crossing block; the identity +part contributes zero. Hence its rank is exactly `rank(N)` for the active +letter and zero for the other. In the rank-one model the two call charges are +therefore `(q_m(x),q_m(y))=(1,0)` and +`(q_(m-1)(x),q_(m-1)(y))=(0,1)`. This is why the argument includes every +non-coordinate scalar projector and any number of dirty roles. + +### 3. Exact endpoint crossing ranks + +A target `r^k` translates H by k. A target `r^k x` maps H to the interval + +``` +H + (k+c-m+1). +``` + +A permutation's crossing submatrix has one 1 in each participating row and +column; its rank equals its number of crossing addresses. By (1), the target's +crossing ranks in the two representations are + +``` +c=m: d_n(k+e), +c=m-1: d_n(k). +``` + +The endpoint is diagonal in scalar roles. Its crossing blocks are direct sums, +so ranks add over roles; identity spectators contribute zero. Subadditivity +now yields `#x>=A` and `#y>=B` for every finite R and every word length. +Formal equality implies represented equality; we never use the converse. +Indeed a negative control below explicitly demonstrates the common kernel of +these proof representations. + +The same reasoning also bounds **total scalar rank** per label if paid calls +are allowed arbitrary-rank idempotents: x rank mass is at least A and y rank +mass at least B. This is a rank-linear corollary, not a sharp invocation-count +claim for batched calls or a statement about recursive child-rank pricing. + +## Uniform attaining identity and complete invoice + +Choose the representative `k' in [-m,m-1]` of each k. For a rotation, freely +reduce `(xy)^k'`; for a reflection, freely reduce `(xy)^k' x`. Negative powers +mean repetitions of yx. The resulting letter counts are + +``` +x: |k'+e| = d_n(k+e), y: |k'| = d_n(k). +``` + +For e=1 the interval `-m<=k'<=m-1` is precisely what ensures both equalities; +this simultaneous choice is not automatic for odd n. + +On role i use its coordinate projector E_i. Direct multiplication in the full +formal group algebra gives +`D_E(g) D_E(h) = D_E(gh)`, and calls on different coordinate roles commute. +Consequently the above literal words attain the complete diagonal boundary. +The rightmost factor acts first; the implementation executes each displayed +word right-to-left. No finite representation is used to certify this identity. + +| Resource | Complete attaining implementation | +|---|---| +| Target roles | W, arbitrary dirty inputs | +| Extra dirty roles | Arbitrarily many allowed; zero needed | +| x / y paid calls | A / B, including all endpoint work | +| Scalar basis changes | Zero needed by attaining word | +| Clean allocations, COPYs, resets | None | +| Extra restoration, free frame/address changes | None in this formal implementation | +| Native supplier / physical realization | Not supplied or priced as free | + +On any concrete n-address action `rho_c`, each reflection can be implemented +by disjoint swaps. For even n a reflection `a -> c-a` has two fixed addresses +if c is even and none if c is odd. Thus x uses `(n-2)/2` or `n/2` swaps per +call, and y has the opposite parity. A three-XOR swap needs no clean data bit; +this gives an explicit implementation of the witness, not an optimal physical +algorithm or an admitted recursive supplier tariff. Free scalar mixing in the +lower-bound relaxation only strengthens the no-compression result. + +## Exact executable evidence and reproduction + +``` +uv run --python 3.12 --no-project python -I -B research/finite-dihedral-cut-bound/verify.py +uv run --python 3.12 --no-project python scripts/research_package.py --package research/finite-dihedral-cut-bound +``` + +The verifier is standard-library-only. It distinguishes three engines: + +1. Full formal F2[G] coefficient multiplication using dihedral normal forms. +2. Independently applied literal permutations on the **faithful regular** 2n + addresses, including every dirty basis column and non-coordinate calls. +3. The two n-address proof representations, with binary Gaussian elimination + of their actual crossing submatrices rather than substituting the theorem's + claimed rank formula. + +Finite checks corroborate implementations; the universal result is the written +proof above. The proof is not Lean-checked and no independent human review is +claimed. The retained source-binding working example is orientation only, not +selected cold replay. See the generated receipt and validation record for +actually executed domains, counters and environment. + +Observed on macOS arm64, CPython **3.12.12**: the direct isolated replay and +registered optimized replay both passed. The receipt records **1,027** complete +forward/inverse dirty fixtures, **134,864** regular basis columns, **9,420** +mixed words, **47,872** representation-product checks, **3,720** rank-one call +cut checks over all **155** projectors through four roles, and **348** checks +over all **174** invertible scalar maps through three roles. All **9,249** +single-call omissions and **13** additional semantic/model controls reject. +A deliberately incomplete receipt also rejects under `-O` with +`receipt differs from exact recomputation`. Exact commands and environment are +in [VALIDATION.json](VALIDATION.json); the repeatable counts and digest are in +[RECEIPT.json](RECEIPT.json). No native, hosted CI or selected cold replay was run. + +Controls include omitted paid calls, wrong letter/order, residual dirty +workspace, illegal projectors/labels, odd-period simultaneous-attainment failure, +and the wrong parity-insensitive reflection offset. An invertible off-diagonal +perturbation by `Omega=sum_{g in G}[g]` is invisible in **both** n-point proof +representations: each permutation coefficient there occurs twice. It remains +nonzero in the formal algebra and faithful regular action and is rejected by +the endpoint verifier. Thus represented lower-bound checks are not mistakenly +used as sufficient endpoint certificates. + +## Provenance, overlap and credit + +Base `0b1cccf86e2f5132ed286a26ef0a681a495740ea`; independent OS nonce +`63537661f5ee8acaa486b70f82726911`, track `bit-mechanisms`, emitted card +`bit-new-register-model`, method target-specific relaxation. Complete chooser +output is retained in `SELECTION.json`; original source byte/blob pins and +catalogue/selected-record provenance are in `SOURCES.json`. The selected record +remains unchanged at SHA256 +`10b9e340fd8e354a37a0c4813c90e5de1dd42044b5f6aca4a3fc5a42b685fa32`. + +Closest inspected live predecessors: + +* Adam Gall, [PR1911](https://github.com/CrocSwap/integer-mult-bounds/pull/1911), + head `712593f82739203639d0a169b88c6bcac6f0590c`: infinite-dihedral sharp + tariffs and the precise finite-torsion open question. No source code copied. +* Cinna Davis, [PR1821](https://github.com/CrocSwap/integer-mult-bounds/pull/1821), + head `a986127fa82b680a5bbb29f49fec4c8c3a944bde`: D16 central pair at R=2. + The present result replaces that bounded-register gap with a uniform proof. +* steph4n-gh, [PR1573](https://github.com/CrocSwap/integer-mult-bounds/pull/1573), + head `0b8c5a69297c794f2de22c04494c83e41300ae36`: arbitrary-register D8 + central targets and separate tariffs, already established. The natural + representation/zero-projector-sum argument is a predecessor, not this proof. +* Arham Tahir, [PR1919](https://github.com/CrocSwap/integer-mult-bounds/pull/1919), + head `f5610483cab0b5547be778a4e8983faf78aefa69`: rank-bounded D8 central + block calls and their invocation optimum. We do not claim that optimum. +* [PR1792](https://github.com/CrocSwap/integer-mult-bounds/pull/1792), head + `cc3a4adbae23fb07687803d1361bb7a1bcd449b0`: D8/UT3 scope audit identifying + the already-completed arbitrary-workspace result and the danger of stale + next-question text. Its navigation warning is respected here. +* woklerx, retained PR1443 D8 census; eumemic PR288 register model; + Ali Romman PR468 three-register obstruction; Gareth Davidson PR1333 + nonabelian affine direction; their attribution remains unchanged. + +Initial shared overlap snapshot: 579 open PRs and 547 discussion records, +completely paginated at 2026-10-14T14:10:13Z / 14:11:43Z. The final offline +recheck at 14:30:45Z used the refreshed **584 open PRs** (14:27:47Z) and +**565 discussion records** including comments/replies (14:29:09Z), both +complete. The only new exact dihedral/cut matches were this package and this +round's own claims. Targeted live predecessor heads were unchanged. A live +all-state dihedral PR search and local README/ledger search also included the +merged PR1443 predecessor and the PR1792 D8 scope audit. + +The helper's closed-PR coverage remains only local notes and the ledger; +arbitrary code diffs are not searched, and cached records may miss live changes. +No-match results are not novelty certificates. The mathematical change is +finite torsion and a new balanced-cut invariant, not the seed or a larger census. +[Precise pre-computation claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/1929#discussioncomment-18925900). + +Prepared for **Adam Gall** with substantial **OpenAI Codex GPT-6 Astra** +assistance in proof, implementation, verification and writing. All engines were +written in the same AI-assisted investigation; algorithmic independence is not +independent human authorship. Apache-2.0. No supplier, frontier or kappa change. + +## Open next questions + +1. **Odd periods.** The even half-interval proof and simultaneous choice of + representatives do not automatically extend. At n=3 the farthest reflection + has separate cyclic distances (1,1) but no word with those counts. Determine + the missing joint tariff constraint before attempting an odd-period theorem. +2. **Physical admission.** Specify and fully price an all-size native reflection + child, including frame/compiler, hosting, restoration, precision and tape. + Until such a bridge exists, even the exact formal theorem is only a + mechanism-screening side result, not an exponent result. diff --git a/research/finite-dihedral-cut-bound/RECEIPT.json b/research/finite-dihedral-cut-bound/RECEIPT.json new file mode 100644 index 0000000000..4f24435fe5 --- /dev/null +++ b/research/finite-dihedral-cut-bound/RECEIPT.json @@ -0,0 +1,49 @@ +{ + "counts": { + "all_rank_call_cut_checks": 1088, + "all_rank_idempotents": 68, + "formal_dirty_fixtures": 1027, + "free_scalar_cut_checks": 348, + "free_scalar_invertible_maps": 174, + "mixed_words_through_three": 9420, + "omission_controls": 9249, + "rank_one_call_cut_checks": 3720, + "rank_one_projectors": 155, + "regular_dirty_columns_forward_and_inverse": 134864, + "representation_products": 47872, + "target_cut_ranks": 1088, + "word_cut_inequalities": 18840 + }, + "deterministic_evidence_sha256": "68d1e74610dd053ba77dffa515c554e9b056f6a9e63e644768702e695a3ffc5c", + "finite_domains": { + "all_idempotent_periods": [2, 4, 6, 10], + "all_idempotent_roles": [1, 2, 3], + "all_ordered_target_pair_periods": [2, 4, 6, 8], + "even_periods_all_targets": [2, 4, 6, 8, 10, 12, 14, 16, 18, 20, 22, 24, 26, 28, 30, 32], + "free_scalar_roles": [2, 3], + "free_scalar_period": 6, + "mixed_word_max_length": 3, + "mixed_word_periods": [2, 4, 6, 8, 10], + "rank_one_call_periods": [2, 4, 6, 8, 10, 16], + "rank_one_projector_roles": [1, 2, 3, 4] + }, + "negative_controls": [ + "odd_period_scope", + "non_idempotent_projector", + "rank_two_undercharged_projector", + "unpaid_rotation_label", + "missing_role", + "odd_separate_minima_not_jointly_attainable", + "fixed_offset_shortcut_n6", + "fixed_offset_shortcut_n10", + "wrong_paid_label", + "wrong_execution_order", + "dirty_workspace_not_restored", + "nonfaithful_endpoint_false_positive", + "direct_rotation_not_unit_tariff" + ], + "no_new_kappa": true, + "result": "PASS_FINITE_DIHEDRAL_CUT_BOUND", + "schema_version": 1, + "theorem_scope": "all even n>=2, all target counts, every finite dirty workspace; written proof" +} diff --git a/research/finite-dihedral-cut-bound/SELECTION.json b/research/finite-dihedral-cut-bound/SELECTION.json new file mode 100644 index 0000000000..aa3b495b34 --- /dev/null +++ b/research/finite-dihedral-cut-bound/SELECTION.json @@ -0,0 +1,60 @@ +{ + "seed": "63537661f5ee8acaa486b70f82726911", + "track": "bit-mechanisms", + "suggestions": [ + { + "task_id": "bit-helper-contract", + "scope_key": "bfb61f829a81535adeae", + "question": "Can one precisely specified helper-mixing word satisfy a replacement for the inherited H2/K interface?", + "method": "Seek an exact dirty-input or chronological-cut counterexample to the proposed replacement.", + "starting_points": ["research/r439-bsection-stars-seed01/README.md", "research/r439-copy-path-sharing-barrier/README.md"], + "acceptance_gate": "A full boundary contract and paid profile; unchanged scalar counts alone are insufficient.", + "first_step": { + "command": ["python3", "-B", "research/r439-bsection-stars-seed01/verify.py"], + "expected": "PASS_R439_BSECTION_STARS", + "inspect": "Compare the two false H2/K flags with the unchanged paid profile in its README.", + "scope": "Positive control / source-bound orientation only; this is not a new construction or full cold replay." + }, + "first_experiment": "Write one replacement H2/K implication for a single helper-star operation, then try to falsify it on dirty inputs.", + "bottleneck_link": "A legitimate replacement could admit a cheaper bit circuit; scalar savings alone do not alter the selected moment.", + "allowed_variations": ["Choose one helper-star or quartet instance; narrow to one boundary implication."], + "scope_change_triggers": ["Changing only source count or scalar addition count without an interface argument."], + "overlap_terms": ["H2_D_frame0_targets_from_helpers", "K_equals_D", "helper-star"], + "scope_rule": "If you change the card's premise, record scope_status=changed and explain why. A package metadata check cannot establish mathematical relevance." + }, + { + "task_id": "bit-new-register-model", + "scope_key": "7084092dd726e7ba1f2f", + "question": "Can an explicitly larger or nonabelian register model escape the scoped three-register obstruction?", + "method": "Derive a target-specific relaxation bound for that same explicit alphabet.", + "starting_points": ["research/bit-three-register-lower-bound/README.md", "certificates/selected-result.json"], + "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_rule": "If you change the card's premise, record scope_status=changed and explain why. A package metadata check cannot establish mathematical relevance." + } + ], + "base_commit": "0b1cccf86e2f5132ed286a26ef0a681a495740ea", + "catalog_assessed_on": "2026-10-13", + "priority_revision": 3, + "priority_log": "docs/research/research-priority-log.md", + "catalog_sha256": "6686ad58f1fbdbc87134a78901b60fd53a20d3984355e91defbbebc9e9fa8075", + "selected_record_sha256": "10b9e340fd8e354a37a0c4813c90e5de1dd42044b5f6aca4a3fc5a42b685fa32", + "selected": { + "kappa": "836330098538459/500000000000000000", + "review": "docs/research/community-batch1099-review.md", + "source_manifest": "research/community-frontier1094-audit/SELECTED-SOURCE.json", + "reproduce": "make frontier1094-verify" + }, + "status": "SUGGESTIONS_ONLY_NOT_RESERVED", + "next_step": "Check live overlap, refine one question's object and domain, and record a bounded task card. A different seed or scope key is not evidence of novelty." +} diff --git a/research/finite-dihedral-cut-bound/SOURCES.json b/research/finite-dihedral-cut-bound/SOURCES.json new file mode 100644 index 0000000000..484d40c500 --- /dev/null +++ b/research/finite-dihedral-cut-bound/SOURCES.json @@ -0,0 +1,30 @@ +{ + "schema_version": 1, + "base_commit": "0b1cccf86e2f5132ed286a26ef0a681a495740ea", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "ae6a99f28aa468649eb66a361e764d769363bf11", + "sha256": "10b9e340fd8e354a37a0c4813c90e5de1dd42044b5f6aca4a3fc5a42b685fa32" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "06c96f5579bb67ed1b86d334e78fbed7da6945f1", + "sha256": "6686ad58f1fbdbc87134a78901b60fd53a20d3984355e91defbbebc9e9fa8075" + }, + { + "path": "research/bit-dihedral-commutator/README.md", + "usage": "input", + "git_blob": "b7619a5d56f32daf7f48d6cc3a0e260c5a333510", + "sha256": "4f3f9df6d6d96a26ccb0fcd2ef947cce5d53b0d992da22e866f1e025be4c0492" + }, + { + "path": "research/bit-three-register-lower-bound/README.md", + "usage": "input", + "git_blob": "25e41c370c101a33a6deb978de08b03ed7539b79", + "sha256": "c12b33ef388deece0cbf891505a2ce2c0779a0c3a6cf1f0f7f7039bab59cbebd" + } + ] +} diff --git a/research/finite-dihedral-cut-bound/TASK.json b/research/finite-dihedral-cut-bound/TASK.json new file mode 100644 index 0000000000..6adacd48cc --- /dev/null +++ b/research/finite-dihedral-cut-bound/TASK.json @@ -0,0 +1,79 @@ +{ + "schema_version": 1, + "task_id": "bit-new-register-model", + "priority_revision": 3, + "base_commit": "0b1cccf86e2f5132ed286a26ef0a681a495740ea", + "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": "For every even rotation period n, exact formal F2[D_{2n}] diagonal targets r^k_i x^e_i with only paid reflections x,y, arbitrary binary rank-one idempotents, free scalar mixing, and arbitrary finite restored dirty workspace: determine the sharp separate letter tariffs by balanced address-cut rank.", + "scope_change_reason": "Instantiate the emitted nonabelian-family variation with even finite dihedral groups, changing the abelian rational address premise and closing PR1911's explicit torsion-aware lower-bound question. Unlike another finite register census, the proposed theorem covers all word lengths, even periods, heterogeneous targets and dirty-workspace counts.", + "bottleneck_link": "A formal-model side result screening a nonabelian sharing route before physical synthesis. Even granting free scalar mixing and arbitrary dirty workspace, a sharp direct-word floor rules out local compression in this alphabet. No selected supplier or kappa improvement follows.", + "budget_minutes": 120, + "stop_rule": "Prove the two valid finite-group representations, exact per-call cut ranks, crossing-rank subadditivity, and simultaneous formal attainability before accepting the theorem. Corroborate n=2,6,10 parity boundaries and every target for even n through 32; stop this fixed question after complete proof and bounded controls, without expanding a failed search.", + "outcome": "completed", + "evidence": "Written torsion-aware cut-rank theorem with simultaneous full-formal attaining words. Exact research run: 47,872 representation products, 1,088 target cut ranks, 155 rank-one projectors, 1,027 forward/inverse dirty fixtures, 134,864 faithful regular basis columns, 9,420 complete short mixed words, 9,249 omission controls and 13 additional scope/semantic controls. Reproduce via VERIFY.json; final exercised commands and environment are in VALIDATION.json.", + "author": "Adam Gall, with substantial OpenAI Codex assistance", + "ai_assistance": "OpenAI Codex GPT-6 Astra assisted research, proof, implementation and writing; no independent human or proof-assistant verification is implied.", + "selection_seed": "63537661f5ee8acaa486b70f82726911", + "selection_track": "bit-mechanisms", + "selection_scope_key": "7084092dd726e7ba1f2f", + "refined_scope_key": "7084092dd726e7ba1f2f/even-finite-dihedral/all-dirty-registers/balanced-address-cut-rank", + "claim_url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1929#discussioncomment-18925900", + "optimistic_full_budget": "For target r^k x^e, d_n(k+e) x calls and d_n(k) y calls, summed over all target roles; scalar mixing granted free, all workspace dirty and fully restored. Attaining coordinate word needs no workspace, COPY, free address relabeling, or uncharged restoration. Physical compiler/hosting/tape costs remain unestablished, not zero.", + "falsification": "Any invalid presentation relation, non-coordinate projector whose active cut rank exceeds one, target crossing-rank mismatch, subadditivity failure, or wrong formal boundary falsifies the claimed derivation.", + "predecessors": [ + {"pr": 1911, "head": "712593f82739203639d0a169b88c6bcac6f0590c", "credit": "Adam Gall; infinite-dihedral Laurent-minor theorem and explicit finite-torsion open question, not reused as a finite-group proof"}, + {"pr": 1821, "head": "a986127fa82b680a5bbb29f49fec4c8c3a944bde", "credit": "Cinna Davis; exact D16 central-pair minimum at two scalar roles"}, + {"pr": 1573, "head": "0b8c5a69297c794f2de22c04494c83e41300ae36", "credit": "steph4n-gh; arbitrary-register D8 central-target sharp tariffs, already established and not claimed anew"}, + {"pr": 1919, "head": "f5610483cab0b5547be778a4e8983faf78aefa69", "credit": "Arham Tahir; rank-bounded D8 central block-call invocation and rank tariffs, distinct from the even-period rank-one theorem"} + ], + "open_questions": [ + { + "question": "For odd rotation periods, what joint tariff constraint replaces simultaneous attainment of the two cyclic-distance bounds?", + "why_it_matters": "The balanced even cut and simultaneous shortest representatives do not extend automatically; n=3 already gives incompatible separate minima for the farthest reflection.", + "first_step": "Analyze the odd-period farthest-reflection endpoint with a justified necessary invariant beyond the two individual cyclic distances.", + "blocked_by": "The present proof is even-period only; no odd-period lower-bound theorem is asserted." + }, + { + "question": "Can either paid reflection be realized as a legal native bit-supplier child at a useful full cost?", + "why_it_matters": "Formal call counts alone do not establish recursive moment or kappa changes.", + "first_step": "Specify an all-size physical frame/compiler implementation and charge hosting, preparation, restoration, precision and tape.", + "blocked_by": "No such supplier interface is supplied here; this remains a formal-model obstruction." + } + ] +} diff --git a/research/finite-dihedral-cut-bound/VALIDATION.json b/research/finite-dihedral-cut-bound/VALIDATION.json new file mode 100644 index 0000000000..9c796c33b9 --- /dev/null +++ b/research/finite-dihedral-cut-bound/VALIDATION.json @@ -0,0 +1,50 @@ +{ + "schema_version": 1, + "observed_on": "2026-10-14", + "environment_observed_at": "2026-10-14T14:29:41.467209+00:00", + "environment": { + "python": "3.12.12 (main, Jan 14 2026, 23:36:32) [Clang 21.1.4 ]", + "platform": "macOS-27.0.1-arm64-arm-64bit", + "machine": "arm64", + "dependencies": "Python standard library only; invoked through uv with --python 3.12 --no-project" + }, + "research_orientation": { + "command": "uv run --python 3.12 --no-project python -B scripts/research_baseline.py", + "result": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "scope": "Source bindings and retained arithmetic, not selected cold replay; complex supplier binds." + }, + "exact_research_experiment": { + "command": "uv run --python 3.12 --no-project python -I -B research/finite-dihedral-cut-bound/verify.py --emit", + "result": "PASS_FINITE_DIHEDRAL_CUT_BOUND; complete deterministic certificate emitted", + "scope": "Before adding the 174 free-scalar-map controls; all other receipt counters and evidence digest were observed here." + }, + "final_verification": [ + { + "command": "uv run --python 3.12 --no-project python -I -B research/finite-dihedral-cut-bound/verify.py", + "exit_code": 0, + "result": "PASS_FINITE_DIHEDRAL_CUT_BOUND all_rank_call_cut_checks=1088 all_rank_idempotents=68 formal_dirty_fixtures=1027 free_scalar_cut_checks=348 free_scalar_invertible_maps=174 mixed_words_through_three=9420 omission_controls=9249 rank_one_call_cut_checks=3720 rank_one_projectors=155 regular_dirty_columns_forward_and_inverse=134864 representation_products=47872 target_cut_ranks=1088 word_cut_inequalities=18840 controls=13 no_new_kappa" + }, + { + "command": "uv run --python 3.12 --no-project python scripts/research_package.py --package research/finite-dihedral-cut-bound", + "exit_code": 0, + "result": "Same complete semantic counters under -I -O -B; PASS_REGISTERED_RESEARCH_PACKAGE research/finite-dihedral-cut-bound outcome=completed", + "scope": "Registered Python3.12 replay including source/provenance metadata and declared optimized command." + }, + { + "command": "uv run --python 3.12 --no-project python -I -O -B research/finite-dihedral-cut-bound/verify.py --receipt /tmp/imb-round2-02-invalid-receipt.json", + "control_input": {"result": "PASS_FINITE_DIHEDRAL_CUT_BOUND", "counts": {"formal_dirty_fixtures": 1027}}, + "exit_code": 1, + "result": "ValueError: receipt differs from exact recomputation", + "scope": "Expected rejection of an incomplete certificate despite a passing-looking label and correct fixture count; temporary control input removed afterward." + } + ], + "proof_review": "Checked finite-presentation relations, parity-sensitive shifted offsets c=m and m-1, rank of arbitrary scalar-projector Kronecker crossing blocks, subadditivity, all reflection endpoint shifts, and simultaneous canonical representatives in [-m,m-1]. Finite checks corroborate these arguments, not a universal extrapolation.", + "not_exercised": [ + "Selected frontier cold replay or outer assembly", + "Native physical bit-supplier compiler, frame, hosting, precision or tape admission", + "Odd-period universal theorem", + "Lean/proof-assistant verification", + "Independent human review", + "Hosted CI" + ] +} diff --git a/research/finite-dihedral-cut-bound/VERIFY.json b/research/finite-dihedral-cut-bound/VERIFY.json new file mode 100644 index 0000000000..3b3483fba5 --- /dev/null +++ b/research/finite-dihedral-cut-bound/VERIFY.json @@ -0,0 +1,23 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/bit-dihedral-commutator/README.md", + "research/bit-three-register-lower-bound/README.md" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-O", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Uniform-proof corroboration: all even periods through 32, complete rank-one projector alphabets through four roles, all short mixed words through length three, full formal and faithful-regular dirty boundaries, sharp bills, source pins, certificate comparison and semantic rejecting controls." + } + ] +} diff --git a/research/finite-dihedral-cut-bound/verify.py b/research/finite-dihedral-cut-bound/verify.py new file mode 100755 index 0000000000..7d1133e433 --- /dev/null +++ b/research/finite-dihedral-cut-bound/verify.py @@ -0,0 +1,535 @@ +#!/usr/bin/env python3 +"""Exact finite-dihedral cut checks; the uniform theorem is in README.md. + +Adam Gall, with substantial OpenAI Codex assistance. Apache-2.0. +Standard library only. All checks survive python -O. +""" +from __future__ import annotations + +import argparse +from collections import Counter +from hashlib import sha256 +from itertools import product +import json +from pathlib import Path + +PACKAGE = Path(__file__).resolve().parent +ROOT = PACKAGE.parents[1] +PERIODS = tuple(range(2, 33, 2)) +CALL_PERIODS = (2, 4, 6, 8, 10, 16) +WORD_PERIODS = (2, 4, 6, 8, 10) + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def xor_rows(rows): + result = 0 + for row in rows: + result ^= row + return result + + +def rank(rows): + pivots = {} + for value in rows: + while value: + p = value.bit_length() - 1 + if p not in pivots: + pivots[p] = value + break + value ^= pivots[p] + return len(pivots) + + +def binary_product(a, b): + return tuple(xor_rows(b[j] for j in range(len(b)) if row >> j & 1) for row in a) + + +def identity(size): + return tuple(1 << i for i in range(size)) + + +def projectors(roles): + result = [] + for u in range(1, 1 << roles): + for v in range(1, 1 << roles): + if (u & v).bit_count() % 2: + result.append(tuple(v if u >> i & 1 else 0 for i in range(roles))) + require(len(result) == (2**roles - 1) * 2**(roles - 1), "projector coverage") + require(len(result) == len(set(result)), "duplicate projector") + return result + + +def validate_projector(nrows): + roles = len(nrows) + require(roles > 0 and all(type(row) is int and 0 <= row < 1 << roles for row in nrows), + "projector dimensions") + require(binary_product(nrows, nrows) == nrows and rank(nrows) == 1, + "not a rank-one idempotent") + + +def distance(n, k): + k %= n + return min(k, n - k) + + +def bill(n, targets): + require(n >= 2 and n % 2 == 0, "even period required") + require(all(e in (0, 1) for _, e in targets), "invalid normal-form parity") + return (sum(distance(n, k + e) for k, e in targets), + sum(distance(n, k) for k, _ in targets)) + + +def short_word(n, target): + k, e = target + bill(n, [target]) + k = (k + n // 2) % n - n // 2 + letters = list("xy" * k if k >= 0 else "yx" * -k) + if e: + letters.append("x") + reduced = [] + for letter in letters: + if reduced and reduced[-1] == letter: + reduced.pop() + else: + reduced.append(letter) + return tuple(reduced) # Product order: rightmost acts first. + + +def group_product(n, a, b): + ak, ae = divmod(a, 2) + bk, be = divmod(b, 2) + return 2 * ((ak + (-1 if ae else 1) * bk) % n) + (ae ^ be) + + +def poly_left(n, g, polynomial): + answer = 0 + while polynomial: + bit = polynomial & -polynomial + answer ^= 1 << group_product(n, g, bit.bit_length() - 1) + polynomial ^= bit + return answer + + +def formal_identity(roles): + return tuple(tuple(int(i == j) for j in range(roles)) for i in range(roles)) + + +def formal_target(n, targets, roles): + return tuple(tuple((1 << (2 * (targets[i][0] % n) + targets[i][1]) + if i < len(targets) else 1) if i == j else 0 + for j in range(roles)) for i in range(roles)) + + +def formal_call(n, matrix, nrows, label): + require(label in ("x", "y"), "unpaid address label") + g = 1 if label == "x" else 2 * (n - 1) + 1 + roles = len(matrix) + result = [] + for i, nrow in enumerate(nrows): + delta = [xor_rows(matrix[j][k] for j in range(roles) if nrow >> j & 1) + for k in range(roles)] + result.append(tuple(matrix[i][k] ^ delta[k] ^ poly_left(n, g, delta[k]) + for k in range(roles))) + return tuple(result) + + +def direct_calls(n, targets, roles): + require(roles >= len(targets), "missing target role") + calls = [] + for i, target in enumerate(targets): + nrows = tuple(1 << i if j == i else 0 for j in range(roles)) + calls.extend((nrows, label) for label in reversed(short_word(n, target))) + return tuple(calls) + + +def formal_run(n, roles, calls): + result = formal_identity(roles) + for nrows, label in calls: + result = formal_call(n, result, nrows, label) + return result + + +# Independent literal-permutation engine. Operators are packed binary rows on +# ALL dirty basis inputs, not scalar/register-only columns. Each paid call reads +# one immutable pre-call state, including for non-coordinate projectors. +def inverse_permutation(p): + require(sorted(p) == list(range(len(p))), "not a permutation") + result = [0] * len(p) + for i, j in enumerate(p): + result[j] = i + return tuple(result) + + +def compose(p, q): + return tuple(p[q[i]] for i in range(len(p))) + + +def regular_letters(n): + # Two n-point layers indexed e*n+k. These formulas do not call group_product. + return { + "x": tuple((1 - e) * n + (-k) % n for e in range(2) for k in range(n)), + "y": tuple((1 - e) * n + (-k - 1) % n for e in range(2) for k in range(n)), + } + + +def proof_letters(n, c): + return {"x": tuple((c - a) % n for a in range(n)), + "y": tuple((c - 1 - a) % n for a in range(n))} + + +def permutation_table(n, letters): + ident = tuple(range(len(letters["x"]))) + rotation = compose(letters["x"], letters["y"]) + power = ident + table = [] + for _ in range(n): + table.extend((power, compose(power, letters["x"]))) + power = compose(rotation, power) + require(power == ident, "rotation torsion") + require(compose(letters["x"], letters["x"]) == ident, "x involution") + require(compose(letters["y"], letters["y"]) == ident, "y involution") + return tuple(table) + + +def literal_call(matrix, nrows, p): + width = len(p) + pinv = inverse_permutation(p) + result = list(matrix) + for i, row in enumerate(nrows): + for j in range(len(nrows)): + if row >> j & 1: + for a in range(width): + result[i * width + a] ^= matrix[j * width + a] ^ matrix[j * width + pinv[a]] + return tuple(result) + + +def literal_run(roles, calls, letters): + result = identity(roles * len(letters["x"])) + for nrows, label in calls: + result = literal_call(result, nrows, letters[label]) + return result + + +def represent_formal(matrix, table): + roles = len(matrix) + width = len(table[0]) + inverses = tuple(inverse_permutation(p) for p in table) + rows = [0] * (roles * width) + for i in range(roles): + for j in range(roles): + polynomial = matrix[i][j] + while polynomial: + bit = polynomial & -polynomial + p = inverses[bit.bit_length() - 1] + for a in range(width): + rows[i * width + a] ^= 1 << (j * width + p[a]) + polynomial ^= bit + return tuple(rows) + + +def crossing_rank(matrix, n, roles): + half = n // 2 + mask = sum(1 << (i * n + a) for i in range(roles) for a in range(half, n)) + return rank(matrix[i * n + a] & mask for i in range(roles) for a in range(half)) + + +def check_sources(): + pins = json.loads((PACKAGE / "SOURCES.json").read_text()) + for item in pins["files"]: + if item["usage"] == "input": + require(sha256((ROOT / item["path"]).read_bytes()).hexdigest() == item["sha256"], + "source changed: " + item["path"]) + selection = json.loads((PACKAGE / "SELECTION.json").read_text()) + task = json.loads((PACKAGE / "TASK.json").read_text()) + require(selection["seed"] == task["selection_seed"] == "63537661f5ee8acaa486b70f82726911", + "selection nonce") + require(selection["base_commit"] == pins["base_commit"] == task["base_commit"], "base pin") + require(selection["track"] == task["selection_track"] == "bit-mechanisms", "track") + card = next(s for s in selection["suggestions"] if s["task_id"] == task["task_id"]) + require(card["scope_key"] == task["selection_scope_key"], "card scope key") + provenance = {entry["path"]: entry["sha256"] for entry in pins["files"]} + require(selection["selected_record_sha256"] == provenance["certificates/selected-result.json"], + "selected record provenance") + require(selection["catalog_sha256"] == provenance["docs/research/agent-task-catalog.json"], + "catalogue provenance") + + +def experiment(): + counts = Counter() + evidence = sha256() + negative = [] + + def record(value): + evidence.update(json.dumps(value, separators=(",", ":")).encode() + b"\n") + + # Derive actual group representations and endpoint cut ranks for every target. + for n in PERIODS: + all_targets = [(k, e) for k in range(n) for e in range(2)] + for c in (n // 2, n // 2 - 1): + table = permutation_table(n, proof_letters(n, c)) + for a in range(2 * n): + for b in range(2 * n): + require(compose(table[a], table[b]) == table[group_product(n, a, b)], + "presentation homomorphism") + counts["representation_products"] += 1 + for target in all_targets: + endpoint = formal_target(n, [target], 1) + q = crossing_rank(represent_formal(endpoint, table), n, 1) + expected = bill(n, [target])[0 if c == n // 2 else 1] + require(q == expected, "target crossing formula") + record((n, c, target, q)) + counts["target_cut_ranks"] += 1 + + # Complete scalar-projector alphabets, including n=2,6,10 parity boundaries. + for roles in range(1, 5): + plist = projectors(roles) + counts["rank_one_projectors"] += len(plist) + for nrows in plist: + validate_projector(nrows) + for n in CALL_PERIODS: + for c in (n // 2, n // 2 - 1): + letters = proof_letters(n, c) + for label in ("x", "y"): + operator = literal_call(identity(roles * n), nrows, letters[label]) + q = crossing_rank(operator, n, roles) + expected = int((label == "x") == (c == n // 2)) + require(q == expected, "non-coordinate call charge") + require(literal_call(operator, nrows, letters[label]) == identity(roles * n), + "paid call not involutive") + counts["rank_one_call_cut_checks"] += 1 + + # Every GL(2,2) and GL(3,2) free scalar map has zero cut rank and preserves + # a genuinely mixed paid word's crossing rank on either side. + for roles in (2, 3): + n = 6 + sample_calls = tuple((p, g) for p, g in zip(projectors(roles)[:3], ("x", "y", "x"))) + for scalar in product(range(1 << roles), repeat=roles): + if rank(scalar) != roles: + continue + lifted = tuple(sum(1 << (j * n + a) for j in range(roles) if scalar[i] >> j & 1) + for i in range(roles) for a in range(n)) + require(crossing_rank(lifted, n, roles) == 0, "free scalar crossing charge") + for c in (n // 2, n // 2 - 1): + operator = literal_run(roles, sample_calls, proof_letters(n, c)) + q = crossing_rank(operator, n, roles) + require(crossing_rank(binary_product(lifted, operator), n, roles) == q and + crossing_rank(binary_product(operator, lifted), n, roles) == q, + "free scalar rank invariance") + counts["free_scalar_cut_checks"] += 1 + counts["free_scalar_invertible_maps"] += 1 + + # Separate corollary: all idempotents through three scalar roles, every rank. + for roles in range(1, 4): + for nrows in product(range(1 << roles), repeat=roles): + if binary_product(nrows, nrows) != nrows: + continue + r = rank(nrows) + counts["all_rank_idempotents"] += 1 + for n in (2, 4, 6, 10): + for c in (n // 2, n // 2 - 1): + for label, p in proof_letters(n, c).items(): + actual = crossing_rank(literal_call(identity(roles * n), nrows, p), n, roles) + expected = r if ((label == "x") == (c == n // 2)) else 0 + require(actual == expected, "block rank charge") + counts["all_rank_call_cut_checks"] += 1 + + # Exhaust every two-role paid word through length three, without pruning or + # deduplication. Formal and faithful-regular engines agree at every prefix; + # the two nonfaithful proof quotients separately obey the tariff bound. + alphabet = tuple((p, g) for p in projectors(2) for g in ("x", "y")) + for n in WORD_PERIODS: + reg_letters = regular_letters(n) + reg_table = permutation_table(n, reg_letters) + quotient_letters = tuple(proof_letters(n, c) for c in (n // 2, n // 2 - 1)) + stack = [(0, formal_identity(2), identity(4 * n), + (identity(2 * n), identity(2 * n)), (0, 0))] + while stack: + depth, fm, rm, quotients, used = stack.pop() + if depth == 3: + continue + for p, g in alphabet: + next_formal = formal_call(n, fm, p, g) + next_regular = literal_call(rm, p, reg_letters[g]) + require(represent_formal(next_formal, reg_table) == next_regular, + "formal/faithful-regular disagreement") + next_used = (used[0] + (g == "x"), used[1] + (g == "y")) + next_quotients = tuple(literal_call(quotients[i], p, quotient_letters[i][g]) + for i in range(2)) + for i in range(2): + old_q = crossing_rank(quotients[i], n, 2) + new_q = crossing_rank(next_quotients[i], n, 2) + charge = int(g == ("x" if i == 0 else "y")) + require(new_q <= old_q + charge and new_q <= next_used[i], + "crossing subadditivity") + counts["word_cut_inequalities"] += 1 + counts["mixed_words_through_three"] += 1 + stack.append((depth + 1, next_formal, next_regular, next_quotients, next_used)) + + # Uniform direct-word constructor corroborated on complete finite target + # domains, plus heterogeneous higher-role fixtures with dirty spectators. + fixtures = [(n, ((k, e),), 2) for n in PERIODS for k in range(n) for e in range(2)] + for n in (2, 4, 6, 8): + elements = tuple(product(range(n), range(2))) + fixtures.extend((n, targets, 3) for targets in product(elements, repeat=2)) + fixtures.extend([ + (10, ((5, 0), (5, 1), (-4, 1), (12, 0)), 7), + (6, ((3, 0), (3, 1), (-2, 1), (8, 0), (0, 1)), 9), + (8, ((4, 0), (4, 0)), 7), + ]) + for n, targets, roles in fixtures: + calls = direct_calls(n, targets, roles) + expected = formal_target(n, targets, roles) + actual = formal_run(n, roles, calls) + require(actual == expected, "formal attaining boundary") + counts_by_label = (sum(g == "x" for _, g in calls), sum(g == "y" for _, g in calls)) + require(counts_by_label == bill(n, targets), "simultaneous sharp bill") + letters = regular_letters(n) + table = permutation_table(n, letters) + literal = literal_run(roles, calls, letters) + require(literal == represent_formal(expected, table), "literal dirty boundary") + inverse = expected + inverse_literal = literal + for p, g in reversed(calls): + inverse = formal_call(n, inverse, p, g) + inverse_literal = literal_call(inverse_literal, p, letters[g]) + require(inverse == formal_identity(roles), "formal inverse") + require(inverse_literal == identity(roles * 2 * n), "literal inverse") + for c, wanted in zip((n // 2, n // 2 - 1), bill(n, targets)): + qtable = permutation_table(n, proof_letters(n, c)) + require(crossing_rank(represent_formal(expected, qtable), n, roles) == wanted, + "heterogeneous cut rank additivity") + for omit in range(len(calls)): + mutated = formal_run(n, roles, calls[:omit] + calls[omit + 1:]) + require(mutated != expected, "omitted call accepted") + counts["omission_controls"] += 1 + counts["formal_dirty_fixtures"] += 1 + counts["regular_dirty_columns_forward_and_inverse"] += 2 * roles * 2 * n + record((n, targets, roles, counts_by_label, expected)) + + # Semantic negative controls, with explicit exceptions rather than asserts. + def must_reject(name, operation): + try: + operation() + except ValueError: + negative.append(name) + else: + raise ValueError("control accepted: " + name) + + must_reject("odd_period_scope", lambda: bill(3, [(1, 1)])) + must_reject("non_idempotent_projector", lambda: validate_projector((2, 0))) + must_reject("rank_two_undercharged_projector", lambda: validate_projector((1, 2))) + must_reject("unpaid_rotation_label", lambda: formal_call(6, formal_identity(2), (1, 0), "r")) + must_reject("missing_role", lambda: direct_calls(6, [(1, 0), (2, 0)], 1)) + + # The excluded odd-period simultaneous-minimum inference fails already at n=3. + odd_target = 2 * 1 + 1 + cheap = ((), ("x",), ("y",), ("x", "y"), ("y", "x")) + for word in cheap: + value = 0 + for g in word: + value = group_product(3, value, 1 if g == "x" else 5) + require(value != odd_target, "odd-period false simultaneous word") + require((distance(3, 2), distance(3, 1)) == (1, 1), "odd scope fixture") + negative.append("odd_separate_minima_not_jointly_attainable") + + # Using the usual c=0 action instead of the shifted action is not the proof. + for n in (6, 10): + wrong = proof_letters(n, 0) + qx = crossing_rank(literal_call(identity(n), (1,), wrong["x"]), n, 1) + qy = crossing_rank(literal_call(identity(n), (1,), wrong["y"]), n, 1) + require((qx, qy) != (1, 0) and (qx, qy) != (0, 1), "wrong offset was isolated") + negative.append("fixed_offset_shortcut_n" + str(n)) + + n, roles, targets = 6, 3, ((1, 0), (2, 1)) + calls = direct_calls(n, targets, roles) + target = formal_target(n, targets, roles) + wrong_label = tuple((p, "y" if g == "x" else "x") if i == 0 else (p, g) + for i, (p, g) in enumerate(calls)) + require(formal_run(n, roles, wrong_label) != target, "wrong label accepted") + negative.append("wrong_paid_label") + require(formal_run(n, roles, tuple(reversed(calls))) != target, "wrong order accepted") + negative.append("wrong_execution_order") + dirty_calls = calls + (((0, 0, 4), "x"),) + dirty = formal_run(n, roles, dirty_calls) + require(dirty[:2] == target[:2] and dirty != target, "spectator restoration control") + require(literal_run(roles, dirty_calls, regular_letters(n)) != + represent_formal(target, permutation_table(n, regular_letters(n))), + "regular spectator restoration control") + negative.append("dirty_workspace_not_restored") + + # An invertible off-diagonal Omega perturbation is hidden by BOTH proof + # representations but not by the formal or faithful-regular engines. + n = 6 + clean = formal_identity(2) + omega = (1 << (2 * n)) - 1 + hidden = ((1, omega), (0, 1)) + for c in (n // 2, n // 2 - 1): + table = permutation_table(n, proof_letters(n, c)) + require(represent_formal(hidden, table) == represent_formal(clean, table), + "common-kernel control not hidden") + faithful = permutation_table(n, regular_letters(n)) + require(hidden != clean and represent_formal(hidden, faithful) != represent_formal(clean, faithful), + "represented-only endpoint accepted") + require(binary_product(represent_formal(hidden, faithful), represent_formal(hidden, faithful)) == + identity(4 * n), "hidden dirty shear not invertible") + negative.append("nonfaithful_endpoint_false_positive") + + # A direct central rotation is outside the paid alphabet: at n=10 its cut + # costs five, so silently declaring it a unit operation invalidates the bound. + n = 10 + central = formal_target(n, [(5, 0)], 1) + for c in (5, 4): + table = permutation_table(n, proof_letters(n, c)) + require(crossing_rank(represent_formal(central, table), n, 1) == 5, + "free rotation surcharge control") + negative.append("direct_rotation_not_unit_tariff") + + require(counts["mixed_words_through_three"] == 9420, "short-word domain truncated") + require(counts["formal_dirty_fixtures"] == 1027, "target domain truncated") + require(counts["rank_one_projectors"] == 155, "projector domain truncated") + return { + "schema_version": 1, + "result": "PASS_FINITE_DIHEDRAL_CUT_BOUND", + "theorem_scope": "all even n>=2, all target counts, every finite dirty workspace; written proof", + "finite_domains": { + "even_periods_all_targets": list(PERIODS), + "rank_one_projector_roles": [1, 2, 3, 4], + "rank_one_call_periods": list(CALL_PERIODS), + "all_idempotent_roles": [1, 2, 3], + "all_idempotent_periods": [2, 4, 6, 10], + "free_scalar_roles": [2, 3], + "free_scalar_period": 6, + "mixed_word_periods": list(WORD_PERIODS), + "mixed_word_max_length": 3, + "all_ordered_target_pair_periods": [2, 4, 6, 8], + }, + "counts": dict(sorted(counts.items())), + "negative_controls": negative, + "deterministic_evidence_sha256": evidence.hexdigest(), + "no_new_kappa": True, + } + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--emit", action="store_true", help="research mode: emit newly computed receipt") + parser.add_argument("--receipt", type=Path, default=PACKAGE / "RECEIPT.json") + args = parser.parse_args() + check_sources() + receipt = experiment() + if args.emit: + print(json.dumps(receipt, indent=2, sort_keys=True)) + else: + expected = json.loads(args.receipt.read_text()) + require(receipt == expected, "receipt differs from exact recomputation") + counts = receipt["counts"] + print(receipt["result"], " ".join(f"{key}={value}" for key, value in counts.items()), + f"controls={len(receipt['negative_controls'])}", "no_new_kappa") + + +if __name__ == "__main__": + main()