From ccea0bf1100b54d3ae84b72e5850cfa491cb3d4c Mon Sep 17 00:00:00 2001 From: Nick Petalas Date: Tue, 27 Oct 2026 16:16:28 +0000 Subject: [PATCH] feat(research): prove four inverse C3 targets need eight calls --- research/c3-four-inverse-tariff/PROOF.md | 98 ++++++ research/c3-four-inverse-tariff/README.md | 122 +++++++ research/c3-four-inverse-tariff/SOURCES.json | 18 ++ research/c3-four-inverse-tariff/TASK.json | 64 ++++ research/c3-four-inverse-tariff/VERIFY.json | 34 ++ research/c3-four-inverse-tariff/verify.py | 314 +++++++++++++++++++ 6 files changed, 650 insertions(+) create mode 100644 research/c3-four-inverse-tariff/PROOF.md create mode 100644 research/c3-four-inverse-tariff/README.md create mode 100644 research/c3-four-inverse-tariff/SOURCES.json create mode 100644 research/c3-four-inverse-tariff/TASK.json create mode 100644 research/c3-four-inverse-tariff/VERIFY.json create mode 100644 research/c3-four-inverse-tariff/verify.py diff --git a/research/c3-four-inverse-tariff/PROOF.md b/research/c3-four-inverse-tariff/PROOF.md new file mode 100644 index 0000000000..b49af0ebe7 --- /dev/null +++ b/research/c3-four-inverse-tariff/PROOF.md @@ -0,0 +1,98 @@ +# Four inverse cyclic targets need eight calls + +This scoped proof was produced by Nick Petalas. New work is Apache-2.0. + +Let A=F2[g]/(g^3+1), the full formal group algebra F2[C3]. There are +exactly four scalar roles, each with arbitrary dirty input in A. The paid +alphabet consists of + + D_N(g) = I + (1+g) N, + N = u v^T over F2, v^T u = 1. + +Each call costs one. Any binary invertible scalar matrix is free. The +required complete endpoint is T=g^2 I_4. No extra role, clean allocation, +erasure, free g^2 call or free address operation is allowed. + +**Theorem.** The minimum paid-call count is eight. + +## Remove free scalar bridges + +For any S in GL_4(F2), conjugation sends D_N(g) to D_(SNS^-1)(g). +Move every scalar bridge to one endpoint, conjugating the intervening +couplings. Augmentation g=1 sends every paid factor to I and sends T to I. +Thus the remaining scalar endpoint factor is I. This reduces every program +to a product of paid factors with the same count and legal binary couplings. +It accounts for arbitrary interleaved scalar changes, not only a fixed basis. + +## Only five calls could improve on eight + +Write F4=F2[w]/(w^2+w+1). Specialize g to w. Put d=1+w=w^2. Each paid +factor is I+dN and has determinant w, since N is a rank-one idempotent. +The target is w^2 I_4 and has determinant w^8=w^2. A k-call word therefore +requires k=2 modulo 3. Also rank(T-I)=4 in F4. Telescoping a product of k +rank-one increments bounds rank(T-I) by k. Among k<8, only k=5 survives. +These are necessary conditions on a formal identity; specialization is not +used as a sufficient formal-endpoint test in the proof. + +## A product with four independent update directions + +Consider four factors F_i=I+d u_i v_i^T with binary u_i,v_i and v_i^T u_i=1, +in chronological order i=1,2,3,4. If rank(F_4 F_3 F_2 F_1-I)=4, their four +image vectors u_i are independent. Indeed the image of the product minus I +lies in span_F4(u_1,u_2,u_3,u_4), by telescoping left updates. Binary vectors +are independent over F4 exactly when they are independent over F2. + +Conjugate by the binary matrix with columns u_1,...,u_4. Each factor now +updates only row i, and its binary row functional a_i has a_ii=1. Let L +and U be the strict lower and strict upper parts of the binary matrix with +rows a_i. If M is the final product, its i-th row satisfies + + M_i = e_i^T + d (sum_(j=i) a_ij e_j^T). + +Earlier rows already have their final values; later rows are still their +identity rows. Consequently + + (I+d L) M = I+d(I+U). (1) + +This is a row-once identity for the stated four factors. It does not assume +that their functionals or projectors commute. + +Suppose, in addition, M=d I+P with P binary. Substitute in (1), use +w^2=w+1 and d^2=w, and compare the coefficients of 1 and w. They give + + I+P+LP = U, + L+LP = U. + +Subtracting gives P=I+L. A strict lower triangular L makes I+L invertible. +Thus such a four-factor product requires rank_F2(P)=4. In particular it +cannot have rank(P)=1. + +## Exclude five calls + +Assume F_4 F_3 F_2 F_1 F_0 = d I, with five legal paid factors after +specialization. Since F_0^-1=I+w N_0, removing the chronological first +factor gives + + F_4 F_3 F_2 F_1 = (d I)(I+w N_0) = d I+N_0. (2) + +The right side minus I is w I+N_0. It is invertible: on im(N_0) it is +multiplication by w+1, and on ker(N_0) by w. Both scalars are nonzero. +The preceding four-direction lemma applies. Its binary basis change sends +N_0 to a binary rank-one projector P, while leaving d I fixed. Equation +(2) would therefore require rank(P)=4. This contradicts rank(P)=1. +Five calls are impossible, completing the lower bound. + +## Attainment and scope + +On each coordinate role apply its coordinate projector twice. This is eight +positive-g calls and gives g^2 on that role, hence T exactly in the full +formal algebra. All four input columns remain arbitrary. There are no +spectators to restore and no auxiliary input is silently set to zero. + +The argument proves this four-role tariff only. In a larger register space +the target with restored spectators is no longer a scalar matrix. Removing +the first factor then need not leave the full-rank four-direction situation +above. No lower bound with extra roles is claimed. Additional paid labels, +nonbinary scalar coefficients and different endpoints also need new analysis. +No native, physical or recursive supplier cost follows from the formal count. +Independent human and formal proof-kernel review are unclaimed. diff --git a/research/c3-four-inverse-tariff/README.md b/research/c3-four-inverse-tariff/README.md new file mode 100644 index 0000000000..673d4ff987 --- /dev/null +++ b/research/c3-four-inverse-tariff/README.md @@ -0,0 +1,122 @@ +# Four inverse C3 targets have exact eight-call cost + +Four copies of the inverse of a single order-three label cannot share a +saving in the stated binary register model. The endpoint +`diag(g^2,g^2,g^2,g^2)` in the full formal algebra `F2[C3]` needs exactly +**eight positive-g rank-one idempotent calls**, even with free interleaved +`GL_4(F2)` scalar mixing and arbitrary dirty inputs on all four roles. + +Claim type: scoped algebraic proof with exact finite corroboration. This is +an original changed-alphabet side result for `bit-new-register-model`. +It supplies no new kappa or selected-frontier change. + +[PROOF.md](PROOF.md) proves the lower bound without enumeration. Rank and +determinant reduce every possible saving to five calls. Remove the first +factor. The remaining four updates have independent binary image directions, +so each changes one row exactly once in their image basis. Comparing the two +F4 coefficients in that triangular factorization would force a rank-one +projector to have rank four. Eight coordinate calls attain the endpoint in +the full group ring. + +## Exact evidence and reproduction + +From the repository root, using CPython 3.12 and its standard library: + +```sh +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/c3-four-inverse-tariff/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -O -W error -B research/c3-four-inverse-tariff/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/c3-four-inverse-tariff +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/c3-four-inverse-tariff --check-source-history +``` + +Another CPython 3.12 installation can replace the absolute interpreter path. +Expected scientific output is `PASS_C3_FOUR_INVERSE_TARIFF minimum=8 +five_call_hits=0`. The runner also prints `PASS_REGISTERED_RESEARCH_PACKAGE`. +The committed-byte check requires a publication commit and full Git history. + +The read-only verifier performs two exact meet-in-the-middle exclusions. +Scalarity of the target permits simultaneous binary conjugation of the +chronological first coupling to E00. Each remaining four-factor word splits +into two products of length at most two. The F4 packed-row engine and a +separate full F2[C3] coefficient-convolution engine each enumerate 8,361 +distinct such products and test all 8,361 complements. Both find zero hits. +Full-ring augmentation and F4 together are also checked to distinguish all +eight group-ring elements. Product representatives are safe because only +the complete product affects a later factor; no sampling is used. + +Additional checks enumerate all 65,536 binary four-by-four matrices to confirm +the complete 120-projector inventory, construct a normalization basis for +each projector, and check all 4,096 row-once binary functional choices in +the proof's factorization identity. The eight-call witness passes every +formal coefficient and all twelve faithful regular-action dirty-input columns. +All eight single-call omissions reject. Six controls include positive identity, +one-call and five-call joins, nilpotent rejection and order-three identities. +All acceptance checks remain active with Python optimization enabled. + +Every run prints a generated JSON receipt bound to all package files by +SHA256. There is no handwritten receipt and no generated checkout output. +The mathematical proof and finite checks are separate evidence. + +## Sources and overlap + +Canonical base is `19fdb086ea96af9a9f87936a2b888e10af4ed810`, priority revision +8. The current selected-source baseline passed its binding checks only. +[SOURCES.json](SOURCES.json) pins the historical catalogue and selected record; +no predecessor executable or scientific receipt is imported or replayed. +The advance [CLAIM](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19221497) +reserved the original four-role five-call question. + +The retained eumemic register model and its subsequent finite-group work +supply the context. Wentao Li's #2513 cyclic 2-power theorem concerns a +characteristic-two chain ring and unit-cost arbitrary nonidentity powers. +It does not address this odd-order semisimple algebra with only positive g +paid. Ross Richardson's #4269 cubic caller uses rational rank-one nilpotent +shears over Q[N]/(N^3-1), rather than binary rank-one idempotent label calls. +Cinna Davis's #1799 uses C3 for a three-destination complex fanout family, +which is a different object. These results are cited, not re-checked. + +Entry overlap covered 341 open PRs and 5,523 Discussion records with complete +remote pagination. The sparse local search covered 243 of 8,136 tracked note +paths; distinctive main-tree searches and merged/all-state PR searches +supplemented it. Unpublished work, arbitrary diffs and absent local notes +remain outside that coverage. No search is a proof of novelty. + +## Limitations and implementation constraints + +The theorem fixes exactly four dirty roles and permits only the positive g +label, binary rank-one idempotent couplings and binary scalar mixing. +Extra restored roles, g^2 as an independent paid label, clean state, +nonbinary mixing and restricted finite-address realizations are outside scope. +All physical scalar, frame, access, ownership, routing, restoration, native, +compiler, precision, stock, tape and complete supplier invoices are unpriced. +No complete multiplication theorem is claimed. Independent human and formal +proof-kernel review are unclaimed. Lean, Docker, the selected cold replay and +predecessor scientific suites were not run. + +The verifier has no recursion, dynamic execution, external solver, subprocess +or dependency. Its largest fixed inventories are 65,536 four-bit-row matrices +and two 8,361-entry product tables. Loop bounds are fixed in the code, and +functions stay under 60 physical lines. CPython's integer/tuple/dictionary +allocation and iterator dispatch are managed-runtime deviations from Power of +Ten rules 3 and 9. The fixed domains bound live storage; the same warning-strict +normal and optimized commands check both implementations. A larger-role replay +would require a new explicit capacity bound before expanding these domains. + +## Open next questions + +Can one additional restored dirty role lower the eight-call count for the +same four inverse targets? First retain the same alphabet and analyze how the +first update can meet both the target and spectator subspaces. The current +scalar-target argument no longer applies, and no five-role search was run. +A physical positive-g primitive and a complete paid caller would be required +before any formal saving could affect the BIT budget. + +## Credit + +This contribution was produced by Nick Petalas. Credit eumemic's register +framework, Ali Romman's retained rank-one register context, Wentao Li's +cyclic-root work, Ross Richardson's separate cubic-caller boundary and the +finite-group contributors for the surrounding questions. The new four-role +obstruction and its verifier are the contribution here. Elementary finite-field, +rank and determinant arguments are classical; global literature priority is +unclaimed. New work is Apache-2.0. Predecessor files and credit are unchanged. diff --git a/research/c3-four-inverse-tariff/SOURCES.json b/research/c3-four-inverse-tariff/SOURCES.json new file mode 100644 index 0000000000..d596e2e530 --- /dev/null +++ b/research/c3-four-inverse-tariff/SOURCES.json @@ -0,0 +1,18 @@ +{ + "schema_version": 1, + "base_commit": "19fdb086ea96af9a9f87936a2b888e10af4ed810", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "581f8d87008354eb5b869f7ed9de1317ad837ce8", + "sha256": "2a0220e866417774606e0f991e41b9c1d26b1f43b97857238cf478dbc7d330b5" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec", + "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81" + } + ] +} diff --git a/research/c3-four-inverse-tariff/TASK.json b/research/c3-four-inverse-tariff/TASK.json new file mode 100644 index 0000000000..a4229a0bd3 --- /dev/null +++ b/research/c3-four-inverse-tariff/TASK.json @@ -0,0 +1,64 @@ +{ + "schema_version": 1, + "task_id": "bit-new-register-model", + "priority_revision": 8, + "base_commit": "19fdb086ea96af9a9f87936a2b888e10af4ed810", + "original_card": { + "id": "bit-new-register-model", + "question": "Can an explicitly larger or nonabelian register model escape the scoped three-register obstruction?", + "starting_points": [ + "docs/research/research-family-status.md", + "research/bit-three-register-lower-bound/README.md", + "certificates/selected-result.json", + "research/bit-gl3-mixed-targets-length10/README.md", + "docs/research/community-efficient1000-review.md" + ], + "methods": [ + "Construct the smallest exact identity in a newly specified legal operation alphabet.", + "Derive a target-specific relaxation bound for that same explicit alphabet." + ], + "acceptance_gate": "Name the changed hypothesis, all counted roles and a uniform identity; finite column tests alone do not certify it. A scoped local result may be retained without a complete supplier. Expanding it into further construction rounds requires the family-level budget and obligation gate in research-family-status.md; an optimistic passing relaxation alone is not acceptance.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_selected_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Resolve the current selected review, separate complex/ordinary BIT/admitted BIT/outer budgets, and compare the card against live handoffs before starting. Historical ceilings require exact source/model equivalence.", + "scope": "Source-binding orientation only; not a scientific replay or all-size proof. Materialize selected inputs if this checkout is sparse." + }, + "first_experiment": "First compare the alphabet, role count and length with the fully replayed #1974 census and #2027 mixed-root tariff. Identify a changed premise and a legal native implementation; then price one smallest completed instance before searching larger words.", + "bottleneck_link": "A small-width completed saving changes the bit primitive; a finite-address identity alone is insufficient.", + "allowed_variations": [ + "Choose a fixed larger register count or a specified nonabelian operation family." + ], + "scope_change_triggers": [ + "Remaining inside the already-excluded three-register abelian model.", + "Repeating the two-register GL3 census or a covered three-register length without changing a hypothesis; a formal group-algebra word without native conversion is a partial result." + ], + "overlap_terms": [ + "three-register", + "nonabelian", + "group algebra" + ] + }, + "scope_status": "changed", + "actual_scope": "Exact positive-g call tariff for four inverse cyclic targets over F2[C3], on exactly four arbitrary dirty roles with free binary scalar mixing.", + "scope_change_reason": "The original card requests a changed supplier model with native pricing. This original bounded experiment instead proves a formal-algebra obstruction for a specified odd-order alphabet; it is a side result with no native realization or complete invoice.", + "bottleneck_link": "Changed BIT primitives may help the next supplier cap. This excludes a five-call sharing attempt before native development; it does not alter the currently binding complex supplier.", + "budget_minutes": 60, + "stop_rule": "Stop at the first verified new construction or sharp obstruction. The first exact result is minimum eight on four roles; do not extend to extra roles.", + "outcome": "completed", + "evidence": "PROOF.md; two exact 8361-candidate joins, complete projector inventory, row-once identity checks and full dirty formal witness.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "Can one additional restored dirty role reduce the same four inverse target tariff?", + "why_it_matters": "The present scalar-target proof cannot constrain this changed endpoint and a saving could motivate a new primitive.", + "first_step": "Keep the positive-g alphabet and analyze the first coupling relative to target and spectator subspaces before a bounded five-role search.", + "blocked_by": "No five-role lower bound, witness, native realization or complete physical invoice is supplied." + } + ] +} diff --git a/research/c3-four-inverse-tariff/VERIFY.json b/research/c3-four-inverse-tariff/VERIFY.json new file mode 100644 index 0000000000..2b1bd2ccdd --- /dev/null +++ b/research/c3-four-inverse-tariff/VERIFY.json @@ -0,0 +1,34 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Scoped proof corroboration, both exact joins, projector inventory, triangular identity, full formal witness and semantic controls" + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "All acceptance predicates remain active under optimized Python" + } + ] +} diff --git a/research/c3-four-inverse-tariff/verify.py b/research/c3-four-inverse-tariff/verify.py new file mode 100644 index 0000000000..5c500c71fd --- /dev/null +++ b/research/c3-four-inverse-tariff/verify.py @@ -0,0 +1,314 @@ +#!/usr/bin/env python3 +"""Exact four-role C3 tariff certificate. Standard library; writes nothing.""" +import hashlib +import json +from pathlib import Path + +ROLES = 4 +EVEN = 0x55 +IDENTITY = tuple(1 << (2 * i) for i in range(ROLES)) +TARGET = tuple(3 << (2 * i) for i in range(ROLES)) + + +def need(condition, message): + if not condition: + raise ValueError(message) + + +def omega(row): + a, b = row & EVEN, (row >> 1) & EVEN + return b | ((a ^ b) << 1) + + +def binary_rank(rows, width=4): + pivots = [0] * width + rank = 0 + for original in rows: + row = original + for bit in range(width - 1, -1, -1): + if not (row >> bit) & 1: + continue + if pivots[bit]: + row ^= pivots[bit] + else: + pivots[bit] = row + rank += 1 + break + return rank + + +def projectors(): + return tuple((u, v) for u in range(1, 16) for v in range(1, 16) + if (u & v).bit_count() % 2 == 1) + + +def left_gate(matrix, coupling, inverse=False): + u, v = coupling + need(0 < u < 16 and 0 < v < 16 and (u & v).bit_count() % 2 == 1, + "coupling must be a binary rank-one idempotent") + total = 0 + for j in range(ROLES): + if (v >> j) & 1: + total ^= matrix[j] + delta = omega(total) if inverse else total ^ omega(total) + return tuple(row ^ (delta if (u >> i) & 1 else 0) + for i, row in enumerate(matrix)) + + +def multiply(left, right): + result = [] + for row in left: + total = 0 + for j in range(ROLES): + coefficient = (row >> (2 * j)) & 3 + if coefficient & 1: + total ^= right[j] + if coefficient & 2: + total ^= omega(right[j]) + result.append(total) + return tuple(result) + + +def field_table(gates): + table = {IDENTITY: ()} + for i, gate in enumerate(gates): + table[left_gate(IDENTITY, gate)] = (i,) + for i, first in enumerate(gates): + prefix = left_gate(IDENTITY, first) + for j, second in enumerate(gates): + table.setdefault(left_gate(prefix, second), (i, j)) + return table + + +def field_join(target, gates, table): + # Chronological first factor is E00. The endpoint is scalar, so binary + # simultaneous conjugation makes this normalization complete. + first = gates.index((1, 1)) + wanted = multiply(target, left_gate(IDENTITY, gates[first], inverse=True)) + hits = [] + for word in table.values(): + complement = wanted + # P=G_last...G_first, so right multiplication by P^-1 takes the + # inverse factors in chronological order, not reversed order. + for index in word: + inverse = left_gate(IDENTITY, gates[index], inverse=True) + complement = multiply(complement, inverse) + if complement in table: + witness = (first,) + word + table[complement] + actual = IDENTITY + for index in witness: + actual = left_gate(actual, gates[index]) + need(actual == target, "join produced a false endpoint") + hits.append(witness) + return hits + + +def ring_times(a, b): + result = 0 + for i in range(3): + for j in range(3): + if ((a >> i) & 1) and ((b >> j) & 1): + result ^= 1 << ((i + j) % 3) + return result + + +def ring_identity(): + return tuple(int(i == j) for i in range(4) for j in range(4)) + + +def ring_gate(matrix, coupling, right=False, inverse=False): + # Separate full group-ring implementation; no F4 arithmetic is imported. + u, v = coupling + delta = 5 if inverse else 3 # 1+g^2 or 1+g. + out = list(matrix) + if right: + for i in range(4): + total = 0 + for k in range(4): + if (u >> k) & 1: + total ^= matrix[4 * i + k] + for j in range(4): + if (v >> j) & 1: + out[4 * i + j] ^= ring_times(total, delta) + else: + for j in range(4): + total = 0 + for k in range(4): + if (v >> k) & 1: + total ^= matrix[4 * k + j] + for i in range(4): + if (u >> i) & 1: + out[4 * i + j] ^= ring_times(total, delta) + return tuple(out) + + +def ring_join(gates): + identity = ring_identity() + table = {identity: ()} + for i, gate in enumerate(gates): + table[ring_gate(identity, gate)] = (i,) + for i, first in enumerate(gates): + prefix = ring_gate(identity, first) + for j, second in enumerate(gates): + table.setdefault(ring_gate(prefix, second), (i, j)) + target = tuple(4 * x for x in identity) + wanted = ring_gate(target, (1, 1), right=True, inverse=True) + hits = 0 + for word in table.values(): + complement = wanted + for index in word: + complement = ring_gate(complement, gates[index], right=True, + inverse=True) + hits += int(complement in table) + return len(table), hits + + +def check_projectors(gates): + enumerated = set() + for code in range(1 << 16): + rows = tuple((code >> (4 * i)) & 15 for i in range(4)) + if binary_rank(rows) != 1: + continue + square = [] + for row in rows: + total = 0 + for j in range(4): + if (row >> j) & 1: + total ^= rows[j] + square.append(total) + if tuple(square) == rows: + enumerated.add(rows) + constructed = {tuple(v if (u >> i) & 1 else 0 for i in range(4)) + for u, v in gates} + need(enumerated == constructed and len(gates) == 120, + "rank-one idempotent inventory mismatch") + for u, v in gates: + kernel = [x for x in range(1, 16) if not (v & x).bit_count() % 2] + basis = [u] + for x in kernel: + if binary_rank(basis + [x]) > len(basis): + basis.append(x) + need(len(basis) == 4 and all(not (v & x).bit_count() % 2 + for x in basis[1:]), + "binary normalization basis failed") + return len(enumerated) + + +def check_triangular_identity(): + delta = 3 + count = 0 + positions = [(i, j) for i in range(4) for j in range(4) if i != j] + for code in range(1 << len(positions)): + vectors = [1 << i for i in range(4)] + for bit, (i, j) in enumerate(positions): + if (code >> bit) & 1: + vectors[i] |= 1 << j + matrix = IDENTITY + for i in range(4): + matrix = left_gate(matrix, (1 << i, vectors[i])) + lower = list(IDENTITY) + rhs = [] + for i in range(4): + row = 1 << (2 * i) + upper = 0 + for j in range(4): + if (vectors[i] >> j) & 1: + if j < i: + lower[i] ^= delta << (2 * j) + else: + upper ^= delta << (2 * j) + rhs.append(row ^ upper) + need(multiply(tuple(lower), matrix) == tuple(rhs), + "row-once triangular factorization failed") + count += 1 + return count + + +def check_ring_and_witness(): + def image(a): + return ((a & 1) ^ (2 if a & 2 else 0) ^ (3 if a & 4 else 0)) + def field_times(a, b): + return (a if b & 1 else 0) ^ (omega(a) if b & 2 else 0) + need(len({(a.bit_count() % 2, image(a)) for a in range(8)}) == 8, + "augmentation/F4 representation is not faithful") + for a in range(8): + for b in range(8): + need(image(ring_times(a, b)) == field_times(image(a), image(b)), + "field/group-ring product mismatch") + word = tuple((1 << i, 1 << i) for i in range(4) for _ in range(2)) + actual = ring_identity() + for gate in word: + actual = ring_gate(actual, gate) + target = tuple(4 * x for x in ring_identity()) + need(actual == target, "eight-call witness failed") + for omitted in range(8): + mutant = ring_identity() + for i, gate in enumerate(word): + if i != omitted: + mutant = ring_gate(mutant, gate) + need(mutant != target, "omitted call was not detected") + # Full left-regular action on each of the twelve arbitrary dirty columns. + for role in range(4): + for address in range(3): + output = [ring_times(actual[4 * i + role], 1 << address) + for i in range(4)] + need(output == [((1 << ((address + 2) % 3)) if i == role else 0) + for i in range(4)], "dirty regular column failed") + return 12 + + +def controls(gates, table): + need(field_join(IDENTITY, gates, table), "three-call identity control lost") + one = left_gate(IDENTITY, (1, 1)) + need(field_join(one, gates, table), "one-call positive control lost") + probe = IDENTITY + for i in (0, 23, 71, 11, 94): + probe = left_gate(probe, gates[i]) + need(field_join(probe, gates, table), "five-call positive control lost") + try: + left_gate(IDENTITY, (1, 2)) + except ValueError: + pass + else: + raise ValueError("nilpotent was accepted as an idempotent") + need(left_gate(one, (1, 1)) != IDENTITY, + "order-three gate was treated as an involution") + need(left_gate(left_gate(one, (1, 1)), (1, 1)) == IDENTITY, + "three equal calls did not close") + return 6 + + +def main(): + gates = projectors() + inventory = check_projectors(gates) + table = field_table(gates) + need(len(table) == 8361, "two-factor field inventory changed") + need(not field_join(TARGET, gates, table), "five-call saving exists") + ring_size, ring_hits = ring_join(gates) + need((ring_size, ring_hits) == (8361, 0), "full-ring exclusion disagrees") + result = { + "claim_type": "scoped proof with exact finite corroboration", + "minimum": 8, + "roles": 4, + "rank_one_idempotents": inventory, + "two_factor_products": len(table), + "normalized_join_candidates_per_engine": len(table), + "five_call_hits_per_engine": ring_hits, + "row_once_factorizations": check_triangular_identity(), + "dirty_regular_columns": check_ring_and_witness(), + "omitted_call_controls": 8, + "semantic_controls": controls(gates, table), + } + root = Path(__file__).resolve().parent + files = ("PROOF.md", "README.md", "SOURCES.json", "TASK.json", + "VERIFY.json", "verify.py") + result["package_sha256"] = { + name: hashlib.sha256((root / name).read_bytes()).hexdigest() + for name in files + } + print(json.dumps(result, sort_keys=True)) + print("PASS_C3_FOUR_INVERSE_TARIFF minimum=8 five_call_hits=0") + + +if __name__ == "__main__": + main()