From cbae979564366db77afd2f999b95622e0d4b1d33 Mon Sep 17 00:00:00 2001 From: Ali Romman <226877337+aliromman@users.noreply.github.com> Date: Fri, 23 Oct 2026 11:54:05 -0500 Subject: [PATCH 1/2] Retain inverse-circuit source for the orthogonal witness construction --- .../check_witness.py | 68 ++++ .../orthogonal-inverse-witness/literal.py | 92 ++++++ .../vendor/UPSTREAM-PROOF.md | 246 ++++++++++++++ .../vendor/UPSTREAM-README.md | 151 +++++++++ .../vendor/algebra.py | 153 +++++++++ .../vendor/dirty-sandwich.json | 105 ++++++ .../vendor/fields.py | 67 ++++ .../vendor/syntax.py | 71 ++++ .../vendor/wrong-order.json | 38 +++ research/orthogonal-inverse-witness/verify.py | 302 ++++++++++++++++++ .../orthogonal-inverse-witness/witness.py | 59 ++++ 11 files changed, 1352 insertions(+) create mode 100644 research/orthogonal-inverse-witness/check_witness.py create mode 100644 research/orthogonal-inverse-witness/literal.py create mode 100644 research/orthogonal-inverse-witness/vendor/UPSTREAM-PROOF.md create mode 100644 research/orthogonal-inverse-witness/vendor/UPSTREAM-README.md create mode 100644 research/orthogonal-inverse-witness/vendor/algebra.py create mode 100644 research/orthogonal-inverse-witness/vendor/dirty-sandwich.json create mode 100644 research/orthogonal-inverse-witness/vendor/fields.py create mode 100644 research/orthogonal-inverse-witness/vendor/syntax.py create mode 100644 research/orthogonal-inverse-witness/vendor/wrong-order.json create mode 100644 research/orthogonal-inverse-witness/verify.py create mode 100644 research/orthogonal-inverse-witness/witness.py diff --git a/research/orthogonal-inverse-witness/check_witness.py b/research/orthogonal-inverse-witness/check_witness.py new file mode 100644 index 0000000000..9b48d37690 --- /dev/null +++ b/research/orthogonal-inverse-witness/check_witness.py @@ -0,0 +1,68 @@ +"""Check the concrete witness by full literal replay, without the producer. + +Prepared by Ali Romman with substantial OpenAI Codex assistance. Apache-2.0. +""" + +import argparse +from fractions import Fraction +import json +from pathlib import Path +import sys + +sys.path.insert(0, str(Path(__file__).resolve().parent)) +from literal import degree_bound, replay +from syntax import fingerprint, validate + + +def check(program, witness): + if validate(program).characteristic: + raise ValueError("the SPD construction requires Q") + keys = {"schema", "program_sha256", "word", "dimension", "input", "output", + "epsilon", "epsilon_cap", "numerator_degree_bound", "grid_size", + "grid_index", "endpoint_difference"} + if not isinstance(witness, dict) or set(witness) != keys: + raise ValueError("invalid witness fields") + if witness["schema"] != "spd-inverse-witness/v1": + raise ValueError("invalid witness schema") + if witness["program_sha256"] != fingerprint(program): + raise ValueError("program binding mismatch") + word = witness["word"] + if not isinstance(word, list) or any(type(a) is not str or a not in program["operators"] for a in word): + raise ValueError("invalid path word") + n = len(word) + 1 + q = sum(ins["op"] != "linear" for side in ("left", "right") for ins in program[side]) + for key in ("dimension", "input", "output", "numerator_degree_bound", "grid_size", "grid_index"): + if type(witness[key]) is not int: + raise ValueError("integer witness field required") + if witness["dimension"] != n or n > len(program["roles"]) + q: + raise ValueError("dimension bound mismatch") + if not 0 <= witness["input"] < len(program["roles"]) or not 0 <= witness["output"] < len(program["roles"]): + raise ValueError("invalid role index") + degree = degree_bound(program, n) + if witness["numerator_degree_bound"] != degree or witness["grid_size"] != degree + 1: + raise ValueError("grid bound mismatch") + cap, epsilon = Fraction(witness["epsilon_cap"]), Fraction(witness["epsilon"]) + index = witness["grid_index"] + if not 0 < cap <= Fraction(1, 4) or not 1 <= index <= degree + 1: + raise ValueError("invalid grid range") + if epsilon != cap * (degree + 2 - index) / (degree + 1): + raise ValueError("invalid grid point") + difference = replay(program, word, epsilon, witness["input"]) + if witness["endpoint_difference"] != [[str(x) for x in row] for row in difference]: + raise ValueError("literal endpoint mismatch") + if not difference[witness["output"]][0]: + raise ValueError("zero endpoint is not a witness") + return difference + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("program", type=Path) + parser.add_argument("witness", type=Path) + args = parser.parse_args() + check(json.loads(args.program.read_text()), json.loads(args.witness.read_text())) + print("PASS_SPD_INVERSE_WITNESS_CHECKED") + + +if __name__ == "__main__": + main() diff --git a/research/orthogonal-inverse-witness/literal.py b/research/orthogonal-inverse-witness/literal.py new file mode 100644 index 0000000000..14c4a53977 --- /dev/null +++ b/research/orthogonal-inverse-witness/literal.py @@ -0,0 +1,92 @@ +"""Execute the complete program with rational path matrices and true inverses. + +Prepared by Ali Romman with substantial OpenAI Codex assistance. Apache-2.0. +""" + +from fractions import Fraction +from pathlib import Path +import sys + +sys.path.insert(0, str(Path(__file__).resolve().parent / "vendor")) +from syntax import validate + + +def parameters(program, word, epsilon): + if validate(program).characteristic: + raise ValueError("the SPD construction requires Q") + if any(a not in program["operators"] for a in word): + raise ValueError("unknown path label") + if not 0 < epsilon <= Fraction(1, 4): + raise ValueError("epsilon must be in (0, 1/4]") + n = len(word) + 1 + bands = {} + for a in program["operators"]: + off = [epsilon / 2 if b == a else Fraction(0) for b in word] + diagonal = [1 - epsilon] * n + pivots = diagonal[:] + for j in range(1, n): + pivots[j] -= off[j - 1] ** 2 / pivots[j - 1] + if any(t <= 0 for t in pivots): + raise ValueError("nonpositive path pivot") + bands[a] = (diagonal, off, pivots) + return bands + + +def action(band, vector, direction): + diagonal, off, pivots = band + n = len(vector) + if direction == 1: + result = [diagonal[j] * vector[j] for j in range(n)] + for j, edge in enumerate(off): + result[j] += edge * vector[j + 1] + result[j + 1] += edge * vector[j] + return result + if direction != -1: + raise ValueError("direction must be +1 or -1") + result = vector[:] + for j in range(1, n): + result[j] -= off[j - 1] * result[j - 1] / pivots[j - 1] + result[-1] /= pivots[-1] + for j in range(n - 2, -1, -1): + result[j] = (result[j] - off[j] * result[j + 1]) / pivots[j] + return result + + +def replay(program, word, epsilon, input_index): + bands = parameters(program, word, epsilon) + roles, n = program["roles"], len(word) + 1 + if type(input_index) is not int or not 0 <= input_index < len(roles): + raise ValueError("invalid input role") + endpoints = [] + for side in ("left", "right"): + regs = {role: [Fraction(i == input_index and j == n - 1) + for j in range(n)] for i, role in enumerate(roles)} + for ins in program[side]: + dst = ins["dst"] + if ins["op"] == "linear": + result = [Fraction(0)] * n + for src, scalar in ins["terms"]: + for j, value in enumerate(regs[src]): + result[j] += Fraction(scalar) * value + else: + src = dst if ins["op"] == "apply" else ins["src"] + value = action(bands[ins["operator"]], regs[src], ins["direction"]) + result = value if ins["op"] == "apply" else [ + old + Fraction(ins["coefficient"]) * new + for old, new in zip(regs[dst], value)] + regs[dst] = result + endpoints.append([regs[role] for role in roles]) + return [[a - b for a, b in zip(left, right)] + for left, right in zip(*endpoints)] + + +def degree_bound(program, dimension): + forward = inverse = 0 + for side in ("left", "right"): + for ins in program[side]: + if ins["op"] != "linear": + if ins["direction"] == 1: + forward += 1 + else: + inverse += 1 + return forward + dimension * inverse diff --git a/research/orthogonal-inverse-witness/vendor/UPSTREAM-PROOF.md b/research/orthogonal-inverse-witness/vendor/UPSTREAM-PROOF.md new file mode 100644 index 0000000000..d2433c24ca --- /dev/null +++ b/research/orthogonal-inverse-witness/vendor/UPSTREAM-PROOF.md @@ -0,0 +1,246 @@ +# Compact certificates with actual inverse calls + +This is a scoped written proof for the register grammar below. The implementation +and finite tests corroborate it; there is no proof-assistant or independent human +verification claim. The contribution answers the inverse-frontend question in +[zxv's PR5235](https://github.com/CrocSwap/integer-mult-bounds/pull/5235), pinned at +`48976daa4dce59b4867ef046da72a370e389925d`. That package supplies the +independent-operator register bridge, invariant certificates and unipotent +witness method. Here inverse occurrences denote the **actual inverse of the +same generator**, and therefore need a different, cyclic realization and a +sound passage from formal series to arbitrary invertible substitutions. + +Recognizable rational series, the Magnus substitution and weighted-automata +equivalence are classical. See Stefan Kiefer, +[Notes on Equivalence and Minimization of Weighted Automata](https://arxiv.org/abs/2009.01217), +and Retakh, Reutenauer and Vaintrob, +[Noncommutative rational functions and Farber's invariants of boundary links](https://arxiv.org/abs/math/0004112), +Remark 2.3 and Proposition 2.4, which recall the Magnus embedding and the +Schutzenberger/Fliess characterization. We claim a project-specific interface, +explicit state bound and executable certificate bridge, not a new general +automata/PIT algorithm or a new Magnus theorem. The argument below is +self-contained and does not require the injectivity theorem for the group +algebra embedding. + +## 1. Grammar and statement + +Fix a field K, a finite alphabet of independently chosen invertible operators +G_a on a common finite-dimensional K-vector space, and r >= 1 named registers. +All r initial vectors are independent; no dirty helper is assumed zero. +A program is a finite sequence of: + +1. scalar linear assignment to a register, with all sources read before the + assignment, including when the destination is also a source; +2. `dst <- G_a^s dst`, where s is +1 or -1; +3. `dst <- dst + c G_a^s src`, with the old source and destination, also when + `src == dst`. + +All scalar coefficients lie in K. Compare two such programs on the same +ordered roles and alphabet, returning **every** final register. Let q be the +total number of unary occurrences in both programs, including queries, inverse +occurrences, and queries with coefficient zero. Put D = r + q. + +**Theorem.** There are effectively constructed scalar matrices +U in K^(r x D), V in K^(D x r), and T_a in K^(D x D) such that: + +- the complete endpoint difference, expanded at G_a = I + Y_a, has coefficient + matrix U T_a1 ... T_ak V at every word a1...ak, including k=0; +- the programs have equal complete endpoints for every payload dimension and + every invertible substitution if and only if all these coefficients vanish; +- equality has a finite certificate consisting of at most D path rows, their + initial-span coordinates and transition-closure coordinates; +- failure has a nonzero coefficient word of length k < D and an explicit + simultaneous unipotent substitution in dimension k+1 <= D witnessing it. + +The search below finds a shortest nonzero coefficient word. The independent +certificate checker certifies its nonzeroness, **not shortestness**. It does +not claim a least-dimensional witness among arbitrary invertible matrices. + +The executable supports K=Q and prime fields F_p with p <= 2^31-1. Rational +input denominators must be nonzero in F_p. The written theorem holds over any +field. There are no commutation, involution, Clifford, adjoint or other +relations; a failure need not persist after imposing such extra relations. +Only inverses of named generators are in the grammar, not inverses of arbitrary +operator sums or matrices of operators. + +## 2. One atom per unary occurrence + +Create r leaf atoms x_i. Maintain each register as a scalar row in the atom +list. Each linear instruction updates that row. Each unary occurrence with +pre-instruction source row e creates a fresh atom z_j = G_a^s (e z). +An apply instruction replaces the destination by z_j; a query adds c z_j to +the old destination. Even a self-source query takes e before the update. + +Compile the two programs with separate mutable register tables but the same r +leaf atoms. Append all unary atoms from both sides to one list. Their source +rows use earlier atoms only. Thus there are exactly D atoms. U is the +left-minus-right matrix of all final role expressions; it retains each input +role and each output role independently. An atom is an algebraic compiler +record, not a clean physical register or a free allocation. + +Work in noncommutative formal series K<> and put G_a=1+Y_a. Its inverse +is the formal geometric series, well-defined over every characteristic. For a +forward occurrence and an inverse occurrence, respectively, the defining +equations are + + z_j = e z + Y_a e z, + z_j = e z - Y_a z_j. + +The second equation follows by multiplying z_j=(1+Y_a)^(-1)e z by 1+Y_a. +It is the inverse-aware step: a negative diagonal feedback term, not a new +independent operator label and not a truncated polynomial expansion. + +Let E have row e at every unary atom and zero leaf rows. Let V0 embed the r +input roles at the leaf rows. For each a, let A_a have row e at a forward +a-occurrence, row -unit_j at an inverse a-occurrence, and zero elsewhere. +Then, with scalar matrices commuting entrywise with the series letters, + + z = E z + V0 x + sum_a Y_a A_a z. + +E is strictly lower triangular. Consequently H=(I-E)^(-1) is the finite +scalar matrix I+E+...+E^(D-1). Set V=H V0 and T_a=H A_a. The equations become + + z = V x + sum_a Y_a T_a z. + +This system has a unique formal solution: each coefficient of positive length +is determined by shorter coefficients. Iterating gives exactly + + [a1 ... ak](U z) = U T_a1 ... T_ak V. + +Word order is matrix-product order: `[B,A]` means BA and applies A first. +The inverse feedback means T_a need not be nilpotent. Infinite nonzero tails +are allowed even though D is finite. + +The producer uses the equivalent triangular recurrences + + V_j = e V, + (T_b)_j = e T_b + 1_(b=a) e (forward), + (T_b)_j = e T_b - 1_(b=a) unit_j (inverse), + +where e only reads earlier rows. The checker instead reconstructs E,A_a and +the triangular inverse H. These are separately transcribed compilers. + +## 3. Finite closure certificates + +A positive certificate provides b <= D path rows B_l=U_o T_w and scalar +coordinate matrices L and C_a satisfying + + U = L B, B T_a = C_a B for every a, B V = 0. + +These finite equations imply U T_w V=0 for every word by induction. +Independence, minimality and reachability of B are unnecessary for soundness; +the supplied paths merely specify B compactly and bind it to the program. + +Conversely, if every coefficient is zero, the reachable space +R=span{U_o T_w} has dimension at most D, is transition-stable and annihilates V. +Choose a basis from reachable path rows. Its initial and closure coordinates +give the displayed certificate. A basis of paths shorter than D exists: +R_k, the span of paths of length at most k, cannot stop increasing and later +increase again, since R_(k+1)=R_k+sum_a R_k T_a. If R_0=0, everything is zero; +otherwise at most D-1 strict increases are possible. + +Breadth-first search tests output projections of accepted independent path +rows and appends their independent successors. Rejected dependent rows add no +possible earlier distinguishing length: their expression uses accepted rows +of no greater length, whose successors span their successors. Hence a first +nonzero projection occurs at a shortest coefficient word, of length < D. +Exact elimination is in the producer only. The checker rebuilds the path rows +and verifies the displayed equations, or verifies one claimed nonzero +coefficient on failure. No acceptance check relies on Python `assert`. + +With alphabet size s, dense production takes polynomially many field +operations (O(s D^3) for reachable-space search and coordinates, plus parsing +and compilation). Coordinate storage is O(s D^2+rD), with at most O(D^2) +path letters. The simple checker may rebuild each path from scratch, costing +O(D^4+sD^3) field operations. These are arithmetic bounds, not bounds on +rational coefficient bit lengths or a practical scaling guarantee. + +## 4. Why zero series implies every invertible substitution + +Formal series cannot be evaluated directly at arbitrary matrices by summing an +infinite series. The following argument supplies the missing step. + +Fix any dimension n and any tuple of invertible matrices M_a over K. Introduce +one central indeterminate t and substitute + + G_a(t) = I + t(M_a-I). + +Each G_a(t) has determinant with constant term 1, so is invertible over K(t) +and its inverse has a well-defined expansion in K[[t]]. The program endpoint +is therefore a matrix of rational functions regular at t=0. Its formal +expansion is precisely the specialization Y_a -> t(M_a-I) of the series from +Section 2: in each degree there are only finitely many words, so substitution +is legitimate. + +If the noncommutative endpoint series is zero, this matrix has identically +zero power series at t=0. A rational function regular at zero with zero formal +expansion is zero in K(t): multiply by its denominator, whose constant term is +nonzero. Finally every inverse occurrence is regular at t=1, since +det G_a(1)=det M_a != 0. Evaluating the zero rational endpoint at t=1 proves +equality for this arbitrary invertible tuple M_a. This is valid over finite +fields as well; it uses a formal indeterminate, not sampling field elements. + +Thus a finite closure certificate proves the complete universal invertible +endpoint claim, without assuming convergence, generic numerical invertibility +or an infinite-field polynomial identity heuristic. + +## 5. Nonzero series gives an explicit invertible witness + +Suppose c=(U T_a1 ... T_ak V)_(o,i) is nonzero. On the basis e_0,...,e_k let + + N_a = sum_(j=0 to k-1, a_(j+1)=a) E_(j,j+1), + G_a = I + N_a. + +All N_a share the same strictly upper-triangular flag. All products of more +than k such matrices vanish, and each inverse G_a^(-1) is the finite sum +I-N_a+N_a^2-...+(-N_a)^k. Therefore the formal-series substitution now really +is a finite calculation, also for programs containing inverse calls. + +In matrix entry (0,k), shorter words give zero, longer words give zero, and a +word of length k gives one exactly when its labels are a1,...,ak in order. +The literal endpoint difference in block (o,i), entry (0,k), equals c. +Use input e_k in role i and zero vectors in other roles to exhibit a concrete +failure. The universal check had kept all roles independent; this choice of +one witness input imposes no clean-state assumption on the theorem. +For k=0 take dimension one and all G_a=I. + +This proves the converse in Section 1 and the constructive dimension bound. +The literal matrix oracle computes inverses by Gaussian elimination and +executes the original instructions; it does not reuse T_a or the producer. + +## 6. Boundaries and discriminating examples + +The dirty-sandwich example has roles x,h,y, all arbitrary. It temporarily +changes h to h+A x, adds B h to y, restores h, and subtracts B h. Its complete +endpoint is (x,h,y+B A x). The reference program temporarily applies A to x, +queries B x into y, and applies A^(-1) to x. Both full endpoints agree. +Deleting any one of the eight left-side instructions yields a detectable +failure in each tested field. This example certifies the stated algebraic +boundary; it is not a proposed faster physical implementation or a new echo +construction. + +A false commutator identity B^(-1)A^(-1)BA=I has a nonzero degree-two +coefficient. Scalar/one-dimensional substitutions cannot reveal that error; +the certificate's unipotent witness does. Self-source queries, omitted helper +returns and wrong inverse signs have distinct rejecting fixtures. + +The family G^(-1)(I-G)^d expands to (-Y)^d/(1+Y), so its first coefficient +occurs at degree d and its tail continues indefinitely. The replay checks +coefficients beyond the program's number of unary occurrences. In F_p, +G^p-I=Y^p supplies a characteristic-sensitive delayed witness. + +The stress example computes (A+B)^64 x, which has 2^64 distinct noncommutative +words, on both sides, and inserts a C^(-1),C cancellation on one side. +The complete two-role comparison uses D=260 states and no expanded words. +The helper is explicitly overwritten on both sides in this stress program; +the separate dirty-sandwich example tests actual helper restoration. + +For a termwise tensor substitution choose the new generators G_a^(tensor f) +and their actual inverses. The theorem then applies at the enlarged payload +dimension. Scalar coefficients stay scalar; no tensor power of a sum or of +the whole register-role matrix is taken. This is only an algebraic interface +lemma. Native realizations, phases, rounding, rectangular typing, precision, +stock, hosting, fixed-tape cost, complete paid invoices and supplier admission +are not proved here. No selected frontier or kappa changes. + +Prepared by Krzysztof Wójt with substantial OpenAI Codex assistance. Apache-2.0. diff --git a/research/orthogonal-inverse-witness/vendor/UPSTREAM-README.md b/research/orthogonal-inverse-witness/vendor/UPSTREAM-README.md new file mode 100644 index 0000000000..1f895da660 --- /dev/null +++ b/research/orthogonal-inverse-witness/vendor/UPSTREAM-README.md @@ -0,0 +1,151 @@ +# Compact certificates for dirty circuits with actual inverse calls + +A name such as `A_inverse` is an independent symbol unless the verifier +implements its relation to `A`. This package closes that specific gap in +[zxv's PR5235](https://github.com/CrocSwap/integer-mult-bounds/pull/5235), exact +head `48976daa4dce59b4867ef046da72a370e389925d`. + +For two linear register programs with r independent input roles and q total +unary occurrences, **D=r+q states** suffice to certify equality of **every +returned role** under all invertible operator substitutions and all payload +dimensions. Forward and inverse occurrences share the same generator. A failed +identity yields explicit unipotent matrices and an input in dimension at most +D. No expansion of reduced words or infinite series is needed. + +The [written proof](PROOF.md) constructs a finite feedback realization at +`G=I+Y`, proves the passage to arbitrary invertible matrices using a central +indeterminate, and gives sound/complete closure certificates. These are a new +repository interface and implementation of classical rational-series ideas, +not a new general weighted-automata or Magnus theorem. This is author-checked +scoped algebra, not supplier admission or a new kappa. + +## Interface and use + +Programs are JSON with `field: 0` for Q or a prime p <= 2^31-1 for F_p, an +ordered list of `roles`, named `operators`, and `left`/`right` instruction lists. +Every role starts as a separate arbitrary vector and every role is compared at +exit. Scalar coefficients are integers or exact fraction strings; denominators +must be invertible in the selected field. See the three [examples](examples). + +| Instruction | Exact semantics | +|---|---| +| `linear`, `dst`, `terms: [[role,c], ...]` | Replace dst by the scalar sum, reading all old values. | +| `apply`, `dst`, `operator`, `direction: 1` or `-1` | Apply G or its actual inverse to dst. | +| `query`, `dst`, `src`, `operator`, `direction`, `coefficient` | Add c G^direction(src) to dst, reading the old source even when src=dst. | + +The [dirty-sandwich example](examples/dirty-sandwich.json) compares two complete +programs with endpoint `(x,h,y+B A x)` and restores arbitrary dirty h. The +[wrong-order example](examples/wrong-order.json) produces a three-dimensional +counterexample; its [literal matrices and input](examples/wrong-order.witness.json) +make the noncommutation failure directly inspectable. The +[binary inverse-tail example](examples/binary-inverse-tail.json) needs a +degree-five coefficient and has a genuinely infinite formal tail. + +Generate and check a certificate from the repository root: + +```sh +python3.12 -B research/inverse-dirty-certificates/certify.py \ + research/inverse-dirty-certificates/examples/dirty-sandwich.json \ + --output /tmp/dirty-sandwich-certificate.json +python3.12 -B research/inverse-dirty-certificates/check_certificate.py \ + research/inverse-dirty-certificates/examples/dirty-sandwich.json \ + /tmp/dirty-sandwich-certificate.json +``` + +For a false identity, `certify.py` also accepts `--witness /tmp/witness.json`, +which writes the actual invertible matrices, all initial role vectors and the +endpoint discrepancy. A valid negative certificate is successfully checked +with verdict `different`; CLI exit success means valid evidence, not equality. + +`check_certificate.py` imports neither `algebra.py` nor the producer. It +reconstructs the feedback equations separately and performs no elimination or +search. It shares only strict syntax and exact field arithmetic. The literal +free-group and matrix oracles are a separate implementation in `oracles.py`. +All were prepared in the same assisted research session; this is not an +independent scientific review claim. + +## Evidence and scope + +The deterministic replay checks: + +- 504 signed-word cancellation/deletion cases over Q, F2 and F5; +- 160 scalar/apply/query differential programs against literal reduced words; +- 64 dirty-boundary, order, self-source and characteristic controls; +- 36 delayed/infinite-tail cases, including positive-characteristic witnesses; +- 324 literal invertible-matrix substitutions of the full dirty boundary; +- 16 malformed/false certificate rejections and 15 invalid-program rejections; +- three committed example certificates and two explicit matrix witnesses. + +The `(A+B)^64` stress endpoint contains **2^64 distinct words** before +comparison. Its inverse-aware certificate uses **260 states and 64 invariant +rows**. It overwrites a helper identically on both sides; actual dirty-helper +restoration is checked separately. This is a compact-representation example, +not a claim about performance on every existing supplier. + +The proof permits arbitrary fields. This executable supports Q and prime +fields only. Inverse calls are exact square linear operations. Extra operator +relations, rectangular types, nonlinear or rounded leaves, native realization, +phase conventions, precision, stock, hosting, tapes and the complete paid/outer +bill remain outside scope. A negative result for independently invertible +generators may disappear under additional relations. The checker does not +certify shortestness of a failure word or a minimum matrix dimension. + +Normal and optimized registered replays, source/history checks and the +Git-free export are recorded in [VALIDATION.json](VALIDATION.json). Finite tests +corroborate the universal written proof; no Lean or independent human review is +claimed. No selected record or predecessor source is changed. + +## Reproduce + +Python 3.12, standard library only. From the repository root: + +```sh +python3.12 -B scripts/research_package.py --package research/inverse-dirty-certificates --check-only +python3.12 scripts/research_package.py --package research/inverse-dirty-certificates +python3.12 -W error -B research/inverse-dirty-certificates/verify.py +python3.12 -W error -O -B research/inverse-dirty-certificates/verify.py +``` + +One direct replay took about 16 seconds on the recorded host. Default replay +does not write package files. `--write-examples` is an explicit regeneration +mode; `--quick` is a development smoke test and is not the registered replay. +The direct verifier is standalone and works in a Git-free package export. +The registered runner additionally validates the pinned Git provenance. + +## Open next questions + +1. Bind one existing inverse-bearing native word to this grammar while + preserving every input and returned helper. Compare against its existing + reduced-word oracle at an exact source head. The remaining blocker is the + adapter's source/type/phase contract; this package does not infer it. +2. Add one other explicitly named relation model, such as commuting pairs. + Start with a normalization theorem and a noncommuting rejection fixture. + Quotienting the present transition matrices without a new proof is unsound. +3. Reduce checker path recomputation on a larger real adapter. Compare identical + closure equations and complete endpoints before changing representation; + exact rational coefficient growth remains an unmeasured scaling constraint. + +These are released questions, not claims on further work. Details and the scope +change from the generic formal-interface card are in [TASK.json](TASK.json). + +## Credit + +Prepared by **Krzysztof Wójt (@krzysztofwojt)** with substantial **OpenAI Codex +assistance**, including a separately delegated exact-oracle implementation. +Apache-2.0. Classical sources are cited in [PROOF.md](PROOF.md). + +Credit **zxv's PR5235** for the compact independent-operator register bridge, +invariant certificates, unipotent witnesses and the explicit inverse-frontend +question. Its dirty-echo lineage (**androolloyd**, **Chafik Boukhalfa/chafreaky +#628**, **Ali Romman #621**), **Cinna Davis #4100/#4088**, **ToikY**'s free-word +tensor audit, **Sagar Thakrar #3687**, **roger-sato #3693**, and the dirty-phase +audit following **Charles Bethin #1278** retain their results and attribution. +No predecessor source code or archived artifact is copied or modified. + +The fresh main base is `ff3cc58e370d0f678e529246f8c73e8094e18fcf`, priority +revision 7. [SOURCES.json](SOURCES.json) distinguishes ancestor provenance from +the contextual pending predecessor, which is not a replay dependency. +The [canonical claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/5236#discussioncomment-19147346) +records live overlap and status. The checked corpus and targeted searches are +evidence of due diligence, not coverage of unpublished work or arbitrary +historical diffs. diff --git a/research/orthogonal-inverse-witness/vendor/algebra.py b/research/orthogonal-inverse-witness/vendor/algebra.py new file mode 100644 index 0000000000..a9e9c8d6f1 --- /dev/null +++ b/research/orthogonal-inverse-witness/vendor/algebra.py @@ -0,0 +1,153 @@ +"""Compact feedback realization and exact reachable-space search. + +This is the producer implementation; check_certificate.py does not import it. +Prepared for Krzysztof Wójt with OpenAI Codex assistance. Apache-2.0. +""" + +from collections import deque + +from syntax import fingerprint, validate + + +def add_scaled(dst, src, scalar, field): + if scalar: + for j, value in enumerate(src): + if value: + dst[j] = field.add(dst[j], field.mul(scalar, value)) + + +def row_times(row, matrix, field): + result = [field.zero] * len(matrix[0]) + for scalar, source in zip(row, matrix): + add_scaled(result, source, scalar, field) + return result + + +def compile_program(program): + """Return U,T,V with coefficients U T_word V after G=I+Y. + + Both sides share the original leaf atoms. Each unary occurrence creates + exactly one further atom, including inverse and zero-coefficient queries. + """ + f = validate(program) + roles = program["roles"] + r = len(roles) + q = sum(ins["op"] != "linear" for side in ("left", "right") for ins in program[side]) + d = r + q + atoms = [] + finals = [] + for side in ("left", "right"): + regs = {name: [f.one if j == i else f.zero for j in range(d)] + for i, name in enumerate(roles)} + for ins in program[side]: + dst = ins["dst"] + if ins["op"] == "linear": + result = [f.zero] * d + for name, coefficient in ins["terms"]: + add_scaled(result, regs[name], f.parse(coefficient), f) + regs[dst] = result + continue + source = dst if ins["op"] == "apply" else ins["src"] + dependency = regs[source][:] + j = r + len(atoms) + atoms.append((ins["operator"], ins["direction"], dependency)) + if ins["op"] == "apply": + regs[dst] = [f.one if k == j else f.zero for k in range(d)] + else: + result = regs[dst][:] + result[j] = f.add(result[j], f.parse(ins["coefficient"])) + regs[dst] = result + finals.append([regs[name] for name in roles]) + u = [[f.sub(x, y) for x, y in zip(a, b)] for a, b in zip(*finals)] + v = [[f.one if i == j else f.zero for j in range(r)] for i in range(d)] + transitions = {a: [[f.zero] * d for _ in range(d)] for a in program["operators"]} + for j, (symbol, direction, dependency) in enumerate(atoms, r): + v[j] = row_times(dependency[:j], v[:j], f) + for a, matrix in transitions.items(): + matrix[j] = row_times(dependency[:j], matrix[:j], f) + if a == symbol: + if direction == 1: + add_scaled(matrix[j], dependency, f.one, f) + else: + matrix[j][j] = f.sub(matrix[j][j], f.one) + return {"field": f, "dimension": d, "U": u, "T": transitions, "V": v} + + +class ReachableBasis: + """Echelon rows with exact coordinates in the original path rows.""" + + def __init__(self, field): + self.field = field + self.rows = [] + self.echelon = [] + + def reduce(self, row): + f = self.field + residual = row[:] + coefficients = [f.zero] * len(self.rows) + for pivot, normalized, coordinates in self.echelon: + scalar = residual[pivot] + if scalar: + add_scaled(residual, normalized, f.neg(scalar), f) + add_scaled(coefficients, coordinates, scalar, f) + return residual, coefficients + + def append(self, row): + f = self.field + residual, removed = self.reduce(row) + pivot = next((j for j, x in enumerate(residual) if x), None) + if pivot is None: + return False + scale = residual[pivot] + normalized = [f.div(x, scale) for x in residual] + coordinates = [f.div(f.neg(x), scale) for x in removed] + [f.div(f.one, scale)] + self.rows.append(row[:]) + self.echelon.append((pivot, normalized, coordinates)) + return True + + def coordinates(self, row): + remainder, coefficients = self.reduce(row) + if any(remainder): + raise ValueError("row is outside the claimed span") + return coefficients + + +def produce(program): + model = compile_program(program) + f, u, t, v = (model[k] for k in ("field", "U", "T", "V")) + basis = ReachableBasis(f) + paths = [] + queue = deque() + for output, row in enumerate(u): + if basis.append(row): + path = {"output": output, "word": []} + paths.append(path) + queue.append((row, path)) + while queue: + row, path = queue.popleft() + projected = row_times(row, v, f) + if any(projected): + i = next(i for i, value in enumerate(projected) if value) + return { + "schema": "inverse-dirty-certificate/v1", + "program_sha256": fingerprint(program), + "verdict": "different", + "output": path["output"], "input": i, "word": path["word"], + "coefficient": f.dump(projected[i]), + } + for symbol, matrix in t.items(): + successor = row_times(row, matrix, f) + if basis.append(successor): + successor_path = {"output": path["output"], "word": path["word"] + [symbol]} + paths.append(successor_path) + queue.append((successor, successor_path)) + encode = lambda rows: [[f.dump(x) for x in row] for row in rows] + return { + "schema": "inverse-dirty-certificate/v1", + "program_sha256": fingerprint(program), + "verdict": "equal", + "paths": paths, + "initial": encode([basis.coordinates(row) for row in u]), + "closure": {a: encode([basis.coordinates(row_times(b, matrix, f)) + for b in basis.rows]) for a, matrix in t.items()}, + } diff --git a/research/orthogonal-inverse-witness/vendor/dirty-sandwich.json b/research/orthogonal-inverse-witness/vendor/dirty-sandwich.json new file mode 100644 index 0000000000..c1254508e7 --- /dev/null +++ b/research/orthogonal-inverse-witness/vendor/dirty-sandwich.json @@ -0,0 +1,105 @@ +{ + "schema": "inverse-dirty-program/v1", + "field": 0, + "roles": [ + "x", + "h", + "y" + ], + "operators": [ + "A", + "B" + ], + "left": [ + { + "op": "apply", + "dst": "h", + "operator": "A", + "direction": -1 + }, + { + "op": "linear", + "dst": "h", + "terms": [ + [ + "h", + 1 + ], + [ + "x", + 1 + ] + ] + }, + { + "op": "apply", + "dst": "h", + "operator": "A", + "direction": 1 + }, + { + "op": "query", + "dst": "y", + "src": "h", + "operator": "B", + "direction": 1, + "coefficient": 1 + }, + { + "op": "apply", + "dst": "h", + "operator": "A", + "direction": -1 + }, + { + "op": "linear", + "dst": "h", + "terms": [ + [ + "h", + 1 + ], + [ + "x", + -1 + ] + ] + }, + { + "op": "apply", + "dst": "h", + "operator": "A", + "direction": 1 + }, + { + "op": "query", + "dst": "y", + "src": "h", + "operator": "B", + "direction": 1, + "coefficient": -1 + } + ], + "right": [ + { + "op": "apply", + "dst": "x", + "operator": "A", + "direction": 1 + }, + { + "op": "query", + "dst": "y", + "src": "x", + "operator": "B", + "direction": 1, + "coefficient": 1 + }, + { + "op": "apply", + "dst": "x", + "operator": "A", + "direction": -1 + } + ] +} diff --git a/research/orthogonal-inverse-witness/vendor/fields.py b/research/orthogonal-inverse-witness/vendor/fields.py new file mode 100644 index 0000000000..2442625a15 --- /dev/null +++ b/research/orthogonal-inverse-witness/vendor/fields.py @@ -0,0 +1,67 @@ +"""Exact Q / prime-field arithmetic shared by the two implementations. + +Prepared for Krzysztof Wójt with OpenAI Codex assistance. Apache-2.0. +""" + +from fractions import Fraction +from functools import lru_cache +from math import isqrt + + +@lru_cache(maxsize=64) +def prime(p): + if p < 2 or p > 2**31 - 1: + return False + if p % 2 == 0: + return p == 2 + return all(p % d for d in range(3, isqrt(p) + 1, 2)) + + +class Field: + def __init__(self, characteristic=0): + if type(characteristic) is not int or ( + characteristic != 0 and not prime(characteristic) + ): + raise ValueError("field must be 0 (Q) or a prime at most 2^31-1") + self.characteristic = characteristic + self.zero = 0 if characteristic else Fraction(0) + self.one = 1 if characteristic else Fraction(1) + + def parse(self, value): + if type(value) not in (int, str, Fraction): + raise ValueError("scalar must be an integer or an exact fraction string") + try: + value = Fraction(value) + except (ValueError, ZeroDivisionError) as error: + raise ValueError("invalid exact scalar") from error + p = self.characteristic + if not p: + return value + if value.denominator % p == 0: + raise ValueError("scalar denominator is zero in the field") + return value.numerator * pow(value.denominator, -1, p) % p + + def add(self, x, y): + return (x + y) % self.characteristic if self.characteristic else x + y + + def sub(self, x, y): + return (x - y) % self.characteristic if self.characteristic else x - y + + def mul(self, x, y): + return (x * y) % self.characteristic if self.characteristic else x * y + + def neg(self, x): + return -x % self.characteristic if self.characteristic else -x + + def div(self, x, y): + if not y: + raise ValueError("division by zero") + if self.characteristic: + return x * pow(y, -1, self.characteristic) % self.characteristic + return x / y + + def dump(self, x): + return str(x) + + def is_zero(self, x): + return x == 0 diff --git a/research/orthogonal-inverse-witness/vendor/syntax.py b/research/orthogonal-inverse-witness/vendor/syntax.py new file mode 100644 index 0000000000..5a91dd1921 --- /dev/null +++ b/research/orthogonal-inverse-witness/vendor/syntax.py @@ -0,0 +1,71 @@ +"""Strict syntax and byte-independent binding, not an algebraic compiler. + +Prepared for Krzysztof Wójt with OpenAI Codex assistance. Apache-2.0. +""" + +import hashlib +import json + +from fields import Field + + +def exact_keys(obj, keys): + if not isinstance(obj, dict) or set(obj) != set(keys): + raise ValueError(f"expected exactly these keys: {sorted(keys)}") + + +def names(values, nonempty=False): + if not isinstance(values, list) or (nonempty and not values): + raise ValueError("expected a list of names") + if any(not isinstance(x, str) or not x for x in values): + raise ValueError("names must be nonempty strings") + if len(set(values)) != len(values): + raise ValueError("duplicate name") + + +def validate(program): + exact_keys(program, {"schema", "field", "roles", "operators", "left", "right"}) + if program["schema"] != "inverse-dirty-program/v1": + raise ValueError("unknown program schema") + field = Field(program["field"]) + names(program["roles"], nonempty=True) + names(program["operators"]) + roles, operators = set(program["roles"]), set(program["operators"]) + for side in ("left", "right"): + if not isinstance(program[side], list): + raise ValueError("instruction sequence must be a list") + for ins in program[side]: + if not isinstance(ins, dict): + raise ValueError("instruction must be an object") + op = ins.get("op") + if op == "linear": + exact_keys(ins, {"op", "dst", "terms"}) + if not isinstance(ins["terms"], list): + raise ValueError("linear terms must be a list") + for term in ins["terms"]: + if not isinstance(term, list) or len(term) != 2 or term[0] not in roles: + raise ValueError("invalid linear term or undeclared source") + field.parse(term[1]) + elif op in ("apply", "query"): + keys = {"op", "dst", "operator", "direction"} + if op == "query": + keys |= {"src", "coefficient"} + exact_keys(ins, keys) + if ins["operator"] not in operators: + raise ValueError("undeclared operator") + if type(ins["direction"]) is not int or ins["direction"] not in (-1, 1): + raise ValueError("direction must be exactly +1 or -1") + if op == "query": + if ins["src"] not in roles: + raise ValueError("undeclared query source") + field.parse(ins["coefficient"]) + else: + raise ValueError("unknown instruction") + if ins["dst"] not in roles: + raise ValueError("undeclared destination") + return field + + +def fingerprint(program): + payload = json.dumps(program, sort_keys=True, separators=(",", ":"), ensure_ascii=True) + return hashlib.sha256(payload.encode("ascii")).hexdigest() diff --git a/research/orthogonal-inverse-witness/vendor/wrong-order.json b/research/orthogonal-inverse-witness/vendor/wrong-order.json new file mode 100644 index 0000000000..3beca6f4b1 --- /dev/null +++ b/research/orthogonal-inverse-witness/vendor/wrong-order.json @@ -0,0 +1,38 @@ +{ + "schema": "inverse-dirty-program/v1", + "field": 0, + "roles": [ + "x" + ], + "operators": [ + "A", + "B" + ], + "left": [ + { + "op": "apply", + "dst": "x", + "operator": "A", + "direction": 1 + }, + { + "op": "apply", + "dst": "x", + "operator": "B", + "direction": 1 + }, + { + "op": "apply", + "dst": "x", + "operator": "A", + "direction": -1 + }, + { + "op": "apply", + "dst": "x", + "operator": "B", + "direction": -1 + } + ], + "right": [] +} diff --git a/research/orthogonal-inverse-witness/verify.py b/research/orthogonal-inverse-witness/verify.py new file mode 100644 index 0000000000..c290e18c22 --- /dev/null +++ b/research/orthogonal-inverse-witness/verify.py @@ -0,0 +1,302 @@ +"""Check exact witnesses against separate dense and reduced-word oracles. + +Prepared by Ali Romman with substantial OpenAI Codex assistance. Apache-2.0. +""" + +import argparse +from copy import deepcopy +from fractions import Fraction as Q +import hashlib +import json +from pathlib import Path +import random +import sys + +ROOT = Path(__file__).resolve().parent +sys.path.insert(0, str(ROOT)) +from witness import construct +from check_witness import check +from literal import action, parameters, replay + + +def require(value, message): + if not value: + raise ValueError(message) + + +def rejected(call): + try: + call() + except (ValueError, TypeError, ZeroDivisionError): + return + raise ValueError("invalid case was accepted") + + +def program(roles=None): + return {"schema": "inverse-dirty-program/v1", "field": 0, + "roles": roles or ["x"], "operators": ["A", "B"], "left": [], "right": []} + + +def apply(dst, a, direction): + return {"op": "apply", "dst": dst, "operator": a, "direction": direction} + + +def linear(dst, terms): + return {"op": "linear", "dst": dst, "terms": terms} + + +def query(dst, src, a, direction, coefficient): + return {"op": "query", "dst": dst, "src": src, "operator": a, + "direction": direction, "coefficient": coefficient} + + +def dense_inverse(matrix): + n = len(matrix) + rows = [row[:] + [Q(i == j) for j in range(n)] for i, row in enumerate(matrix)] + for col in range(n): + pivot = next(i for i in range(col, n) if rows[i][col]) + rows[col], rows[pivot] = rows[pivot], rows[col] + v = rows[col][col] + rows[col] = [x / v for x in rows[col]] + for i in range(n): + if i != col: + v = rows[i][col] + rows[i] = [x - v * y for x, y in zip(rows[i], rows[col])] + return [row[n:] for row in rows] + + +def matvec(matrix, vector): + return [sum((a * b for a, b in zip(row, vector)), Q(0)) for row in matrix] + + +def dense_replay(p, w): + n, e = w["dimension"], Q(w["epsilon"]) + matrices = {} + for a in p["operators"]: + matrix = [[Q(i == j) * (1 - e) for j in range(n)] for i in range(n)] + for j, label in enumerate(w["word"]): + if label == a: + matrix[j][j + 1] = matrix[j + 1][j] = e / 2 + inverse = dense_inverse(matrix) + for j in range(n): + radius = sum(abs(matrix[j][k]) for k in range(n) if k != j) + require(matrix[j][j] - radius >= 1 - 2 * e, "lower spectral bound") + require(matrix[j][j] + radius <= 1, "upper spectral bound") + column = [inverse[k][j] for k in range(n)] + require(matvec(matrix, column) == [Q(k == j) for k in range(n)], "true inverse") + matrices[a, 1], matrices[a, -1] = matrix, inverse + results = [] + for side in ("left", "right"): + values = [[Q(i == w["input"] and j == n - 1) for j in range(n)] + for i in range(len(p["roles"]))] + for ins in p[side]: + target = p["roles"].index(ins["dst"]) + old = [v[:] for v in values] + if ins["op"] == "linear": + values[target] = [sum((Q(c) * old[p["roles"].index(src)][j] + for src, c in ins["terms"]), Q(0)) for j in range(n)] + else: + source = target if ins["op"] == "apply" else p["roles"].index(ins["src"]) + product = matvec(matrices[ins["operator"], ins["direction"]], old[source]) + values[target] = product if ins["op"] == "apply" else [ + x + Q(ins["coefficient"]) * y for x, y in zip(old[target], product)] + results.append(values) + return [[x - y for x, y in zip(a, b)] for a, b in zip(*results)] + + +def group_difference(p): + """Expand only the small tests in the free-group basis.""" + finals = [] + for side in ("left", "right"): + regs = {role: {(i, ()): Q(1)} for i, role in enumerate(p["roles"])} + for ins in p[side]: + result = {} + def add(source, c, letter=None): + for (i, word), value in source.items(): + if letter is None: + out = word + elif word and word[0] == (letter[0], -letter[1]): + out = word[1:] + else: + out = (letter,) + word + key = i, out + result[key] = result.get(key, Q(0)) + c * value + dst = ins["dst"] + if ins["op"] == "linear": + for src, c in ins["terms"]: + add(regs[src], Q(c)) + else: + src = dst if ins["op"] == "apply" else ins["src"] + if ins["op"] == "query": + add(regs[dst], Q(1)) + c = Q(1) if ins["op"] == "apply" else Q(ins["coefficient"]) + add(regs[src], c, (ins["operator"], ins["direction"])) + regs[dst] = {key: value for key, value in result.items() if value} + finals.append(regs) + return finals[0] != finals[1] + + +def grid_roots(count): + p = program(["x", "h"]) + for j in range(1, count + 1): + root = Q(count + 2 - j, 4 * (count + 1)) + alpha = 1 / (1 - root) + p["left"] += [linear("h", [["x", 1]]), apply("x", "A", -1), + linear("x", [["x", 1], ["h", str(-alpha)]]), linear("h", [])] + p["right"] = [linear("x", []), linear("h", [])] + return p + + +def stress(count): + p = program(["x", "h"]) + for _ in range(count): + p["left"] += [linear("h", [["x", 1]]), linear("x", [["x", 2]]), + query("x", "h", "A", -1, -1), query("x", "h", "B", -1, -1)] + p["left"].append(linear("h", [])) + p["right"] = [linear("x", []), linear("h", [])] + return p + + +def run(small): + digest = hashlib.sha256() + dense_count = 0 + def inspect(p, cap=Q(1, 4), dense=True): + nonlocal dense_count + w = construct(p, cap) + literal = check(p, w) + if dense: + require(literal == dense_replay(p, w), "independent dense endpoint") + dense_count += 1 + digest.update(json.dumps(w, sort_keys=True).encode()) + return w + + wrong = json.loads((ROOT / "vendor/wrong-order.json").read_text()) + wrong_witness = inspect(wrong) + require(wrong_witness["dimension"] == 3, "commutator must have degree two") + tiny = inspect(wrong, Q(1, 2**40)) + require(Q(tiny["epsilon"]) <= Q(1, 2**40), "arbitrary small cap") + sandwich = json.loads((ROOT / "vendor/dirty-sandwich.json").read_text()) + rejected(lambda: construct(sandwich)) + deletion_count = 0 + for index in range(len(sandwich["left"])): + p = deepcopy(sandwich) + del p["left"][index] + require(group_difference(p), "deleted sandwich instruction is detectable") + inspect(p) + deletion_count += 1 + + roots = [] + for count in (1, 2, 4, 7): + p = grid_roots(count) + w = inspect(p) + require(w["word"] == [] and w["grid_index"] == count + 1, "must use last grid point") + for j in range(1, count + 1): + require(replay(p, [], Q(count + 2 - j, 4 * (count + 1)), 0)[0][0] == 0, "grid root") + roots.append({"roots": count, "grid_size": w["grid_size"], + "accepted_index": w["grid_index"], "difference": w["endpoint_difference"][0][0]}) + + # This case returns a changed dirty role even though x is unchanged. + dirty = program(["x", "h"]) + dirty["left"] = [apply("h", "A", -1)] + dw = inspect(dirty) + require(dw["input"] == dw["output"] == 1, "retain every dirty input and return") + # The source and destination alias in this inverse query. + self_query = program() + self_query["left"] = [query("x", "x", "A", -1, -1)] + self_query["right"] = [linear("x", [])] + inspect(self_query) + constant = program() + constant["left"] = [linear("x", [["x", 2]])] + cw = inspect(constant) + require(cw["grid_size"] == cw["dimension"] == 1, "constant boundary") + + controls = 0 + changes = {"program_sha256": "0" * 64, "dimension": 4, "input": True, + "output": 7, "word": ["C"], "epsilon": "0", "epsilon_cap": "1/2", + "numerator_degree_bound": -1, "grid_index": 0, "grid_size": 0, + "endpoint_difference": [["0"] * 3]} + for key, value in changes.items(): + bad = deepcopy(wrong_witness) + bad[key] = value + rejected(lambda: check(wrong, bad)) + controls += 1 + bad_program = deepcopy(wrong) + bad_program["field"] = 2 + rejected(lambda: construct(bad_program)) + rejected(lambda: construct(wrong, Q(0))) + rejected(lambda: construct(wrong, Q(1, 3))) + controls += 3 + + random_count, equal_count, negative_count = 0, 0, 0 + rng = random.Random(52625268) + for index in range(12 if small else 160): + p = program(["x", "h", "y"]) + for side in ("left", "right"): + for _ in range(rng.randrange(3, 9)): + dst, src = rng.choice(p["roles"]), rng.choice(p["roles"]) + a, sign = rng.choice(p["operators"]), rng.choice((-1, 1)) + kind = rng.randrange(3) + if kind == 0: + ins = apply(dst, a, sign) + elif kind == 1: + ins = query(dst, src, a, sign, str(Q(rng.randrange(-2, 3), 2))) + else: + ins = linear(dst, [[src, rng.randrange(-2, 3)], [dst, 1]]) + p[side].append(ins) + if index % 4 == 0: + p["right"] = deepcopy(p["left"]) + [apply("h", "B", 1), apply("h", "B", -1)] + if group_difference(p): + inspect(p) + negative_count += 1 + else: + rejected(lambda: construct(p)) + equal_count += 1 + random_count += 1 + + depth = 5 if small else 32 + sw = inspect(stress(depth), dense=False) + require(sw["dimension"] == depth + 1 and sw["word"] == ["A"] * depth, "delayed inverse series") + # Check exact inverse action on all basis vectors on independent path labels. + vector_checks = 0 + for length in range(1, 5 if small else 12): + word = [rng.choice(("A", "B")) for _ in range(length)] + for band in parameters(wrong, word, Q(1, 4)).values(): + for j in range(length + 1): + vector = [Q(i == j) for i in range(length + 1)] + require(action(band, action(band, vector, -1), 1) == vector, "solve residual") + vector_checks += 1 + result = {"schema": "spd-inverse-verification/v1", "status": "PASS", + "random_programs": random_count, "random_equal": equal_count, + "random_different": negative_count, "dense_full_replays": dense_count, + "sandwich_deletions": deletion_count, "rejecting_controls": controls, + "true_inverse_basis_checks": vector_checks, "forced_grid_examples": roots, + "commutator": wrong_witness, "near_identity_epsilon": tiny["epsilon"], + "stress": {"lowest_degree_words": 2**depth, "states": 2 + 2 * depth, + "dimension": sw["dimension"], "degree_bound": sw["numerator_degree_bound"], + "grid_size": sw["grid_size"], "accepted_index": sw["grid_index"]}, + "witness_digest": digest.hexdigest()} + return result + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--small", action="store_true") + parser.add_argument("--write-result", action="store_true") + args = parser.parse_args() + result = run(args.small) + if not args.small: + source = json.loads((ROOT / "SOURCES.json").read_text()) + for row in source["files"]: + if "/vendor/" in row["path"]: + path = ROOT / "vendor" / Path(row["path"]).name + require(hashlib.sha256(path.read_bytes()).hexdigest() == row["sha256"], "source bytes") + if args.write_result: + (ROOT / "RESULT.json").write_text(json.dumps(result, indent=2) + "\n", encoding="utf-8") + else: + require(result == json.loads((ROOT / "RESULT.json").read_text()), "committed receipt") + print(json.dumps(result, sort_keys=True)) + print("PASS_SPD_INVERSE_CIRCUIT_WITNESS") + + +if __name__ == "__main__": + main() diff --git a/research/orthogonal-inverse-witness/witness.py b/research/orthogonal-inverse-witness/witness.py new file mode 100644 index 0000000000..1b85f74b37 --- /dev/null +++ b/research/orthogonal-inverse-witness/witness.py @@ -0,0 +1,59 @@ +"""Construct an SPD witness for a false complete rational inverse identity. + +Prepared by Ali Romman with substantial OpenAI Codex assistance. Apache-2.0. +""" + +import argparse +from fractions import Fraction +import json +from pathlib import Path +import sys + +sys.path.insert(0, str(Path(__file__).resolve().parent)) +from literal import degree_bound, replay +from algebra import produce +from syntax import validate + + +def construct(program, epsilon_cap=Fraction(1, 4)): + if validate(program).characteristic: + raise ValueError("the SPD construction requires Q") + epsilon_cap = Fraction(epsilon_cap) + if not 0 < epsilon_cap <= Fraction(1, 4): + raise ValueError("epsilon cap must be in (0, 1/4]") + coefficient = produce(program) + if coefficient["verdict"] != "different": + raise ValueError("equal programs have no distinguishing witness") + word = coefficient["word"] + n = len(word) + 1 + degree = degree_bound(program, n) + for index in range(1, degree + 2): + epsilon = epsilon_cap * (degree + 2 - index) / (degree + 1) + difference = replay(program, word, epsilon, coefficient["input"]) + if difference[coefficient["output"]][0]: + return { + "schema": "spd-inverse-witness/v1", + "program_sha256": coefficient["program_sha256"], + "word": word, "dimension": n, + "input": coefficient["input"], "output": coefficient["output"], + "epsilon": str(epsilon), "epsilon_cap": str(epsilon_cap), + "numerator_degree_bound": degree, + "grid_size": degree + 1, "grid_index": index, + "endpoint_difference": [[str(x) for x in row] for row in difference], + } + raise ValueError("the proved root budget was exhausted") + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("program", type=Path) + parser.add_argument("--output", type=Path, required=True) + parser.add_argument("--epsilon-cap", default="1/4") + args = parser.parse_args() + result = construct(json.loads(args.program.read_text()), Fraction(args.epsilon_cap)) + args.output.write_text(json.dumps(result, indent=2) + "\n", encoding="utf-8") + print("PASS_SPD_INVERSE_WITNESS_PRODUCED") + + +if __name__ == "__main__": + main() From 9bebc267c4608e51fcc94a543b8e0d66077cdfbb Mon Sep 17 00:00:00 2001 From: Ali Romman <226877337+aliromman@users.noreply.github.com> Date: Fri, 23 Oct 2026 12:05:41 -0500 Subject: [PATCH 2/2] Construct exact orthogonal witnesses for complete inverse circuits --- research/orthogonal-inverse-witness/PROOF.md | 159 ++++++++++++++++++ research/orthogonal-inverse-witness/README.md | 65 +++++++ .../orthogonal-inverse-witness/RESULT.json | 72 ++++++++ .../orthogonal-inverse-witness/SOURCES.json | 150 +++++++++++++++++ research/orthogonal-inverse-witness/TASK.json | 95 +++++++++++ .../orthogonal-inverse-witness/VALIDATION.md | 32 ++++ .../orthogonal-inverse-witness/VERIFY.json | 34 ++++ .../check_witness.py | 14 +- .../orthogonal-inverse-witness/literal.py | 60 +++---- research/orthogonal-inverse-witness/verify.py | 86 +++++++--- .../orthogonal-inverse-witness/witness.py | 26 +-- 11 files changed, 716 insertions(+), 77 deletions(-) create mode 100644 research/orthogonal-inverse-witness/PROOF.md create mode 100644 research/orthogonal-inverse-witness/README.md create mode 100644 research/orthogonal-inverse-witness/RESULT.json create mode 100644 research/orthogonal-inverse-witness/SOURCES.json create mode 100644 research/orthogonal-inverse-witness/TASK.json create mode 100644 research/orthogonal-inverse-witness/VALIDATION.md create mode 100644 research/orthogonal-inverse-witness/VERIFY.json diff --git a/research/orthogonal-inverse-witness/PROOF.md b/research/orthogonal-inverse-witness/PROOF.md new file mode 100644 index 0000000000..aeaae8bd63 --- /dev/null +++ b/research/orthogonal-inverse-witness/PROOF.md @@ -0,0 +1,159 @@ +# Rational orthogonal witnesses for inverse circuits + +Prepared by Ali Romman with substantial OpenAI Codex assistance. Apache-2.0. +This is a written proof. The exact tests support it; they are not a proof-assistant result. + +## Contract and result + +Use the complete rational register grammar of Krzysztof Wójt's +[PR #5262](https://github.com/CrocSwap/integer-mult-bounds/pull/5262), at +`6f92ccf1e61c4668c8ee687bd1df8b42932b8759`. Its proof and source notices are +retained in `vendor/UPSTREAM-PROOF.md` and `vendor/UPSTREAM-README.md`. +There are r independent input roles, and both programs return every role. +A scalar linear assignment reads all old values. An apply instruction uses +one named G_a or its actual inverse. A query adds c G_a^(+/-1) src to dst +from the old values, also when src equals dst. Let q count all apply and query +occurrences in both programs, including zero-coefficient queries. Put N=r+q. +Only inverses of named generators are allowed, not inverses of sums. + +**Theorem.** If the two programs differ at any invertible matrix tuple over Q, +then for each rational cap 0= 1 - 2 * e, "lower spectral bound") - require(matrix[j][j] + radius <= 1, "upper spectral bound") - column = [inverse[k][j] for k in range(n)] - require(matvec(matrix, column) == [Q(k == j) for k in range(n)], "true inverse") + transpose = list(map(list, zip(*matrix))) + require(inverse == transpose, "inverse must be transpose") + require(mm(transpose, matrix) == identity, "exact orthogonality") + require(determinant(matrix) == 1, "special orthogonal determinant") matrices[a, 1], matrices[a, -1] = matrix, inverse results = [] for side in ("left", "right"): @@ -138,11 +161,15 @@ def add(source, c, letter=None): def grid_roots(count): p = program(["x", "h"]) + p["left"] = [linear("h", [["x", 1]]), apply("x", "A", 1), + linear("x", [["x", 1], ["h", -1]])] + grid = 4 * count + 3 for j in range(1, count + 1): - root = Q(count + 2 - j, 4 * (count + 1)) - alpha = 1 / (1 - root) - p["left"] += [linear("h", [["x", 1]]), apply("x", "A", -1), - linear("x", [["x", 1], ["h", str(-alpha)]]), linear("h", [])] + root = Q(grid + 1 - j, 4 * grid) + alpha = 2 * (1 - root**2 / 4) / (1 + root**2 / 4) + p["left"] += [linear("h", [["x", 1]]), linear("x", [["h", str(-alpha)]]), + query("x", "h", "A", 1, 1), query("x", "h", "A", -1, 1)] + p["left"].append(linear("h", [])) p["right"] = [linear("x", []), linear("h", [])] return p @@ -174,7 +201,7 @@ def inspect(p, cap=Q(1, 4), dense=True): wrong_witness = inspect(wrong) require(wrong_witness["dimension"] == 3, "commutator must have degree two") tiny = inspect(wrong, Q(1, 2**40)) - require(Q(tiny["epsilon"]) <= Q(1, 2**40), "arbitrary small cap") + require(Q(tiny["parameter"]) <= Q(1, 2**40), "arbitrary small cap") sandwich = json.loads((ROOT / "vendor/dirty-sandwich.json").read_text()) rejected(lambda: construct(sandwich)) deletion_count = 0 @@ -189,12 +216,28 @@ def inspect(p, cap=Q(1, 4), dense=True): for count in (1, 2, 4, 7): p = grid_roots(count) w = inspect(p) - require(w["word"] == [] and w["grid_index"] == count + 1, "must use last grid point") + require(w["word"] == ["A"] and w["grid_index"] == count + 1, "must skip all grid roots") for j in range(1, count + 1): - require(replay(p, [], Q(count + 2 - j, 4 * (count + 1)), 0)[0][0] == 0, "grid root") + require(replay(p, ["A"], Q(4 * count + 4 - j, 4 * (4 * count + 3)), 0)[0][0] == 0, "grid root") roots.append({"roots": count, "grid_size": w["grid_size"], "accepted_index": w["grid_index"], "difference": w["endpoint_difference"][0][0]}) + difference = program() + difference["left"] = [apply("x", "A", 1)] + difference["right"] = [apply("x", "A", -1)] + short = inspect(difference) + require(short["word"] == ["A"], "shortest coefficient is required") + for t in (Q(1, 4), Q(1, 7), Q(1, 100)): + require(replay(difference, ["A", "A"], t, 0)[0][0] == 0, + "a longer nonzero coefficient need not survive Cayley substitution") + nested = [("A", 1), ("B", 1), ("A", -1), ("B", -1)] + for degree in range(2, 6): + p = program() + p["left"] = [apply("x", a, sign) for a, sign in nested] + w = inspect(p) + require(w["dimension"] == degree + 1, "nested commutator leading degree") + nested = nested + [("A", 1)] + [(a, -sign) for a, sign in reversed(nested)] + [("A", -1)] + # This case returns a changed dirty role even though x is unchanged. dirty = program(["x", "h"]) dirty["left"] = [apply("h", "A", -1)] @@ -212,7 +255,7 @@ def inspect(p, cap=Q(1, 4), dense=True): controls = 0 changes = {"program_sha256": "0" * 64, "dimension": 4, "input": True, - "output": 7, "word": ["C"], "epsilon": "0", "epsilon_cap": "1/2", + "output": 7, "word": ["C"], "parameter": "0", "parameter_cap": "1/2", "numerator_degree_bound": -1, "grid_index": 0, "grid_size": 0, "endpoint_difference": [["0"] * 3]} for key, value in changes.items(): @@ -264,13 +307,14 @@ def inspect(p, cap=Q(1, 4), dense=True): for j in range(length + 1): vector = [Q(i == j) for i in range(length + 1)] require(action(band, action(band, vector, -1), 1) == vector, "solve residual") + require(sum(x*x for x in action(band, vector, 1)) == 1, "exact Euclidean norm") vector_checks += 1 - result = {"schema": "spd-inverse-verification/v1", "status": "PASS", + result = {"schema": "orthogonal-inverse-verification/v1", "status": "PASS", "random_programs": random_count, "random_equal": equal_count, "random_different": negative_count, "dense_full_replays": dense_count, "sandwich_deletions": deletion_count, "rejecting_controls": controls, - "true_inverse_basis_checks": vector_checks, "forced_grid_examples": roots, - "commutator": wrong_witness, "near_identity_epsilon": tiny["epsilon"], + "true_inverse_basis_checks": vector_checks, "nested_commutators": 4, "nonshortest_zero_controls": 3, "forced_grid_examples": roots, + "commutator": wrong_witness, "near_identity_parameter": tiny["parameter"], "stress": {"lowest_degree_words": 2**depth, "states": 2 + 2 * depth, "dimension": sw["dimension"], "degree_bound": sw["numerator_degree_bound"], "grid_size": sw["grid_size"], "accepted_index": sw["grid_index"]}, @@ -295,7 +339,7 @@ def main(): else: require(result == json.loads((ROOT / "RESULT.json").read_text()), "committed receipt") print(json.dumps(result, sort_keys=True)) - print("PASS_SPD_INVERSE_CIRCUIT_WITNESS") + print("PASS_ORTHOGONAL_INVERSE_CIRCUIT_WITNESS") if __name__ == "__main__": diff --git a/research/orthogonal-inverse-witness/witness.py b/research/orthogonal-inverse-witness/witness.py index 1b85f74b37..5ee87c5942 100644 --- a/research/orthogonal-inverse-witness/witness.py +++ b/research/orthogonal-inverse-witness/witness.py @@ -1,4 +1,4 @@ -"""Construct an SPD witness for a false complete rational inverse identity. +"""Construct an orthogonal witness for a false complete rational inverse identity. Prepared by Ali Romman with substantial OpenAI Codex assistance. Apache-2.0. """ @@ -15,12 +15,12 @@ from syntax import validate -def construct(program, epsilon_cap=Fraction(1, 4)): +def construct(program, parameter_cap=Fraction(1, 4)): if validate(program).characteristic: - raise ValueError("the SPD construction requires Q") - epsilon_cap = Fraction(epsilon_cap) - if not 0 < epsilon_cap <= Fraction(1, 4): - raise ValueError("epsilon cap must be in (0, 1/4]") + raise ValueError("the orthogonal construction requires Q") + parameter_cap = Fraction(parameter_cap) + if not 0 < parameter_cap <= Fraction(1, 4): + raise ValueError("parameter cap must be in (0, 1/4]") coefficient = produce(program) if coefficient["verdict"] != "different": raise ValueError("equal programs have no distinguishing witness") @@ -28,15 +28,15 @@ def construct(program, epsilon_cap=Fraction(1, 4)): n = len(word) + 1 degree = degree_bound(program, n) for index in range(1, degree + 2): - epsilon = epsilon_cap * (degree + 2 - index) / (degree + 1) - difference = replay(program, word, epsilon, coefficient["input"]) + parameter = parameter_cap * (degree + 2 - index) / (degree + 1) + difference = replay(program, word, parameter, coefficient["input"]) if difference[coefficient["output"]][0]: return { - "schema": "spd-inverse-witness/v1", + "schema": "orthogonal-inverse-witness/v1", "program_sha256": coefficient["program_sha256"], "word": word, "dimension": n, "input": coefficient["input"], "output": coefficient["output"], - "epsilon": str(epsilon), "epsilon_cap": str(epsilon_cap), + "parameter": str(parameter), "parameter_cap": str(parameter_cap), "numerator_degree_bound": degree, "grid_size": degree + 1, "grid_index": index, "endpoint_difference": [[str(x) for x in row] for row in difference], @@ -48,11 +48,11 @@ def main(): parser = argparse.ArgumentParser(description=__doc__) parser.add_argument("program", type=Path) parser.add_argument("--output", type=Path, required=True) - parser.add_argument("--epsilon-cap", default="1/4") + parser.add_argument("--parameter-cap", default="1/4") args = parser.parse_args() - result = construct(json.loads(args.program.read_text()), Fraction(args.epsilon_cap)) + result = construct(json.loads(args.program.read_text()), Fraction(args.parameter_cap)) args.output.write_text(json.dumps(result, indent=2) + "\n", encoding="utf-8") - print("PASS_SPD_INVERSE_WITNESS_PRODUCED") + print("PASS_ORTHOGONAL_INVERSE_WITNESS_PRODUCED") if __name__ == "__main__":