From 1927d11aee9c32a76ccaf531d0b223c966d637e0 Mon Sep 17 00:00:00 2001 From: Nick Petalas Date: Wed, 11 Nov 2026 11:29:05 +0000 Subject: [PATCH] docs(research): classify both active feedback edges --- research/two-edge-feedback-rigidity/PROOF.md | 150 ++++++++++++ research/two-edge-feedback-rigidity/README.md | 81 +++++++ .../two-edge-feedback-rigidity/SOURCES.json | 36 +++ research/two-edge-feedback-rigidity/TASK.json | 90 +++++++ .../two-edge-feedback-rigidity/VERIFY.json | 34 +++ research/two-edge-feedback-rigidity/verify.py | 220 ++++++++++++++++++ 6 files changed, 611 insertions(+) create mode 100644 research/two-edge-feedback-rigidity/PROOF.md create mode 100644 research/two-edge-feedback-rigidity/README.md create mode 100644 research/two-edge-feedback-rigidity/SOURCES.json create mode 100644 research/two-edge-feedback-rigidity/TASK.json create mode 100644 research/two-edge-feedback-rigidity/VERIFY.json create mode 100644 research/two-edge-feedback-rigidity/verify.py diff --git a/research/two-edge-feedback-rigidity/PROOF.md b/research/two-edge-feedback-rigidity/PROOF.md new file mode 100644 index 0000000000..79ae26c174 --- /dev/null +++ b/research/two-edge-feedback-rigidity/PROOF.md @@ -0,0 +1,150 @@ +# Rigidity of the two existing feedback edges + +This scoped proof and its new verifier were produced by Nick Petalas. +Apache-2.0. The saved-bank interface and its known attaining pair are credited +to unpaidmoon, PR #6961, building on Cinna Davis's PR #5220 active schedule. + +## The inherited interface + +Rightmost operators act first. Write Q for the central Gaussian, C for C1, +D for D1 and b for the unchanged third-input coefficient +Q^-1 C3 D1 D3. Let F and G be the two feedback operators, respectively. +The predecessor's saved first-FULL Y row and the pre-query-2 coded X row are + +```text +L = [Q^-1 C D, D, -Q^-1 C D, 0], +K = [0, -Q D, C D, 0]. +``` + +Here K is C times the pair-0 X row at that cut. Query 2 returns +S = Q^-1 (K + F L). The cancellation identity in #6961 gives the row after +query 4 as + +```text +R(F,G) = B + Q^-1 G Q^-1 (K + F L), +B = [0, 0, b, 0]. (1) +``` + +These are inherited schedule premises, not a new native replay. For reference, +the zero x0 column of K is the cancellation of the first thin against FULL1; +the bridge adds D x1 to that X bank. The full schedule, phase conventions, +owned captures and helper contracts remain those of the cited predecessors. +This contribution begins with (1) and classifies both F and G simultaneously. + +## Theorem + +Let A be any associative unital ring. Let Q,D be units in A, let C^2=1, +and assume QD=DQ. Take any b in A and define (1). The operators F,G may +be arbitrary elements of A; their invertibility is not assumed. Then + +```text +R(F,G) = [D Q^-1, 0, b, 0] + if and only if +F = Q and G = C Q. (2) +``` + +It already suffices to impose the following two constraints on the row: + +```text +R_1 = 0, +R_0 + R_2 = D Q^-1 + b. (3) +``` + +Subscripts 0,1,2,3 correspond to the four original input banks x0,y0,x1,y1. +This is a statement about independent coefficients, so it retains arbitrary +values in all four banks. + +### Proof + +The saved row satisfies L_0+L_2=0, whereas K_0+K_2=C D. Hence (1) gives + +```text +R_0+R_2-b = Q^-1 G Q^-1 C D. (4) +``` + +The sum has eliminated F without any assumption about F. If (3) holds, +equation (4), followed by right multiplication by D^-1, gives + +```text +Q^-1 G Q^-1 C = D Q^-1 D^-1 = Q^-1. +``` + +Multiply on the left by Q and on the right by C Q. Since C^2=1, +this forces G=C Q. In particular, G is forced to be a unit even though +the theorem did not assume it. + +Substituting this value into the second-input column of (1) gives + +```text +R_1 = Q^-1 C (F-Q) D. +``` + +Both outside factors are units. Therefore R_1=0 forces F=Q. +This proves necessity using only (3). Conversely, with F=Q and G=C Q, + +```text +K+Q L = [C D, 0, 0, 0], +R(Q,C Q) = B + Q^-1 C [C D, 0, 0, 0] + = [Q^-1 D, 0, b, 0] + = [D Q^-1, 0, b, 0]. +``` + +This also proves sufficiency and the equivalence of (2) and (3). No field +division, determinant, degree argument, word enumeration, faithful group +representation, Q^4 relation or C/D commutation was used. In particular, +the classification survives any quotient in which the interface equations +and the stated unit relations hold. This is the same rigidity theorem, +not a physical-cost claim. ∎ + +## What the classification changes + +PR #6961 supplied the pair (Q,C Q), both one-edge obstructions, and explicitly +excluded classification of every pair from its claim. The new step is the +elimination (4), which forces that pair even when both operators vary over +the entire algebra. A larger polynomial or word search on these same two +edges cannot yield another way to meet this row contract. A further relation +among physical operators cannot create a second pair of operator values while +preserving (1) and its unit hypotheses; it can identify different expressions +for the same pair. + +The existing attaining pair is not new. Its ordinary bill and unchanged scalar +suffix are studied separately in unpaidmoon's open PR #7077. The new proof +does not replay or recertify that bill or the complete final banks. It does +not exclude a new saved source, a changed insertion point, a new decoder, +an altered row target, or a changed source schedule. + +## Executable evidence and its boundary + +The verifier independently represents (1) by exact 2-by-2 matrices over +Z/2, Z/3 and Z/4, including noncommuting Q,C and nonunit candidate F,G. +It enumerates every F,G for each declared fixture and checks the complete +accepted set, plus the aggregate predicate (3). A separate scalar evaluator +applies the two feedback operations to every eight-scalar input for its +three designated fixtures. This finite corroboration is distinct from the +all-ring proof above. These reduced-interface fixtures are not native +realizations of the inherited full schedule. + +Controls reject a reversed noncommutative product, show why either an x0-only +check or a zero-y0-only check is insufficient, and reject singular Q/D, +noninvolutory C, noncommuting Q/D and malformed fixture values. The verifier +imports no predecessor scientific program and runs no predecessor census. + +All loops have fixed domains: modulus at most four, four matrix entries, +two scalar coordinates, at most 75 fixtures, at most 65,536 operator pairs +per fixture and at most 65,536 scalar inputs per designated fixture. +There is no recursion or dynamic code evaluation. Checks use explicit failures +and remain enabled under optimization. The script owns no subprocesses or +network resources; its optional new receipt uses an exclusive context-managed +file and binds all six authored package files by SHA256. + +Power-of-Ten rule 3 deviation: CPython's integers, tuples, dictionaries and +iteration machinery allocate during verification. Fixed allocation is not +available in this interpreter. The fixed domains above bound live data; a +census retains at most its 65,536 matrix pairs if every pair were accepted, +and all 75 small result records. Normal and optimized warning-strict replays +check the actual path. A fixed-allocation port would need a separate native +implementation. No low-level fixed-allocation compliance is claimed. +Functions stay below 60 physical lines. There are no callback dispatch tables, +hidden imports, mutable shared state or suppressed diagnostics. The repository's +registered-package checks provide the applicable recurring validation; a new +whole-repository lint configuration is outside this isolated result. diff --git a/research/two-edge-feedback-rigidity/README.md b/research/two-edge-feedback-rigidity/README.md new file mode 100644 index 0000000000..467d323b61 --- /dev/null +++ b/research/two-edge-feedback-rigidity/README.md @@ -0,0 +1,81 @@ +# The autonomous row forces a unique two-edge feedback pair + +Scoped written proof with exact finite corroboration, produced by Nick Petalas. +For the unchanged saved-bank interface of +[unpaidmoon's #6961](https://github.com/CrocSwap/integer-mult-bounds/pull/6961), +the only two feedback operators attaining its autonomous four-input row are +`F1=Q` and `F2=C1 Q`. Both operators may vary arbitrarily in the predecessor's +algebra. The known pair itself is credited to #6961. The new result is its +uniqueness, which the predecessor explicitly left unproved. + +The sum of the first and third output columns eliminates F1 and forces F2. +The zero second column then forces F1. [PROOF.md](PROOF.md) proves the result +over every associative unital ring with the declared units and commutation +relation. It uses no search bound or faithful representation assumption. +Any quotient preserving those interface equations has the same unique pair +of operator values. This closes further two-edge tuning within that interface. + +No new κ, complete caller, native construction, physical tariff or selected +frontier change is claimed. The row still contains two input jobs in one bank. +The existing pair's separate ordinary bill and final-bank question belong to +[#7077](https://github.com/CrocSwap/integer-mult-bounds/pull/7077); they are cited, +not reverified. New saved sources, different insertion points and different +decoder or target contracts remain outside this theorem. + +## Reproduction + +From the repository root: + +```sh +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/two-edge-feedback-rigidity/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -O -W error -B research/two-edge-feedback-rigidity/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/two-edge-feedback-rigidity +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/two-edge-feedback-rigidity --check-source-history +``` + +CPython 3.12 and its standard library suffice. The direct verifier is also +Git-free and reads only the six authored files in this directory. It prints +`PASS_TWO_EDGE_FEEDBACK_RIGIDITY`, exact enumerated coverage and source hashes. +Add `--receipt /absolute/new/path.json` to save that generated receipt outside +the package. It refuses to overwrite an existing file. Default replay writes +no artifacts. The registered normal and optimized checks have 120-second +timeouts. Provenance validation uses full Git history separately. + +The matrix census checks 97,090 operator pairs on 75 fixtures, with exactly +one solution per fixture. These include all 72 binary unit triples satisfying +the reduced hypotheses, two specified ternary triples and one Z/4 triple. +It includes singular candidate feedback operators. The independent scalar +evaluator checks all 78,658 inputs of the latter three fixtures. Three semantic +controls and six invalid-fixture controls also pass. The finite fixtures +corroborate the new abstract theorem; they do not replay the predecessor's +physical word or certify its native premises. + +## Open next questions + +- Can a different chronological saved source replace one of these edges with + a favorable complete bill? Start by changing one of K or L and deriving its + four independent input columns. The unchanged pair is rigid; source + availability, full endpoint restoration and physical costs remain blockers. +- Can a consumer use the unique row without separately decoding its two jobs? + Start with an explicit producer/consumer boundary and include the complete + ordinary and recursive invoice. No such consumer is supplied here. + +Structured first steps and blockers are in [TASK.json](TASK.json). + +## Credit and limits + +Credit unpaidmoon #6961 for the one-edge obstructions, the saved-bank identities +and the attaining pair; Cinna Davis #5220 for the active schedule and operator +algebra; Dugongue / David Ganz #4948 and Dillon #4933 for the retained chronology +and normalizers; Chris R / Clear1nsight for passive-caller packaging; and their +retained native, compiler and precision lineage. The new simultaneous +classification, abstract proof and reduced-interface verifier were produced by +Nick Petalas. Apache-2.0. + +The original `joint-query-controller` card has changed scope to a local +classification at a fixed interface. It supplies no favorable full caller bill. +`SOURCES.json` pins predecessor documents as provenance only. No predecessor +scientific code, selected cold replay, native, Lean or Docker suite is run. +All five selected assumptions remain. Independent human and formal proof-kernel +review are unclaimed. CPython's bounded dynamic-allocation deviation is recorded +in PROOF.md. diff --git a/research/two-edge-feedback-rigidity/SOURCES.json b/research/two-edge-feedback-rigidity/SOURCES.json new file mode 100644 index 0000000000..5965cf6822 --- /dev/null +++ b/research/two-edge-feedback-rigidity/SOURCES.json @@ -0,0 +1,36 @@ +{ + "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/active-feedback-outside-edge/README.md", + "usage": "provenance", + "git_blob": "f4f14eb7e46d0aad69048eacbae3cc279bfae033", + "sha256": "5ec2b59ccdac4bcf413eb43ac894028a1e8146885579d3f229dd2ccf93617895" + }, + { + "path": "research/active-feedback-outside-edge/PROOF.md", + "usage": "provenance", + "git_blob": "920b67909ae7707ec8729772b95384bd3669fa59", + "sha256": "7159786b7fa2f16580e363d04364d421deb2f67416d4b5624dc0d4c3538dff3c" + }, + { + "path": "research/coded-active-feedback/PROOF.md", + "usage": "provenance", + "git_blob": "9716baebb4895b07acf9db0cbce010590b03945a", + "sha256": "c6233d2759811190c7ea1be455c9351b61c29f6a8afc8584e7bc0dfbc00f3a3d" + } + ] +} diff --git a/research/two-edge-feedback-rigidity/TASK.json b/research/two-edge-feedback-rigidity/TASK.json new file mode 100644 index 0000000000..e965b6fe60 --- /dev/null +++ b/research/two-edge-feedback-rigidity/TASK.json @@ -0,0 +1,90 @@ +{ + "schema_version": 1, + "task_id": "joint-query-controller", + "priority_revision": 8, + "base_commit": "e54523517d0f03e58352e647c403a5af3e525a57", + "original_card": { + "id": "joint-query-controller", + "question": "Can a changed query demand or caller remove real work while satisfying native chronology and restoration?", + "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" + ], + "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 source-bound arbitrary-input identity and legal producer/consumer boundary with the complete paid and productive target invoice, including restoration, ownership, native alignment and extra charges. Price under the actual current model; historical ceiling.py assumptions must be established before use. A favorable optimistic relaxation keeps a route open but is not a completed supplier. A scoped local result remains useful; expansion requires the family-level budget gate.", + "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": "Choose an exact caller and a new demand/interface hypothesis. Read the scoped #5617/#5631/#5649/#5747 and #5720/#5745 objections before rebuilding an excluded schedule. Compare the complete matched source/consumer protocols including all retained helper outputs. For an active-mode injection, first check #5745: its canonical delivery claim repays the eight removed centre jobs. Audit that exact claim or change its channel/feedback hypothesis; do not repeat the same free-injection search. Stop if the full favorable budget fails or the required restored output is unobservable.", + "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": [ + "query demand", + "active mode", + "5720", + "5745", + "5747", + "caller" + ], + "existing_checks": [ + { + "scope": "PR #4166: author-checked installed producer/service/return/bridge connection; native-component comparison loses.", + "evidence": "research/qq16-caller-install/README.md", + "remaining": "Complete matched physical protocol bill, or changed source-compatible demand/circuit; no affordable supplier yet.", + "status": "author-checked", + "source_commit": "0b082d22a0e9a442d264ab0633e35ef26c790630", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "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": "Classify both existing feedback operators simultaneously at the reduced saved-bank interface: the autonomous row forces F1=Q and F2=C1 Q.", + "scope_change_reason": "Take the explicit unproved all-pairs classification in PR6961 rather than seek a new physical QQ16 caller. The result closes two-edge tuning at the fixed row contract, without a favorable complete bill.", + "bottleneck_link": "The earlier two-edge witness supplies a coupled component rather than a complete caller. Uniqueness means that merely enlarging both feedback operator grammars cannot change that row solution; a useful construction must change a source, cut, decoder or target contract.", + "budget_minutes": 60, + "stop_rule": "Ship the first proved classification with bounded corroboration. Do not extend to new sources, decoders or costs.", + "outcome": "completed", + "evidence": "PROOF.md and verify.py; generated hash-bound receipts are optional external outputs.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "Can a different chronological saved source replace one existing edge with a favorable complete bill?", + "why_it_matters": "The unchanged two-edge row has a unique solution, so another operator search cannot find a different solution at this interface.", + "first_step": "Change one of the K or L rows and derive all four independent input columns at its legal chronological cut.", + "blocked_by": "Source availability, full endpoint restoration and physical costs are not supplied." + }, + { + "question": "Can an explicit consumer use the unique coupled row directly?", + "why_it_matters": "Two jobs in one output bank are not independent target credit.", + "first_step": "State a producer/consumer boundary and its complete ordinary and recursive invoice.", + "blocked_by": "No such consumer, delivery or cost certificate is supplied." + } + ] +} diff --git a/research/two-edge-feedback-rigidity/VERIFY.json b/research/two-edge-feedback-rigidity/VERIFY.json new file mode 100644 index 0000000000..c5c546f1ae --- /dev/null +++ b/research/two-edge-feedback-rigidity/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": 120, + "checks": "New all-pairs reduced-interface solution sets, aggregate criterion, literal arbitrary-input endpoints and nine controls." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Repeat every mathematical and invalid-input check with optimization enabled." + } + ] +} diff --git a/research/two-edge-feedback-rigidity/verify.py b/research/two-edge-feedback-rigidity/verify.py new file mode 100644 index 0000000000..d492cddace --- /dev/null +++ b/research/two-edge-feedback-rigidity/verify.py @@ -0,0 +1,220 @@ +#!/usr/bin/env python3 +"""Exact corroboration of the reduced two-edge rigidity theorem. + +New theorem and verifier produced by Nick Petalas. Apache-2.0. +No predecessor scientific program is imported or executed. +""" + +import argparse +import hashlib +import itertools +import json +import math +from pathlib import Path +import platform + + +IDENTITY = (1, 0, 0, 1) +ZERO = (0, 0, 0, 0) + + +def need(condition, message): + if not condition: + raise ValueError(message) + + +def add(a, b, modulus): + return tuple((a[i] + b[i]) % modulus for i in range(4)) + + +def neg(a, modulus): + return tuple(-a[i] % modulus for i in range(4)) + + +def mul(a, b, modulus): + return ( + (a[0] * b[0] + a[1] * b[2]) % modulus, + (a[0] * b[1] + a[1] * b[3]) % modulus, + (a[2] * b[0] + a[3] * b[2]) % modulus, + (a[2] * b[1] + a[3] * b[3]) % modulus, + ) + + +def inverse(a, modulus): + determinant = (a[0] * a[3] - a[1] * a[2]) % modulus + need(math.gcd(determinant, modulus) == 1, "matrix is not a unit") + scale = pow(determinant, -1, modulus) + result = tuple(scale * x % modulus for x in (a[3], -a[1], -a[2], a[0])) + need(mul(a, result, modulus) == mul(result, a, modulus) == IDENTITY, + "matrix inverse failed") + return result + + +def validate(q, c, d, modulus): + need(type(modulus) is int and modulus in (2, 3, 4), "unsupported modulus") + for value in (q, c, d): + need(type(value) is tuple and len(value) == 4, + "matrix must have four entries") + need(all(type(x) is int and 0 <= x < modulus for x in value), + "matrix entries must be canonical integers") + qi = inverse(q, modulus) + inverse(d, modulus) + need(mul(c, c, modulus) == IDENTITY, "C is not an involution") + need(mul(q, d, modulus) == mul(d, q, modulus), "Q and D do not commute") + return qi + + +def row(q, c, d, b, f, g, modulus): + """Block-row evaluation of B + Q^-1 G Q^-1 (K + F L).""" + qi = inverse(q, modulus) + h = mul(mul(qi, c, modulus), d, modulus) + k = (ZERO, neg(mul(q, d, modulus), modulus), mul(c, d, modulus), ZERO) + late = (h, d, neg(h, modulus), ZERO) + left = mul(mul(qi, g, modulus), qi, modulus) + base = (ZERO, ZERO, b, ZERO) + return tuple(add(base[i], mul(left, add(k[i], mul(f, late[i], modulus), + modulus), modulus), modulus) + for i in range(4)) + + +def action(matrix, vector, modulus): + return ((matrix[0] * vector[0] + matrix[1] * vector[1]) % modulus, + (matrix[2] * vector[0] + matrix[3] * vector[1]) % modulus) + + +def literal(q, c, d, b, f, g, inputs, modulus): + """Evaluate the two feedback applications on values, without block rows.""" + qi = inverse(q, modulus) + x, y, z, _ = inputs + dx, dy, dz = (action(d, v, modulus) for v in (x, y, z)) + h0 = action(qi, action(c, dx, modulus), modulus) + h2 = action(qi, action(c, dz, modulus), modulus) + late = tuple((h0[i] + dy[i] - h2[i]) % modulus for i in range(2)) + first, second = action(c, dz, modulus), action(q, dy, modulus) + feedback = action(f, late, modulus) + argument = tuple((first[i] - second[i] + feedback[i]) % modulus + for i in range(2)) + response = action(qi, argument, modulus) + feed = action(qi, action(g, response, modulus), modulus) + base = action(b, z, modulus) + return tuple((base[i] + feed[i]) % modulus for i in range(2)) + + +def matrices(modulus): + need(modulus in (2, 3, 4), "matrix enumeration is bounded by modulus four") + return tuple(itertools.product(range(modulus), repeat=4)) + + +def binary_fixtures(): + values = matrices(2) + units = tuple(a for a in values if (a[0] * a[3] - a[1] * a[2]) % 2) + involutions = tuple(c for c in units if mul(c, c, 2) == IDENTITY) + return tuple((2, q, c, d) for q in units for c in involutions for d in units + if mul(q, d, 2) == mul(d, q, 2)) + + +def census(fixture): + modulus, q, c, d = fixture + qi = validate(q, c, d, modulus) + b = (1, 1, 0, 1) + target = (mul(d, qi, modulus), ZERO, b, ZERO) + expected = (q, mul(c, q, modulus)) + accepted = [] + tested = 0 + for f in matrices(modulus): + for g in matrices(modulus): + tested += 1 + output = row(q, c, d, b, f, g, modulus) + if output == target: + accepted.append((f, g)) + # Check the stronger two-constraint characterization separately. + aggregate = add(output[0], output[2], modulus) + reduced = output[1] == ZERO and aggregate == add(target[0], b, modulus) + need(reduced == (output == target), "aggregate characterization failed") + need(accepted == [expected], "finite solution set is not the unique pair") + return {"modulus": modulus, "Q": q, "C": c, "D": d, + "pairs_tested": tested, "solutions": accepted} + + +def literal_checks(fixture): + modulus, q, c, d = fixture + qi = validate(q, c, d, modulus) + b = (1, 1, 0, 1) + f, g = q, mul(c, q, modulus) + checked = 0 + for raw in itertools.product(range(modulus), repeat=8): + inputs = tuple((raw[i], raw[i + 1]) for i in range(0, 8, 2)) + first = action(mul(d, qi, modulus), inputs[0], modulus) + third = action(b, inputs[2], modulus) + expected = tuple((first[i] + third[i]) % modulus for i in range(2)) + need(literal(q, c, d, b, f, g, inputs, modulus) == expected, + "literal arbitrary-input endpoint failed") + checked += 1 + return checked + + +def controls(): + modulus = 3 + q, c, d = (0, 1, 2, 0), (1, 0, 0, 2), IDENTITY + qi = validate(q, c, d, modulus) + b = IDENTITY + target = (qi, ZERO, b, ZERO) + need(mul(q, c, modulus) != mul(c, q, modulus), "noncommuting control collapsed") + wrong_order = row(q, c, d, b, q, mul(q, c, modulus), modulus) + need(wrong_order != target, "wrong multiplication order was accepted") + old = row(q, c, d, b, IDENTITY, mul(mul(c, q, modulus), q, modulus), modulus) + need(old[0] == target[0] and old != target, "first-column-only control failed") + missing = row(q, c, d, b, q, ZERO, modulus) + need(missing[1] == ZERO and missing != target, "zero-y-only control failed") + rejected = 0 + invalid = ((ZERO, c, d, 3), (q, c, ZERO, 3), + (q, ZERO, d, 3), (q, c, c, 3), + (q, c, d, True), ((False, 1, 2, 0), c, d, 3)) + for args in invalid: + try: + validate(*args) + except ValueError: + rejected += 1 + else: + raise ValueError("invalid fixture was accepted") + return {"wrong_order_rejected": True, "first_column_alone_insufficient": True, + "zero_y_alone_insufficient": True, "invalid_fixtures_rejected": rejected} + + +def source_hashes(): + here = Path(__file__).resolve().parent + names = ("verify.py", "README.md", "PROOF.md", "TASK.json", "SOURCES.json", "VERIFY.json") + return {name: hashlib.sha256((here / name).read_bytes()).hexdigest() for name in names} + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--receipt", type=Path, help="write a new hash-bound receipt outside the package") + args = parser.parse_args() + if args.receipt is not None: + need(args.receipt.is_absolute(), "receipt path must be absolute") + need(not args.receipt.is_relative_to(Path(__file__).resolve().parent), + "receipt must be outside the package") + fixtures = binary_fixtures() + ( + (3, (0, 1, 2, 0), (1, 0, 0, 2), (0, 1, 2, 0)), + (3, (1, 1, 0, 1), (0, 1, 1, 0), IDENTITY), + (4, (1, 1, 0, 1), (0, 1, 1, 0), (1, 2, 0, 1)), + ) + results = [census(fixture) for fixture in fixtures] + literal_cases = sum(literal_checks(fixture) for fixture in fixtures[-3:]) + result = {"status": "PASS_TWO_EDGE_FEEDBACK_RIGIDITY", + "claim_type": "scoped written proof with exact finite corroboration", + "python": platform.python_version(), "fixtures": len(fixtures), + "pairs_tested": sum(item["pairs_tested"] for item in results), + "unique_solutions": len(results), "literal_inputs_checked": literal_cases, + "controls": controls(), "censuses": results, "files_sha256": source_hashes()} + payload = json.dumps(result, sort_keys=True, indent=2) + "\n" + if args.receipt is not None: + with args.receipt.open("x", encoding="utf-8") as handle: + written = handle.write(payload) + need(written == len(payload), "partial receipt write") + print(payload, end="") + + +if __name__ == "__main__": + main()