From 8fbd8d3a8fdea5c9fc4cf4c529ea43ccc7570917 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Krzysztof=20W=C3=B3jt?= <97155365+krzysztofwojt@users.noreply.github.com> Date: Fri, 23 Oct 2026 15:21:23 +0200 Subject: [PATCH] Prove the exact mixed-target semilinear call tariff --- research/semilinear-mixed-tariff/PROOF.md | 172 ++++++ research/semilinear-mixed-tariff/README.md | 128 +++++ research/semilinear-mixed-tariff/SOURCES.json | 24 + research/semilinear-mixed-tariff/TASK.json | 71 +++ research/semilinear-mixed-tariff/VERIFY.json | 34 ++ .../semilinear-mixed-tariff/small_words.py | 489 ++++++++++++++++++ research/semilinear-mixed-tariff/verify.py | 286 ++++++++++ 7 files changed, 1204 insertions(+) create mode 100644 research/semilinear-mixed-tariff/PROOF.md create mode 100644 research/semilinear-mixed-tariff/README.md create mode 100644 research/semilinear-mixed-tariff/SOURCES.json create mode 100644 research/semilinear-mixed-tariff/TASK.json create mode 100644 research/semilinear-mixed-tariff/VERIFY.json create mode 100644 research/semilinear-mixed-tariff/small_words.py create mode 100644 research/semilinear-mixed-tariff/verify.py diff --git a/research/semilinear-mixed-tariff/PROOF.md b/research/semilinear-mixed-tariff/PROOF.md new file mode 100644 index 0000000000..bc81fbd7ec --- /dev/null +++ b/research/semilinear-mixed-tariff/PROOF.md @@ -0,0 +1,172 @@ +# Mixed targets have no call sharing in prime-degree binary semilinear groups + +This is a scoped algebraic proof. It answers Nick Petalas's mixed-target +question in PR #5202; his normal-C7 theorem, F8 representation and rank method +retain their credit. Cinna Davis's PR #2011 supplies the order-21 model and +earlier orbit census. Neither predecessor census is an assumption of the +self-contained argument below. No physical supplier or new kappa is claimed. + +## Model and theorem + +Let p be an **odd prime**, F = F_(2^p), and + + G_p = F^* semidirect C_p, + (a,j)(b,k) = (a b^(2^j), j+k mod p). + +Call a nonidentity element with j=0 **normal**, and an element with j!=0 +**outside**. At p=3 this is C7 semidirect C3 with the action in #2011/#5202. +All nonidentity labels are allowed, at unit price. + +Work in Mat_r(F2[G_p]), for any finite r>=1. Every register starts arbitrarily +dirty. A paid operation is + + D_N(g) = I + N tensor ([g]+[1]), + g != 1, N=x y^T over F2, y^T x=1. + +Thus N is a rank-one idempotent. Arbitrary GL_r(F2) scalar maps may be +interleaved freely. No other address operation, clean workspace, COPY or ERASE +is free. The required endpoint is the **full formal operator** + + T = diag([g_1],...,[g_r]). + +Let n be the number of normal targets, m the number of outside targets, and +w=n+m. Identity targets designate restored dirty registers. Repeated target +labels are permitted. + +**Theorem.** The minimum paid-call count is exactly w. If a word is optimal, +then, after moving its free scalar maps to the right, it has exactly n normal +calls and m outside calls. In every normalized normal call, both x and y are +supported only on normal target roles. In every normalized outside call they +are supported only on outside target roles. In particular, no normalized +optimal paid factor touches a restored identity role, and the two target +types never mix in a normalized optimal word. + +These support statements concern the normalized algebraic word. They do not +claim that an implementation's interleaved free scalar maps avoid workspace. +They also do not force coordinate projectors within either target class. + +## A constant-displacement representation + +On the p-dimensional binary vector space F, use + + rho(a,j)(z) = a z^(2^j). + +This is a group representation by the displayed group law. For a!=1 and j=0, +rho(a,0)-I is multiplication by a-1, so has binary rank p. + +For 0 1 sends every paid factor and T to I, so +the remaining scalar product is I. We have a normalized paid-only word of +the same length and the same labels. + +Under R, each paid factor A has + + A-I = N tensor (R(g)-I), rank(A-I)=p. + +The represented target has rank(R(T)-I)=p w. Rank subadditivity and + + AB-I = (A-I)B + (B-I) + +give p w <= p L for a normalized word of L calls. Thus L>=w, with no +restriction on r or on the number of restored dirty registers. + +Conversely, for each g_i!=1 apply D_(E_ii)(g_i). These w coordinate factors +attain T **in the full formal algebra**, for every input in every role. +The other roles are identically restored. This proves the exact minimum; +equality merely in a representation is not used for attainment. + +Writing c_N,c_O for the two paid label counts, the separate representations +also give + + p c_N + (p-1)c_O >= p n + (p-1)m, + c_O >= m. + +At L=c_N+c_O=n+m the first inequality implies c_O<=m. Therefore c_O=m and +c_N=n. At p=3 these are precisely the missing paired inequalities +3c7+2c3>=3n+2m and c3>=m. + +## Rigidity of optimal normalized factors + +For any product A_1...A_L, telescoping from the right and from the left gives + + col(A_1...A_L-I) <= sum_i col(A_i-I), + row(A_1...A_L-I) <= sum_i row(A_i-I). + +Here <= means subspace inclusion. For example, the first follows from +the expansion sum_i (A_i-I) A_(i+1)...A_L; the second follows from +sum_i A_1...A_(i-1)(A_i-I). If the word is optimal, the left side has +dimension pL, while the sum of the individual dimensions on the right is +also pL. Consequently both inclusions are equalities, and **each** factor's +column and row spaces lie inside the corresponding target spaces. + +Project the column containment to one register role t. For a factor with +N=x y^T and x_t=1, the projected column space is col(R(g)-I). The target's +space in that role is col(R(g_t)-I). The identity target has zero space, +so x_t must be zero there. A normal call has full dimension p in the rho +block and zero in the chi block. It cannot fit inside an outside target's +(p-1)-dimensional rho image. An outside call has a nonzero chi image, so +cannot fit inside a normal target's zero chi block. Thus x has the stated +type support. Applying the identical argument to row spaces and y proves +the corresponding assertion for y. This proves the rigidity statement. + +## Boundary, credit and verification + +The p=3 all-normal case is already #5202's theorem. The additions are all +mixed/outside target lists, the normalized optimal-factor support theorem, +and the odd-prime-degree family. The proof above includes the inherited +representation/rank steps to be readable without an unmerged dependency. +The exact checks are finite corroboration, not a proof of universal quantifiers +or independent human acceptance. Elementary finite-field facts and ordinary +rank algebra are used explicitly, with no numerical or asymptotic premise. + +The prime-degree and odd-characteristic-order hypotheses are used at the two +specified steps. No conclusion for composite degrees or p=2 follows from +this argument. Nonuniform label prices, restricted alphabets, higher-rank +paid factors, non-diagonal targets and extra free address maps have different +boundaries. Native realization, ownership, routing, restoration implementation, +precision, hosting, stock/compiler and full recursive/outer costs are unpriced. +The theorem supplies no physical supplier or complete multiplication theorem. + +Predecessors: Nick Petalas, PR #5202 at +`99ed6d2fc13101cb5ec0d3b1cdc826b75bc27fc7`; Cinna Davis / 1337isnot1337, +PR #2011 at `b971a6c68d6f60c2693b2057ecf3489efb75efc4` and PR #3893; +eumemic / #288 and the retained register-model lineage. Prepared by +Krzysztof Wojt with substantial OpenAI Codex assistance. Apache-2.0. diff --git a/research/semilinear-mixed-tariff/README.md b/research/semilinear-mixed-tariff/README.md new file mode 100644 index 0000000000..dc95473ba5 --- /dev/null +++ b/research/semilinear-mixed-tariff/README.md @@ -0,0 +1,128 @@ +# Exact mixed-target tariff for binary semilinear groups + +**Scoped written proof, with exact finite corroboration; no new kappa.** +For every odd prime p, in the full formal algebra +`F2[C_(2^p-1) semidirect C_p]` with Frobenius action, any diagonal target +with w nonidentity entries needs **exactly w** unit-price rank-one idempotent +calls. The theorem allows arbitrary finite restored dirty workspace and free +binary scalar mixing. Repeated labels and arbitrary mixtures of normal and +outside labels are included. + +At p=3 this answers the mixed-target question explicitly left open by +[Nick Petalas's PR #5202](https://github.com/CrocSwap/integer-mult-bounds/pull/5202). +His all-normal tariff and F8 rank representation retain their credit; +[Cinna Davis's #2011](https://github.com/CrocSwap/integer-mult-bounds/pull/2011) +retains the group/model and three-role orbit census. These earlier results are +not repeated as the contribution. + +The new quotient character supplies the missing outside-call budget. Its +sum with the natural representation has displacement rank p for **every** +nonidentity group element. Rank telescoping gives the lower bound, while w +coordinate calls attain the full formal endpoint. [PROOF.md](PROOF.md) gives +all quantifiers and the proof without an unmerged code dependency. + +There is also an equality theorem: after scalar normalization, an optimal +word has exactly as many normal/outside calls as the respective target counts. +Both vectors of every paid rank-one projector stay within its own target type. +No normalized optimal paid factor touches an identity-target dirty register. +Interleaved free maps themselves may use workspace; within-type noncoordinate +projectors are allowed and have a checked positive example. + +## Scope and evidence + +| Check | Exact finite coverage | +|---|---| +| Natural plus character representation | Every label at p=3,5,7: 21,155,889 labels | +| Representation multiplication | All 441 and 24,025 ordered pairs at p=3,5; 3,556 left/right generator pairs at p=7 | +| Paid displacement ranks | All 6 two-role idempotents for each nonidentity label: 6,372 matrices over finite fields | +| Free scalar normalization | All 168 GL3(F2) maps and 28 idempotents: 4,704 covariances | +| Separate full formal checker | All 14,400 two-role and 313,600 three-role ordered two-call words, without rank-based pruning | +| Literal endpoints in that census | All 1,600 two-target endpoints attained; 672 are mixed-type; no support-rigidity violations | +| Arbitrary-dirty regular action | Four mixed calls on five registers, surrounded by dense inverse scalar maps: all 105 basis inputs match and all 21 dirty-role basis inputs restore; a changed label gives 21 mismatches | +| Hypothesis and corruption controls | Omitted representation blocks, rank-two paid gate, missing outside budget, composite degree, p=2 character, wrong group law, omitted formal terms, forbidden support and wrong target | + +The universal statements rest on the written proof, not on extrapolation from +these dimensions. `small_words.py` was implemented separately by a supporting +Luna agent, then inspected and run by the primary agent. It compares complete +formal coefficients rather than represented ranks. This is AI-assisted +corroboration, not independent human or proof-kernel review. + +The composite-degree fixture checks that Frobenius cubed on F512 has natural +displacement rank 6, so adding one character gives 7, not 9. It invalidates +that extension of this proof; it does **not** disprove the tariff for composite +degrees. The p=2 control similarly tests the missing character hypothesis. + +## Reproduce + +CPython 3.12, standard library only, from the repository root: + +```sh +python3.12 -I -W error -B research/semilinear-mixed-tariff/verify.py +python3.12 -I -O -W error -B research/semilinear-mixed-tariff/verify.py +python3.12 -B scripts/research_package.py --package research/semilinear-mixed-tariff +python3.12 -B scripts/check_research_commit.py --package research/semilinear-mixed-tariff --check-source-history +``` + +The direct verifier prints `PASS_SEMILINEAR_MIXED_TARIFF`, exact coverage and +fresh SHA256 values for every package file. It does not write artifacts, fetch +sources or require Git. The registered commands additionally authenticate the +package's historical provenance. Each command has a 60-second timeout; local +direct runtime is about one second. Committed-package export and a Git-free +read-only replay are separate publication checks, reported in the PR. + +## Value, coordination and boundaries + +Scientific base: canonical main `ec2780e8aeb1c88acaf5e9e470ef8c68e7fbbb6c`, +priority revision 7. [Canonical investigation #5230](https://github.com/CrocSwap/integer-mult-bounds/discussions/5230) +and [handoff pointer](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19146275) +record the claim. This changes `bit-new-register-model` to the explicitly open +mixed-target algebraic question. The result rules out call sharing throughout +this formal family before any physical implementation is proposed. + +Before claim, the overlap scan covered 344 open PRs, 4,466 closed PRs, 4,453 +Discussion records and 6,996 main notes, with complete pagination; live open +PR bodies and recent handoffs were checked again. Exact #2011 and #5202 heads +were read. Recent krzysztofwojt scopes, including #5204 and the active +fifteen-owner six-cycle investigation, were excluded. Related #5199, #5203 +and #5205 concern other groups/alphabets/targets. No conflicting mixed +semilinear tariff appeared. Historical diffs and unpublished work remain +coverage limits; the final live refresh is recorded in the PR. + +The price is one per arbitrary nonidentity label, not a physical recursive +cost. Native realization, ownership, routing, restoration implementation, +frames/hosting, precision, stock/compiler and full recursive/outer costs are +**unknown** here. No native supplier, complete multiplication theorem, new +kappa or selected-frontier change is claimed. No Lean, Docker, selected cold +replay or predecessor census was run. The family is closed at this formal +unit-price question; physical expansion would require a new contract and bill. + +## Open next questions + +1. What is the sharp tariff when normal and outside calls have different + positive prices? Begin with two normal order-21 targets and test whether + three outside calls can attain them; the paired rank inequalities permit + that count but do not supply a word. This could distinguish algebraic + count optimality from an actual priced interface. The nonuniform full + formal optimum and physical prices remain unknown. +2. Does a constant-displacement certificate, or a genuine sharing word, exist + at an odd composite degree? Start at degree nine with the order-three + Frobenius elements exposed by the boundary control. The present single + character no longer equalizes ranks. No such extension is claimed or reserved. + +## Credit and exact sources + +- **Nick Petalas, #5202**, head `99ed6d2fc13101cb5ec0d3b1cdc826b75bc27fc7`: + normal-C7 theorem, natural rank budget, free-scalar normalization and the + explicit mixed-target handoff. Its `PROOF.md` SHA256 is + `7bd232212ba6359533ec333c36b781c7aba84490fa246c349ad5a3a510bb5d47`. + This is a citation, not a runtime input; the new proof is self-contained. +- **Cinna Davis / 1337isnot1337, #2011**, head + `b971a6c68d6f60c2693b2057ecf3489efb75efc4`: order-21 model and prior orbit + census. Its retained main README is pinned as provenance in `SOURCES.json`. +- **Cinna Davis, #3893**, the S3 representation-rank precedent; **eumemic, + #288**, and the retained register-model lineage. + +Prepared by **Krzysztof Wojt with substantial OpenAI Codex assistance**, +including bounded Luna overlap inventory and an independently implemented +finite checker, inspected and integrated by the primary agent. Apache-2.0. +No independent human or formal proof-kernel review is claimed. diff --git a/research/semilinear-mixed-tariff/SOURCES.json b/research/semilinear-mixed-tariff/SOURCES.json new file mode 100644 index 0000000000..e42d3d47d0 --- /dev/null +++ b/research/semilinear-mixed-tariff/SOURCES.json @@ -0,0 +1,24 @@ +{ + "schema_version": 1, + "base_commit": "ec2780e8aeb1c88acaf5e9e470ef8c68e7fbbb6c", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "c35482cd9035843b15a634cc8276a7e1e40e8395", + "sha256": "6fe0a099b89aa2aed796a13c3a21dafc63f3388ebf397464e44e0451893b9375" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "f126dd2e2dad2b669e75d1d0d0bd05c600725602", + "sha256": "f7a48bfa2659b88378282a8eee7d9fe52cdf505594124c4d1686b58510fffd72" + }, + { + "path": "research/bit-semidir21-orbit-seed8f89/README.md", + "usage": "provenance", + "git_blob": "13e399921e5dd556a7ce8645362ffb5d550b5e75", + "sha256": "534422d3f152b0f1e4a8357056036d1629b0aee75e58301c7436f5b723260eb0" + } + ] +} diff --git a/research/semilinear-mixed-tariff/TASK.json b/research/semilinear-mixed-tariff/TASK.json new file mode 100644 index 0000000000..59256a0593 --- /dev/null +++ b/research/semilinear-mixed-tariff/TASK.json @@ -0,0 +1,71 @@ +{ + "schema_version": 1, + "task_id": "bit-new-register-model", + "priority_revision": 7, + "base_commit": "ec2780e8aeb1c88acaf5e9e470ef8c68e7fbbb6c", + "original_card": { + "id": "bit-new-register-model", + "question": "Can an explicitly larger or nonabelian register model escape the scoped three-register obstruction?", + "starting_points": [ + "docs/research/research-family-status.md", + "research/bit-three-register-lower-bound/README.md", + "certificates/selected-result.json", + "research/bit-gl3-mixed-targets-length10/README.md", + "docs/research/community-efficient1000-review.md" + ], + "methods": [ + "Construct the smallest exact identity in a newly specified legal operation alphabet.", + "Derive a target-specific relaxation bound for that same explicit alphabet." + ], + "acceptance_gate": "Name the changed hypothesis, all counted roles and a uniform identity; finite column tests alone do not certify it. A scoped local result may be retained without a complete supplier. Expanding it into further construction rounds requires the family-level budget and obligation gate in research-family-status.md; an optimistic passing relaxation alone is not acceptance.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Read Model section 1 of the three-register bound and identify the exact excluded free operations.", + "scope": "Positive control / source-bound orientation only; this is not a new construction or full cold replay." + }, + "first_experiment": "First compare the alphabet, role count and length with the fully replayed #1974 census and #2027 mixed-root tariff. Identify a changed premise and a legal native implementation; then price one smallest completed instance before searching larger words.", + "bottleneck_link": "A small-width completed saving changes the bit primitive; a finite-address identity alone is insufficient.", + "allowed_variations": [ + "Choose a fixed larger register count or a specified nonabelian operation family." + ], + "scope_change_triggers": [ + "Remaining inside the already-excluded three-register abelian model.", + "Repeating the two-register GL3 census or a covered three-register length without changing a hypothesis; a formal group-algebra word without native conversion is a partial result." + ], + "overlap_terms": [ + "three-register", + "nonabelian", + "group algebra" + ] + }, + "scope_status": "changed", + "actual_scope": "Exact unit-price tariff for every mixed diagonal target in F2[C_(2^p-1) semidirect C_p] for odd prime p, with arbitrary finite restored dirty workspace and free binary scalar mixing; support rigidity of optimal normalized factors.", + "scope_change_reason": "Take PR5202's explicitly released mixed-target handoff. Add a quotient character to its natural rank budget, then prove the same constant-displacement principle in prime degrees. The previous normal-C7 theorem and finite orbit census are credited, not audit deliverables.", + "bottleneck_link": "Scoped algebraic obstruction to saving paid calls in this nonabelian register family. Physical realization and complete supplier costs remain unknown; no kappa claim.", + "budget_minutes": 240, + "stop_rule": "Stop after the exact mixed-target theorem and its bounded verification; no wider construction campaign or physical admission.", + "outcome": "completed", + "evidence": "Written constant-displacement and equality-support proof; finite fields at p=3,5,7, exact two-call formal enumeration at r=2,3, free-scalar covariance, and hypothesis/corruption controls. Universal quantifiers rest on PROOF.md.", + "author": "Krzysztof Wojt with substantial OpenAI Codex assistance", + "ai_assistance": "Substantial OpenAI Codex assistance. A Luna worker supplied bounded overlap inventory and a separate exact small-word checker. Primary inspected, corrected and reran it; no independent human or formal proof-kernel review.", + "open_questions": [ + { + "question": "What is the sharp tariff with different positive normal/outside call prices?", + "why_it_matters": "A formal unit-price optimum does not decide a nonuniform physical bill.", + "first_step": "For p=3 and two normal targets, test the three-outside-call count allowed by the paired rank inequalities.", + "blocked_by": "No full formal optimum or physical price contract is known here." + }, + { + "question": "Can odd composite degrees admit a constant-displacement certificate or a sharing word?", + "why_it_matters": "The present result excludes sharing only at prime degrees.", + "first_step": "Study degree nine and its order-three Frobenius labels; the recorded rank-six fixture blocks the present one-character proof.", + "blocked_by": "Displacement ranks are no longer equalized; no replacement certificate or word is supplied." + } + ], + "claim_url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/5230" +} diff --git a/research/semilinear-mixed-tariff/VERIFY.json b/research/semilinear-mixed-tariff/VERIFY.json new file mode 100644 index 0000000000..4c27ab7cf0 --- /dev/null +++ b/research/semilinear-mixed-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": 60, + "checks": "Exact finite-field representation and gate ranks, scalar normalization, independently implemented full formal word census and corruption controls; source-bound receipt." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 60, + "checks": "Same mathematical checks and rejection controls with Python assertions disabled." + } + ] +} diff --git a/research/semilinear-mixed-tariff/small_words.py b/research/semilinear-mixed-tariff/small_words.py new file mode 100644 index 0000000000..8e050fd06d --- /dev/null +++ b/research/semilinear-mixed-tariff/small_words.py @@ -0,0 +1,489 @@ +"""Finite exact word enumeration for the order-21 semilinear mixed tariff. + +Implemented by OpenAI Codex at Krzysztof Wojt's request, 2026-10-23. This is +finite computational corroboration in the full formal group algebra, not an +independent human review or a proof beyond the enumerated dimensions/word +length. + +Apache-2.0. Separately implemented supporting checker; inspected and integrated +by the primary Codex agent. +""" + +from __future__ import annotations + +from collections import Counter +from functools import lru_cache +from itertools import product +import json + + +Element = tuple[int, int] +Matrix = tuple[int, ...] # Rows, each encoded as an r-bit integer. +AlgebraMatrix = dict[int, Matrix] + + +def require(condition: bool, message: str) -> None: + """Raise in normal and optimized Python alike when a check fails.""" + if not condition: + raise RuntimeError(message) + + +ELEMENTS: tuple[Element, ...] = tuple((i, j) for i in range(7) for j in range(3)) +ELEMENT_INDEX = {g: i for i, g in enumerate(ELEMENTS)} +IDENTITY = (0, 0) +IDENTITY_INDEX = ELEMENT_INDEX[IDENTITY] + + +def group_product(a: Element, b: Element) -> Element: + """Multiply (i,j)(k,l)=(i+2^j k mod 7,j+l mod 3).""" + i, j = a + k, ell = b + return ((i + pow(2, j, 7) * k) % 7, (j + ell) % 3) + + +GROUP_TABLE: tuple[tuple[int, ...], ...] = tuple( + tuple(ELEMENT_INDEX[group_product(a, b)] for b in ELEMENTS) + for a in ELEMENTS +) + + +def valid_group_table(table: tuple[tuple[int, ...], ...] | list[list[int]]) -> bool: + """Check identity and associativity for a finite multiplication table.""" + size = len(table) + if size == 0 or any(len(row) != size for row in table): + return False + if any(not (0 <= table[a][b] < size) for a in range(size) for b in range(size)): + return False + if any(table[IDENTITY_INDEX][a] != a or table[a][IDENTITY_INDEX] != a for a in range(size)): + return False + return all( + table[table[a][b]][c] == table[a][table[b][c]] + for a in range(size) + for b in range(size) + for c in range(size) + ) + + +def zero_matrix(r: int) -> Matrix: + return (0,) * r + + +def identity_matrix(r: int) -> Matrix: + return tuple(1 << row for row in range(r)) + + +def matrix_xor(a: Matrix, b: Matrix) -> Matrix: + return tuple(x ^ y for x, y in zip(a, b)) + + +@lru_cache(maxsize=None) +def matrix_product(a: Matrix, b: Matrix) -> Matrix: + """Multiply binary matrices represented by row bitmasks.""" + out: list[int] = [] + for row in a: + value = 0 + remaining = row + while remaining: + bit = remaining & -remaining + column = bit.bit_length() - 1 + value ^= b[column] + remaining ^= bit + out.append(value) + return tuple(out) + + +def rank_one_idempotents(r: int) -> tuple[tuple[int, int, Matrix], ...]: + """Enumerate N=xy^T with nonzero x,y and y^T x=1 over F2.""" + result: list[tuple[int, int, Matrix]] = [] + for x in range(1, 1 << r): + for y in range(1, 1 << r): + if bin(x & y).count("1") % 2 != 1: + continue + matrix = tuple(y if (x >> row) & 1 else 0 for row in range(r)) + require(matrix_product(matrix, matrix) == matrix, "generated matrix is not idempotent") + result.append((x, y, matrix)) + return tuple(result) + + +def add_coefficient(coefficients: AlgebraMatrix, group_index: int, matrix: Matrix) -> None: + old = coefficients.get(group_index) + coefficients[group_index] = matrix if old is None else matrix_xor(old, matrix) + + +def factor_coefficients(r: int, g: Element, n: Matrix) -> AlgebraMatrix: + """Coefficients of D_N(g)=I+([g]+[1])N in M_r(F2[G]).""" + coefficients: AlgebraMatrix = {} + add_coefficient(coefficients, IDENTITY_INDEX, matrix_xor(identity_matrix(r), n)) + add_coefficient(coefficients, ELEMENT_INDEX[g], n) + return coefficients + + +def normalized_signature(coefficients: AlgebraMatrix) -> tuple[tuple[int, Matrix], ...]: + return tuple( + (group_index, matrix) + for group_index, matrix in sorted(coefficients.items()) + if any(matrix) + ) + + +def algebra_matrix_product( + a: AlgebraMatrix, + b: AlgebraMatrix, + table: tuple[tuple[int, ...], ...] | list[list[int]] = GROUP_TABLE, +) -> AlgebraMatrix: + """Full formal group-algebra matrix product, with coefficient XOR.""" + out: AlgebraMatrix = {} + for ga, ma in a.items(): + for gb, mb in b.items(): + group_index = table[ga][gb] + add_coefficient(out, group_index, matrix_product(ma, mb)) + return {g: m for g, m in out.items() if any(m)} + + +def scalar_coefficients(matrix: Matrix) -> AlgebraMatrix: + """Embed a binary scalar matrix as the identity-group coefficient.""" + return {IDENTITY_INDEX: matrix} + + +def apply_algebra_to_vector( + coefficients: AlgebraMatrix, + vector: int, + table: tuple[tuple[int, ...], ...] | list[list[int]] = GROUP_TABLE, +) -> int: + """Apply M_r(F2[G]) to a packed vector in the left regular module.""" + out = 0 + remaining = vector + while remaining: + bit = remaining & -remaining + input_index = bit.bit_length() - 1 + input_role, input_group = divmod(input_index, len(ELEMENTS)) + for group_index, matrix in coefficients.items(): + output_group = table[group_index][input_group] + for output_role, row in enumerate(matrix): + if (row >> input_role) & 1: + output_index = output_role * len(ELEMENTS) + output_group + out ^= 1 << output_index + remaining ^= bit + return out + + +def inverse_binary_matrix(matrix: Matrix) -> Matrix: + """Invert a square binary matrix by exact Gauss-Jordan elimination.""" + r = len(matrix) + augmented = [matrix[row] | (1 << (r + row)) for row in range(r)] + for column in range(r): + pivot = next((row for row in range(column, r) if (augmented[row] >> column) & 1), None) + require(pivot is not None, "scalar matrix is singular") + augmented[column], augmented[pivot] = augmented[pivot], augmented[column] + for row in range(r): + if row != column and ((augmented[row] >> column) & 1): + augmented[row] ^= augmented[column] + left_mask = (1 << r) - 1 + require(all((row & left_mask) == (1 << i) for i, row in enumerate(augmented)), "scalar inverse elimination failed") + return tuple(row >> r for row in augmented) + + +def target_coefficients(r: int, roles: tuple[int, int], labels: tuple[Element, Element]) -> AlgebraMatrix: + """Literal diagonal monomial target, with identity on every dirty role.""" + coefficients: AlgebraMatrix = {} + targeted = dict(zip(roles, labels)) + for role in range(r): + label = targeted.get(role, IDENTITY) + diagonal_unit = tuple((1 << role) if row == role else 0 for row in range(r)) + add_coefficient(coefficients, ELEMENT_INDEX[label], diagonal_unit) + return {g: m for g, m in coefficients.items() if any(m)} + + +def label_kind(g: Element) -> str: + return "normal" if g[1] == 0 else "outside" + + +def endpoint_class(labels: tuple[Element, Element]) -> str: + left, right = (label_kind(g) for g in labels) + return "mixed" if left != right else f"homogeneous_{left}" + + +def factor_is_rigid( + factor: tuple[Element, int, int, Matrix], + roles: tuple[int, int], + labels: tuple[Element, Element], +) -> bool: + """Require both x and y to avoid dirty roles and opposite-type targets.""" + g, x, y, _matrix = factor + kind = label_kind(g) + allowed = 0 + for role, label in zip(roles, labels): + if label_kind(label) == kind: + allowed |= 1 << role + return (x & ~allowed) == 0 and (y & ~allowed) == 0 + + +def noncoordinate_control(r: int) -> None: + """Check complementary noncoordinate idempotents realize diag([g],[g]).""" + require(r >= 2, "noncoordinate control needs two target roles") + g = (1, 0) + # In the first 2x2 block, N=[[1,1],[0,0]] and M=I+N=[[0,1],[0,1]]. + # Their decompositions are x y^T with (x,y)=(01,11),(11,10) in bit order. + n = (0b11, 0) + (0,) * (r - 2) + m = (0b10, 0b10) + (0,) * (r - 2) + require(matrix_product(n, n) == n and matrix_product(m, m) == m, "control idempotents invalid") + require(matrix_xor(n, m) == tuple(0b01 << row for row in range(2)) + (0,) * (r - 2), "control N+M mismatch") + require(matrix_product(n, m) == zero_matrix(r), "control idempotents are not complementary") + word = algebra_matrix_product(factor_coefficients(r, g, n), factor_coefficients(r, g, m)) + target = target_coefficients(r, (0, 1), (g, g)) + require(normalized_signature(word) == normalized_signature(target), "noncoordinate equal-label word failed") + require((n[0] & 0b10) != 0 and (m[0] & 0b10) != 0, "control accidentally coordinate-only") + + +def arbitrary_dirty_basis_replay() -> dict[str, object]: + """Replay a mixed four-call word on every basis vector of F2[G]^5.""" + r = 5 + # Dense invertible circulant matrix; every row and column has weight 3. + scalar = (0b00111, 0b01110, 0b11100, 0b11001, 0b10011) + scalar_inverse = inverse_binary_matrix(scalar) + require(matrix_product(scalar, scalar_inverse) == identity_matrix(r), "S*S^-1 is not identity") + require(matrix_product(scalar_inverse, scalar) == identity_matrix(r), "S^-1*S is not identity") + require(all(bin(row).count("1") > 1 for row in scalar), "S is not role-mixing") + require(all(bin(row).count("1") > 1 for row in scalar_inverse), "S^-1 is not role-mixing") + require( + all(sum((scalar[row] >> column) & 1 for row in range(r)) > 1 for column in range(r)), + "S has an unmixed input role", + ) + require( + all(sum((scalar_inverse[row] >> column) & 1 for row in range(r)) > 1 for column in range(r)), + "S^-1 has an unmixed input role", + ) + + labels = ((1, 0), (2, 1), (3, 2), (4, 0), IDENTITY) + scalar_op = scalar_coefficients(scalar) + inverse_op = scalar_coefficients(scalar_inverse) + paid_ops: list[AlgebraMatrix] = [] + for role, label in enumerate(labels[:4]): + coordinate = tuple((1 << role) if row == role else 0 for row in range(r)) + conjugated = matrix_product(matrix_product(scalar_inverse, coordinate), scalar) + x = sum(1 << row for row in range(r) if (scalar_inverse[row] >> role) & 1) + y = scalar[role] + factorization = tuple(y if (x >> row) & 1 else 0 for row in range(r)) + require(factorization == conjugated, "conjugated paid idempotent factorization mismatch") + require(matrix_product(conjugated, conjugated) == conjugated, "conjugated paid matrix is not idempotent") + paid_ops.append(factor_coefficients(r, label, conjugated)) + + # As a matrix word this is S D_0 D_1 D_2 D_3 S^-1. The paid + # idempotents are S^-1 E_ii S, so conjugation leaves the exact diagonal + # endpoint; the surrounding free maps do mix the dirty fifth role. + operators = [scalar_op, *paid_ops, inverse_op] + + def replay(input_vector: int, ops: list[AlgebraMatrix]) -> int: + value = input_vector + for operator in reversed(ops): + value = apply_algebra_to_vector(operator, value) + return value + + basis_count = r * len(ELEMENTS) + mismatches = 0 + dirty_restored = 0 + inputs_by_role = [0] * r + for input_index in range(basis_count): + role, group_index = divmod(input_index, len(ELEMENTS)) + input_vector = 1 << input_index + inputs_by_role[role] += 1 + actual = replay(input_vector, operators) + endpoint_label = labels[role] + output_group = GROUP_TABLE[ELEMENT_INDEX[endpoint_label]][group_index] + expected = 1 << (role * len(ELEMENTS) + output_group) + if actual != expected: + mismatches += 1 + if role == r - 1 and actual == input_vector: + dirty_restored += 1 + require(mismatches == 0, f"regular-action basis replay has {mismatches} endpoint mismatches") + require(dirty_restored == len(ELEMENTS), "dirty role was not restored on every group basis state") + + # Check free-map inverse restoration alone on every basis input. + inverse_cancellation_mismatches = sum( + replay(1 << input_index, [scalar_op, inverse_op]) != (1 << input_index) + for input_index in range(basis_count) + ) + require(inverse_cancellation_mismatches == 0, "free S/S^-1 restoration failed") + + dirty_basis = 1 << ((r - 1) * len(ELEMENTS) + IDENTITY_INDEX) + mixed_dirty = apply_algebra_to_vector(scalar_op, dirty_basis) + mixed_dirty_roles = { + index // len(ELEMENTS) + for index in range(basis_count) + if (mixed_dirty >> index) & 1 + } + require(len(mixed_dirty_roles) > 1 and r - 1 in mixed_dirty_roles, "S did not mix the dirty role") + + # Mutate one paid label while preserving the free maps and idempotents. + mutated_labels = ((5, 0), labels[1], labels[2], labels[3], IDENTITY) + mutated_paid_ops = list(paid_ops) + first_role = 0 + first_coordinate = tuple((1 << first_role) if row == first_role else 0 for row in range(r)) + first_conjugated = matrix_product(matrix_product(scalar_inverse, first_coordinate), scalar) + mutated_paid_ops[0] = factor_coefficients(r, mutated_labels[0], first_conjugated) + mutated_operators = [scalar_op, *mutated_paid_ops, inverse_op] + mutation_mismatches = 0 + for input_index in range(basis_count): + role, group_index = divmod(input_index, len(ELEMENTS)) + expected_label = labels[role] + output_group = GROUP_TABLE[ELEMENT_INDEX[expected_label]][group_index] + expected = 1 << (role * len(ELEMENTS) + output_group) + if replay(1 << input_index, mutated_operators) != expected: + mutation_mismatches += 1 + require(mutation_mismatches > 0, "mutated paid label escaped basis comparison") + + return { + "registers": r, + "basis_inputs_checked": basis_count, + "basis_inputs_by_role": inputs_by_role, + "endpoint_mismatches": mismatches, + "dirty_group_basis_inputs_restored": dirty_restored, + "inverse_cancellation_basis_mismatches": inverse_cancellation_mismatches, + "dirty_role_mixed_by_S": sorted(mixed_dirty_roles), + "mutated_paid_label_basis_mismatches": mutation_mismatches, + "endpoint_labels": [list(label) for label in labels], + } + + +def negative_controls(r: int) -> dict[str, bool]: + """Exercise mutation detectors independently of the enumerated result.""" + # A valid semidirect product is noncommutative; this catches direct-product + # or wrong-action substitutions before the word enumeration starts. + require(group_product((0, 1), (1, 0)) == (2, 1), "semidirect action product wrong") + require(group_product((1, 0), (0, 1)) == (1, 1), "reverse product wrong") + require(group_product((0, 1), (1, 0)) != group_product((1, 0), (0, 1)), "group control lost noncommutativity") + require(valid_group_table(GROUP_TABLE), "constructed multiplication table is invalid") + corrupted = [list(row) for row in GROUP_TABLE] + corrupted[1][1] = (corrupted[1][1] + 1) % len(ELEMENTS) + require(not valid_group_table(corrupted), "corrupted multiplication table escaped detection") + + g, h = (1, 0), (2, 1) + n = tuple(1 if row == 0 else 0 for row in range(r)) + m = tuple((1 << 1) if row == 1 else 0 for row in range(r)) + first = factor_coefficients(r, g, n) + second = factor_coefficients(r, h, m) + target = target_coefficients(r, (0, 1), (g, h)) + require(normalized_signature(algebra_matrix_product(first, second)) == normalized_signature(target), "coordinate control word failed") + + # Dropping either summand ([g]N or [1]N) changes the target word. + dropped_g = dict(first) + dropped_g.pop(ELEMENT_INDEX[g]) + dropped_identity = dict(first) + dropped_identity[IDENTITY_INDEX] = identity_matrix(r) + require(normalized_signature(algebra_matrix_product(dropped_g, second)) != normalized_signature(target), "dropped [g]N term escaped detection") + require(normalized_signature(algebra_matrix_product(dropped_identity, second)) != normalized_signature(target), "dropped [1]N term escaped detection") + + # The support detector must reject a rank-one factor on a dirty role. + dirty = tuple(1 << row if row == r - 1 else 0 for row in range(r)) + dirty_factor = (g, 1 << (r - 1), 1 << (r - 1), dirty) + require(not factor_is_rigid(dirty_factor, (0, 1), (g, h)), "dirty-role support escaped detection") + + wrong_target = target_coefficients(r, (0, 1), (g, (3, 1))) + require(normalized_signature(algebra_matrix_product(first, second)) != normalized_signature(wrong_target), "deliberate wrong target escaped detection") + return { + "corrupted_multiplication_detected": True, + "dropped_factor_terms_detected": True, + "forbidden_dirty_support_detected": True, + "wrong_target_detected": True, + } + + +def enumerate_dimension(r: int) -> dict[str, object]: + idempotents = rank_one_idempotents(r) + nonidentity = tuple(g for g in ELEMENTS if g != IDENTITY) + factors: list[tuple[Element, int, int, Matrix, AlgebraMatrix]] = [] + for g in nonidentity: + for x, y, n in idempotents: + factors.append((g, x, y, n, factor_coefficients(r, g, n))) + + targets: dict[tuple[tuple[int, Matrix], ...], tuple[tuple[int, int], tuple[Element, Element]]] = {} + endpoints_by_class: Counter[str] = Counter() + roles_list = tuple((i, j) for i in range(r) for j in range(i + 1, r)) + for roles in roles_list: + for labels in product(nonidentity, repeat=2): + labels_pair = (labels[0], labels[1]) + endpoint = normalized_signature(target_coefficients(r, roles, labels_pair)) + require(endpoint not in targets, "duplicate literal target encoding") + targets[endpoint] = (roles, labels_pair) + endpoints_by_class[endpoint_class(labels_pair)] += 1 + + word_counts: Counter[str] = Counter() + rigidity_violations: Counter[str] = Counter() + first_violation: list[dict[str, object]] = [] + counts_by_endpoint: Counter[tuple[tuple[int, Matrix], ...]] = Counter() + + for g1, x1, y1, n1, coeffs1 in factors: + for g2, x2, y2, n2, coeffs2 in factors: + word = normalized_signature(algebra_matrix_product(coeffs1, coeffs2)) + endpoint = targets.get(word) + if endpoint is None: + continue + roles, labels = endpoint + cls = endpoint_class(labels) + target_type_counts = Counter(label_kind(label) for label in labels) + paid_type_counts = Counter(label_kind(g) for g in (g1, g2)) + require( + paid_type_counts == target_type_counts, + f"matched word has wrong paid-label type counts: {paid_type_counts} != {target_type_counts}", + ) + word_counts[cls] += 1 + counts_by_endpoint[word] += 1 + first_factor = (g1, x1, y1, n1) + second_factor = (g2, x2, y2, n2) + if not factor_is_rigid(first_factor, roles, labels) or not factor_is_rigid(second_factor, roles, labels): + rigidity_violations[cls] += 1 + if len(first_violation) < 3: + first_violation.append({ + "factor_labels": [list(g1), list(g2)], + "factor_x": [x1, x2], + "factor_y": [y1, y2], + "target_roles": list(roles), + "target_labels": [list(labels[0]), list(labels[1])], + }) + + require(all(counts_by_endpoint[target] > 0 for target in targets), "some two-target endpoint lacks a length-two word") + require( + sum(rigidity_violations.values()) == 0, + "enumerated realizing word violates type-restricted target support: " + + json.dumps(first_violation, sort_keys=True), + ) + total_words = len(factors) ** 2 + expected_idempotents = {2: 6, 3: 28}.get(r) + require(expected_idempotents is not None and len(idempotents) == expected_idempotents, "unexpected idempotent inventory size") + expected_endpoints = (r * (r - 1) // 2) * (len(nonidentity) ** 2) + require(len(targets) == expected_endpoints, "unexpected endpoint inventory size") + + return { + "registers": r, + "rank_one_idempotents": len(idempotents), + "paid_factors": len(factors), + "ordered_length_two_words": total_words, + "literal_two_target_endpoints": len(targets), + "endpoint_counts": dict(sorted(endpoints_by_class.items())), + "realizable_endpoints": len(counts_by_endpoint), + "matching_ordered_words": sum(word_counts.values()), + "matching_words_by_class": dict(sorted(word_counts.items())), + "max_words_for_one_endpoint": max(counts_by_endpoint.values()), + "rigidity_violation_words": sum(rigidity_violations.values()), + "rigidity_violations_by_class": dict(sorted(rigidity_violations.items())), + "first_rigidity_violations": first_violation, + } + + +def run_checks() -> dict[str, object]: + """Run exact full-algebra enumeration and deterministic negative controls.""" + require(valid_group_table(GROUP_TABLE), "group multiplication table failed validation") + noncoordinate_control(2) + noncoordinate_control(3) + return { + "group_order": len(ELEMENTS), + "group_noncommutative_control": True, + "noncoordinate_equal_label_control": True, + "negative_controls": negative_controls(3), + "regular_action_basis_replay": arbitrary_dirty_basis_replay(), + "dimensions": [enumerate_dimension(2), enumerate_dimension(3)], + } + + +if __name__ == "__main__": + print(json.dumps(run_checks(), sort_keys=True, indent=2)) diff --git a/research/semilinear-mixed-tariff/verify.py b/research/semilinear-mixed-tariff/verify.py new file mode 100644 index 0000000000..0977e91288 --- /dev/null +++ b/research/semilinear-mixed-tariff/verify.py @@ -0,0 +1,286 @@ +#!/usr/bin/env python3 +"""Exact finite corroboration of PROOF.md, not proof by sampling. + +Krzysztof Wojt with substantial OpenAI Codex assistance. Apache-2.0. +Standard library, no network/Git dependency and no generated package files. +""" + +from __future__ import annotations + +import hashlib +import itertools +import json +from pathlib import Path +import runpy + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +class Field: + """Polynomial-basis arithmetic; every nonzero inverse is checked.""" + + def __init__(self, degree, polynomial): + require(degree >= 1 and polynomial.bit_length() == degree + 1, + "bad polynomial degree") + self.degree, self.size, self.polynomial = degree, 1 << degree, polynomial + self.table = [[self.multiply(a, b) for b in range(self.size)] + for a in range(self.size)] + self.inverse = [0] + [self.power(a, self.size - 2) + for a in range(1, self.size)] + require(all(self.table[a][self.inverse[a]] == 1 + for a in range(1, self.size)), "reducible polynomial") + + def multiply(self, a, b): + out = 0 + while b: + if b & 1: + out ^= a + b >>= 1 + a <<= 1 + if a & self.size: + a ^= self.polynomial + return out + + def power(self, a, exponent): + result = 1 + while exponent: + if exponent & 1: + result = self.table[result][a] + a = self.table[a][a] + exponent >>= 1 + return result + + +def binary_rank(columns): + pivots = {} + for vector in columns: + while vector: + pivot = vector.bit_length() - 1 + if pivot not in pivots: + pivots[pivot] = vector + break + vector ^= pivots[pivot] + return len(pivots) + + +def field_rank(matrix, field): + a = [list(row) for row in matrix] + row = 0 + for col in range(len(a[0]) if a else 0): + pivot = next((i for i in range(row, len(a)) if a[i][col]), None) + if pivot is None: + continue + a[row], a[pivot] = a[pivot], a[row] + inv = field.inverse[a[row][col]] + a[row] = [field.table[inv][v] for v in a[row]] + for i in range(len(a)): + if i != row and a[i][col]: + scale = a[i][col] + a[i] = [v ^ field.table[scale][w] + for v, w in zip(a[i], a[row])] + row += 1 + return row + + +def apply_binary(columns, vector): + result = 0 + while vector: + bit = vector & -vector + result ^= columns[bit.bit_length() - 1] + vector ^= bit + return result + + +def natural(field, label): + a, j = label + return tuple(field.table[a][field.power(1 << k, 1 << j)] + for k in range(field.degree)) + + +def group_product(field, left, right): + a, j = left + b, k = right + return (field.table[a][field.power(b, 1 << j)], (j + k) % field.degree) + + +def displacement(field, character_field, root, label): + """Actual (p+1)-square rho(g)-I direct-sum chi(g)-1 matrix.""" + columns, p = natural(field, label), field.degree + a = [[0] * (p + 1) for _ in range(p + 1)] + for i in range(p): + for j in range(p): + a[i][j] = ((columns[j] >> i) & 1) ^ (i == j) + a[p][p] = character_field.power(root, label[1]) ^ 1 + return a + + +def rank_one_idempotents(r): + for x in range(1, 1 << r): + for y in range(1, 1 << r): + if (x & y).bit_count() % 2: + yield x, y + + +def paid_displacement(block, x, y, r): + d = len(block) + return [[block[i % d][j % d] if ((x >> (i // d)) & 1) + and ((y >> (j // d)) & 1) else 0 + for j in range(r * d)] for i in range(r * d)] + + +def check_family(p, polynomial, character_degree, character_polynomial, + exhaustive_products): + field, cf = Field(p, polynomial), Field(character_degree, character_polynomial) + root = next(z for z in range(2, cf.size) if cf.power(z, p) == 1) + require(all(cf.power(root, j) != 1 for j in range(1, p)), "nonprimitive character") + labels = [(a, j) for a in range(1, field.size) for j in range(p)] + reps = {g: natural(field, g) for g in labels} + blocks = {g: displacement(field, cf, root, g) for g in labels} + ranks = {"identity": 0, "normal": 0, "outside": 0} + for a, j in labels: + g = a, j + kind = "identity" if g == (1, 0) else "normal" if j == 0 else "outside" + expected = 0 if kind == "identity" else p if kind == "normal" else p - 1 + require(binary_rank([v ^ (1 << k) for k, v in enumerate(reps[g])]) + == expected, "natural rank law") + require(field_rank(blocks[g], cf) == (0 if kind == "identity" else p), + "constant displacement rank") + ranks[kind] += 1 + products = itertools.product(labels, labels) if exhaustive_products else ( + pair for g in labels for h in [(2, 0), (1, 1)] + for pair in [(g, h), (h, g)]) + product_count = 0 + for g, h in products: + product = group_product(field, g, h) + require(tuple(apply_binary(reps[g], v) for v in reps[h]) == reps[product], + "semilinear composition") + require(cf.table[cf.power(root, g[1])][cf.power(root, h[1])] + == cf.power(root, product[1]), "quotient character composition") + product_count += 1 + # Actual field elimination on tensor factors checks scalar extension and + # the rank-one boundary, instead of only summing expected block ranks. + factors = 0 + for g in labels: + if g == (1, 0): + continue + for x, y in rank_one_idempotents(2): + require(field_rank(paid_displacement(blocks[g], x, y, 2), cf) == p, + "paid factor rank") + factors += 1 + return {"p": p, "labels": len(labels), "rank_classes": ranks, + "products": product_count, "product_scope": + "all ordered pairs" if exhaustive_products else "left/right generator pairs", + "paid_factors": factors}, (field, cf, root, blocks) + + +def binary_matrix_product(left, right): + return tuple(apply_binary(left, v) for v in right) + + +def binary_inverse(columns): + r = len(columns) + return tuple(next(x for x in range(1 << r) + if apply_binary(columns, x) == 1 << k) for k in range(r)) + + +def check_scalar_normalization(): + r, checked = 3, 0 + for s in itertools.product(range(8), repeat=r): + if binary_rank(s) != r: + continue + inverse = binary_inverse(s) + require(binary_matrix_product(s, inverse) == (1, 2, 4), "inverse control") + for x, y in rank_one_idempotents(r): + n = tuple(x if (y >> j) & 1 else 0 for j in range(r)) + conjugate = binary_matrix_product(binary_matrix_product(s, n), inverse) + require(binary_rank(conjugate) == 1, "conjugate rank") + require(binary_matrix_product(conjugate, conjugate) == conjugate, + "conjugate idempotence") + require(binary_matrix_product(s, n) == binary_matrix_product(conjugate, s), + "free scalar covariance") + checked += 1 + require(checked == 168 * 28, "complete GL3/idempotent coverage") + return checked + + +def rejected(action, message): + try: + action() + except (ValueError, StopIteration): + return 1 + raise ValueError("negative control accepted: " + message) + + +def check_controls(context): + field, cf, root, blocks = context + count = rejected(lambda: Field(3, 0b1001), "reducible field polynomial") + wrong = [row[:] for row in blocks[(1, 1)]] + wrong[-1][-1] = 0 + count += rejected(lambda: require(field_rank(wrong, cf) == 3, "missing character"), + "omitted character block") + wrong = [row[:] for row in blocks[(2, 0)]] + for row in wrong[:-1]: + for j in range(3): + row[j] = 0 + count += rejected(lambda: require(field_rank(wrong, cf) == 3, "missing natural block"), + "omitted natural block") + # A rank-two gate updates two equal labels in one call: a different model. + block = blocks[(2, 0)] + twice = [[0] * 8 for _ in range(8)] + for t in range(2): + for i in range(4): + for j in range(4): + twice[4*t+i][4*t+j] = block[i][j] + require(field_rank(twice, cf) == 6, "rank-two contrast") + count += rejected(lambda: require(field_rank(twice, cf) == 3, "gate rank"), + "higher-rank gate silently treated as rank one") + # Natural rank alone accepts two normal calls for three outside targets. + # This is a relaxation fixture, NOT a claimed full formal word. + require(3 * 2 >= 2 * 3, "natural-only diagnostic") + count += rejected(lambda: require(0 >= 3, "quotient deficit"), + "missing outside-call count constraint") + composite = Field(9, 0b1000010001) + columns = natural(composite, (1, 3)) + actual = binary_rank([v ^ (1 << k) for k, v in enumerate(columns)]) + require(actual == 6, "composite-degree boundary fixture") + count += rejected(lambda: require(actual + 1 == 9, "prime-degree hypothesis missing"), + "composite degree") + require([z for z in range(cf.size) if cf.power(z, 2) == 1] == [1], + "characteristic-two repeated-root boundary") + count += rejected(lambda: next(z for z in range(2, cf.size) + if cf.power(z, 2) == 1), "p=2 character") + g, h = (1, 1), (2, 0) + incorrect = (field.table[g[0]][h[0]], (g[1] + h[1]) % 3) + count += rejected(lambda: require(group_product(field, g, h) == incorrect, + "twist missing"), "untwisted group law") + return count + + +def main(): + family_stats, contexts = [], [] + for args in [(3, 0b1011, 2, 0b111, True), + (5, 0b100101, 4, 0b10011, True), + (7, 0b10000011, 3, 0b1011, False)]: + stats, context = check_family(*args) + family_stats.append(stats) + contexts.append(context) + scalar_checks = check_scalar_normalization() + controls = check_controls(contexts[0]) + package = Path(__file__).resolve().parent + # Separate implementation: full formal coefficients, no represented ranks. + small = runpy.run_path(str(package / "small_words.py"))["run_checks"]() + hashes = {path.name: hashlib.sha256(path.read_bytes()).hexdigest() + for path in sorted(package.iterdir()) + if path.is_file() and path.suffix in {".py", ".md", ".json"}} + result = {"status": "PASS_SEMILINEAR_MIXED_TARIFF", "families": family_stats, + "scalar_covariances": scalar_checks, "primary_rejection_controls": controls, + "full_formal_small_words": small, "package_sha256": hashes, + "scope": "finite corroboration; universal claims proved in PROOF.md; no new kappa"} + print(json.dumps(result, sort_keys=True, indent=2)) + + +if __name__ == "__main__": + main()