From e88627a4a85d57d204e950e9b35c29736490bbae Mon Sep 17 00:00:00 2001 From: Nick Petalas Date: Wed, 28 Oct 2026 16:26:22 +0000 Subject: [PATCH] feat(research): prove single lower-phase deletion --- research/single-lower-phase-deletion/PROOF.md | 183 +++++++++++ .../single-lower-phase-deletion/README.md | 155 +++++++++ .../single-lower-phase-deletion/SOURCES.json | 48 +++ .../single-lower-phase-deletion/TASK.json | 94 ++++++ .../single-lower-phase-deletion/VERIFY.json | 34 ++ .../single-lower-phase-deletion/verify.py | 297 ++++++++++++++++++ 6 files changed, 811 insertions(+) create mode 100644 research/single-lower-phase-deletion/PROOF.md create mode 100644 research/single-lower-phase-deletion/README.md create mode 100644 research/single-lower-phase-deletion/SOURCES.json create mode 100644 research/single-lower-phase-deletion/TASK.json create mode 100644 research/single-lower-phase-deletion/VERIFY.json create mode 100644 research/single-lower-phase-deletion/verify.py diff --git a/research/single-lower-phase-deletion/PROOF.md b/research/single-lower-phase-deletion/PROOF.md new file mode 100644 index 0000000000..08d32990f4 --- /dev/null +++ b/research/single-lower-phase-deletion/PROOF.md @@ -0,0 +1,183 @@ +# Deleting one lower-only phase + +This contribution was produced by Nick Petalas. Apache-2.0. + +## Exact model and statement + +Fix a field k, a positive width m and a finite number R of scalar registers. +Write + +\[ + u_A=\begin{pmatrix}I&A\\0&I\end{pmatrix},\qquad + v_K=\begin{pmatrix}I&0\\K&I\end{pmatrix},\qquad + U=\{u_A:A\in M_m(k)\},\quad V=\{v_K:K\in M_m(k)\}. +\] + +Let C be any commutative coefficient ring. The application here is k=Q and +C=F2, with rational or dyadic address matrices and free binary register +mixing. Brackets denote *formal group-algebra labels*, not evaluation of +an address matrix in characteristic two. + +Consider a state matrix + +\[ + X=LFB,\qquad L,B\in M_R(C[U]),\qquad F\in M_R(C[V]). +\] + +Let epsilon:C[V]->C be augmentation, sending every [v_K] to 1. +For any chosen set of matrix entries J, assume X_ij belongs to C[U] for +every (i,j) in J. Then + +\[ + \boxed{X_{ij}=(L\,\epsilon(F)\,B)_{ij}\quad((i,j)\in J).} +\] + +Thus the lower-only phase can be replaced by its scalar augmentation +without changing any required upper-supported entry. No condition is +imposed on other entries. With clean auxiliaries initially zero, J can be +just the data-to-data block and auxiliary outputs can be garbage. With +arbitrary dirty auxiliaries, J must also include each required data-from- +auxiliary zero entry. Any required restoration entries must likewise be +included. If every entry is upper-supported, the entire formal endpoint +is unchanged. + +For a circuit, L and B consist of upper-shear paid calls and scalar mixing. +F consists of any finite sequence of lower-left updates on individual +registers and scalar mixing, with no intervening upper call. Its +augmentation is precisely the product of the scalar mixing matrices in +that phase. Every lower update augments to identity. If those mixing +matrices are invertible, their product is an allowed free mixing map. +Deleting the lower updates preserves every paid call and its rational rank. + +This is a scoped reduction. Internal register-dependent Levi maps, +additional alternating lower phases and endpoints with non-upper labels +are not covered. General full-Borel words remain open. + +## The label lemma + +Direct multiplication over k gives + +\[ + u_Av_Ku_D= + \begin{pmatrix} + I+AK&A+D+AKD\\K&I+KD + \end{pmatrix}. \tag{1} +\] + +Suppose u_A v_K u_D = u_(A') v_(K') u_(D'). The lower-left +block gives K=K'. The two diagonal blocks give AK=A'K and KD=KD'. +Consequently + +\[ + AKD=A'KD=A'KD', +\] + +and comparison of the upper-right blocks gives A+D=A'+D'. +No inverse of K, integrality condition or rank assumption was used. +This includes K=0, when the label is simply u_(A+D). + +Therefore the following map on the *set of distinct group labels* is +well-defined: + +\[ + f:UVU\longrightarrow U,\qquad f(u_Av_Ku_D)=u_{A+D}. \tag{2} +\] + +It is identity on U. For all E,H it satisfies + +\[ + f(u_E g u_H)=u_E f(g)u_H. \tag{3} +\] + +Indeed prefixing and suffixing just replace A,D by E+A,D+H. +The additive identity u_E u_A=u_(E+A) proves (3). + +Extend f C-linearly to the free C-module spanned by UVU, calling the map +P. Equal labels have equal images by the lemma, so cancellations in the +formal group algebra are respected. Equation (3) makes P a C[U]-bimodule +map, and P fixes C[U]. It is not asserted to be a ring homomorphism or to +extend to the entire group algebra. + +## Circuit reduction + +Every entry of LFB lies in the span of UVU. Expand its finite sums and +apply (2) term by term. For upper labels a,b and a lower label v, + +\[ + P([a][v][b])=[a][b]. +\] + +Linearity and matrix multiplication therefore give + +\[ + P(LFB)=L\,\epsilon(F)\,B. \tag{4} +\] + +At each required entry, the upper-support assumption gives P(X_ij)=X_ij. +Equation (4) proves the statement. This works over every C, in particular +the binary superposition algebra, without reducing rational addresses +modulo two. Arbitrarily many registers do not change the argument. + +A contiguous phase in an ordinary left-multiplication circuit has the +required factorization. The analogous right-multiplication circuit also +does. If a model allows both left and right moves, the assertion requires +the displayed *final factorization*, not just contiguity in wall-clock +order. A phase acting on both sides of an existing upper word can leave +two lower factors separated by that word. No reduction for that broader +bidirectional case is asserted. + +## What changes for the source question + +Sagar Thakrar's [PR2613](https://github.com/CrocSwap/integer-mult-bounds/pull/2613) +asks whether inserting D+=K H can escape the upper-shear superposition +obstruction, beginning with one such update. The theorem above removes +*every* contiguous lower-only phase under the explicit upper-supported +endpoint and alphabet conditions. It covers singular K and even +denominators, which a mod-two natural-representation argument cannot +automatically cover. + +Any obstruction already established for the remaining upper-only word +therefore transfers without changing its paid profile. The existing +width-two abelian floor, when its full target hypotheses are supplied, is +a predecessor premise from eumemic's PR288 as cited by PR2613. No new +derivation or replay of that floor is claimed here. In particular, this +package's new theorem is not a new census of three-call words or a claim +about every full-Borel word. dcharb78's PR3183 separately reports a finite +width-two block-Borel screen; it is not used in this proof. + +## Why the hypotheses matter + +If a required entry may retain a lower label, deletion need not preserve +it: the one-register word v_1 differs from identity. + +Allowing an additional internal Levi factor also breaks naive deletion. +In one dimension let d=diag(2,1). Then + +\[ + u_1\,d\,u_{-1/2}\,d^{-1}=I, +\] + +but deleting d and d^-1 leaves u_(1/2). This is a control on enlarging the +middle alphabet, not a counterexample to the lower-unipotent theorem. + +Nor may one apply P as an unrestricted multiplicative map across many +alternating lower phases. In one address dimension, + +\[ + u_1v_1u_1v_{-1/3}u_{-3}v_{-1/3}=I, \tag{5} +\] + +whereas deleting the three separated lower factors leaves u_-1. +Equation (5) follows by direct 2-by-2 multiplication. It supplies no +profitable paid word and no physical construction; it rejects a false +unrestricted deletion rule. + +## Evidence boundary + +The universal result is the algebraic proof above. The standalone verifier +checks literal matrix products, complete small finite-field collision +classes, singular rational fixtures, and full formal superposition words. +It imports no predecessor executable and supplies no finite-to-universal +inference. Physical legality, native realization, chronological compiler, +restoration outside the declared endpoint, precision/tape/stock and the +complete signed invoice remain separate. No new kappa is claimed. diff --git a/research/single-lower-phase-deletion/README.md b/research/single-lower-phase-deletion/README.md new file mode 100644 index 0000000000..7ea5d40041 --- /dev/null +++ b/research/single-lower-phase-deletion/README.md @@ -0,0 +1,155 @@ +# One lower-only phase cannot change an upper-shear endpoint + +This contribution was produced by Nick Petalas. Apache-2.0. + +A contiguous phase of lower-left updates and binary register mixing can be +deleted from a rational upper-shear superposition word whenever its required +data entries are supported on upper-shear labels. The replacement preserves +those entries and every paid call, including its rational rank. Width, +register count, rational denominators and the rank of each lower update are +unrestricted in the written theorem. + +This is a **scoped proof with exact finite corroboration**, not a search +failure, new finite supplier or complete multiplication theorem. No new +kappa is claimed. + +## The new reduction + +For upper shears u_A and lower shears v_K, the map + +\[ + [u_Av_Ku_B]\longmapsto[u_{A+B}] +\] + +is well-defined on distinct formal labels. This remains true for singular +K. Its linear extension is an upper-shear bimodule retraction. Therefore, +if X=L F B with L,B over the upper-shear group algebra and F over the +lower-shear group algebra, then + +\[ + P(X)=L\,\epsilon(F)\,B. +\] + +At every required entry already supported on upper labels, P is identity. +The scalar augmentation epsilon(F) is exactly the phase's binary mixing +after all lower updates are deleted. [PROOF.md](PROOF.md) gives the full +argument over any address field and any commutative coefficient ring. + +For ordinary circuits with all moves multiplying on one side, a contiguous +lower-only phase has this factorization. In a model with both left and +right actions, the final factorization must be supplied separately. +Contiguity in chronological order alone is insufficient for this argument. + +## Reproduce + +From the repository root, with CPython 3.12 and its standard library: + +```sh +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/single-lower-phase-deletion/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -O -B research/single-lower-phase-deletion/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/single-lower-phase-deletion +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/single-lower-phase-deletion --check-source-history +``` + +Any CPython 3.12 executable may replace the displayed path. Each direct run +prints `PASS_SINGLE_LOWER_PHASE_DELETION` in a generated JSON receipt bound +to the package files by SHA256. Default replay writes no files. The same +standalone check works without Git or predecessor packages. + +The verifier checks: + +- All 4,256 triples in four complete finite-field domains: width one over + F2, F3 and F5, and width two over F2. It compares all 1,420 repeated labels + with their previously computed A+B. The respective distinct-label counts + are 6, 21, 105 and 2,704. +- 144 literal rational triples at widths one through three, including 92 + singular K matrices, and 144 outer bimodule identities. An independent + recovery formula uses a checked inner inverse H with K H K=K, rather + than the generating A and B. +- 24 complete binary group-algebra factorizations, containing 112 entries. + Projection agrees with phase deletion throughout; all 42 upper-supported + entries agree directly. +- Six hypothesis or mutation controls and three invalid-dimension + rejections. These distinguish a singular-K collision, an incorrect raw + upper-right-block rule, a non-upper endpoint, internal Levi maps, + separated lower phases and unconstrained auxiliary output. Checks remain + enabled under optimized Python. + +Finite checks corroborate the written proof. No finite enumeration is used +to infer its all-width conclusion. + +## Scope and predecessor credit + +The source question is the first open question of Sagar Thakrar's +[PR2613](https://github.com/CrocSwap/integer-mult-bounds/pull/2613), which +proposes one inserted lower-left update in a rational shear superposition +word. That package supplies the model and the distinct 2-integral +obstruction. eumemic's PR288 supplies the original register model and +upper-only width-two obstruction; Swapnil Jain's framework supplies the +credited related rank functional and free class. Their scientific results +are cited as premises, not replayed or claimed as new here. + +ywz65's [PR2671](https://github.com/CrocSwap/integer-mult-bounds/pull/2671) +and Nick Petalas's +[PR6027](https://github.com/CrocSwap/integer-mult-bounds/pull/6027) concern +common invariant lattice filters. This theorem uses no integrality or +lattice-feasibility assumption and does not extend those filters. +dcharb78's [PR3183](https://github.com/CrocSwap/integer-mult-bounds/pull/3183) +reports a separate finite width-two block-Borel screen. This contribution +neither audits that screen nor claims its call-count result. Exact main +READMEs and the source proof are pinned as provenance in +[SOURCES.json](SOURCES.json); no predecessor executable is imported. + +The active card is `bit-helper-contract`, changed from G20 helper +construction to the explicit full-Borel handoff. This is a local interface +obstruction relevant to a proposed way around paid-call floors. Its new +step is the single-phase deletion theorem. General literature priority +for elementary block multiplication or bimodule methods is unclaimed. +The [advance claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19246973) +records the question and source baseline. + +Required endpoints must be supported on upper labels. Arbitrary independent +internal Levi maps, multiple alternating lower phases and an arbitrary +bidirectional chronological phase are outside the theorem. The supplied +Levi and three-phase identities reject broader naive deletion rules. +No complete full-Borel impossibility result is claimed. The reduction +preserves an existing paid profile; it does not produce an improved one. + +Physical lower-update legality, native operators, boundary conversions, +dirty restoration beyond the declared data block, stock, precision/tape, +uniform compiler and the full signed invoice remain separate obligations. +No selected-word replay, native replay, Lean, Docker or complete multiplier +ran. Independent human and formal proof-kernel review are unclaimed. + +## Open next questions + +- Can separated lower-only phases provide a favorable completed rational + superposition word? Start with a width-two word with two such phases, + its full formal data block and complete paid/target invoice. No such + saving word or physical caller is supplied here; the projection cannot + be multiplied across arbitrary phases. +- What deletion criterion survives internal register-dependent Levi maps? + Specify the enlarged middle alphabet and test equality of double-coset + labels against the proposed deleted labels. The simple Levi identity + already rejects naive deletion, so another search needs a changed + reduction and full boundary accounting. + +Structured first steps and blockers are in [TASK.json](TASK.json). + +## Implementation bounds + +The executable is a bounded verifier, not a public matrix solver. Its +largest address matrix is 6 by 6, scalar register count is at most three, +and group-algebra support is capped at 256 labels per entry. Finite-field +enumeration has at most 16^3 triples per domain. Functions remain below +60 physical lines, control flow is nonrecursive, and invariant checks use +explicit exceptions that survive `-O`. + +Power-of-ten rule 3 has a managed-runtime deviation in `verify.py`. +CPython allocates exact Fraction values, tuples and sets during checking. +Fixed dimensions, fixture counts, rational input alphabets and support +caps bound the computation and live data. No external matrix or circuit +is read. Each declared replay has a 60-second timeout. A public solver +would require separate bit-size and memory budgets. Warning-strict normal +and optimized runs provide the available standard-library diagnostics; +there is no project Python type-checker configuration for this package. diff --git a/research/single-lower-phase-deletion/SOURCES.json b/research/single-lower-phase-deletion/SOURCES.json new file mode 100644 index 0000000000..ca4e5d5827 --- /dev/null +++ b/research/single-lower-phase-deletion/SOURCES.json @@ -0,0 +1,48 @@ +{ + "schema_version": 1, + "base_commit": "721c03822c421b7f7fcbb2598993b947c4d88419", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "d59b5035e7b4cbaa9d688a1d32dd0d6eb79c466a", + "sha256": "9b8d0eea95b3bf0dfcb7938a732a6439b87a2685dec2a5ab9e525b3b34debbfa" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec", + "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81" + }, + { + "path": "research/bit-full-borel-2adic-floor/README.md", + "usage": "provenance", + "git_blob": "7ab7cdc4fab95a91939eef7fe1a220fa6a02343f", + "sha256": "9237eae400e6d63ee1f3f53bf75ff29b4136d9d1d354c3a8d25a691711813af2" + }, + { + "path": "research/bit-full-borel-2adic-floor/PROOF.md", + "usage": "provenance", + "git_blob": "f5b6ff4c8ce068a3f31d9dfa55b9c92daf2bc3de", + "sha256": "c88a75a10400b931c604c30c0d84395966c4c10cfe39b1f9ee15ac8a565aa8de" + }, + { + "path": "research/paired-diagonal-borel-gauge/README.md", + "usage": "provenance", + "git_blob": "55788f0f6b209d800f19cf53a29403500071e1d5", + "sha256": "beb65171fd265dfaadef59aa778c5192d9880217a2c10d88c48184a8b25972f1" + }, + { + "path": "research/projector-anchored-paired-lattices/README.md", + "usage": "provenance", + "git_blob": "f41634f35d442bf5f9c0426904f5c145f6f561da", + "sha256": "85f055f11f6932a0e11f7d85c9481d920a9e452f9dbbf13375b279bc464e3338" + }, + { + "path": "research/r439-sub10k-sixway-and-star-dual-witnesses/README.md", + "usage": "provenance", + "git_blob": "3425f0ac5f6e53f421f33519f2e7a5eb532b427e", + "sha256": "55c39aa7aa4ac2096d7086a8847c3a06d471c5c90928862f6fe1265b536bdb21" + } + ] +} diff --git a/research/single-lower-phase-deletion/TASK.json b/research/single-lower-phase-deletion/TASK.json new file mode 100644 index 0000000000..898fa183d2 --- /dev/null +++ b/research/single-lower-phase-deletion/TASK.json @@ -0,0 +1,94 @@ +{ + "schema_version": 1, + "task_id": "bit-helper-contract", + "priority_revision": 8, + "base_commit": "721c03822c421b7f7fcbb2598993b947c4d88419", + "original_card": { + "id": "bit-helper-contract", + "question": "Can a changed G20 helper path or independent-target split improve the complete BIT moment without losing its physical endpoint?", + "starting_points": [ + "docs/research/current-priorities.md", + "docs/research/research-family-status.md", + "certificates/selected-result.json", + "docs/research/pr-intake-evidence/pr5599-completion/PROOF-REVIEW.md", + "research/g20-helper-split/README.md", + "research/g20-conjugation-admission/README.md" + ], + "methods": [ + "Construct and independently check one source-bound instance of the stated first experiment.", + "Seek an exact counterexample or target-specific complete-budget obstruction to that same proposed change." + ], + "acceptance_gate": "A full boundary contract and paid profile; unchanged scalar counts alone are insufficient. A scoped local result may be retained without a complete supplier. Expanding it into further construction rounds requires the family-level budget and obligation gate in research-family-status.md; an optimistic passing relaxation alone is not acceptance.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_selected_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Read revision 8, the selected review and live exact-source handoffs. Then follow this card's bounded first_experiment.", + "scope": "Source-bound orientation only, not a supplier replay or theorem proof." + }, + "first_experiment": "First read #5679/#5708 and their audits as pending component proposals. Choose one uncovered helper group/cut on an exact word; compare arbitrary-input native action, targets, owned storage, both orientations and full signed bill. Stop if the gain is only a scalar count or repaid by lost targets. Do not rerun the frozen #5609 common-frame domain without changing its hypothesis.", + "bottleneck_link": "Judge the actual current supplier contract and complete signed target/paid bill; frozen-profile ceilings require an applicability proof.", + "allowed_variations": [ + "One exact source head, helper/cut region or quantified proposition and changed hypothesis; check live handoffs first. Different seeds are not different scopes." + ], + "scope_change_triggers": [ + "Changing source head, helper/cut domain, operation alphabet or caller boundary without recording the new scope.", + "Treating an archived proposal or local numerical pass as complete supplier admission." + ], + "overlap_terms": [ + "G20", + "helper split", + "5679", + "5708", + "independent target" + ], + "existing_checks": [ + { + "scope": "Selected PR5599: complete helper-subspace construction and independent caller replay; five framework assumptions remain.", + "evidence": "docs/research/pr-intake-evidence/pr5599-completion/PROOF-REVIEW.md", + "remaining": "The next experiment must identify uncovered source-specific work. Successor archive intake does not transfer this admission.", + "status": "reviewed", + "source_commit": "09dd0965711ca7eeb169057a420abab1c9052137", + "selected_record_sha256": "2a0220e866417774606e0f991e41b9c1d26b1f43b97857238cf478dbc7d330b5" + } + ] + }, + "scope_status": "changed", + "actual_scope": "Delete a single lower-unipotent phase L F B in rational shear superposition words, preserving all upper-supported required data entries and the exact paid profile.", + "scope_change_reason": "The active G20 helper card is changed to the explicit rational full-Borel handoff in PR2613. The new result is an arbitrary-width algebraic reduction, not a G20 census, lattice filter, predecessor audit or physical supplier.", + "bottleneck_link": "A proposed nonabelian escape from upper-shear call obstructions must change the paid/target interface. This theorem eliminates one entire lower-only phase under a named factorization and endpoint contract, identifying the necessary interleaving, Levi or endpoint change before further construction.", + "budget_minutes": 60, + "stop_rule": "Stop at the first proved deletion result and package it. Do not search larger full-Borel words or rerun predecessor floors.", + "outcome": "completed", + "evidence": "PROOF.md proves the label retraction and L F B deletion over arbitrary fields and coefficient rings. verify.py corroborates 4256 finite-field triples, 144 rational triples including 92 singular K, 144 bimodule identities, 24 formal factorizations and explicit hypothesis controls.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "Can two or more separated lower-only phases provide a favorable complete rational superposition word?", + "why_it_matters": "The deletion theorem removes the single-phase route without changing its paid profile. A genuinely interleaved construction escapes that theorem.", + "first_step": "Specify one width-two word with two separated lower phases, its full formal data block, all free factors and the complete paid/target invoice.", + "blocked_by": "No saving word or full physical caller is supplied; the single-phase projection cannot be multiplied across arbitrary phases." + }, + { + "question": "What is the exact deletion criterion when internal register-dependent Levi maps are admitted?", + "why_it_matters": "These maps belong to the broader full-Borel handoff and are excluded from this theorem.", + "first_step": "State the enlarged middle alphabet and test whether equality of its double-coset labels forces equality of the proposed deleted labels.", + "blocked_by": "The simple Levi identity in PROOF.md already rejects naive deletion; a changed reduction needs its own boundary and cost proof." + } + ], + "claim_url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19246973", + "upstream_checkpoint": { + "commit": "721c03822c421b7f7fcbb2598993b947c4d88419", + "priority_revision": 8, + "utc": "2026-10-28T16:12:07Z" + }, + "environment": { + "python": "Python 3.12.15", + "platform": "Darwin arm64" + }, + "claim_type": "scoped proof with finite corroboration" +} diff --git a/research/single-lower-phase-deletion/VERIFY.json b/research/single-lower-phase-deletion/VERIFY.json new file mode 100644 index 0000000000..d41d175685 --- /dev/null +++ b/research/single-lower-phase-deletion/VERIFY.json @@ -0,0 +1,34 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 60, + "checks": "Exact collision classes, rational singular-K projection, bimodule identity, full binary formal factorizations, endpoint and alphabet controls." + }, + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-O", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 60, + "checks": "The same exact checks with assertions disabled; explicit contracts and rejection controls remain active." + } + ] +} diff --git a/research/single-lower-phase-deletion/verify.py b/research/single-lower-phase-deletion/verify.py new file mode 100644 index 0000000000..66e95fcd69 --- /dev/null +++ b/research/single-lower-phase-deletion/verify.py @@ -0,0 +1,297 @@ +"""Exact finite corroboration of PROOF.md; standard library, read-only. + +Produced by Nick Petalas. Apache-2.0. +""" + +import hashlib +import itertools +import json +import random +from fractions import Fraction as Q +from math import isqrt +from pathlib import Path + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def dimension(a): + n = isqrt(len(a)) + require(n * n == len(a) and 1 <= n <= 6, "matrix extent") + return n + + +def identity(n): + require(1 <= n <= 6, "identity extent") + return tuple(Q(i == j) for i in range(n) for j in range(n)) + + +def add(a, b, sign=1): + require(len(a) == len(b), "addition extent") + return tuple(x + sign * y for x, y in zip(a, b)) + + +def multiply(a, b): + n = dimension(a) + require(len(b) == len(a), "product extent") + return tuple(sum((a[i*n+k] * b[k*n+j] for k in range(n)), Q(0)) + for i in range(n) for j in range(n)) + + +def shear(a, lower=False): + m = dimension(a) + require(m <= 3, "shear width") + n = 2 * m + g = list(identity(n)) + for i in range(m): + for j in range(m): + row, col = (m+i, j) if lower else (i, m+j) + g[row*n+col] = a[i*m+j] + return tuple(g) + + +def block(g, row, col): + n = dimension(g) + require(n % 2 == 0 and row in (0, 1) and col in (0, 1), "block") + m = n // 2 + return tuple(g[(row*m+i)*n+col*m+j] for i in range(m) for j in range(m)) + + +def inner_inverse(k): + """Row/column elimination gives D=P K T, and H=T D P.""" + n = dimension(k) + a, p, t = [list(x) for x in (k, identity(n), identity(n))] + rank = 0 + for z in range(n): + pivots = [(i, j) for i in range(z, n) for j in range(z, n) + if a[i*n+j]] + if not pivots: + break + i, j = pivots[0] + for x in (a, p): + for c in range(n): + x[z*n+c], x[i*n+c] = x[i*n+c], x[z*n+c] + for x in (a, t): + for r in range(n): + x[r*n+z], x[r*n+j] = x[r*n+j], x[r*n+z] + pivot = a[z*n+z] + for x in (a, p): + for c in range(n): + x[z*n+c] /= pivot + for r in range(n): + if r != z: + coefficient = a[r*n+z] + for x in (a, p): + for c in range(n): + x[r*n+c] -= coefficient * x[z*n+c] + for c in range(n): + if c != z: + coefficient = a[z*n+c] + for x in (a, t): + for r in range(n): + x[r*n+c] -= coefficient * x[r*n+z] + rank += 1 + d = tuple(Q(i == j and i < rank) for i in range(n) for j in range(n)) + require(tuple(a) == d, "elimination diagonal") + h = multiply(multiply(tuple(t), d), tuple(p)) + require(multiply(multiply(k, h), k) == k, "inner inverse identity") + return h + + +def project_label(g): + """For known UVU labels recover A+B without the generating A or B.""" + m = dimension(g) // 2 + k = block(g, 1, 0) + left = add(block(g, 0, 0), identity(m), -1) + right = add(block(g, 1, 1), identity(m), -1) + correction = multiply(multiply(left, inner_inverse(k)), right) + return shear(add(block(g, 0, 1), correction, -1)) + + +def is_upper(g): + m = dimension(g) // 2 + zero = (Q(0),) * (m*m) + return (block(g, 1, 0) == zero and block(g, 0, 0) == identity(m) + and block(g, 1, 1) == identity(m)) + + +def finite_product(a, b, n, prime): + return tuple(sum(a[i*n+k]*b[k*n+j] for k in range(n)) % prime + for i in range(n) for j in range(n)) + + +def collision_checks(): + triples = collisions = 0 + classes = [] + for m, prime in ((1, 2), (1, 3), (1, 5), (2, 2)): + matrices = list(itertools.product(range(prime), repeat=m*m)) + labels = {} + for a, k, b in itertools.product(matrices, repeat=3): + ua, vk, ub = (tuple(map(int, shear(x, low))) + for x, low in ((a, False), (k, True), (b, False))) + g = finite_product(finite_product(ua, vk, 2*m, prime), ub, 2*m, prime) + total = tuple((x+y) % prime for x, y in zip(a, b)) + if g in labels: + require(labels[g] == total, "finite collision changes A+B") + collisions += 1 + labels[g] = total + triples += 1 + classes.append({"width": m, "prime": prime, "labels": len(labels)}) + return {"triples": triples, "repeated_labels": collisions, "domains": classes} + + +def rational_checks(rng): + counts = {"triples": 0, "singular_k": 0, "bimodule": 0} + values = (Q(-2), Q(-1, 2), Q(0), Q(1, 3), Q(1), Q(3, 2)) + for m in (1, 2, 3): + for index in range(48): + a, b, e, h = [tuple(rng.choice(values) for _ in range(m*m)) + for _ in range(4)] + k = tuple(Q(i == j and i < index % (m+1)) + for i in range(m) for j in range(m)) + s, t = list(identity(m)), list(identity(m)) + if m > 1: + s[1], t[m] = Q(1, 2), Q(-2, 3) + k = multiply(multiply(tuple(s), k), tuple(t)) + g = multiply(multiply(shear(a), shear(k, True)), shear(b)) + require(project_label(g) == shear(add(a, b)), "rational projection") + outer = multiply(multiply(shear(e), g), shear(h)) + target = shear(add(add(e, add(a, b)), h)) + require(project_label(outer) == target, "bimodule law") + counts["triples"] += 1 + counts["singular_k"] += index % (m+1) < m + counts["bimodule"] += 1 + return counts + + +def algebra_product(a, b): + require(len(a) <= 256 and len(b) <= 256, "algebra support bound") + result = set() + for x in a: + for y in b: + z = multiply(x, y) + result.symmetric_difference_update((z,)) + require(len(result) <= 256, "algebra result bound") + return frozenset(result) + + +def state_identity(registers, m): + one = frozenset((identity(2*m),)) + return [[one if i == j else frozenset() for j in range(registers)] + for i in range(registers)] + + +def state_product(a, b): + r = len(a) + require(r == len(b) and 1 <= r <= 3, "register extent") + result = [[frozenset() for _ in range(r)] for _ in range(r)] + for i in range(r): + for j in range(r): + for z in range(r): + result[i][j] ^= algebra_product(a[i][z], b[z][j]) + return result + + +def projected(state): + result = [] + for row in state: + output = [] + for cell in row: + value = set() + for g in cell: + value.symmetric_difference_update((project_label(g),)) + output.append(frozenset(value)) + result.append(output) + return result + + +def phase(rng, registers, m, lower): + state = state_identity(registers, m) + augmented = state_identity(registers, m) + for _ in range(2): + role = rng.randrange(registers) + frame = tuple(rng.choice((Q(-1, 2), Q(0), Q(1))) for _ in range(m*m)) + gate = state_identity(registers, m) + gate[role][role] = frozenset((shear(frame, lower),)) + state = state_product(gate, state) + if registers > 1: + target, source = rng.sample(range(registers), 2) + mixing = state_identity(registers, m) + mixing[target][source] = frozenset((identity(2*m),)) + state = state_product(mixing, state) + augmented = state_product(mixing, augmented) + return state, augmented + + +def circuit_checks(rng): + counts = {"factorizations": 0, "entries": 0, "upper_supported_entries": 0} + for m, registers in itertools.product((1, 2), (1, 2, 3)): + for _ in range(4): + left, _ = phase(rng, registers, m, False) + right, _ = phase(rng, registers, m, False) + middle, augmentation = phase(rng, registers, m, True) + actual = state_product(state_product(left, middle), right) + deleted = state_product(state_product(left, augmentation), right) + require(projected(actual) == deleted, "formal phase identity") + for i in range(registers): + for j in range(registers): + if all(is_upper(g) for g in actual[i][j]): + require(actual[i][j] == deleted[i][j], "endpoint deletion") + counts["upper_supported_entries"] += 1 + counts["entries"] += 1 + counts["factorizations"] += 1 + require(counts["upper_supported_entries"] > 0, "endpoint coverage") + return counts + + +def controls(): + zero, one = (Q(0),), (Q(1),) + k = (Q(1), Q(0), Q(0), Q(0)) + d = (Q(0), Q(0), Q(0), Q(1, 2)) + vk = shear(k, True) + require(multiply(multiply(shear(d), vk), shear(tuple(-x for x in d))) == vk, + "singular collision witness") + require(shear(d) != identity(4), "left-only mutant survives") + g = multiply(multiply(shear(one), shear(one, True)), shear(one)) + require(shear(block(g, 0, 1)) != project_label(g), "raw block mutant survives") + require(shear(one, True) != project_label(shear(one, True)), "endpoint control") + diagonal = (Q(2), Q(0), Q(0), Q(1)) + inverse = (Q(1, 2), Q(0), Q(0), Q(1)) + levi_word = multiply(multiply(multiply(shear(one), diagonal), shear((Q(-1, 2),))), inverse) + require(levi_word == identity(2) and shear((Q(1, 2),)) != levi_word, "Levi control") + word = identity(2) + for value, lower in ((1, False), (1, True), (1, False), + (Q(-1, 3), True), (-3, False), (Q(-1, 3), True)): + word = multiply(word, shear((Q(value),), lower)) + require(word == identity(2) and shear((Q(-1),)) != word, "alternation control") + state = state_identity(3, 2) + state[2][2] = frozenset((vk,)) + require(projected(state) == state_identity(3, 2), "auxiliary projection") + require(state[0][:2] == state_identity(3, 2)[0][:2], "clean data boundary") + failures = 0 + for bad in ((), (Q(1), Q(2)), (Q(0),) * 49): + try: + dimension(bad) + except ValueError: + failures += 1 + require(failures == 3, "dimension rejection") + require(project_label(shear(zero)) == identity(2), "zero K coverage") + return {"hypothesis_and_mutation_controls": 6, "dimension_rejections": failures} + + +def main(): + rng = random.Random(2613001) + counts = {"collisions": collision_checks(), "rational": rational_checks(rng), + "circuits": circuit_checks(rng), "controls": controls()} + package = Path(__file__).resolve().parent + files = sorted(p for p in package.iterdir() if p.is_file()) + hashes = {p.name: hashlib.sha256(p.read_bytes()).hexdigest() for p in files} + print(json.dumps({"status": "PASS_SINGLE_LOWER_PHASE_DELETION", "counts": counts, + "claim_type": "scoped proof with finite corroboration", + "sha256": hashes}, indent=2, sort_keys=True)) + + +if __name__ == "__main__": + main()