From 121b10ff0ffba6832b805a405e9f3bdd08cdd582 Mon Sep 17 00:00:00 2001 From: Nick Petalas Date: Mon, 2 Nov 2026 21:15:35 +0000 Subject: [PATCH] feat(research): prove the fixed border needs two repair cuts --- research/border-single-correction/PROOF.md | 150 +++++++++++++ research/border-single-correction/README.md | 104 +++++++++ .../border-single-correction/SOURCES.json | 18 ++ research/border-single-correction/TASK.json | 88 ++++++++ research/border-single-correction/VERIFY.json | 34 +++ research/border-single-correction/verify.py | 199 ++++++++++++++++++ 6 files changed, 593 insertions(+) create mode 100644 research/border-single-correction/PROOF.md create mode 100644 research/border-single-correction/README.md create mode 100644 research/border-single-correction/SOURCES.json create mode 100644 research/border-single-correction/TASK.json create mode 100644 research/border-single-correction/VERIFY.json create mode 100644 research/border-single-correction/verify.py diff --git a/research/border-single-correction/PROOF.md b/research/border-single-correction/PROOF.md new file mode 100644 index 0000000000..da050a367d --- /dev/null +++ b/research/border-single-correction/PROOF.md @@ -0,0 +1,150 @@ +# The fixed border needs two repair locations + +This contribution was produced by Nick Petalas. Apache-2.0. + +## Statement and predecessor + +Take Ali Romman's five-call border in +[PR6398, BOUNDARY-MODULES.md, sections 2 and 3](https://github.com/aliromman/integer-mult-bounds/blob/dee2663ba0918be86993fd9d63c8d64b020f4c83/research/mixed-projector-root-headroom/BOUNDARY-MODULES.md). +Its five chronological factors, parameterized by a nonzero scalar `e`, +are fixed throughout this result. Three independent invertible commuting +stage variables are `A,B,C`; the central involution is `S`. +The target is `S diag(ABC,A,B,C)` on four arbitrary input fields. + +**Theorem.** Over any field of characteristic other than two, no linear +repair confined to one of the six cuts can make this fixed word equal its +target as a formal identity in `S,A,B,C` modulo `S^2=1`. The repair may be an arbitrary +matrix depending on `S` and `e`, of any rank, but must be independent of +`A,B,C`. Consequently a product of arbitrarily many such operations at one +cut also cannot repair it. The minimum number of distinct repair cuts is two, +attained by the predecessor's two rank-one corrections. + +The cut is fixed as part of the word, independently of the stage variables. +There are four fields and no additional workspace. The theorem does not +cover retuning the original factors, moving stage operations, using a stage +or its inverse inside a repair, nonlinear recovery or approximate recovery. +It is a scoped algebraic obstruction, not a supplier or kappa claim. + +The predecessor supplies the border and its two-correction construction. +The new result is the exclusion of every single repair location, including +arbitrary-rank and arbitrarily long central-only blocks. It does not replay +the predecessor's native word, root search, counts or price exclusions. + +## Normalize the nonzero border parameter + +Write `Q_i(e)=I+(S-1)u_i(e)v_i(e)` for the five query matrices and `D_i` +for their left stage multipliers. In chronological order, these are + +| i | u_i(e) | v_i(e) | D_i | +| --- | --- | --- | --- | +| 0 | (1,0,0,0) | (0,1/e,0,0) | diag(A,A,1,1) | +| 1 | (-1/e,1,0,0) | (0,1,-e^2,0) | I | +| 2 | (-e,0,1,0) | (-1/e,0,-1,0) | diag(B,1,B,1) | +| 3 | (-e,0,1,-1) | (-1/e,0,0,0) | I | +| 4 | (1,0,0,1/e) | (-1,0,0,e) | diag(C,1,1,C) | + +Let `E=diag(e,1,e^2,e^2)`. Each outer product satisfies + +`u_i(e)v_i(e) = E^-1 u_i(1)v_i(1) E`. + +All `D_i` and the target commute with `E`. Therefore the entire word, +each prefix and suffix, and the unique required repair at any cut are +conjugates by `E` of their `e=1` counterparts. Since `E` is invertible +and independent of the stages, existence of a stage-independent repair +is equivalent at `e` and at one. This similarity is an algebraic proof +device, not a claim of free physical normalization. + +## A two-point middle-stage witness at every cut + +It suffices to specialize `S=-1`, `A=C=1`, and write `B=b`. +These scalar stages are a valid restriction of a formal identity. +In fact the two witnesses `b=1,-1` are already unitary scalar stages. +Set + +`M_i = D_i (I-2u_i(1)v_i(1))`. + +For the three full sites `v_i u_i=0`, so the inverse of their query +factor is `I+2u_i v_i`. At the other two sites `v_i u_i=1`, so their +query factors are their own inverses. Thus every factor is invertible +for `b!=0`. Define, for `0<=k<=5`, + +`P_k=M_(k-1)...M_0`, `L_k=M_4...M_k`, and `T=-diag(b,1,b,1)`. + +Empty products are identity matrices. Any inserted matrix `K` satisfying +`L_k K P_k=T` is uniquely forced to be + +`K_k(b) = L_k^-1 T P_k^-1`. + +Direct multiplication gives the following complete table. Coordinates are +zero-based and `E_ij` is a matrix unit. Each row lists `K_k(b)-I`. + +| cut k | Required displacement | +| --- | --- | +| 0 | `-2/b E_03 + 2 E_12` | +| 1 | `-4 E_02 - 2/b E_03 + 2 E_12` | +| 2 | `-2/b E_03 - 2 E_12` | +| 3 | `2 E_03 + 4/b E_10 + 2/b E_12 - 4 E_23` | +| 4 | `4 E_00 - 2 E_03 + 2/b E_12 + 8 E_30 - 4 E_33` | +| 5 | `-2 E_03 + 2/b E_12` | + +For cuts zero through two, entry `(0,3)` equals `-2/b`. +For cuts three through five, entry `(1,2)` equals `2/b`. +Each changes by a nonzero multiple of four between `b=1` and `b=-1` +in every characteristic other than two. The unique required matrices +therefore differ. No matrix independent of `b` works at either cut for +both inputs. This excludes all six cuts, without restricting the rank, +determinant, central dependence or internal factorization of `K`. + +Conjugation by `E` proves the same exclusion for every nonzero `e`. +Any central-only linear block at a single cut has one aggregate matrix +independent of the stages, so the exclusion covers the whole block. + +The specialization is sufficient for the negative result: no interpolation +in general stages or numeric approximation to the actual native operators +is assumed. The failure already appears on two scalar stage characters. + +## Sharpness and the scope of the cost consequence + +The predecessor's corrections are + +`I+(S-1)e^2 E_12` at cut two, and +`I+(S-1)e E_03` at cut five. + +Its exact identity proves that these two locations attain the target on +arbitrary inputs. Both displacements have rank one and square to zero. +Combining that cited upper bound with the new single-cut exclusion proves +the exact minimum of two repair locations in the stated model. The verifier +also executes the attaining word on its finite fixtures, solely as the +positive witness accompanying this new lower bound. + +The predecessor already prices these two direct corrections and excludes +their complete invoice at its candidate saving. This contribution does +not recount or strengthen that price calculation. It establishes that +concentrating all stage-independent recovery at one cut cannot replace +them, even with a higher-rank central operation or unlimited local scalar +mixing. Different two-cut recoveries, stage-sensitive operations, changed +factors, additional fields and precision transfer remain open. + +## Exact evidence + +`verify.py` computes all required corrections by exact rational inversion, +independently of the displayed formulas. It checks every cut at both +middle-stage witnesses for each of six nonzero border parameters. It then +uses the correction required at `b=1` on the `b=-1` word and requires that +the purported endpoint fail at every cut. These are 36 explicit rejected +recovery attempts, not a sampled assertion that all possible matrices fail; +uniqueness supplies the quantifier over all matrices. + +There are also 36 normalized table checks and 48 attaining two-correction +fixtures, plus five domain/singularity rejection controls. Each entry of +`b K_k(b)` has polynomial degree at most two: exactly one inverse stage +factor involves `b^-1`, and `T` has degree one. The displayed candidate +table has the same bound. The checks at `b=1,2,3`, included in the six +normalized values, therefore certify the table coefficients over the +rationals by interpolation. All coefficients are integers before adjoining +`b^-1`, so the identities transfer to every field. The two-point failure +uses only `1,-1`, so it remains valid in every characteristic other than two. + +The all-parameter theorem rests on this written uniqueness, similarity +and two-point argument. The finite fixtures are exact corroboration and +a coefficient certificate, not formal proof-kernel acceptance. diff --git a/research/border-single-correction/README.md b/research/border-single-correction/README.md new file mode 100644 index 0000000000..569a45df71 --- /dev/null +++ b/research/border-single-correction/README.md @@ -0,0 +1,104 @@ +# Two repair cuts are necessary for the fixed five-call border + +This contribution was produced by Nick Petalas. Apache-2.0. + +**Claim type: scoped algebraic proof with exact finite evidence.** +Ali Romman's [PR6398 five-call border](https://github.com/aliromman/integer-mult-bounds/blob/dee2663ba0918be86993fd9d63c8d64b020f4c83/research/mixed-projector-root-headroom/BOUNDARY-MODULES.md) +cannot reach its exact diagonal target through a central-only linear repair +confined to any single cut. This excludes an arbitrary-rank operation or an +arbitrarily long block of such operations at that cut. The minimum number +of distinct repair locations is **two**, attained by the predecessor's +two rank-one corrections. + +For each of the six cuts, invertibility uniquely determines the inserted +repair matrix. The required matrices differ between the two middle stages +`B=1` and `B=-1`, already at `A=C=1` and central character `S=-1`. +The repair cannot be independent of the stages. An exact diagonal similarity +extends the argument to every nonzero border parameter, over any field of +characteristic other than two. [PROOF.md](PROOF.md) gives the six required +matrices and the complete argument. + +This answers a part of PR6398's different-recovery question. Increasing the +rank or scalar complexity of a repair at one location cannot remove its +need for stage information. A future recovery must cross a stage boundary, +use stage-dependent operations, change the word or change another stated +hypothesis. The predecessor's native construction, two-correction word +and reported losing invoice retain their credit; they are premises rather +than audit deliverables. + +## Reproduce + +From the repository root, using only CPython 3.12 and its standard library: + +```sh +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/border-single-correction/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -O -W error -B research/border-single-correction/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/border-single-correction +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/border-single-correction --check-source-history +``` + +Other hosts may substitute a CPython 3.12 interpreter. The verifier prints +`PASS_BORDER_SINGLE_CORRECTION` in a generated JSON receipt, including all +36 cut/parameter witnesses, 36 normalized table checks, 48 two-correction +positive fixtures and five domain/singularity controls. Every frozen +one-cut correction is explicitly rejected on the other middle stage. +All checks remain active under `-O`. The receipt binds package files by +SHA256 and is printed to stdout; redirect it outside the checkout to save it. + +The package imports no predecessor solver and does not rerun a predecessor +scientific suite. The source is cited at the exact public head above. +Its definition is transcribed explicitly into the proof and standalone +verifier. It is an external scholarly reference, not an unresolvable Git +input pin. The declared Git provenance binds the base card and selected record. + +## Scope and limitations + +The theorem concerns a formal identity in three independent invertible +commuting stage variables and a central involution. The negative-character +specialization is essential; a concrete central operator equal to identity +is outside the obstruction. There are exactly four arbitrary input fields, +the original five factors stay fixed, and the repair location is fixed +independently of the stage values. Repairs may depend arbitrarily on the +central operator and nonzero border parameter, but not on the stages. + +Retuned original factors, adaptive cut selection, additional workspace, +stage-sensitive recovery, approximate endpoints and physical implementations +are excluded. This does not lower or rederive the predecessor's invoice, +fund recursive precision, admit a supplier, change selected kappa or prove +a complete multiplication theorem. No Lean, Docker, selected cold replay, +native replay or predecessor root search was run. Independent human and +formal proof-kernel review are unclaimed. + +Canonical main was checked at `7c49fe32c55de02c2c873655c804b16e4c3fef0a`, +priority revision 8. The selected source-binding positive control passed; +it is metadata orientation, not supplier validation. The original +coverage-law-change card is narrowed to an exact recovery-location obstruction +for a changed caller boundary. The [advance claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19360652) +records that scope before the proof was packaged. + +Credit Ali Romman for PR6398's border and recovery question, its two-correction +upper bound and source-specific pricing. Credit Cinna Davis for the caller +interfaces, Jacob Alan Sussman for productive recursion, and the retained +native, helper, compiler, BIT and analytic lineage identified in PR6398. +The new uniqueness table and single-cut obstruction are the contribution here. +All predecessor notices and credit remain unchanged by citation. + +Power-of-ten inspection: the verifier uses no recursion, matrices have four +rows, words have at most seven factors, and every scientific loop ranges +over a fixed finite set. Functions stay below 60 lines. Exact fractions and +collections allocate dynamically, a managed-runtime deviation bounded by +these fixed domains. Five rejection-control callbacks have explicit local +targets. Matrix dimensions are internal invariants; zero parameters, invalid +cuts and singular inversion fail explicitly. Warning-strict normal and +optimized commands are registered. No output files or processes are created. + +## Open next questions + +- Can a changed two-cut recovery cost less than the existing two rank-one + queries? Start with explicit central operations on both sides of the + middle stage and a full signed invoice. The present result supplies a + location lower bound, not a complete tariff optimum. +- Can a stage-sensitive operation or changed original factor yield a + favorable exact caller? Start from the required correction table and price + the missing middle-stage dependence, including inverse access and cleanup. + Physical stage delivery and complete recursive costs remain the blockers. diff --git a/research/border-single-correction/SOURCES.json b/research/border-single-correction/SOURCES.json new file mode 100644 index 0000000000..594089b9c7 --- /dev/null +++ b/research/border-single-correction/SOURCES.json @@ -0,0 +1,18 @@ +{ + "schema_version": 1, + "base_commit": "7c49fe32c55de02c2c873655c804b16e4c3fef0a", + "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" + } + ] +} diff --git a/research/border-single-correction/TASK.json b/research/border-single-correction/TASK.json new file mode 100644 index 0000000000..7eca853dca --- /dev/null +++ b/research/border-single-correction/TASK.json @@ -0,0 +1,88 @@ +{ + "schema_version": 1, + "task_id": "coverage-law-change", + "priority_revision": 8, + "base_commit": "7c49fe32c55de02c2c873655c804b16e4c3fef0a", + "original_card": { + "id": "coverage-law-change", + "question": "Can a completed call earn more independent productive target credit without an offsetting paid bill?", + "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": "Use #5599 as a completed positive control, then choose one uncovered cut/module beyond an applicable frozen exclusion. Derive independence, saturation and chronological availability rather than counting rational rank alone. Price target credits and all new jobs together, then check compiler and actual caller compatibility. Stop on a nonphysical credit or an unfavorable complete relaxation.", + "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": [ + "target credit", + "helper split", + "coverage law" + ], + "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": "refined", + "actual_scope": "Prove the exact minimum of two stage-independent repair locations for the fixed PR6398 five-call border, allowing arbitrary-rank central-only blocks at any single cut.", + "scope_change_reason": "The current caller frontier leaves different recovery methods open. Select its new five-call border rather than replaying the selected supplier or repeating a root optimization.", + "bottleneck_link": "A favorable formal border invoice lacks affordable exact recovery. Excluding every single-cut central-only repair directs the next construction toward stage-sensitive or multi-cut recovery.", + "budget_minutes": 60, + "stop_rule": "Stop at the first proved original recovery obstruction; do not extend to changed words or new root searches.", + "outcome": "completed", + "evidence": "PROOF.md and warning-strict normal/optimized verify.py; generated stdout receipts bind all package files.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "Can a changed two-cut recovery improve the complete price of the existing two rank-one corrections?", + "why_it_matters": "The formal border still needs affordable exact recovery.", + "first_step": "Specify both cut operations and derive the complete signed invoice.", + "blocked_by": "No tariff optimum or physical realization follows from the location bound." + }, + { + "question": "Can a stage-sensitive operation or changed original factor supply a favorable exact caller?", + "why_it_matters": "The obstruction forces some middle-stage information into one-cut recovery.", + "first_step": "Use the required correction table to price middle-stage inverse access and cleanup.", + "blocked_by": "Stage delivery, restoration and full recursive costs are unresolved." + } + ], + "claim_url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19360652", + "predecessor": { + "pr": 6398, + "author": "aliromman", + "head": "dee2663ba0918be86993fd9d63c8d64b020f4c83", + "path": "research/mixed-projector-root-headroom/BOUNDARY-MODULES.md", + "role": "External cited definition, open recovery question and attaining two-correction upper bound. No predecessor suite is imported." + }, + "claim_type": "scoped algebraic proof with exact finite evidence" +} diff --git a/research/border-single-correction/VERIFY.json b/research/border-single-correction/VERIFY.json new file mode 100644 index 0000000000..86ffced80a --- /dev/null +++ b/research/border-single-correction/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": "All six cuts, exact unique corrections, parameter similarity, coefficient table, frozen-repair rejection, attaining two-cut fixtures and domain controls." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 60, + "checks": "The same full exact evidence and rejection controls with assertions disabled." + } + ] +} diff --git a/research/border-single-correction/verify.py b/research/border-single-correction/verify.py new file mode 100644 index 0000000000..2d1a59858a --- /dev/null +++ b/research/border-single-correction/verify.py @@ -0,0 +1,199 @@ +"""Exact witnesses for the fixed border's one-operation recovery obstruction.""" + +from fractions import Fraction as Q +import hashlib +import json +from pathlib import Path + + +N = 4 + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def identity(): + return tuple(tuple(Q(i == j) for j in range(N)) for i in range(N)) + + +def diagonal(values): + require(len(values) == N, "diagonal dimension") + return tuple(tuple(Q(values[i]) if i == j else Q(0) + for j in range(N)) for i in range(N)) + + +def multiply(a, b): + return tuple(tuple(sum(a[i][k] * b[k][j] for k in range(N)) + for j in range(N)) for i in range(N)) + + +def inverse(a): + rows = [list(a[i]) + list(identity()[i]) for i in range(N)] + for col in range(N): + pivot = next((i for i in range(col, N) if rows[i][col]), None) + require(pivot is not None, "singular matrix") + rows[col], rows[pivot] = rows[pivot], rows[col] + scale = rows[col][col] + rows[col] = [x / scale for x in rows[col]] + for row in range(N): + if row != col: + scale = rows[row][col] + rows[row] = [x - scale * y + for x, y in zip(rows[row], rows[col])] + result = tuple(tuple(row[N:]) for row in rows) + require(multiply(a, result) == identity(), "inverse postcondition") + return result + + +def rank(a): + rows = [list(row) for row in a] + found = 0 + for col in range(N): + pivot = next((i for i in range(found, N) if rows[i][col]), None) + if pivot is None: + continue + rows[found], rows[pivot] = rows[pivot], rows[found] + scale = rows[found][col] + rows[found] = [x / scale for x in rows[found]] + for row in range(found + 1, N): + scale = rows[row][col] + rows[row] = [x - scale * y + for x, y in zip(rows[row], rows[found])] + found += 1 + return found + + +def difference(a, b): + return tuple(tuple(a[i][j] - b[i][j] for j in range(N)) + for i in range(N)) + + +def query(u, v, central): + return tuple(tuple(Q(i == j) + (central - 1) * u[i] * v[j] + for j in range(N)) for i in range(N)) + + +def factors(e, a, b, c, central=-1): + e, a, b, c, central = map(Q, (e, a, b, c, central)) + require(all((e, a, b, c)), "zero parameter") + require(central in (-1, 1), "central character") + us = ((1, 0, 0, 0), (-1/e, 1, 0, 0), (-e, 0, 1, 0), + (-e, 0, 1, -1), (1, 0, 0, 1/e)) + vs = ((0, 1/e, 0, 0), (0, 1, -e*e, 0), (-1/e, 0, -1, 0), + (-1/e, 0, 0, 0), (-1, 0, 0, e)) + stages = ((a, a, 1, 1), (1, 1, 1, 1), (b, 1, b, 1), + (1, 1, 1, 1), (c, 1, 1, c)) + return tuple(multiply(diagonal(d), query(u, v, central)) + for u, v, d in zip(us, vs, stages)) + + +def product(items): + require(len(items) <= 7, "word length") + value = identity() + for item in items: + value = multiply(item, value) + return value + + +def target(a, b, c, central=-1): + return diagonal((central*a*b*c, central*a, central*b, central*c)) + + +def required_at_cut(word, goal, cut): + require(0 <= cut <= 5 and len(word) == 5, "cut domain") + prefix, suffix = product(word[:cut]), product(word[cut:]) + value = multiply(multiply(inverse(suffix), goal), inverse(prefix)) + require(multiply(multiply(suffix, value), prefix) == goal, + "required correction identity") + return value + + +def table(b): + b = Q(b) + require(b != 0, "zero middle stage") + return ( + ((1, 0, 0, -2/b), (0, 1, 2, 0), (0, 0, 1, 0), (0, 0, 0, 1)), + ((1, 0, -4, -2/b), (0, 1, 2, 0), (0, 0, 1, 0), (0, 0, 0, 1)), + ((1, 0, 0, -2/b), (0, 1, -2, 0), (0, 0, 1, 0), (0, 0, 0, 1)), + ((1, 0, 0, 2), (4/b, 1, 2/b, 0), (0, 0, 1, -4), (0, 0, 0, 1)), + ((5, 0, 0, -2), (0, 1, 2/b, 0), (0, 0, 1, 0), (8, 0, 0, -3)), + ((1, 0, 0, -2), (0, 1, 2/b, 0), (0, 0, 1, 0), (0, 0, 0, 1)), + ) + + +def check_cut(e, cut): + corrections = [] + for b in (Q(1), Q(-1)): + word = factors(e, 1, b, 1) + correction = required_at_cut(word, target(1, b, 1), cut) + gauge = diagonal((e, 1, e*e, e*e)) + expected = multiply(multiply(inverse(gauge), table(b)[cut]), gauge) + require(correction == expected, "similarity/table mismatch") + require(rank(difference(correction, identity())) == 2, + "required correction must have rank-two displacement") + corrections.append(correction) + require(corrections[0] != corrections[1], "stage dependence missing") + word = factors(e, 1, -1, 1) + wrong = word[:cut] + (corrections[0],) + word[cut:] + require(product(wrong) != target(1, -1, 1), "frozen correction accepted") + return {"e": str(e), "cut": cut, + "required_plus": [[str(x) for x in row] for row in corrections[0]], + "required_minus": [[str(x) for x in row] for row in corrections[1]]} + + +def check_two_corrections(e, a, b, c, central): + word = factors(e, a, b, c, central) + first = query((0, e*e, 0, 0), (0, 0, 1, 0), central) + last = query((e, 0, 0, 0), (0, 0, 0, 1), central) + repaired = word[:2] + (first,) + word[2:] + (last,) + require(product(repaired) == target(a, b, c, central), + "cited two-correction attainment") + + +def rejection_controls(): + controls = ( + ("zero border", lambda: factors(0, 1, 1, 1)), + ("zero stage", lambda: factors(1, 1, 0, 1)), + ("central domain", lambda: factors(1, 1, 1, 1, 0)), + ("cut domain", lambda: required_at_cut(factors(1, 1, 1, 1), identity(), 6)), + ("singular inverse", lambda: inverse(diagonal((0, 1, 1, 1)))), + ) + for name, action in controls: + try: + action() + except ValueError: + continue + raise ValueError("control accepted: " + name) + return [name for name, _ in controls] + + +def main(): + parameters = tuple(map(Q, (1, -1, "1/2", "-1/2", 2, 3))) + witnesses = [check_cut(e, cut) for e in parameters for cut in range(6)] + for b in map(Q, (1, -1, 2, -2, 3, -3)): + word = factors(1, 1, b, 1) + for cut in range(6): + require(required_at_cut(word, target(1, b, 1), cut) == table(b)[cut], + "normalized table fixture") + attainment = 0 + for e in parameters: + for a, b, c in ((1, 1, 1), (2, 3, 5), (-1, 2, -3), (3, -1, 2)): + for central in (-1, 1): + check_two_corrections(e, Q(a), Q(b), Q(c), central) + attainment += 1 + controls = rejection_controls() + package = Path(__file__).resolve().parent + hashes = {p.name: hashlib.sha256(p.read_bytes()).hexdigest() + for p in sorted(package.iterdir()) if p.is_file()} + print(json.dumps({"status": "PASS_BORDER_SINGLE_CORRECTION", + "cut_parameter_witnesses": witnesses, + "normalized_table_checks": 36, + "two_correction_fixtures": attainment, + "rejection_controls": controls, + "package_sha256": hashes}, sort_keys=True, indent=2)) + + +if __name__ == "__main__": + main()