diff --git a/research/polynomial-cost-distribution/PROOF.md b/research/polynomial-cost-distribution/PROOF.md new file mode 100644 index 0000000000..6a682dab6d --- /dev/null +++ b/research/polynomial-cost-distribution/PROOF.md @@ -0,0 +1,153 @@ +# The joint degree-cost law over finite polynomial fields + +Let K be a field, R=K[t], and use two data roles with no auxiliary roles. +A paid factor is I+u y^T, where u is in R^2 and y is in K^2. +Every matrix in GL2(K) is free, at any position in a word. Products are +written in algebraic order. For a nonzero polynomial matrix M, its entry +degree is the maximum degree of its entries. The cost c(M) is the smallest +number of paid factors in any such word for M. + +## The result + +For K=F_q, write g_q=(q^2-1)(q^2-q). For every D>=1 and 1<=r<=D, +the exact number of M in GL2(F_q[t]) having entry degree D and cost r is + + N_q(D,r) = g_q (q+1) (q-1)^r q^(D-1) binom(D-1,r-1). + +There are no other costs at degree D. At degree zero there are g_q targets, +all with cost zero. Summing over r gives + + N_q(D) = g_q (q^2-1) q^(2D-2), + #{M : degree(M)<=D} = g_q q^(2D). + +Thus if M is uniform among the invertible targets of exact degree D, + + c(M)-1 ~ Binomial(D-1, (q-1)/q), + E[c(M)] = 1+(D-1)(q-1)/q, + Var[c(M)] = (D-1)(q-1)/q^2. + +This is a scoped algebraic counting proof. It supplies no physical supplier +or multiplication exponent. The count and distribution extend the binary +degree-four census in Nick Petalas's #4763. The polynomial-matrix presentation +and degree method retain Hirosi Nagao's classical credit, *On GL(2,K[x])*, +1959, Theorem 2 and its proof. The following argument gives the needed cost +reduction explicitly rather than claiming a new group presentation. + +## 1. Constant-free directional factors over an arbitrary field + +Choose one representative y=(a,b) of each line in the projective row line +P^1(K), and put v_y=(-b,a)^T, N_y=v_y y^T. Then N_y^2=0. Define + + T_y(f)=I+f N_y, f in tK[t]. + +Every nonidentity such matrix costs at most one. We first show that every +invertible paid factor reduces to one such factor and a free map. + +Since K[t] is commutative, an invertible product has invertible factors. +The determinant of I+u y^T is 1+y^T u. The only units of K[t] are the +nonzero constants. For y!=0, normalize its projective representative by +rescaling u. Write u=u_0+w with u_0=u(0). Invertibility implies y^T w=0, +so w=f v_y for one f in tK[t]. Let F_0=I+u_0 y^T. It is a free map, +and F_0 v_y=v_y. Consequently + + I+u y^T = F_0 T_y(f). + +The case y=0 is identity. If f=0 the entire factor is free. This also +shows why singular factors cannot yield a cheaper invertible target. + +Conjugation by a free S sends N_y to a nonzero scalar multiple of N_z, +where z is the chosen representative of y^T S^-1. Both matrices have +the same one-dimensional image and kernel, so that scalar is in K^*. +It can be absorbed into f. The scalar need not be one when q>2. + +Move free maps to the right, remove constant coefficients, and merge +adjacent factors with the same projective direction using +T_y(f)T_y(h)=T_y(f+h). Delete zero coefficients. Every invertible word +therefore reduces, without increasing its paid count, to + + T_(y1)(f1) ... T_(yr)(fr) S, + +with S in GL2(K), each f_i nonzero in tK[t], and adjacent y_i distinct. + +## 2. Degree, uniqueness and exact cost + +For distinct directions y,z the scalar y^T v_z is nonzero. In the product +of a reduced sequence of N_y, all consecutive contractions are nonzero. +The product is a nonzero rank-one matrix. If d_i=deg f_i>=1, the unique +term of degree sum d_i in the expanded product of the T_y(f_i) is the +term taking f_i N_(yi) from every factor. Its leading matrix is nonzero. +Every other term has smaller degree. Right multiplication by S preserves +a nonzero leading matrix, so + + degree(T_(y1)(f1) ... T_(yr)(fr) S) = d_1+...+d_r. + +In particular a nonempty reduced product cannot be constant. The endpoint +S is M(0). To compare two reduced expressions for the same M, cancel these +free endpoints and form the inverse of one product times the other. +Here T_y(f)^-1=T_y(-f). Cancel their common initial factors in the middle +of the concatenation. At the first mismatch, distinct directions stay +distinct, or equal directions merge to a nonzero coefficient. All adjacent +directions in the remaining sequence are distinct. Unless the expressions +agree completely, this gives a nonempty reduced word equal to identity, +contradicting the degree statement. The expression is unique. + +Its length r is its exact paid cost: it is itself an r-factor word, and +every other word reduces to that unique expression without increasing +its number of paid factors. This excludes cheaper words of arbitrary +polynomial degrees, with arbitrary free maps inserted. + +Every GL2(K[t]) matrix is reachable. Euclidean reduction of its first +column uses free swaps and paid polynomial shears. Its gcd is a nonzero +constant because the determinant is a unit. A free scaling then makes +that column (1,0)^T. The remaining invertible triangular matrix reduces +using a free diagonal map and a paid shear. Polynomial division decreases +the remainder degree, so this procedure terminates. This is the usual +classical generation argument, included to establish census completeness. + +## 3. Count the unique expressions + +There are q+1 choices of first direction and q choices at every later +factor. At length r this gives (q+1)q^(r-1) direction sequences. +The positive degrees d_1+...+d_r=D have binom(D-1,r-1) compositions. +For any fixed d_i, the number of zero-constant polynomials of degree +exactly d_i is (q-1)q^(d_i-1). Their product is (q-1)^r q^(D-r). +Finally there are g_q choices of free endpoint S. + +Multiplying these independent choices proves N_q(D,r). Uniqueness ensures +that this counts targets rather than words with multiplicity. Every listed +word has exact degree D and exact cost r. The generation argument proves +that no invertible target is omitted. + +The binomial theorem gives + + sum_(r=1)^D (q-1)^r binom(D-1,r-1) = (q-1)q^(D-1). + +This proves the exact-degree total. Summing the resulting geometric +series over degrees zero through D gives g_q q^(2D). Dividing the joint +count by the exact-degree total gives + + Pr(c(M)=r) = binom(D-1,r-1) (q-1)^(r-1) / q^(D-1), + +which is the stated binomial law, including D=1. Its expectation and +variance follow from that law. No independence assertion about a different +sampling measure, such as uniform paid words, is made. + +## Attribution and scope + +This contribution was produced by Nick Petalas. The new contribution is +the explicit all-q joint degree-cost count and its probability law. The +binary normal-form cost proof and finite census are credited to Nick +Petalas #4763; #4276/#4243 provide the preceding right-vector questions +and free-map normal form. Nagao's presentation and degree method are +classical inputs, with [the original paper](https://www.i-repository.net/contents/osakacu/sugaku/DB-M-010-02-04.pdf) +as the primary source. ToikY #4334 and Nick Petalas #4601/#4749 supply the +local-product and semilocal comparisons. Wentao Li #4099 following #2513 +supplies the right-vector alphabet lineage. Those results are cited, not +audited here. No new classical group-presentation theorem is claimed. + +Only two roles, one-variable polynomial coefficients and free base-field +maps are covered. Singular endpoints, multivariate algebras and restored +auxiliary roles are not classified. Preparation, conversion, control, +routing, precision, restoration, stock and a complete physical consumer +are unpriced. This is not supplier admission or a complete multiplication +theorem. Independent human and formal proof-kernel review are unclaimed. diff --git a/research/polynomial-cost-distribution/README.md b/research/polynomial-cost-distribution/README.md new file mode 100644 index 0000000000..315a40de7c --- /dev/null +++ b/research/polynomial-cost-distribution/README.md @@ -0,0 +1,126 @@ +# Exact polynomial degree-cost distribution + +For the two-role alphabet I+u y^T over F_q[t], with y over F_q and free +GL2(F_q) maps anywhere, the paid cost of a uniform invertible target of +exact entry degree D>=1 satisfies + + cost(M)-1 ~ Binomial(D-1, (q-1)/q). + +Writing g_q=(q^2-1)(q^2-q), the exact number with cost r is + + g_q (q+1) (q-1)^r q^(D-1) binom(D-1,r-1), 1<=r<=D. + +The mean is 1+(D-1)(q-1)/q and the variance is (D-1)(q-1)/q^2. +There are g_q(q^2-1)q^(2D-2) targets of exact degree D, and +g_q q^(2D) of degree at most D. Degree-zero targets are the g_q free maps. + +This is a scoped algebraic counting proof with finite corroboration. +[PROOF.md](PROOF.md) extends #4763's binary constant-free cost reduction +to general fields and counts its unique expressions. The contribution is +the all-q joint degree-cost count and binomial law. The classical matrix +presentation and degree method retain Nagao's credit. No new group +presentation, native supplier, multiplication theorem or kappa is claimed. + +## Evidence and reproduction + +The standard-library verifier independently enumerates determinant-unit +matrices by grouping polynomial products with equal nonconstant tails. +It compares that complete set with literal reduced-factor products and +free endpoints, rejecting duplicate expressions and checking every joint +degree-cost count. The bounded censuses are: + +- F2, entry degree at most four: 1,536 targets. +- F3, entry degree at most two: 3,888 targets. +- F4, entry degree at most two: 46,080 targets, using F2[z]/(z^2+z+1). +- F5, entry degree at most one: 12,000 targets. + +The 63,504 targets require 135,570 product-tail comparisons. These are +enumerated counts, not a count of every rejected polynomial matrix. +All 924 invertible degree-one paid parameter tuples across the four fields +pass constant splitting; all free conjugations pass with their required +nonzero scalar. Eight control groups cover merging, cancellation, constants, +nonunit determinants, singular endpoints, conjugation scaling, the binary +degree-four compatibility vector and an incorrect field weight. Exact +normalization, mean and variance checks cover 480 integer pairs 2<=q<=16, +1<=D<=32. Non-prime-power q in that last check tests a numerical identity, +not a nonexistent finite field. + +From the repository root, using CPython 3.12: + +```sh +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B -W error research/polynomial-cost-distribution/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -O -B -W error research/polynomial-cost-distribution/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/polynomial-cost-distribution +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/polynomial-cost-distribution --check-source-history +``` + +Another CPython 3.12 path can replace the local interpreter. Expected marker: + +```text +PASS_POLYNOMIAL_COST_DISTRIBUTION targets=63504 fields=4 probability_cases=480 controls=8 no_new_kappa +``` + +The first output line is a generated receipt containing the census and +SHA256 hashes of all six package files. The verifier also checks the +predecessor proof against its hash in SOURCES.json. The receipt is emitted +to stdout. No handwritten receipt or generated evidence file is committed. + +The card's initial 945-pairing positive control passed. Source-bound selected +metadata orientation passed after materializing its sparse omitted inputs. +Those orientation checks provide no new scientific result or selected +operator replay. The selected conditional kappa remains 0.00302015. + +## Verification limits and code bounds + +The all-field, all-degree claim is a written proof. Finite enumeration +corroborates it in the stated domains. The alphabet has two data roles, +base-field right vectors and free base-field maps. Singular endpoints, +multivariate coefficients and restored auxiliary roles are outside the +classification. Uniform targets of exact degree are the sampling measure; +uniform words or degree-bounded targets have different distributions. +Preparation, conversion, routing, precision, restoration, stock and a +complete physical consumer remain unpriced. No selected replay, Lean or +Docker build was run, and independent human and formal proof-kernel review +are unclaimed. + +Every verifier loop has a finite bound from the fixed four configurations. +There are at most 64 input polynomials, 4,096 product pairs and 16,777,216 +pair comparisons per census before grouping. Every generated sequence has +total degree at most four. Free groups have at most 480 matrices. Probability +checks have 480 cases and at most 32 entries per case. No function reaches +60 physical lines, there is no recursion, and checks remain active under +optimization. The script reads the six package files and one declared proof +input, writes only stdout, and propagates failures. + +Power of Ten rule 3 deviation: Python allocates objects during the finite +census. Fixed input configurations bound collection growth; the largest +observed direct target set has 46,080 entries, and direct sets are discarded +after each field. A fixed-storage implementation is unnecessary for the +research contract and would change the verifier substantially. Revisit it +before allowing arbitrary degree or field-size inputs. Rule 10 limitation: +warning-strict ordinary and optimized execution and in-memory compilation +are available; optional external Python analyzers were unavailable locally. +The registered replay repeats the warning-strict checks in CI. + +## Open next questions + +- Determine the exact cost distribution under a degree-bounded target + measure. The current exact-degree counts give a finite weighted mixture; + a useful first step is a closed form for its moments. The sampling + measure must be stated before comparing typical costs. +- Identify a literal native coefficient producer and consumer before + using the abstract factor law for a supplier. Start with the price of + polynomial left-coefficient preparation. Native conversion, routing, + precision and restoration costs remain blockers. + +## Credit + +This contribution was produced by Nick Petalas. Nick Petalas #4763 supplies +the binary cost theorem and degree-four census; #4276/#4243 supplies its +preceding alphabet criteria and free-map normal form. Hirosi Nagao's +1959 *On GL(2,K[x])*, Theorem 2 and its degree proof, supplies the classical +structural context ([original paper](https://www.i-repository.net/contents/osakacu/sugaku/DB-M-010-02-04.pdf)). +The local-product and semilocal boundary retains ToikY #4334 and Nick +Petalas #4601/#4749 credit. Wentao Li #4099 following #2513 supplies the +right-vector alphabet lineage. Those predecessors are cited, not audited. +Apache-2.0. diff --git a/research/polynomial-cost-distribution/SOURCES.json b/research/polynomial-cost-distribution/SOURCES.json new file mode 100644 index 0000000000..8b617befe0 --- /dev/null +++ b/research/polynomial-cost-distribution/SOURCES.json @@ -0,0 +1,24 @@ +{ + "schema_version": 1, + "base_commit": "624de9dc66858af0945e5f8a0942488d62280d43", + "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/right-vector-polynomial-cost/PROOF.md", + "usage": "input", + "git_blob": "bcdbbef8b1b8111d7ef71577b22226f51bab639a", + "sha256": "40966c44c465b64dc664011ff172e63ae7423629c0c7eb23ad9aba3addd24f50" + } + ] +} diff --git a/research/polynomial-cost-distribution/TASK.json b/research/polynomial-cost-distribution/TASK.json new file mode 100644 index 0000000000..a5ee0f8191 --- /dev/null +++ b/research/polynomial-cost-distribution/TASK.json @@ -0,0 +1,75 @@ +{ + "schema_version": 1, + "task_id": "connector-alphabet-change", + "priority_revision": 7, + "base_commit": "624de9dc66858af0945e5f8a0942488d62280d43", + "original_card": { + "id": "connector-alphabet-change", + "question": "Does one explicit extension of the connector alphabet offer a favorable completed budget?", + "starting_points": [ + "docs/research/research-family-status.md", + "research/universal-connector-boundary/README.md", + "certificates/selected-result.json" + ], + "methods": [ + "Construct and charge a legal extra operation on a minimal instance.", + "Prove a target-specific bound after adding one specified operation family." + ], + "acceptance_gate": "State which fixed-alphabet premise changes and charge its implementation; do not declare it free. 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/universal-connector-boundary/verify.py" + ], + "expected": "PASS_UNIVERSAL_CONNECTOR_BOUNDARY", + "inspect": "Reproduce the 945-pairing control, then read Exact interface to list the allowed calls.", + "scope": "Positive control / source-bound orientation only; this is not a new construction or full cold replay." + }, + "first_experiment": "Add exactly one legally priced operation and test a tiny dirty-input instance before enumerating larger cases.", + "bottleneck_link": "A new legal connector operation could change recursive interface cost; a larger census in the same alphabet is a separate side result.", + "allowed_variations": [ + "Choose one additional operation and a small source count for its first counterexample." + ], + "scope_change_triggers": [ + "Keeping the alphabet and only increasing the source count; record this as a changed assignment.", + "Extending a source-count census without naming a supplier/interface decision it could change; audit #2973 pruning concerns before relying on the affected predecessor exclusions." + ], + "overlap_terms": [ + "universal connector", + "source-toggle", + "connector alphabet" + ] + }, + "scope_status": "changed", + "actual_scope": "Exact joint entry-degree and right-vector paid-cost count for GL2(F_q[t]); cost minus one is Binomial(D-1,(q-1)/q) at every exact degree D>=1.", + "scope_change_reason": "The connector card is changed to a formal-alphabet counting side result building on the binary polynomial cost theorem #4763. The coefficient field and degree are now arbitrary. This supplies an exact distribution, not a new source-toggle construction or a re-audit of the binary census.", + "bottleneck_link": "Quantifies typical and extremal cost in a formal coefficient algebra where the universal bounded-cost abstraction fails. No native supplier bill or multiplication saving follows.", + "budget_minutes": 60, + "stop_rule": "Stop at the first verified exact distribution; package it without extending to other coefficient algebras or sampling measures.", + "outcome": "completed", + "evidence": "PROOF.md proves the quantified all-q joint count and binomial law. verify.py matches all 63504 independently enumerated targets over F2,F3,F4,F5, checks 924 invertible paid parameter tuples, 480 exact probability cases and eight control groups.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "What are the closed-form cost moments under a uniform degree-bounded target measure?", + "why_it_matters": "This differs from exact-degree sampling and weights the geometric degree counts.", + "first_step": "Sum the proved joint counts for degrees zero through D and derive the mean.", + "blocked_by": "The sampling measure must be fixed before comparing typical costs." + }, + { + "question": "Does a literal native interface realize these polynomial coefficients at a useful complete price?", + "why_it_matters": "Formal factor counts alone do not establish a supplier.", + "first_step": "Identify one actual coefficient producer and price left-coefficient preparation.", + "blocked_by": "Native conversion, routing, precision, restoration and stock costs remain unknown." + } + ], + "claim_url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19131579", + "upstream_check": { + "commit": "624de9dc66858af0945e5f8a0942488d62280d43", + "checked_at": "2026-10-22T19:54:59.846355+00:00", + "priority_revision": 7, + "result": "Canonical main and relevant instructions, catalogue, selected record and predecessor proof unchanged. Distinctive main and merged searches found no duplicate. Remote overlap pagination covers 305 open PR bodies and 3723 Discussion records; sparse local-note coverage remains incomplete." + } +} diff --git a/research/polynomial-cost-distribution/VERIFY.json b/research/polynomial-cost-distribution/VERIFY.json new file mode 100644 index 0000000000..53fcce4187 --- /dev/null +++ b/research/polynomial-cost-distribution/VERIFY.json @@ -0,0 +1,34 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/right-vector-polynomial-cost/PROOF.md" + ], + "commands": [ + { + "argv": [ + "{python}", + "-B", + "-W", + "error", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Complete determinant-unit and reduced-word census of 63504 polynomial matrices over F2,F3,F4,F5; joint degree-cost counts, literal factor splitting and free conjugations; 480 exact probability/moment cases and eight control groups. Generated receipt hashes all six package files and checks the pinned proof input." + }, + { + "argv": [ + "{python}", + "-O", + "-B", + "-W", + "error", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Complete determinant-unit and reduced-word census of 63504 polynomial matrices over F2,F3,F4,F5; joint degree-cost counts, literal factor splitting and free conjugations; 480 exact probability/moment cases and eight control groups. Generated receipt hashes all six package files and checks the pinned proof input." + } + ] +} diff --git a/research/polynomial-cost-distribution/verify.py b/research/polynomial-cost-distribution/verify.py new file mode 100644 index 0000000000..c7feea7503 --- /dev/null +++ b/research/polynomial-cost-distribution/verify.py @@ -0,0 +1,280 @@ +#!/usr/bin/env python3 +"""Finite corroboration of the degree-conditioned polynomial cost law.""" +from collections import Counter, defaultdict +from fractions import Fraction +from hashlib import sha256 +from itertools import product +import json +from math import comb +from pathlib import Path + +CONFIGURATIONS = ((2, 4), (3, 2), (4, 2), (5, 1)) +FILES = ("README.md", "PROOF.md", "TASK.json", "SOURCES.json", "VERIFY.json", "verify.py") +ZERO = () +ONE = (1,) +IDENTITY = (ONE, ZERO, ZERO, ONE) + + +def require(condition, message): + if not condition: + raise RuntimeError(message) + + +def raw_multiply(q, a, b): + if q != 4: + return a * b % q + value = 0 + for bit in range(2): + if b & (1 << bit): + value ^= a << bit + if value & 4: + value ^= 7 # F4 = F2[z]/(z^2+z+1). + return value + + +class Field: + def __init__(self, q): + require(q in (2, 3, 4, 5), "unsupported finite field") + self.q = q + self.add = tuple(tuple(a ^ b if q == 4 else (a+b) % q + for b in range(q)) for a in range(q)) + self.mul = tuple(tuple(raw_multiply(q, a, b) for b in range(q)) + for a in range(q)) + self.neg = tuple(next(b for b in range(q) if self.add[a][b] == 0) + for a in range(q)) + self.inv = (0,) + tuple(next(b for b in range(1, q) + if self.mul[a][b] == 1) for a in range(1, q)) + for a, b, c in product(range(q), repeat=3): + require(self.mul[a][self.add[b][c]] == + self.add[self.mul[a][b]][self.mul[a][c]], "field distributivity") + + +def trim(values): + values = list(values) + for _ in range(len(values)): + if not values or values[-1]: + break + values.pop() + return tuple(values) + + +def add(field, a, b): + return trim(field.add[a[i] if i < len(a) else 0][b[i] if i < len(b) else 0] + for i in range(max(len(a), len(b)))) + + +def scale(field, a, c): + return trim(field.mul[x][c] for x in a) + + +def multiply(field, a, b): + require(len(a) <= 9 and len(b) <= 9, "polynomial capacity") + if not a or not b: + return ZERO + out = [0] * (len(a)+len(b)-1) + for i, x in enumerate(a): + for j, y in enumerate(b): + out[i+j] = field.add[out[i+j]][field.mul[x][y]] + return trim(out) + + +def matmul(field, a, b): + return tuple(add(field, multiply(field, a[2*i], b[j]), + multiply(field, a[2*i+1], b[2+j])) + for i in range(2) for j in range(2)) + + +def determinant(field, matrix): + a, b, c, d = matrix + return add(field, multiply(field, a, d), scale(field, multiply(field, b, c), field.neg[1])) + + +def degree(matrix): + return max(len(p)-1 for p in matrix) + + +def directions(field): + return ((0, 1),) + tuple((1, b) for b in range(field.q)) + + +def transvection(field, row, f): + a, b = row + column = (field.neg[b], a) + return tuple(add(field, ONE if i == j else ZERO, + scale(field, f, field.mul[column[i]][row[j]])) + for i in range(2) for j in range(2)) + + +def polynomials(field, cap): + require(0 <= cap <= 4, "degree cap") + return tuple(trim(p) for p in product(range(field.q), repeat=cap+1)) + + +def free_matrices(field): + return tuple(tuple(trim((x,)) for x in m) + for m in product(range(field.q), repeat=4) + if field.add[field.mul[m[0]][m[3]]][field.neg[field.mul[m[1]][m[2]]]]) + + +def inverse_free(field, matrix): + a, b, c, d = matrix + det = determinant(field, matrix) + require(len(det) == 1 and det[0], "free inverse domain") + s = field.inv[det[0]] + return tuple(scale(field, p, s) for p in + (d, scale(field, b, field.neg[1]), scale(field, c, field.neg[1]), a)) + + +def direct_census(field, cap): + """Enumerate every determinant-unit quadruple via equal product tails.""" + polys = polynomials(field, cap) + buckets = defaultdict(list) + for a, d in product(polys, repeat=2): + ad = multiply(field, a, d) + padded = ad + (0,) * (2*cap+1-len(ad)) + buckets[padded[1:]].append((a, d, padded[0])) + targets = set() + comparisons = 0 + for pairs in buckets.values(): + for a, d, ad0 in pairs: + for b, c, bc0 in pairs: + comparisons += 1 + if ad0 != bc0: + targets.add((a, b, c, d)) + return targets, comparisons + + +def normal_forms(field, cap): + levels = [[] for _ in range(cap+1)] + levels[0].append((IDENTITY, None, 0)) + coefficients = tuple(f for f in polynomials(field, cap) if f and f[0] == 0) + for total in range(cap): + for matrix, last, cost in levels[total]: + for row in directions(field): + if row == last: + continue + for f in coefficients: + new_degree = total+len(f)-1 + if new_degree <= cap: + new = matmul(field, matrix, transvection(field, row, f)) + require(degree(new) == new_degree, "reduced degree identity") + levels[new_degree].append((new, row, cost+1)) + return levels + + +def census(field, cap): + direct, comparisons = direct_census(field, cap) + free = free_matrices(field) + order = (field.q**2-1)*(field.q**2-field.q) + require(len(free) == order, "free group cardinality") + seen = {} + histograms = [Counter() for _ in range(cap+1)] + for total, level in enumerate(normal_forms(field, cap)): + for matrix, _, cost in level: + for endpoint in free: + target = matmul(field, matrix, endpoint) + require(target not in seen, "normal-form collision") + seen[target] = cost + histograms[total][cost] += 1 + require(set(seen) == direct, "independent determinant census mismatch") + require(len(seen) == order*field.q**(2*cap), "degree-bounded total") + for total in range(1, cap+1): + for cost in range(1, total+1): + expected = order*(field.q+1)*(field.q-1)**cost*field.q**(total-1)*comb(total-1, cost-1) + require(histograms[total][cost] == expected, "joint degree-cost count") + require(sum(histograms[total].values()) == + order*(field.q**2-1)*field.q**(2*total-2), "exact-degree total") + return {"q": field.q, "maximum_degree": cap, "targets": len(seen), + "product_tail_comparisons": comparisons, + "degree_cost_counts": [dict(c) for c in histograms]} + + +def literal_controls(field): + polys = polynomials(field, 1) + invertible = 0 + for row in directions(field): + a, b = row + v = (field.neg[b], a) + pivot = 0 if v[0] else 1 + for u in product(polys, repeat=2): + matrix = tuple(add(field, ONE if i == j else ZERO, scale(field, u[i], row[j])) + for i in range(2) for j in range(2)) + det = determinant(field, matrix) + if len(det) != 1 or not det[0]: + continue + invertible += 1 + const = tuple(trim((p[0],)) if p else ZERO for p in matrix) + w = add(field, u[pivot], scale(field, trim(u[pivot][:1]), field.neg[1])) + f = scale(field, w, field.inv[v[pivot]]) + require(matmul(field, const, transvection(field, row, f)) == matrix, + "literal paid-factor splitting") + for s in free_matrices(field): + inverse = inverse_free(field, s) + for row in directions(field): + new = matmul(field, matmul(field, s, transvection(field, row, (0, 1))), inverse) + candidates = (transvection(field, z, (0, c)) + for z in directions(field) for c in range(1, field.q)) + require(new in candidates, "scaled free conjugation") + return invertible + + +def formula_controls(results): + # Check full probability law, first moment and second centered moment exactly. + for q in range(2, 17): + for d in range(1, 33): + mass = [Fraction(comb(d-1, r-1)*(q-1)**(r-1), q**(d-1)) + for r in range(1, d+1)] + mean = 1+Fraction((d-1)*(q-1), q) + require(sum(mass) == 1, "probability normalization") + require(sum(r*p for r, p in enumerate(mass, 1)) == mean, "mean") + require(sum((r-mean)**2*p for r, p in enumerate(mass, 1)) == + Fraction((d-1)*(q-1), q*q), "variance") + f = Field(3) + t = (0, 1) + row = (0, 1) + require(matmul(f, transvection(f, row, t), transvection(f, row, t)) == + transvection(f, row, (0, 2)), "equal-direction merging control") + require(matmul(f, transvection(f, row, t), transvection(f, row, (0, 2))) == + IDENTITY, "opposite-coefficient cancellation control") + require(degree(transvection(f, row, ONE)) == 0, "constant coefficient control") + require(len(determinant(f, ((1, 1), ZERO, ZERO, ONE))) == 2, "nonunit determinant control") + require(determinant(f, (ZERO, ZERO, ZERO, ONE)) == ZERO, "singular endpoint control") + s = ((2,), ZERO, ZERO, ONE) + conjugate = matmul(f, matmul(f, s, transvection(f, row, t)), inverse_free(f, s)) + require(conjugate != transvection(f, row, t), "missing conjugation scalar control") + require(results[0]["degree_cost_counts"][4] == {1: 144, 2: 432, 3: 432, 4: 144}, + "binary degree-four compatibility") + require(results[1]["degree_cost_counts"][2] != {1: 1152, 2: 1152}, + "missing field-weight control") + return 8 + + +def receipt(results, paid_counts, controls): + root = Path(__file__).resolve().parent + sources = json.loads((root / "SOURCES.json").read_text()) + for row in sources["files"]: + if row["usage"] == "input": + payload = (root.parent.parent / row["path"]).read_bytes() + require(sha256(payload).hexdigest() == row["sha256"], "source hash") + hashes = {name: sha256((root / name).read_bytes()).hexdigest() for name in FILES} + result = {"schema": "polynomial-cost-distribution/v1", "files_sha256": hashes, + "censuses": results, "invertible_paid_parameters": paid_counts, + "control_groups": controls, "probability_cases": 480} + print(json.dumps(result, sort_keys=True)) + print("PASS_POLYNOMIAL_COST_DISTRIBUTION targets=" + str(sum(r["targets"] for r in results)) + + " fields=4 probability_cases=480 controls=" + str(controls) + " no_new_kappa") + + +def main(): + results = [] + paid_counts = {} + for q, cap in CONFIGURATIONS: + field = Field(q) + results.append(census(field, cap)) + paid_counts[q] = literal_controls(field) + controls = formula_controls(results) + receipt(results, paid_counts, controls) + + +if __name__ == "__main__": + main()