diff --git a/research/odd-five-char2-minrank/PROOF.md b/research/odd-five-char2-minrank/PROOF.md new file mode 100644 index 0000000000..6c87691ca4 --- /dev/null +++ b/research/odd-five-char2-minrank/PROOF.md @@ -0,0 +1,146 @@ +# A strict characteristic-two fitting-rank bound + +This is a scoped proof with exact finite corroboration. Let `K` be any field +of characteristic two and let the labels lie in `F2^5`. Put `j=(1,1,1,1,1)`. +A label is odd when its coordinate sum is one. The complete type set is + +```text +T = {(q,w): q,w are odd and w dot q = 1}. +R = {(q,w) in T: q != j and w != j}. +``` + +Each type occurs once. A matrix `N` indexed by a type set is fitting when +its diagonal entries are nonzero and, for distinct positions `s,t`, + +```text +w_s dot q_t = 1 implies N[s,t] = 0. +``` + +No symmetry, prescribed off-diagonal values, factorization or positivity +is assumed. Binary entries embed in the prime subfield of `K`. + +**Theorem.** Every fitting matrix on `R` has rank at least 22. Every +fitting matrix on `T` has rank at least 53. These are lower bounds; +neither is asserted to be the exact minimum. + +Jose Manuel's PR3512 introduced this odd-type fitting boundary and proved +all-field inequalities. His PR3544 strengthens the odd-dimensional +inequalities and leaves optimal fitting rank open. We use that model, +but do not rely on or recheck either inequality. The characteristic-two +restriction below is essential to the proof and supplies no new rational +fitting-rank bound. + +## 1. Equality in the elementary Hadamard bound + +We first give the elementary linear-algebra argument in any field. Let +`B=W Q^T`, where row `i` of `W` is `w_i^T`, row `i` of `Q` is `q_i^T`, +and the label dimension is `d`. Suppose a fitting matrix has been +normalized to diagonal one, so that its entrywise product with `B` is +the identity. Row scaling by the inverses of the original diagonal +entries makes this normalization without changing rank or zero entries. + +If `N=L H` has rank `r`, define matrices with the indicated entries: + +```text +U[i,(a,k)] = w_i[a] L[i,k], +V[(a,k),i] = q_i[a] H[k,i]. +``` + +Here `1 <= a <= d` and `1 <= k <= r`. Their product has entry +`(UV)[i,j] = (w_i dot q_j) N[i,j]`, so `UV=I_n`. In particular `n<=dr`. +This is the usual Hadamard rank inequality, proved here directly. + +If `n=dr`, both matrices are square and `VU=I_(dr)`. Its `(a,b)` block +has entries + +```text +sum_i q_i[a] w_i[b] H[k,i] L[i,l] = delta_(a,b) delta_(k,l). +``` + +Take its trace over `k=l`. Because +`sum_k H[k,i] L[i,k] = N[i,i] = 1`, this forces + +```text +sum_i q_i w_i^T = r I_d. (1) +``` + +Thus (1) is a necessary condition for saturation. The argument does +not assume that `N` has binary entries. It holds over the full field `K`. +It is an elementary consequence of tensor factorization and cyclic +trace; no claim of worldwide novelty for that general observation is made. + +## 2. The regular type sum + +There are sixteen odd vectors, fifteen different from `j`. For fixed +odd `q != j`, the two equations + +```text +j dot w = 1, q dot w = 1 +``` + +are independent, so they define an affine three-space of eight vectors. +It contains `j`, since `q` is odd and `j dot j=1`. Removing `j` leaves +seven regular sinks. Consequently `|R|=15*7=105`. + +The sum of the vectors in any affine three-space over `F2` is zero. +Removing `j` therefore makes the seven-vector fiber sum equal to `j`. +Likewise the sum of all sixteen odd vectors is zero, so the sum of +the fifteen odd `q != j` is `j`. In characteristic two this gives + +```text +sum_((q,w) in R) q w^T + = sum_(odd q != j) q j^T + = j j^T + = J_5, (2) +``` + +where `J_5` is the all-ones matrix. The verifier independently enumerates +all 105 types and all 25 entries of (2), as well as the seven-element +fibers. The preceding affine-space argument proves the formula without +depending on extrapolation from that enumeration. + +## 3. The strict lower bound + +For `R`, the binary matrix `B[s,t]=w_s dot q_t` factors through `K^5`, +because the field has characteristic two. Section 1 gives +`rank N >= 105/5 = 21`. If its rank were 21, equation (1) would force +the sum in (2) to be `21 I_5 = I_5`. But `J_5 != I_5` over every field: +each off-diagonal entry is one on the left and zero on the right. +Thus rank 21 is impossible, and integrality proves `rank N >= 22`. + +## 4. Adding the special types + +There are sixteen types with `q=j`, sixteen with `w=j`, and one in +both sets. Thus `|T minus R|=31` and `|T|=136`. + +For a type with `q=j`, the corresponding column of `B` is all ones. +Its column of a fitting `N` is zero except at its nonzero diagonal. +For a type with `w=j`, the same statement holds for its row. Deleting +any such row and its matching column reduces rank by exactly one: +expand around that isolated nonzero column or row, or perform ordinary +invertible elimination. Deletion does not change any remaining entry. +Repeat for all 31 special positions. This proves the exact identity + +```text +rank N = 31 + rank N[R,R]. +``` + +The bound from section 3 now gives `rank N >= 31+22=53`. + +## 5. Scope and verification + +The universal quantifier covers arbitrary entries in every +characteristic-two field. The type domains are the complete finite sets +defined above, with one occurrence per type. No bound for arbitrary +nonuniform multiplicities, characteristic-zero matrices or a native +supplier follows. The claim is a scoped obstruction, not a failed-search +extrapolation, a sharp optimum or a multiplication theorem. + +The replay enumerates the new moment certificate and checks exact tensor +inverses and their block traces in F2, F4 and F8. The tight controls use +one or two disjoint five-port coordinate classes, including repeated +types and nonunit diagonal values before normalization. Two nontrivial +fitting fixtures of ranks 132 and 101 corroborate the special-port rank +addition, including allowed entries between special and regular positions. These +finite checks support the written proof; they do not enumerate all +fitting matrices or replace the proof over arbitrary fields. diff --git a/research/odd-five-char2-minrank/README.md b/research/odd-five-char2-minrank/README.md new file mode 100644 index 0000000000..c6eccbfb97 --- /dev/null +++ b/research/odd-five-char2-minrank/README.md @@ -0,0 +1,126 @@ +# Strict rank bounds for the complete five-bit odd-type mask + +Scoped mathematical proof with exact finite corroboration. Over every +field of characteristic two, the complete five-bit odd-type mask has +fitting rank at least **22 on its 105 regular types**, and at least +**53 on all 136 admissible types**. These are lower bounds, not exact minima. +No new kappa is claimed. + +Write `j=11111` and let a type be `(q,w)` with both binary labels odd and +`w dot q=1`. A regular type has `q != j` and `w != j`. Each type occurs +once. A fitting matrix has arbitrary nonzero diagonal and must have +`N[s,t]=0` whenever `s != t` and `w_s dot q_t=1`. It may be asymmetric +and may have arbitrary entries in the full coefficient field. + +The elementary Hadamard rank bound gives 21 on the regular types. +The new step excludes equality. After diagonal normalization, equality +would make the two square tensor factors inverses. Taking block traces +forces `sum(q w^T)=21 I_5=I_5`. The actual type sum is `J_5`, the all-ones +matrix. Its off-diagonal entries contradict this requirement. The 31 +all-ones-source/sink types add rank individually, improving the associated +full-mask lower bound from 52 to 53. [PROOF.md](PROOF.md) gives the argument. + +## Predecessors and scope change + +Jose Manuel / jmbarrancoml's [PR3512](https://github.com/CrocSwap/integer-mult-bounds/pull/3512) +and [PR3544](https://github.com/CrocSwap/integer-mult-bounds/pull/3544) supply +the odd-type fitting model and leave optimal fitting rank open. PR3544, +head `6cfa4333a2e593ea092fe4bda686bb172b5b6d22`, proves the stronger +all-field regular coefficient `17/105` in dimension five. That theorem +is cited, not audited or replayed. The new result concerns the different, +characteristic-two boundary; it does not improve the rational bound. +[SOURCES.json](SOURCES.json) pins the main-retained predecessor documents +as provenance. The verifier imports no predecessor code or data. + +Canonical base is `ff3cc58e370d0f678e529246f8c73e8094e18fcf`, priority +revision 7. The complex-rank-shape-decoder card is explicitly changed to +this algebraic side question. It closes a finite-field equality case +before a changed fitting model is used as a small-unit surrogate. This +is not a decoder construction or evidence of a better paid supplier bill. +The card's historical first command fails on the selected schema with +`KeyError: 'complex_profile'`; the current schema-aware +`scripts/research_selected_baseline.py` orientation passes. Neither is +part of the new proof. + +The [advance claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19147080) +proposed exact values 21 and 52. The +[scope update](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19147122) +records their impossibility and the delivered strict lower bounds. +Targeted main-tree and merged-PR searches, live open PR bodies and +Discussion claims, recent same-account work and local reservations were +checked. The broad scan covers 311 open PRs and 4,484 Discussion records; +sparse local notes and unpublished work remain incomplete coverage. + +## Reproduce + +From the repository root with CPython 3.12 and the standard library: + +```sh +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B -W error research/odd-five-char2-minrank/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -O -B -W error research/odd-five-char2-minrank/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/odd-five-char2-minrank +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/odd-five-char2-minrank --check-source-history +``` + +Any CPython 3.12 installation can replace the local interpreter path. +The expected marker is: + +```text +PASS_ODD_FIVE_CHAR2_MINRANK regular_types=105 regular_lower=22 full_types=136 full_lower=53 tensor_fixtures=18 controls=7 +``` + +The replay enumerates the complete 136-type domain, its 105 regular +positions, fifteen seven-element fibers and all 25 moment entries. +Eighteen tight tensor fixtures over F2/F4/F8 check both inverse products, +block traces and diagonal normalization, including nonbinary field +coefficients and repeated types. Two full-mask fixtures check exact +rank addition `132=31+101`. Seven rejection controls cover the impossible +rank-21 moment, wrong cardinality, a forbidden entry, zero diagonal, +missing normalization, corrupted tensor and zero inversion. + +The verifier writes nothing and emits a fresh receipt bound to all six +package files and the executed results. Checks remain active with `-O`. +The written proof supplies the arbitrary-field quantifier; the replay +neither enumerates all fitting matrices nor certifies a formal proof kernel. + +## Limitations and engineering notes + +Characteristic zero and odd characteristic, nonuniform type multiplicities, +sharpness at ranks 22/53, physical factors, frames, ownership, routing, +restoration, precision, stock, compiler and complete supplier costs remain +outside this result. No selected-frontier update or complete multiplication +theorem is claimed. Independent human and formal proof-kernel review are +unclaimed. Lean, Docker and the selected supplier cold replay are unrun. + +The verifier has no recursion, dynamic code, subprocess or network calls. +Its functions are below 60 lines. It bounds matrices by 136 rows and +columns, tensor matrices by ten rows and columns, fields by eight elements, package reads +by six files of at most one MiB, and all loops by these fixed domains. +Managed Python allocation is a deviation from static allocation; the +finite domains bound live matrix storage. Seven fixed rejection callbacks +are a bounded deviation from avoiding indirect calls. Warning-strict normal +and optimized replay and in-memory compilation supply diagnostics. + +## Open next questions + +1. Is the regular characteristic-two minimum 22? First seek a cover of the + 105 types by 22 compatible classes, or an explicit rank-22 factorization. + Attainment is the missing obligation; a lower bound alone cannot supply it. +2. Can the full regular mask admit rank below 22 in characteristic zero? + Start with a rational factorization respecting the same zeros, using + PR3544's all-field lower bound as a cited premise. The five-column + factorization of the binary parity mask does not survive that field change. + +Structured questions are in [TASK.json](TASK.json). + +## Credit + +This contribution was produced by Nick Petalas. Jose Manuel / jmbarrancoml +supplies the odd-type model, all-field triangular/flag bounds and explicit +open fitting-rank question in PR3512/3544. Philippe Van Velzen supplies the +small-unit setting and prior acyclic/Hadamard method; DreamingOfClouds +supplies the related symmetric-mask Lagrangian and pairing-rank lineage. +The rank inequality, tensor factorization and cyclic trace are classical. +The new contribution is the strict characteristic-two bound for these +complete type sets and its stated proof and exact corroboration. +Predecessor files and credit are unchanged. Apache-2.0. diff --git a/research/odd-five-char2-minrank/SOURCES.json b/research/odd-five-char2-minrank/SOURCES.json new file mode 100644 index 0000000000..1ff43aab34 --- /dev/null +++ b/research/odd-five-char2-minrank/SOURCES.json @@ -0,0 +1,30 @@ +{ + "schema_version": 1, + "base_commit": "ff3cc58e370d0f678e529246f8c73e8094e18fcf", + "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/odd-unit-triangular-rank/PROOF.md", + "usage": "provenance", + "git_blob": "f6ed16234cd1b413efd64ab9b810216051a2d38e", + "sha256": "e856fe9e4e7244ef8c18d3d5709fb12023425809042ffe2008038b431d156701" + }, + { + "path": "research/odd-unit-triangular-rank/README.md", + "usage": "provenance", + "git_blob": "ba317318408e91284bc8551fd8704bdac4459f6e", + "sha256": "bd627569e44fc7b2a37f339ecf5b19170cb00fbafa5f4607bb8a8d3904b50868" + } + ] +} diff --git a/research/odd-five-char2-minrank/TASK.json b/research/odd-five-char2-minrank/TASK.json new file mode 100644 index 0000000000..ba2cb48f62 --- /dev/null +++ b/research/odd-five-char2-minrank/TASK.json @@ -0,0 +1,78 @@ +{ + "schema_version": 1, + "task_id": "complex-rank-shape-decoder", + "priority_revision": 7, + "base_commit": "ff3cc58e370d0f678e529246f8c73e8094e18fcf", + "original_card": { + "id": "complex-rank-shape-decoder", + "question": "Can a decoder deliver the local paid mass in fewer, larger-rank children (block frame climbs instead of rank-1 to rank-3 steps)?", + "starting_points": [ + "docs/research/research-family-status.md", + "research/complex-local-word-ceiling/README.md", + "research/complex-decoder-field-extension-seed44/README.md", + "research/complex-frame-pair-decoders/README.md", + "research/selected-k8-unrestricted-ends/README.md", + "research/eisenstein-reduction-copy-floor/README.md" + ], + "methods": [ + "Find one exact small decoding identity whose frame path climbs in blocks, and price its complete per-call profile.", + "Bound the best effective child rank achievable for one fixed support alphabet, including copies, frames and restoration." + ], + "acceptance_gate": "A per-call local profile, with all copied information, frames and restoration counted, whose ceiling exceeds the selected word's by at least 5%; masked or overcomplete supports must change an assumption of the eight-term all-pairs bound. 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", + "research/complex-local-word-ceiling/verify.py" + ], + "expected": "PASS_COMPLEX_LOCAL_WORD_CEILING", + "inspect": "Read the selected word's per-call local profile, its packing ceiling and the lever table; run levers.py for the ideal budget of the lever you target.", + "scope": "Positive control and planning budget only; this is not a new construction or full cold replay." + }, + "first_experiment": "Before any synthesis, write the candidate per-call local profile (and centre charge / unpaid coordinates if changed) and screen it with ceiling.ceiling(); reject it if even the ideal ceiling does not beat the selected word's by your stated margin. Ideal budget: rank-16 delivery is 2.31x (levers.py).", + "bottleneck_link": "Rank-1 children are about half of recursive cost; the selected word's effective child rank is about 3.9. Larger-rank delivery lowers recursive cost per unit of paid mass.", + "allowed_variations": [ + "One masked, overcomplete or block decoder family with exact labels and supports.", + "A scoped lower bound on effective rank for one alphabet.", + "If the coverage law, template or guard changes, derive an applicable fully charged replacement bound instead of applying the incumbent ceiling outside its scope." + ], + "scope_change_triggers": [ + "Repacking idle remainders of an unchanged word (covered by the packing ceiling).", + "Repeating the eight-term all-pairs search inside its proved scope.", + "Only changing helper terminal subspaces and monotone frames within the fixed scalar word, entrances and cleanup contract already covered by #1995/#2013.", + "Searching below C=40 in the #2017 Eisenstein binary scalar-rectangle or fixed-support block-linear additive pairing model; specify a changed premise instead. This bound does not cover every complex decoder.", + "Continuing a partial cost improvement while leaving the same unpriced consumer, restoration or central-readout obligation unresolved; refresh the family expansion decision first. Local product-retiming evidence has a narrow scope and is not a ban on changed graphs or contracts." + ], + "overlap_terms": [ + "rank shape", + "block climb", + "masked decoder", + "overcomplete", + "effective rank" + ] + }, + "scope_status": "changed", + "actual_scope": "Prove strict characteristic-two fitting-rank lower bounds 22 and 53 for the complete five-bit regular and full odd-type masks.", + "scope_change_reason": "Replace decoder synthesis with the explicitly open algebraic fitting-rank boundary in Jose Manuel PR3512/3544. This is a finite-field side result, not a supplier or rational decoder improvement.", + "bottleneck_link": "A strict finite-field rank obstruction prevents a saturated low-rank surrogate from being mistaken for an attainable small-unit fitting pattern; rational rank and physical costs remain separate.", + "budget_minutes": 60, + "stop_rule": "Ship the first verified original lower bound. Do not pursue attainment or larger dimensions.", + "outcome": "completed", + "evidence": "PROOF.md proves the bounds over every characteristic-two field. verify.py enumerates 136 types, the regular moment, 18 tensor fixtures, two rank-addition fixtures and seven rejection controls.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "Is the regular characteristic-two fitting minimum 22?", + "why_it_matters": "This would turn the strict obstruction into an exact value.", + "first_step": "Seek a cover of all 105 regular types by 22 compatible classes or a literal rank-22 factorization.", + "blocked_by": "No attaining matrix is supplied." + }, + { + "question": "Can the full regular mask have fitting rank below 22 in characteristic zero?", + "why_it_matters": "The retained bit-window application uses rational rather than characteristic-two rank.", + "first_step": "Search rational factors with the same zero pattern, citing PR3544 as the all-field lower-bound premise.", + "blocked_by": "The binary parity mask does not retain its five-column factorization in characteristic zero." + } + ] +} diff --git a/research/odd-five-char2-minrank/VERIFY.json b/research/odd-five-char2-minrank/VERIFY.json new file mode 100644 index 0000000000..1270c0e858 --- /dev/null +++ b/research/odd-five-char2-minrank/VERIFY.json @@ -0,0 +1,32 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [], + "commands": [ + { + "argv": [ + "{python}", + "-B", + "-W", + "error", + "{package}/verify.py" + ], + "timeout_seconds": 60, + "checks": "Complete type moment, tight tensor inverses, rank addition and seven rejecting controls." + }, + { + "argv": [ + "{python}", + "-O", + "-B", + "-W", + "error", + "{package}/verify.py" + ], + "timeout_seconds": 60, + "checks": "The same complete check with optimization enabled; checks use explicit exceptions." + } + ] +} diff --git a/research/odd-five-char2-minrank/verify.py b/research/odd-five-char2-minrank/verify.py new file mode 100644 index 0000000000..9e6b9c8981 --- /dev/null +++ b/research/odd-five-char2-minrank/verify.py @@ -0,0 +1,261 @@ +#!/usr/bin/env python3 +"""Exact finite ingredients and tensor controls for the written rank proof.""" + +import hashlib +import json +import platform +from pathlib import Path + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def dot(x, y): + return (x & y).bit_count() % 2 + + +def multiply(a, b, order): + require(order in (2, 4, 8), "unsupported field") + require(0 <= a < order and 0 <= b < order, "field element out of range") + modulus = {2: 3, 4: 7, 8: 11}[order] + value = 0 + for _ in range(3): + if b & 1: + value ^= a + b >>= 1 + a <<= 1 + if a & order: + a ^= modulus + return value + + +def inverse(a, order): + require(0 < a < order, "inverse of zero or invalid element") + for b in range(1, order): + if multiply(a, b, order) == 1: + return b + raise ValueError("field inverse missing") + + +def identity(n): + require(1 <= n <= 136, "identity dimension out of range") + return [[int(i == j) for j in range(n)] for i in range(n)] + + +def product(left, right, order): + require(1 <= len(left) <= 136 and 1 <= len(right) <= 136, "matrix size") + inner, width = len(right), len(right[0]) + require(1 <= width <= 136, "matrix width") + require(all(len(row) == inner for row in left), "product dimensions") + require(all(len(row) == width for row in right), "ragged right matrix") + result = [[0] * width for _ in left] + for i, row in enumerate(left): + for k, a in enumerate(row): + if a: + for j, b in enumerate(right[k]): + result[i][j] ^= multiply(a, b, order) + return result + + +def rank(matrix, order): + require(1 <= len(matrix) <= 136, "rank row bound") + width = len(matrix[0]) + require(1 <= width <= 136, "rank column bound") + require(all(len(row) == width for row in matrix), "ragged rank input") + rows = [row[:] for row in matrix] + pivot = 0 + for col in range(width): + candidates = [i for i in range(pivot, len(rows)) if rows[i][col]] + if not candidates: + continue + chosen = candidates[0] + rows[pivot], rows[chosen] = rows[chosen], rows[pivot] + scale = inverse(rows[pivot][col], order) + rows[pivot] = [multiply(x, scale, order) for x in rows[pivot]] + for i in range(pivot + 1, len(rows)): + scale = rows[i][col] + if scale: + rows[i] = [x ^ multiply(scale, y, order) + for x, y in zip(rows[i], rows[pivot])] + pivot += 1 + if pivot == len(rows): + break + return pivot + + +def mask(types): + require(1 <= len(types) <= 136, "type count bound") + require(all(0 < q < 32 and 0 < w < 32 for q, w in types), "label bound") + return [[dot(w, q) for q, _ in types] for _, w in types] + + +def outer_sum(types): + return [[sum(((q >> a) & 1) * ((w >> b) & 1) for q, w in types) % 2 + for b in range(5)] for a in range(5)] + + +def fitting(matrix, binary_mask): + n = len(matrix) + require(len(binary_mask) == n, "fitting dimensions") + require(all(len(row) == n for row in matrix + binary_mask), "square input") + require(all(matrix[i][i] for i in range(n)), "zero diagonal") + require(all(not binary_mask[i][j] or not matrix[i][j] + for i in range(n) for j in range(n) if i != j), "forbidden entry") + + +def normalized(matrix, order): + return [[multiply(x, inverse(row[i], order), order) for x in row] + for i, row in enumerate(matrix)] + + +def geometry(): + odd = [x for x in range(32) if dot(x, x)] + all_types = [(q, w) for q in odd for w in odd if dot(q, w)] + regular = [(q, w) for q, w in all_types if q != 31 and w != 31] + special = [(q, w) for q, w in all_types if q == 31 or w == 31] + require((len(odd), len(all_types), len(regular), len(special)) == + (16, 136, 105, 31), "type census") + require(all(sum(q == x for q, _ in regular) == 7 for x in odd if x != 31), + "regular fiber count") + require(outer_sum(regular) == [[1] * 5 for _ in range(5)], "regular moment") + binary_mask = mask(all_types) + require(rank(binary_mask, 2) == 5, "mask rank") + for i, (q, w) in enumerate(all_types): + if q == 31: + require(all(row[i] == 1 for row in binary_mask), "special column") + if w == 31: + require(all(x == 1 for x in binary_mask[i]), "special row") + return all_types, regular, binary_mask + + +def saturation_possible(types, paid_rank): + require(len(types) == 5 * paid_rank, "not a saturation case") + expected = [[(paid_rank % 2) * int(a == b) for b in range(5)] + for a in range(5)] + require(outer_sum(types) == expected, "saturation moment obstruction") + + +def tensor_fixture(order, copies, seed): + require(copies in (1, 2) and seed in range(3), "fixture bounds") + types = [(1 << a, 1 << a) for _ in range(copies) for a in range(5)] + n = len(types) + right = [[0] * n for _ in range(copies)] + left = [[0] * copies for _ in range(n)] + for i in range(n): + b = 1 + (i + seed) % (order - 1) + left[i][i // 5] = inverse(b, order) + right[i // 5][i] = b + matrix = product(left, right, order) + scales = [1 + (2 * i + seed) % (order - 1) for i in range(n)] + raw = [[multiply(scales[i], x, order) for x in row] + for i, row in enumerate(matrix)] + fitting(raw, mask(types)) + require(normalized(raw, order) == matrix, "diagonal normalization") + require(rank(matrix, order) == copies, "fixture rank") + u = [[((w >> a) & 1) * left[i][k] + for a in range(5) for k in range(copies)] + for i, (_, w) in enumerate(types)] + v = [[((q >> a) & 1) * right[k][j] for j, (q, _) in enumerate(types)] + for a in range(5) for k in range(copies)] + require(product(u, v, order) == identity(n), "forward tensor inverse") + reverse = product(v, u, order) + require(reverse == identity(n), "reverse tensor inverse") + traces = [[0] * 5 for _ in range(5)] + for a in range(5): + for b in range(5): + for k in range(copies): + traces[a][b] ^= reverse[a * copies + k][b * copies + k] + require(traces == outer_sum(types), "block trace identity") + saturation_possible(types, copies) + return raw, u, v + + +def rank_addition(all_types, binary_mask, order): + n = len(all_types) + matrix = identity(n) + coordinate = [i for i, (q, w) in enumerate(all_types) + if q == w and q.bit_count() == 1] + require(len(coordinate) == 5, "coordinate class") + for i in coordinate: + for j in coordinate: + matrix[i][j] = 1 + for i, (q, w) in enumerate(all_types): + for j, (r, z) in enumerate(all_types): + if not binary_mask[i][j] and 31 in (q, w, r, z): + matrix[i][j] = (3 * i + 5 * j + 1) % order + fitting(matrix, binary_mask) + indices = [i for i, (q, w) in enumerate(all_types) if q != 31 and w != 31] + regular = [[matrix[i][j] for j in indices] for i in indices] + total_rank, regular_rank = rank(matrix, order), rank(regular, order) + require(total_rank == 31 + regular_rank, "special rank addition") + require((total_rank, regular_rank) == (132, 101), "fixture ranks") + return [order, total_rank, regular_rank] + + +def rejected(call, message): + try: + call() + except ValueError as error: + require(message in str(error), "wrong rejection reason") + return + raise ValueError("negative control accepted") + + +def controls(regular, binary_mask): + rejected(lambda: saturation_possible(regular, 21), "moment obstruction") + rejected(lambda: saturation_possible(regular[:-1], 21), "saturation case") + bad = identity(136) + i, j = next((i, j) for i in range(136) for j in range(136) + if i != j and binary_mask[i][j]) + bad[i][j] = 1 + rejected(lambda: fitting(bad, binary_mask), "forbidden entry") + bad[i][i] = 0 + rejected(lambda: fitting(bad, binary_mask), "zero diagonal") + raw, u, v = tensor_fixture(4, 1, 0) + require(raw != normalized(raw, 4), "normalization control has no effect") + raw_product = [[x * int(i == j) for j, x in enumerate(row)] + for i, row in enumerate(raw)] + rejected(lambda: require(raw_product == identity(5), "unnormalized identity"), + "unnormalized identity") + v[0][0] ^= 1 + rejected(lambda: require(product(u, v, 4) == identity(5), "mutated tensor"), + "mutated tensor") + rejected(lambda: inverse(0, 4), "inverse of zero") + return 7 + + +def receipt(results): + package = Path(__file__).resolve().parent + names = ("README.md", "PROOF.md", "TASK.json", "SOURCES.json", "VERIFY.json", "verify.py") + hashes = {} + for name in names: + path = package / name + require(path.stat().st_size <= 1024 * 1024, "package file size bound") + hashes[name] = hashlib.sha256(path.read_bytes()).hexdigest() + return {"files_sha256": hashes, "results": results, + "result_sha256": hashlib.sha256(json.dumps(results, sort_keys=True).encode()).hexdigest(), + "python": platform.python_version()} + + +def main(): + all_types, regular, binary_mask = geometry() + fixtures = 0 + for order in (2, 4, 8): + for copies in (1, 2): + for seed in range(3): + tensor_fixture(order, copies, seed) + fixtures += 1 + additions = [rank_addition(all_types, binary_mask, order) for order in (2, 4)] + count = controls(regular, binary_mask) + results = {"regular_types": 105, "regular_lower": 22, "full_types": 136, + "full_lower": 53, "mask_rank_F2": 5, "tensor_fixtures": fixtures, + "rank_addition_fixtures": additions, "controls": count} + print(json.dumps(receipt(results), sort_keys=True)) + print("PASS_ODD_FIVE_CHAR2_MINRANK regular_types=105 regular_lower=22 " + f"full_types=136 full_lower=53 tensor_fixtures={fixtures} controls={count}") + + +if __name__ == "__main__": + main()