From 8cfb0297ed41284b17cfcfe3e8eef9c335929b91 Mon Sep 17 00:00:00 2001 From: Nick Petalas Date: Thu, 12 Nov 2026 19:25:55 +0000 Subject: [PATCH] feat(research): lift recovery certificates across scalar fields --- research/commutative-scalar-ascent/PROOF.md | 141 ++++++++++++ research/commutative-scalar-ascent/README.md | 170 ++++++++++++++ .../commutative-scalar-ascent/SOURCES.json | 30 +++ research/commutative-scalar-ascent/TASK.json | 107 +++++++++ .../commutative-scalar-ascent/VERIFY.json | 32 +++ research/commutative-scalar-ascent/algebra.py | 213 +++++++++++++++++ research/commutative-scalar-ascent/ascent.py | 45 ++++ research/commutative-scalar-ascent/verify.py | 216 ++++++++++++++++++ 8 files changed, 954 insertions(+) create mode 100644 research/commutative-scalar-ascent/PROOF.md create mode 100644 research/commutative-scalar-ascent/README.md create mode 100644 research/commutative-scalar-ascent/SOURCES.json create mode 100644 research/commutative-scalar-ascent/TASK.json create mode 100644 research/commutative-scalar-ascent/VERIFY.json create mode 100644 research/commutative-scalar-ascent/algebra.py create mode 100644 research/commutative-scalar-ascent/ascent.py create mode 100644 research/commutative-scalar-ascent/verify.py diff --git a/research/commutative-scalar-ascent/PROOF.md b/research/commutative-scalar-ascent/PROOF.md new file mode 100644 index 0000000000..553b662fa1 --- /dev/null +++ b/research/commutative-scalar-ascent/PROOF.md @@ -0,0 +1,141 @@ +# Scalar ascent of a recovered commutative multiplication tensor + +This constructive proof and certificate adapter were produced by Nick Petalas. +Apache-2.0. Restriction of scalars and normalization of a unital isotope are +classical. The contribution here is the explicit bridge between the existing +prime-field recovery interface and a general extension-field certificate. +No literature-priority claim is made for the underlying algebraic facts. + +## Proposition and conventions + +Let K/F be a finite field extension of degree d. The fields themselves need +not be finite. Let t:U x V -> Z be K-bilinear, with all three K-dimensions +equal to n > 0. Matrices act on column vectors. Restriction uses one fixed +F-basis of K and the same coordinate packing in each of U,V,Z. + +The following conditions are equivalent. + +1. t is K-isotopic to multiplication in a commutative associative unital + K-algebra of dimension n. +2. Res(t) is F-isotopic to multiplication in a commutative associative + unital F-algebra of dimension dn. + +More precisely, suppose a certificate for condition 2 supplies an F-algebra +B, its multiplication table, and invertible F-linear maps + + Res(t)(P a, Q b) = S(ab). + +The maps P,Q,S need not be K-linear and B is not initially supplied with a +K-vector-space structure. Let e be its unit, and pack the vectors P e and Q e +as u in U and v in V. Define K-linear slices + + R_v(x) = t(x,v), L_u(y) = t(u,y). + +Both slices are invertible. The explicit K-bilinear product on Z + + mu(x,y) = t(R_v^(-1) x, L_u^(-1) y) + +is commutative, associative and unital, with unit t(u,v). Its K-table and +the three maps R_v^(-1), L_u^(-1), I_Z form a certificate for condition 1. +This construction requires no decomposition of the K-nucleus and no +Frobenius height computation. + +## Proof + +Condition 1 implies condition 2 by restricting every map and algebra operation +to F. For the converse, apply the given isotopy with b=e and with a=e: + + R_v P = S, L_u Q = S. + +Thus the restricted F-linear maps R_v and L_u are invertible. They are also +K-linear by the stipulated K-bilinearity of t. Their inverses are K-linear: +if A is a K-linear bijection, A(A^(-1)(lambda z)) = lambda z = +A(lambda A^(-1)z), and injectivity equates the two inverse values. + +Now write x=S a and y=S b as F-vectors. The two displayed slice identities +give + + mu(S a,S b) = t(P a,Q b) = S(ab). + +Consequently S is an F-algebra isomorphism from B to (Z,mu). Commutativity, +associativity and the unit S e are identities of the product and therefore +hold for every vector of Z, regardless of scalar presentation. The product +is K-bilinear by its formula. These facts make (Z,mu) a commutative +associative unital K-algebra. Finally S e=t(Pe,Qe)=t(u,v), and the formula +for mu is exactly the claimed K-isotopy. This proves the proposition. + +In particular, the K-action on the recovered algebra could also be described +by a conjugated F-linear action through S. The adapter need not discover or +diagonalize that action. It uses the output coordinates already present in t. + +## Recovering the unit and constructing the certificate + +The source interface returns a multiplication table and P,Q,S, without a +separate unit vector. Solve the linear equations + + sum_i e_i B[i,j,k] = delta[j,k] + +for e. A unital algebra has a unique solution, since two left identities in +a commutative algebra agree by multiplying them. The reference also checks +both unit identities, associativity, commutativity, every source basis +isotopy equality and invertibility of the three supplied maps. Invalid +certificates are rejected before ascent. This is certificate consumption, +not a call to an existing recognizer or a replay of its scientific suite. + +Pack Pe,Qe into K-vectors using the fixed field basis. Compute the slices, +invert them over K and evaluate the product on all pairs of K-basis vectors. +The reference returns `table`, `unit`, `U`, `V`, `W`, with W the identity. +It checks the returned K-certificate as well. For a symbolic recognizer, +the forward implication and this adapter show that applying the general +F-recognizer to Res(t) is a necessary-and-sufficient K-recognition procedure. +The predecessor recognition theorem remains a cited premise. + +The procedure is polynomial in n and d for a supplied exact field interface. +Dense source certificate validation costs at most O((dn)^5) F-operations +and the displayed slice/table construction at most O(n^5) K-operations +using literal contractions. These are loose operation bounds, not a speed +claim, bit-complexity bound or bound on constructing the field. The reference +has hard finite capacities listed in README.md. + +## Two hypotheses that cannot be silently dropped + +K-bilinearity is essential. With F=F2, K=F4, the map t(x,y)=x^2 y is +F-bilinear and F-isotopic to field multiplication, since squaring is an +invertible F-linear map. It is not K-linear in its first argument: +t(a,1)=a^2 differs from a t(1,1)=a for a outside F2. Composing with +invertible K-linear factor maps cannot change that failure of K-bilinearity. +Thus an arbitrary F-tensor with a guessed K-coordinate grouping is outside +the proposition. + +The general commutative recognizer is required. It cannot be replaced by the +prime-field local characteristic-power truncated-polynomial recognizer. +For example, K=F4, n=1, t is K multiplication. Res(t) is multiplication in +the reduced F2-algebra F4 of dimension two. The only dimension-two nonempty +truncated model over F2 is F2[x]/x^2, which has a nonzero square-zero element. +These algebras are not isomorphic. They are not isotopic either: for unital +commutative associative algebras, any isotopy normalizes to an isomorphism +by multiplying its output by the inverse of the images of the two units. +Equivalently, field multiplication has every nonzero slice invertible, +whereas multiplication by x in the dual numbers is a nonzero singular slice. +The reference checks this reduced/nilpotent boundary directly. + +This proposition does not transfer a prescribed algebra-class label, a +special-linear determinant label or an automorphism count through restriction. +Those tasks require their own scalar-aware arguments. + +## Relationship to prior recognition + +Ali Romman's #5540 supplies general prime-field recovery, including +nonreduced algebras, and asks for an extension-field input layer. Its +necessity/sufficiency theorem and source implementation are not rechecked. +Ali Romman's #5637 implements a direct extension-field recognizer for local +characteristic-power truncated polynomial algebras. Its README explicitly +leaves general residue fields and products outside that implementation. + +Nick Petalas's older #6464 already gives a general recognition theorem over +any supplied exact field, using a different cyclic-module construction. +No claim to extend that theorem is made here and its construction is not +used. The new artifact is a scalar-restriction certificate adapter. It +allows the existing prime-field recovery contract to supply K-linear output +without implementing nucleus decomposition over K. Neither its proof nor +its implementation imports a predecessor executable. diff --git a/research/commutative-scalar-ascent/README.md b/research/commutative-scalar-ascent/README.md new file mode 100644 index 0000000000..687d168539 --- /dev/null +++ b/research/commutative-scalar-ascent/README.md @@ -0,0 +1,170 @@ +# Lift recovered prime-field tensors to extension-field algebras + +This constructive proof and certificate adapter were produced by Nick Petalas. +Apache-2.0. + +Let K/F be a finite field extension and t a K-bilinear square tensor. Then t +is K-isotopic to multiplication in a commutative associative unital K-algebra +if and only if its restriction to F is F-isotopic to multiplication in a +commutative associative unital F-algebra. The explicit certificate bridge is + +```text +source unit e; u=P e; v=Q e +R_v(x)=t(x,v); L_u(y)=t(u,y) +mu(x,y)=t(R_v^(-1)x,L_u^(-1)y) +K-certificate: table(mu), unit=t(u,v), U=R_v^(-1), V=L_u^(-1), W=I +``` + +The source maps P,Q,S can be arbitrary F-linear maps. They do not need to be +K-linear. Both displayed slices are invertible K-linear maps, and mu is the +required K-algebra product. [PROOF.md](PROOF.md) proves the quantified +statement and explains both necessary boundary restrictions. + +Claim type: scoped constructive proof with exact finite corroboration. +The contribution is the explicit scalar-restriction certificate adapter and +its bounded implementation. It is not a new general recognition theorem. +No kappa, supplier admission or selected-frontier change is claimed. + +## Before and after + +Ali Romman's [#5540](https://github.com/CrocSwap/integer-mult-bounds/pull/5540) +recovers arbitrary commutative unital multiplication from prime-field tensors +and leaves an extension-field input layer open. The adapter consumes that +certificate shape and returns a K-table and K-linear factor maps without +implementing an extension-field nucleus decomposition. It handles products, +non-Gorenstein algebras and nonsplit residue fields under the same general +commutative contract. + +Ali Romman's [#5637](https://github.com/CrocSwap/integer-mult-bounds/pull/5637) +already supplies a direct extension-field implementation for the local +characteristic-power truncated-polynomial class. Nick Petalas's older +[#6464](https://github.com/CrocSwap/integer-mult-bounds/pull/6464) already proves +general recognition over any supplied exact field. Those results are credited +premises/background, not replay targets or claimed new coverage. This package +uses neither predecessor implementation. It supplies the explicit restriction +bridge to the existing prime-field interface. + +Restriction does not preserve every class label: Res(F4) is a field over F2, +whereas F2[x]/x^2 is not. The adapter must consume a general commutative +recovery certificate. Nor can an arbitrary F-bilinear tensor be passed off as +a K-bilinear input. The semilinear map x^2 y over F4 is a boundary witness. + +## Reproduce + +From the repository root, CPython 3.12 and the standard library suffice: + +```sh +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -W error -B research/commutative-scalar-ascent/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -W error -O -B research/commutative-scalar-ascent/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/commutative-scalar-ascent +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/commutative-scalar-ascent --check-source-history +``` + +Another CPython 3.12 path can replace the recorded interpreter. The direct +marker is `PASS_COMMUTATIVE_SCALAR_ASCENT`. The program emits a generated +receipt binding all eight package files by SHA256 and the complete ordered +fixture output by a deterministic digest. It writes nothing. Both registered +commands run the same checks with runtime requirements enabled under `-O`. + +`ascent.py` exports `ascend(tensor, certificate, field)`. Tensor entries are +`t[i][j][k]`. The input certificate contains `table`, `U`, `V`, `W` in the +restricted prime-field coordinates, with each original K-coordinate expanded +into consecutive low-to-high polynomial coefficients. Its maps use columns +as basis images and satisfy `Res(t)(U a,V b)=W table(a,b)`. The adapter checks +the supplied certificate and returns the corresponding K-certificate plus +`unit`. Invalid certificates raise `ValueError`. It never invokes a recognizer. + +## Evidence + +Local normal and optimized replay passes 78 constructed certificates, 684 +K-basis products, 75 non-K-linear recovery bases, 16,930 field-law triples, +ten rejecting controls and two boundary witnesses. Both registered checks +and the package metadata runner pass on CPython 3.12.15. Generated normal +and optimized reports agree exactly. + +The verifier constructs its own tensors and source certificates. It exercises +F4, F8, F9 and F25, nilpotent and non-Gorenstein algebras, direct products, +nonsplit quadratic residue fields, and dual-number extensions of those +nonsplit fields. Three deterministic independent input/output presentations +are used for each algebra. Prime-field recovery bases are changed separately, +including bases that do not commute with multiplication by the field +coordinate. Returned tables and units are compared with the original +fixture's explicit output-space algebra, independently of the adapter's +slice formula. + +It also checks every field-law triple in the four finite arithmetic domains. +Named controls reject singular maps, an invertible but wrong output map, +noncanonical entries, missing keys, unsupported fields, wrong dimensions, +nonassociative multiplication and noncommutative multiplication. Two explicit +boundary witnesses cover K-bilinearity and the class-recognizer restriction. +The emitted receipt enumerates all counts. These finite checks corroborate +the written proof; they are not a complete tensor census or a replay of +another contributor's numbers. + +## Scope, limits and credit + +This is a changed `formal-interface-lemma` scope at canonical main +`e54523517d0f03e58352e647c403a5af3e525a57`, priority revision 8. It is an +algebraic interface side result, with no proof-assistant acceptance. The +source-binding baseline command passed for selected #7000. No selected +scientific replay was run. Historical source text and the task card are +pinned as provenance in SOURCES.json, rather than imported at runtime. + +The reference accepts the explicitly listed polynomial fields in algebra.py, +with q at most 25 and restricted dimension dn at most 12. These are executable +capacities, not bounds on the theorem. It consumes a certificate; it does not +implement a new end-to-end recognizer or classify the recovered K-algebra. +No special-linear label, automorphism count, rational bit-complexity bound or +runtime speedup is claimed. There is no native implementation, physical +coefficient preparation, dirty restoration program, paid caller, compiler +closure, precision/tape admission or complete multiplication theorem. All +five selected assumptions remain. Independent human and formal proof-kernel +review are unclaimed. + +Credit Ali Romman for #5540's question and recovery interface, #5525 and +#5637; apoursh for #5502; Nick Petalas for #5252; and David Ganz and the +retained tensor/algebra lineage. Restriction of scalars, exact elimination +and unital isotope normalization are classical. No predecessor code is copied. +The new bridge, bounded reference, proof and fixture checks were produced by +Nick Petalas. The #6464 cyclic-module construction is background and is not +used as a step. + +Live PR titles/bodies, recent handoffs, batch reservations, merged searches +and all-main README searches were checked before the +[advance claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19572847). +The cached search reports its own coverage limits, including omitted sparse +notes. Search absence does not prove novelty. Related open work is recorded +in the PR body; no competing result is audited here. + +## Open next questions + +1. Can a public caller connect an actual #5540 recovery certificate to this + adapter with a general exact finite-field input contract? Start with one + source-owned output certificate and its precise coordinate basis. This + package supplies a bounded adapter and new fixtures, not that integration. +2. Which prescribed K-algebra class or determinant labels can be reconstructed + from the restricted F-algebra together with its embedded scalar action? + Start with one nonsplit local component. Ignoring that scalar action is + invalid; no classification or special-linear label transfer is supplied. +3. Can one recovered K-table be used in an affordable native caller? First + charge all coefficient maps, workspace, returns and restoration. No such + physical cost contract is supplied by recognition or this bridge. + +## Verifier engineering bounds + +Every dimension is bounded by 12 and every supported field has at most 25 +values. All loops range over those explicit finite domains or fixed fixture +lists. There is no recursion, subprocess, runtime code generation or write. +Functions remain below sixty physical lines. Internal arithmetic helpers trust +representations validated at the public tensor, matrix and certificate +boundaries. Runtime requirements use explicit exceptions and remain enabled +under optimization. Warning-strict normal/optimized execution and syntax +inspection provide diagnostics; no separate static analyzer is claimed. + +Power of Ten rule 3 deviation: CPython allocates integers, lists and tuples +throughout exact arithmetic. Live tensors have at most 12^3 coefficients, +linear systems at most 12^2 rows and 13 columns, and field tables at most +25^2 entries. Fixtures execute sequentially. Revisit these bounds before +accepting larger dimensions or a production caller. Rules 8 and 9 retain +ordinary Python module loading from two fixed siblings and a fixed list of +negative-control lambdas; no arbitrary imported target or callback is accepted. diff --git a/research/commutative-scalar-ascent/SOURCES.json b/research/commutative-scalar-ascent/SOURCES.json new file mode 100644 index 0000000000..cef318e949 --- /dev/null +++ b/research/commutative-scalar-ascent/SOURCES.json @@ -0,0 +1,30 @@ +{ + "schema_version": 1, + "base_commit": "e54523517d0f03e58352e647c403a5af3e525a57", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "75d77b328ea02ded535e7f23aee5b1e55d0bb1a8", + "sha256": "154c3d30455d778fd3343b6b4851f0fa4665f0f7625b0adb3675e2bafbbf6bf1" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec", + "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81" + }, + { + "path": "research/extension-field-tensor-recognition/README.md", + "usage": "provenance", + "git_blob": "d0c74a3c49fba38e389b6ef8c714882bdd0bf797", + "sha256": "4b297e57762284c69c7202ee183f43c5fe170fbc9104e4ff0cce3faa345c7c97" + }, + { + "path": "research/nonreduced-tensor-recognition/README.md", + "usage": "provenance", + "git_blob": "826c6b010725d98b6ca6599a748c4179264140e9", + "sha256": "2eaed94a9f12ad7b6bb7253b14bff95b86549b3e320f0e91fa4e35c0025536de" + } + ] +} diff --git a/research/commutative-scalar-ascent/TASK.json b/research/commutative-scalar-ascent/TASK.json new file mode 100644 index 0000000000..ecaabdab26 --- /dev/null +++ b/research/commutative-scalar-ascent/TASK.json @@ -0,0 +1,107 @@ +{ + "schema_version": 1, + "task_id": "formal-interface-lemma", + "priority_revision": 8, + "base_commit": "e54523517d0f03e58352e647c403a5af3e525a57", + "original_card": { + "id": "formal-interface-lemma", + "question": "Can one uncovered interface implication be formalized with exact caller and certificate bindings?", + "starting_points": [ + "docs/research/research-family-status.md", + "certificates/selected-result.json", + "research/gate-operand-parity-lean/README.md", + "research/staged544-certified-endpoint/README.md", + "research/unconditional-batched-crt/README.md" + ], + "methods": [ + "Formalize a missing boundary lemma identified by the selected review.", + "Audit a formal theorem-to-certificate binding independently." + ], + "acceptance_gate": "State the exact formalized proposition and remaining assumptions; avoid duplicate arithmetic formalizations already present.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_selected_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Resolve the current selected review, separate complex/ordinary BIT/admitted BIT/outer budgets, and compare the card against live handoffs before starting. Historical ceilings require exact source/model equivalence.", + "scope": "Source-binding orientation only; not a scientific replay or all-size proof. Materialize selected inputs if this checkout is sparse." + }, + "first_experiment": "Write one missing statement with quantified hypotheses, actual caller and existing coverage. A compact-switch lemma is a candidate only after its mathematical contract is reviewed. Establish a bounded proof plan before a separately budgeted proof-assistant build; do not rerun large Lean jobs as orientation.", + "bottleneck_link": "A missing interface proof can reduce the conditional gap even if it does not change kappa.", + "allowed_variations": [ + "Narrow to one formal lemma or one theorem-to-certificate binding." + ], + "scope_change_triggers": [ + "Formalizing already-covered arithmetic and claiming the full multiplication theorem." + ], + "overlap_terms": [ + "hyperplane end", + "formal interface", + "Lean binding", + "3807", + "3857", + "4100", + "gate-operand-parity-lean", + "staged544-certified-endpoint", + "unconditional-batched-crt" + ], + "existing_checks": [ + { + "scope": "PR #3807: scoped gate-operand parity formalization.", + "evidence": "research/gate-operand-parity-lean/README.md", + "remaining": "Exact theorem-to-caller binding and genuinely uncovered interface lemmas.", + "status": "author-checked", + "source_commit": "4c3530f42a6abcc48e7a6bcffd6c901911dc8269", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "PR #3857: certified real-power moment/endpoint arithmetic.", + "evidence": "research/staged544-certified-endpoint/README.md", + "remaining": "Uniform algorithmic implications, not another endpoint digit.", + "status": "author-checked", + "source_commit": "ef4315b8caa605e47a2515004845eb2d2ed71a86", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "PR #4100: compact-switch formalization proposed as future validation.", + "evidence": "research/unconditional-batched-crt/README.md", + "remaining": "Audit the statement and assumptions before a formal proof campaign.", + "status": "author-checked", + "source_commit": "337d04939571a637aeab54a0f58f54fde811663a", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + } + ] + }, + "scope_status": "changed", + "actual_scope": "Construct a scalar-restriction certificate adapter for general commutative multiplication across finite field extensions.", + "scope_change_reason": "The formal-interface card is changed to a constructive algebraic side result answering the extension-field interface question of Ali Romman PR5540. No proof-assistant acceptance or selected assumption discharge is claimed. General arbitrary-field recognition already exists in PR6464; its construction is not used.", + "bottleneck_link": "A recovered multiplication table needs explicit maps in the caller scalar field before it can be considered for a native producer/consumer. This adapter supplies those maps, not the missing physical bill.", + "budget_minutes": 60, + "stop_rule": "Stop at the explicit certificate bridge, bounded standalone implementation and its exact checks. Do not extend to classification, a recognizer rewrite or a physical supplier.", + "outcome": "completed", + "evidence": "PROOF.md gives the quantified equivalence and constructive maps. verify.py emits generated source-hash and fixture receipts with finite exact corroboration and rejecting controls.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "Connect one actual prime-field recovery certificate to a general exact finite-field caller.", + "why_it_matters": "This turns the standalone bridge into an end-to-end input layer.", + "first_step": "Bind one source-owned recovery output and its exact coordinate basis to ascend.", + "blocked_by": "No public integration or general field input interface is included." + }, + { + "question": "Recover scalar-aware prescribed algebra-class and determinant labels after restriction.", + "why_it_matters": "Restriction alone can change the apparent algebra class and determinant information.", + "first_step": "Analyze one nonsplit local component together with its embedded K-action.", + "blocked_by": "A scalar-aware classification proof is separate from the general certificate bridge." + }, + { + "question": "Implement one recovered table in an affordable native caller.", + "why_it_matters": "Algebraic recognition alone supplies no paid recursive gain.", + "first_step": "Specify and charge all coefficient maps, dirty inputs, returns and restoration.", + "blocked_by": "No physical cost contract is supplied." + } + ] +} diff --git a/research/commutative-scalar-ascent/VERIFY.json b/research/commutative-scalar-ascent/VERIFY.json new file mode 100644 index 0000000000..2d0c05da62 --- /dev/null +++ b/research/commutative-scalar-ascent/VERIFY.json @@ -0,0 +1,32 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [], + "commands": [ + { + "argv": [ + "{python}", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Constructed arbitrary-F-basis certificates, normalized K-tables/units, complete bounded field laws, rejecting and boundary controls; generated hash-bound receipt." + }, + { + "argv": [ + "{python}", + "-W", + "error", + "-O", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "The same requirements and source/fixture hashes remain enabled with Python optimization." + } + ] +} diff --git a/research/commutative-scalar-ascent/algebra.py b/research/commutative-scalar-ascent/algebra.py new file mode 100644 index 0000000000..119b1c2bd5 --- /dev/null +++ b/research/commutative-scalar-ascent/algebra.py @@ -0,0 +1,213 @@ +"""Bounded exact arithmetic. Produced by Nick Petalas. Apache-2.0.""" + +MAX_DIM = 12 + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +class Field: + """Small polynomial-basis fields, with canonical integer elements.""" + + def __init__(self, p, modulus): + choices = {2: ((0, 1), (1, 1, 1), (1, 1, 0, 1)), + 3: ((0, 1), (1, 0, 1)), 5: ((0, 1), (2, 0, 1))} + require(type(p) is int and p in choices, 'unsupported characteristic') + require(isinstance(modulus, (list, tuple)) and 2 <= len(modulus) <= 4 and + all(type(a) is int and 0 <= a < p for a in modulus), 'modulus format') + require(tuple(modulus) in choices[p], 'unsupported field modulus') + self.p, self.modulus = p, tuple(modulus) + self.degree = len(modulus) - 1 + self.q = p ** self.degree + self.digits = tuple(tuple((x // p**i) % p for i in range(self.degree)) + for x in range(self.q)) + self.plus = tuple(tuple(self.encode((a+b) % p for a, b in zip(x, y)) + for y in self.digits) for x in self.digits) + self.times = tuple(tuple(self.polynomial_product(x, y) for y in self.digits) + for x in self.digits) + self.negative = tuple(self.encode((-a) % p for a in x) for x in self.digits) + inverses = [0] + for a in range(1, self.q): + candidates = [b for b in range(1, self.q) if self.times[a][b] == 1] + require(len(candidates) == 1, 'modulus is not a field') + inverses.append(candidates[0]) + self.reciprocal = tuple(inverses) + + def encode(self, digits): + return sum(a * self.p**i for i, a in enumerate(digits)) + + def polynomial_product(self, x, y): + d, p = self.degree, self.p + work = [0] * (2*d-1) + for i in range(d): + for j in range(d): + work[i+j] = (work[i+j] + x[i]*y[j]) % p + for k in range(2*d-2, d-1, -1): + coefficient = work[k] + for j in range(d): + work[k-d+j] = (work[k-d+j] - coefficient*self.modulus[j]) % p + return self.encode(work[:d]) + + def add(self, a, b): + return self.plus[a][b] + + def mul(self, a, b): + return self.times[a][b] + + def neg(self, a): + return self.negative[a] + + +def check_matrix(matrix, n, field): + require(type(n) is int and 1 <= n <= MAX_DIM, 'matrix dimension') + require(isinstance(matrix, (list, tuple)) and len(matrix) == n and + all(isinstance(row, (list, tuple)) and len(row) == n for row in matrix), 'matrix shape') + require(all(type(a) is int and 0 <= a < field.q for row in matrix for a in row), + 'canonical matrix entries') + + +def check_tensor(table, field): + require(isinstance(table, (list, tuple)), 'tensor container') + n = len(table) + require(1 <= n <= MAX_DIM, 'tensor dimension') + for matrix in table: + check_matrix(matrix, n, field) + return n + + +def identity(n): + require(type(n) is int and 1 <= n <= MAX_DIM, 'identity dimension') + return [[int(i == j) for j in range(n)] for i in range(n)] + + +def sum_field(values, field): + result = 0 + for value in values: + result = field.add(result, value) + return result + + +def matvec(matrix, vector, field): + return [sum_field((field.mul(a, b) for a, b in zip(row, vector)), field) + for row in matrix] + + +def matmul(left, right, field): + return [list(row) for row in zip(*(matvec(left, column, field) + for column in zip(*right)))] + + +def solve_unique(rows, variables, field): + require(1 <= variables <= MAX_DIM and 1 <= len(rows) <= MAX_DIM**2, + 'linear system bounds') + require(all(len(row) == variables+1 for row in rows), 'linear system shape') + work, pivot_row = [list(row) for row in rows], 0 + for column in range(variables): + candidates = [i for i in range(pivot_row, len(work)) if work[i][column]] + require(candidates, 'linear system not unique') + selected = candidates[0] + work[pivot_row], work[selected] = work[selected], work[pivot_row] + scale = field.reciprocal[work[pivot_row][column]] + work[pivot_row] = [field.mul(scale, a) for a in work[pivot_row]] + for i in range(len(work)): + if i != pivot_row: + coefficient = work[i][column] + work[i] = [field.add(a, field.neg(field.mul(coefficient, b))) + for a, b in zip(work[i], work[pivot_row])] + pivot_row += 1 + require(all(not any(row[:variables]) and row[-1] == 0 + for row in work[variables:]), 'inconsistent linear system') + return [work[i][-1] for i in range(variables)] + + +def inverse(matrix, field): + n = len(matrix) + check_matrix(matrix, n, field) + columns = [] + for column in range(n): + rows = [list(row) + [int(i == column)] for i, row in enumerate(matrix)] + columns.append(solve_unique(rows, n, field)) + return [list(row) for row in zip(*columns)] + + +def evaluate(table, x, y, field): + n = len(table) + result = [0] * n + for i in range(n): + for j in range(n): + coefficient = field.mul(x[i], y[j]) + if coefficient: + for k in range(n): + result[k] = field.add(result[k], field.mul(coefficient, table[i][j][k])) + return result + + +def isotope(table, left, right, output, field): + """Return output * table(left*x, right*y), with column-map conventions.""" + n = check_tensor(table, field) + for matrix in (left, right, output): + check_matrix(matrix, n, field) + return [[matvec(output, evaluate(table, x, y, field), field) + for y in zip(*right)] for x in zip(*left)] + + +def find_unit(table, field): + n = check_tensor(table, field) + rows = [[table[i][j][k] for i in range(n)] + [int(j == k)] + for j in range(n) for k in range(n)] + return solve_unique(rows, n, field) + + +def check_algebra(table, field): + n = check_tensor(table, field) + unit, basis = find_unit(table, field), identity(n) + for i in range(n): + require(evaluate(table, unit, basis[i], field) == basis[i] and + evaluate(table, basis[i], unit, field) == basis[i], 'two-sided unit') + for j in range(n): + require(table[i][j] == table[j][i], 'commutative algebra') + for k in range(n): + require(evaluate(table, table[i][j], basis[k], field) == + evaluate(table, basis[i], table[j][k], field), 'associative algebra') + return unit + + +def unpack(vector, field): + require(all(type(a) is int and 0 <= a < field.q for a in vector), 'K vector') + return [digit for a in vector for digit in field.digits[a]] + + +def pack(vector, field): + require(len(vector) % field.degree == 0 and + all(type(a) is int and 0 <= a < field.p for a in vector), 'F vector') + return [field.encode(vector[i:i+field.degree]) + for i in range(0, len(vector), field.degree)] + + +def restrict_matrix(matrix, field): + n, d = len(matrix), field.degree + check_matrix(matrix, n, field) + require(n*d <= MAX_DIM, 'restricted dimension') + columns = [] + for i in range(n): + for a in range(d): + vector = [0] * n + vector[i] = field.p**a + columns.append(unpack(matvec(matrix, vector, field), field)) + return [list(row) for row in zip(*columns)] + + +def restrict_tensor(table, field): + n, d = check_tensor(table, field), field.degree + require(n*d <= MAX_DIM, 'restricted dimension') + result = [[[0] * (n*d) for _ in range(n*d)] for _ in range(n*d)] + for i in range(n): + for j in range(n): + for a in range(d): + for b in range(d): + coefficient = field.mul(field.p**a, field.p**b) + result[i*d+a][j*d+b] = unpack( + [field.mul(coefficient, c) for c in table[i][j]], field) + return result diff --git a/research/commutative-scalar-ascent/ascent.py b/research/commutative-scalar-ascent/ascent.py new file mode 100644 index 0000000000..38be6e8f0d --- /dev/null +++ b/research/commutative-scalar-ascent/ascent.py @@ -0,0 +1,45 @@ +"""Convert a prime-field recovery certificate to a K-linear one. + +Produced by Nick Petalas. Apache-2.0. +""" + +from algebra import (Field, check_algebra, check_matrix, check_tensor, evaluate, + identity, inverse, isotope, matvec, pack, require, + restrict_tensor) + + +def validate_certificate(tensor, certificate, field): + """Check supplied evidence, without running a tensor recognizer.""" + n = check_tensor(tensor, field) + require(isinstance(certificate, dict) and + set(certificate) >= {'table', 'U', 'V', 'W'}, 'certificate keys') + table = certificate['table'] + require(check_tensor(table, field) == n, 'certificate dimension') + unit = check_algebra(table, field) + for key in ('U', 'V', 'W'): + check_matrix(certificate[key], n, field) + inverse(certificate[key], field) + actual = isotope(tensor, certificate['U'], certificate['V'], identity(n), field) + wanted = isotope(table, identity(n), identity(n), certificate['W'], field) + require(actual == wanted, 'certificate isotopy') + return unit + + +def ascend(tensor, certificate, field): + """Return a K-table and K-linear maps t(Ua,Vb)=W*table(a,b).""" + n = check_tensor(tensor, field) + prime = Field(field.p, (0, 1)) + restricted = restrict_tensor(tensor, field) + unit = validate_certificate(restricted, certificate, prime) + u = pack(matvec(certificate['U'], unit, prime), field) + v = pack(matvec(certificate['V'], unit, prime), field) + basis = identity(n) + left_slice = [list(row) for row in zip(*(evaluate(tensor, u, x, field) for x in basis))] + right_slice = [list(row) for row in zip(*(evaluate(tensor, x, v, field) for x in basis))] + left, right = inverse(right_slice, field), inverse(left_slice, field) + table = isotope(tensor, left, right, identity(n), field) + result = dict(table=table, U=left, V=right, W=identity(n)) + output_unit = validate_certificate(tensor, result, field) + require(output_unit == evaluate(tensor, u, v, field), 'normalized unit') + result['unit'] = output_unit + return result diff --git a/research/commutative-scalar-ascent/verify.py b/research/commutative-scalar-ascent/verify.py new file mode 100644 index 0000000000..a5d0073d62 --- /dev/null +++ b/research/commutative-scalar-ascent/verify.py @@ -0,0 +1,216 @@ +"""Standalone checks of scalar ascent on newly constructed certificates. + +Produced by Nick Petalas. Apache-2.0. +""" + +import copy +import hashlib +import json +from pathlib import Path + +from algebra import (Field, check_algebra, evaluate, identity, inverse, isotope, + matmul, matvec, require, restrict_matrix, restrict_tensor) +from ascent import ascend + + +def truncated(variables): + """K[x_i]/(x_i^2), using bit-mask monomials.""" + require(type(variables) is int and 0 <= variables <= 2, 'fixture variable count') + n = 2**variables + table = [[[0]*n for _ in range(n)] for _ in range(n)] + for i in range(n): + for j in range(n): + if not i & j: + table[i][j][i | j] = 1 + return table + + +def square_zero(): + """The non-Gorenstein algebra K[x,y]/(x,y)^2.""" + table = [[[0]*3 for _ in range(3)] for _ in range(3)] + for i in range(3): + table[0][i][i] = table[i][0][i] = 1 + return table + + +def quadratic(field): + """A nonsplit quadratic field over each tested K.""" + if field.q == 4: + c, b = 2, 1 + elif field.q == 9: + c, b = 4, 0 + else: + raise ValueError('quadratic fixture field') + table = [[[0]*2 for _ in range(2)] for _ in range(2)] + table[0][0][0] = table[0][1][1] = table[1][0][1] = 1 + table[1][1] = [c, b] + roots = [x for x in range(field.q) if + field.add(field.mul(x, x), field.neg(field.add(c, field.mul(b, x)))) == 0] + require(not roots, 'nonsplit fixture polynomial') + return table + + +def direct_product(first, second): + a, b = len(first), len(second) + result = [[[0]*(a+b) for _ in range(a+b)] for _ in range(a+b)] + for offset, table in ((0, first), (a, second)): + for i in range(len(table)): + for j in range(len(table)): + result[offset+i][offset+j][offset:offset+len(table)] = table[i][j] + return result + + +def dualize(table): + n = len(table) + result = [[[0]*(2*n) for _ in range(2*n)] for _ in range(2*n)] + for i in range(n): + for j in range(n): + for a, b in ((0, 0), (0, 1), (1, 0)): + for k in range(n): + result[2*i+a][2*j+b][2*k+a+b] = table[i][j][k] + return result + + +def field_checks(): + triples = 0 + fields = (Field(2, (1, 1, 1)), Field(2, (1, 1, 0, 1)), + Field(3, (1, 0, 1)), Field(5, (2, 0, 1))) + for f in fields: + for a in range(f.q): + require(f.add(a, 0) == a and f.mul(a, 1) == a and + f.add(a, f.neg(a)) == 0, 'field identities') + for b in range(f.q): + require(f.mul(a, b) == f.mul(b, a) and f.add(a, b) == f.add(b, a), + 'commutative field operations') + for c in range(f.q): + require(f.mul(f.mul(a, b), c) == f.mul(a, f.mul(b, c)), 'field associativity') + require(f.add(f.add(a, b), c) == f.add(a, f.add(b, c)), 'additive associativity') + require(f.mul(a, f.add(b, c)) == f.add(f.mul(a, b), f.mul(a, c)), + 'field distributivity') + triples += 1 + return triples + + +def presentation(n, field, seed): + matrix = identity(n) + for i in range(n): + j = (i+1) % n + if i != j: + matrix[i] = [field.add(a, field.mul(1+seed % (field.q-1), b)) + for a, b in zip(matrix[i], matrix[j])] + if seed % 2 and n > 1: + matrix[0], matrix[-1] = matrix[-1], matrix[0] + inverse(matrix, field) + return matrix + + +def make_fixture(table, field, seed): + """Build an arbitrary F-basis certificate, without a predecessor routine.""" + n, prime = len(table), Field(field.p, (0, 1)) + maps = [presentation(n, field, seed+i) for i in range(3)] + tensor = isotope(table, inverse(maps[0], field), inverse(maps[1], field), maps[2], field) + restricted_table = restrict_tensor(table, field) + size = n*field.degree + h = presentation(size, prime, seed+3) + changed = isotope(restricted_table, h, h, inverse(h, prime), prime) + certificate = dict(table=changed) + for key, matrix in zip(('U', 'V', 'W'), maps): + certificate[key] = matmul(restrict_matrix(matrix, field), h, prime) + return tensor, certificate, maps, h + + +def fixture_checks(): + fields = [Field(2, (1, 1, 1)), Field(2, (1, 1, 0, 1)), + Field(3, (1, 0, 1)), Field(5, (2, 0, 1))] + cases, products, non_linear = 0, 0, 0 + witnesses = [] + for field in fields: + prime = Field(field.p, (0, 1)) + tables = [truncated(0), truncated(1), truncated(2), square_zero(), + direct_product(truncated(0), truncated(1))] + if field.q in (4, 9): + residue = quadratic(field) + tables += [residue, direct_product(residue, truncated(1)), dualize(residue)] + for number, table in enumerate(tables): + unit = check_algebra(table, field) + for seed in range(3): + tensor, certificate, maps, h = make_fixture(table, field, seed) + result = ascend(tensor, certificate, field) + require(result['unit'] == matvec(maps[2], unit, field), 'independent unit') + expected = isotope(table, inverse(maps[2], field), + inverse(maps[2], field), maps[2], field) + require(result['table'] == expected, 'independent normalized table') + scalar = [[field.p if i == j else 0 for j in range(len(table))] + for i in range(len(table))] + scalar_f = restrict_matrix(scalar, field) + non_linear += matmul(h, scalar_f, prime) != matmul(scalar_f, h, prime) + witnesses.append([field.q, number, seed, result['unit'], result['table']]) + cases += 1 + products += len(table)**2 + return dict(fixtures=cases, transported_K_basis_products=products, + non_K_linear_recovery_bases=non_linear), witnesses + + +def expect_failure(action, message): + try: + action() + except ValueError as exc: + require(message in str(exc), 'wrong rejection: '+str(exc)) + return 1 + raise ValueError('control incorrectly accepted: '+message) + + +def controls(): + field, failures = Field(2, (1, 1, 1)), 0 + tensor, cert, _, _ = make_fixture(square_zero(), field, 0) + bad = copy.deepcopy(cert) + bad['U'][0] = [0]*len(bad['U']) + failures += expect_failure(lambda: ascend(tensor, bad, field), 'linear system not unique') + bad = copy.deepcopy(cert) + bad['W'][0] = [a ^ b for a, b in zip(bad['W'][0], bad['W'][1])] + failures += expect_failure(lambda: ascend(tensor, bad, field), 'certificate isotopy') + bad = copy.deepcopy(cert) + bad['table'][0][0][0] = field.p + failures += expect_failure(lambda: ascend(tensor, bad, field), 'canonical matrix entries') + failures += expect_failure(lambda: ascend(tensor, {}, field), 'certificate keys') + failures += expect_failure(lambda: Field(2, (0, 0, 1)), 'unsupported field modulus') + failures += expect_failure(lambda: Field(True, (0, 1)), 'unsupported characteristic') + failures += expect_failure(lambda: ascend([[[0]]], cert, field), 'certificate dimension') + failures += expect_failure(lambda: restrict_tensor( + [[[0]*5 for _ in range(5)] for _ in range(5)], Field(2, (1, 1, 0, 1))), + 'restricted dimension') + bad_table = square_zero() + bad_table[1][1][2], bad_table[2][2][1] = 1, 1 + failures += expect_failure(lambda: check_algebra(bad_table, field), 'associative algebra') + bad_table = square_zero() + bad_table[1][2][1] = 1 + failures += expect_failure(lambda: check_algebra(bad_table, field), 'commutative algebra') + frobenius = lambda x, y: field.mul(field.mul(x, x), y) + require(frobenius(2, 1) != field.mul(2, frobenius(1, 1)), 'semilinear escape') + for x in range(field.q): + for y in range(field.q): + require(frobenius(field.mul(x, x), y) == field.mul(x, y), 'F-isotopy escape') + prime = Field(2, (0, 1)) + restricted = restrict_tensor(truncated(0), field) + require(all(evaluate(restricted, list(v), list(v), prime) != [0, 0] + for v in ((1, 0), (0, 1), (1, 1))), 'restriction is reduced') + require(evaluate(truncated(1), [0, 1], [0, 1], prime) == [0, 0], 'class boundary') + return dict(rejecting_controls=failures, boundary_witnesses=2) + + +def main(): + counts, witnesses = fixture_checks() + counts['field_law_triples'] = field_checks() + counts.update(controls()) + require(counts['non_K_linear_recovery_bases'] > 0, 'nonlinear basis coverage') + here = Path(__file__).resolve().parent + names = ('README.md', 'PROOF.md', 'TASK.json', 'SOURCES.json', 'VERIFY.json', + 'algebra.py', 'ascent.py', 'verify.py') + hashes = {name: hashlib.sha256((here/name).read_bytes()).hexdigest() for name in names} + digest = hashlib.sha256(json.dumps(witnesses, separators=(',', ':')).encode()).hexdigest() + print(json.dumps(dict(status='PASS_COMMUTATIVE_SCALAR_ASCENT', **counts, + witness_sha256=digest, source_sha256=hashes), sort_keys=True)) + + +if __name__ == '__main__': + main()