From f736ecedbacfa9a86b9082d5387af702f643b6dd Mon Sep 17 00:00:00 2001 From: Ali Romman <226877337+aliromman@users.noreply.github.com> Date: Fri, 23 Oct 2026 12:30:58 -0500 Subject: [PATCH 1/2] Retain orthogonal witness sources for a finite-precision detector --- .../vendor/orthogonal/PROOF.md | 159 ++++++++ .../vendor/orthogonal/README.md | 65 ++++ .../vendor/orthogonal/check_witness.py | 68 ++++ .../vendor/orthogonal/literal.py | 80 ++++ .../orthogonal/vendor/UPSTREAM-PROOF.md | 246 +++++++++++++ .../orthogonal/vendor/UPSTREAM-README.md | 151 ++++++++ .../vendor/orthogonal/vendor/algebra.py | 153 ++++++++ .../orthogonal/vendor/dirty-sandwich.json | 105 ++++++ .../vendor/orthogonal/vendor/fields.py | 67 ++++ .../vendor/orthogonal/vendor/syntax.py | 71 ++++ .../vendor/orthogonal/vendor/wrong-order.json | 38 ++ .../vendor/orthogonal/verify.py | 346 ++++++++++++++++++ .../vendor/orthogonal/witness.py | 59 +++ 13 files changed, 1608 insertions(+) create mode 100644 research/orthogonal-witness-precision/vendor/orthogonal/PROOF.md create mode 100644 research/orthogonal-witness-precision/vendor/orthogonal/README.md create mode 100644 research/orthogonal-witness-precision/vendor/orthogonal/check_witness.py create mode 100644 research/orthogonal-witness-precision/vendor/orthogonal/literal.py create mode 100644 research/orthogonal-witness-precision/vendor/orthogonal/vendor/UPSTREAM-PROOF.md create mode 100644 research/orthogonal-witness-precision/vendor/orthogonal/vendor/UPSTREAM-README.md create mode 100644 research/orthogonal-witness-precision/vendor/orthogonal/vendor/algebra.py create mode 100644 research/orthogonal-witness-precision/vendor/orthogonal/vendor/dirty-sandwich.json create mode 100644 research/orthogonal-witness-precision/vendor/orthogonal/vendor/fields.py create mode 100644 research/orthogonal-witness-precision/vendor/orthogonal/vendor/syntax.py create mode 100644 research/orthogonal-witness-precision/vendor/orthogonal/vendor/wrong-order.json create mode 100644 research/orthogonal-witness-precision/vendor/orthogonal/verify.py create mode 100644 research/orthogonal-witness-precision/vendor/orthogonal/witness.py diff --git a/research/orthogonal-witness-precision/vendor/orthogonal/PROOF.md b/research/orthogonal-witness-precision/vendor/orthogonal/PROOF.md new file mode 100644 index 0000000000..aeaae8bd63 --- /dev/null +++ b/research/orthogonal-witness-precision/vendor/orthogonal/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 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, parameter = Fraction(witness["parameter_cap"]), Fraction(witness["parameter"]) + index = witness["grid_index"] + if not 0 < cap <= Fraction(1, 4) or not 1 <= index <= degree + 1: + raise ValueError("invalid grid range") + if parameter != cap * (degree + 2 - index) / (degree + 1): + raise ValueError("invalid grid point") + difference = replay(program, word, parameter, 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_ORTHOGONAL_INVERSE_WITNESS_CHECKED") + + +if __name__ == "__main__": + main() diff --git a/research/orthogonal-witness-precision/vendor/orthogonal/literal.py b/research/orthogonal-witness-precision/vendor/orthogonal/literal.py new file mode 100644 index 0000000000..b8ac1a86c4 --- /dev/null +++ b/research/orthogonal-witness-precision/vendor/orthogonal/literal.py @@ -0,0 +1,80 @@ +"""Execute the complete program with rational Cayley 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, parameter): + if validate(program).characteristic: + raise ValueError("the orthogonal construction requires Q") + if any(a not in program["operators"] for a in word): + raise ValueError("unknown path label") + if not 0 < parameter <= Fraction(1, 4): + raise ValueError("parameter must be in (0, 1/4]") + bands = {} + for a in program["operators"]: + off = [parameter / 2 if b == a else Fraction(0) for b in word] + pivots = [Fraction(1)] * (len(word) + 1) + for j in range(1, len(pivots)): + pivots[j] += off[j - 1] ** 2 / pivots[j - 1] + bands[a] = off, pivots + return bands + + +def action(band, vector, direction): + if direction not in (-1, 1): + raise ValueError("direction must be +1 or -1") + off, pivots = band + n = len(vector) + result = vector[:] + # Form (I + direction*t*K/2) v from the old vector. + for j, edge in enumerate(off): + result[j] += direction * edge * vector[j + 1] + result[j + 1] -= direction * edge * vector[j] + # Solve (I - direction*t*K/2) x = result. + for j in range(1, n): + result[j] -= direction * 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] + direction * off[j] * result[j + 1]) / pivots[j] + return result + + +def replay(program, word, parameter, input_index): + bands = parameters(program, word, parameter) + 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): + q = sum(ins["op"] != "linear" for side in ("left", "right") for ins in program[side]) + return dimension * q diff --git a/research/orthogonal-witness-precision/vendor/orthogonal/vendor/UPSTREAM-PROOF.md b/research/orthogonal-witness-precision/vendor/orthogonal/vendor/UPSTREAM-PROOF.md new file mode 100644 index 0000000000..d2433c24ca --- /dev/null +++ b/research/orthogonal-witness-precision/vendor/orthogonal/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-witness-precision/vendor/orthogonal/vendor/UPSTREAM-README.md b/research/orthogonal-witness-precision/vendor/orthogonal/vendor/UPSTREAM-README.md new file mode 100644 index 0000000000..1f895da660 --- /dev/null +++ b/research/orthogonal-witness-precision/vendor/orthogonal/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-witness-precision/vendor/orthogonal/vendor/algebra.py b/research/orthogonal-witness-precision/vendor/orthogonal/vendor/algebra.py new file mode 100644 index 0000000000..a9e9c8d6f1 --- /dev/null +++ b/research/orthogonal-witness-precision/vendor/orthogonal/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-witness-precision/vendor/orthogonal/vendor/dirty-sandwich.json b/research/orthogonal-witness-precision/vendor/orthogonal/vendor/dirty-sandwich.json new file mode 100644 index 0000000000..c1254508e7 --- /dev/null +++ b/research/orthogonal-witness-precision/vendor/orthogonal/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-witness-precision/vendor/orthogonal/vendor/fields.py b/research/orthogonal-witness-precision/vendor/orthogonal/vendor/fields.py new file mode 100644 index 0000000000..2442625a15 --- /dev/null +++ b/research/orthogonal-witness-precision/vendor/orthogonal/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-witness-precision/vendor/orthogonal/vendor/syntax.py b/research/orthogonal-witness-precision/vendor/orthogonal/vendor/syntax.py new file mode 100644 index 0000000000..5a91dd1921 --- /dev/null +++ b/research/orthogonal-witness-precision/vendor/orthogonal/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-witness-precision/vendor/orthogonal/vendor/wrong-order.json b/research/orthogonal-witness-precision/vendor/orthogonal/vendor/wrong-order.json new file mode 100644 index 0000000000..3beca6f4b1 --- /dev/null +++ b/research/orthogonal-witness-precision/vendor/orthogonal/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-witness-precision/vendor/orthogonal/verify.py b/research/orthogonal-witness-precision/vendor/orthogonal/verify.py new file mode 100644 index 0000000000..10eb86e249 --- /dev/null +++ b/research/orthogonal-witness-precision/vendor/orthogonal/verify.py @@ -0,0 +1,346 @@ +"""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 mm(a, b): + return [[sum((x * y for x, y in zip(row, col)), Q(0)) + for col in zip(*b)] for row in a] + + +def determinant(matrix): + a = [row[:] for row in matrix] + value = Q(1) + for j in range(len(a)): + pivot = next((i for i in range(j, len(a)) if a[i][j]), None) + if pivot is None: + return Q(0) + if pivot != j: + a[j], a[pivot] = a[pivot], a[j] + value = -value + value *= a[j][j] + for i in range(j + 1, len(a)): + ratio = a[i][j] / a[j][j] + a[i] = [x - ratio * y for x, y in zip(a[i], a[j])] + return value + + +def dense_replay(p, w): + n, t = w["dimension"], Q(w["parameter"]) + matrices = {} + identity = [[Q(i == j) for j in range(n)] for i in range(n)] + for a in p["operators"]: + plus, minus = deepcopy(identity), deepcopy(identity) + for j, label in enumerate(w["word"]): + if label == a: + plus[j][j + 1], plus[j + 1][j] = t / 2, -t / 2 + minus[j][j + 1], minus[j + 1][j] = -t / 2, t / 2 + matrix = mm(dense_inverse(minus), plus) + inverse = dense_inverse(matrix) + 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"): + 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"]) + 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(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 + + +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["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 + 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"] == ["A"] and w["grid_index"] == count + 1, "must skip all grid roots") + for j in range(1, count + 1): + 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)] + 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"], "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(): + 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") + require(sum(x*x for x in action(band, vector, 1)) == 1, "exact Euclidean norm") + vector_checks += 1 + 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, "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"]}, + "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_ORTHOGONAL_INVERSE_CIRCUIT_WITNESS") + + +if __name__ == "__main__": + main() diff --git a/research/orthogonal-witness-precision/vendor/orthogonal/witness.py b/research/orthogonal-witness-precision/vendor/orthogonal/witness.py new file mode 100644 index 0000000000..5ee87c5942 --- /dev/null +++ b/research/orthogonal-witness-precision/vendor/orthogonal/witness.py @@ -0,0 +1,59 @@ +"""Construct an orthogonal 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, parameter_cap=Fraction(1, 4)): + if validate(program).characteristic: + 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") + word = coefficient["word"] + n = len(word) + 1 + degree = degree_bound(program, n) + for index in range(1, degree + 2): + parameter = parameter_cap * (degree + 2 - index) / (degree + 1) + difference = replay(program, word, parameter, coefficient["input"]) + if difference[coefficient["output"]][0]: + return { + "schema": "orthogonal-inverse-witness/v1", + "program_sha256": coefficient["program_sha256"], + "word": word, "dimension": n, + "input": coefficient["input"], "output": coefficient["output"], + "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], + } + 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("--parameter-cap", default="1/4") + args = parser.parse_args() + 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_ORTHOGONAL_INVERSE_WITNESS_PRODUCED") + + +if __name__ == "__main__": + main() From 26fe40cbca6972a0e392e9248a9cb8a84368530b Mon Sep 17 00:00:00 2001 From: Ali Romman <226877337+aliromman@users.noreply.github.com> Date: Fri, 23 Oct 2026 12:36:28 -0500 Subject: [PATCH 2/2] Prove separation and fund a dyadic detector for orthogonal witnesses --- .../orthogonal-witness-precision/PROOF.md | 193 ++++ .../orthogonal-witness-precision/README.md | 58 ++ .../orthogonal-witness-precision/RESULT.json | 929 ++++++++++++++++++ .../orthogonal-witness-precision/SOURCES.json | 174 ++++ .../orthogonal-witness-precision/TASK.json | 95 ++ .../VALIDATION.md | 36 + .../orthogonal-witness-precision/VERIFY.json | 34 + .../orthogonal-witness-precision/detector.py | 113 +++ .../orthogonal-witness-precision/verify.py | 130 +++ 9 files changed, 1762 insertions(+) create mode 100644 research/orthogonal-witness-precision/PROOF.md create mode 100644 research/orthogonal-witness-precision/README.md create mode 100644 research/orthogonal-witness-precision/RESULT.json create mode 100644 research/orthogonal-witness-precision/SOURCES.json create mode 100644 research/orthogonal-witness-precision/TASK.json create mode 100644 research/orthogonal-witness-precision/VALIDATION.md create mode 100644 research/orthogonal-witness-precision/VERIFY.json create mode 100644 research/orthogonal-witness-precision/detector.py create mode 100644 research/orthogonal-witness-precision/verify.py diff --git a/research/orthogonal-witness-precision/PROOF.md b/research/orthogonal-witness-precision/PROOF.md new file mode 100644 index 0000000000..36d4c06875 --- /dev/null +++ b/research/orthogonal-witness-precision/PROOF.md @@ -0,0 +1,193 @@ +# Exact separation and a funded dyadic endpoint detector + +Prepared by Ali Romman with substantial OpenAI Codex assistance. Apache-2.0. +This is a written proof with finite exact corroboration. + +## Contract and result + +Use the rational complete register grammar from +[PR #5262](https://github.com/CrocSwap/integer-mult-bounds/pull/5262): r +independent input roles, every role returned, old-value scalar assignments, +apply calls G_a^(+/-1), and queries dst += c G_a^(+/-1) src, including aliases. +Only inverses of named generators occur. Let q count all apply/query calls +in both programs, and let m count all instructions in both programs. + +Take any labelled skew path word of length d-1 and a reduced rational +parameter t=A/B with 00. Use the exact special-orthogonal Cayley +matrices O_a(t) of [PR #5315](https://github.com/CrocSwap/integer-mult-bounds/pull/5315). +Give one chosen input role e_(d-1), and give all other roles zero. Let f be +coordinate zero of any chosen output difference. This concrete input does +not change the universal grammar's independent-role contract. + +Let C be the product of the positive reduced denominators of **every** scalar +coefficient occurrence in both programs. Include query coefficients and every +term of a linear assignment, even repeated roles or zero coefficients. Then + + f != 0 implies |f| >= eta = 1/[C (3B)^(dq)]. (1) + +A dyadic implementation below computes fhat with |fhat-f|<=eta/4. Hence + + f=0 iff |fhat|<=eta/4, + f!=0 implies |fhat|>=3eta/4. + +The threshold eta/2 therefore decides this selected endpoint exactly. It +does not need an exact endpoint replay or coefficient certificate as its +decision oracle. A false universal program identity still needs the source +producer's distinguishing word/input/output, or another search for one. +A zero at one chosen tuple is not a universal equality certificate. + +## 1. Integer denominators + +For each path label a, write K_a for its skew adjacency matrix and + + M_a = 2B I - A K_a, P_a = 2B I + A K_a, + O_a = M_a^-1 P_a. + +M_a and P_a have integer entries. Each column has squared Euclidean norm at +most 4B^2+2A^2 <9B^2. Hadamard's determinant bound gives + + 1 <= D_a = det(M_a) <= (3B)^d. + +The determinant is positive: M_a is invertible on the real parameter line, +its determinant is continuous, and at A=0 it is (2B)^d>0. Also P_a=M_a^T, +so its determinant is the same D_a. The adjugate formula shows that every +entry of O_a and O_a^-1 is an integer divided by D_a. Cancellation can only +reduce a reduced denominator. + +Maintain one common integer denominator for all registers on one program +side. At a linear assignment multiply it by the product of the denominators +of that assignment's coefficients. At an apply multiply it by D_a. At a +query multiply it by D_a times the scalar denominator. The unchanged +registers and old destination can use this same denominator. Old source +values also have it before the assignment, including on alias. This proves +by induction that a common denominator for the two endpoint vectors divides + + C product_(all q occurrences) D_(label). + +The endpoint difference has the same divisibility property after the two +side denominators are multiplied. A nonzero numerator is a nonzero integer. +The displayed product is at most C(3B)^(dq), which proves (1). The actual +common denominator need not divide the larger numeric bound C(3B)^(dq); +only this inequality is used. + +For the source witness grid with cap t0=a/b and L=dq, its rational points +have reduced denominator B<=b(L+1). Thus a uniform separation bound over the +whole grid follows by replacing B in (1) with b(dq+1). No floating root +separation or generic numerical noncancellation premise is needed. + +## 2. Complete register gains + +Use the maximum absolute coordinate over the entire r-register bank. Every +entry of an orthogonal matrix has absolute value at most one, so its row +absolute sum is at most d. Assign each instruction the following two bounds: + +| Instruction | beta | gamma | +|---|---:|---:| +| linear dst = sum c_j src_j | max(1, sum abs(c_j)) | 0 | +| apply G_a or G_a^-1 | d | d | +| query dst += c G_a^(+/-1) src | 1+d abs(c) | d abs(c) | + +Beta bounds the exact map on the whole bank; beta>=1 also covers unchanged +roles. Gamma bounds the effect of rounding each operator entry by at most h. +Define G as the product of all beta values in both programs, and Gamma as +the largest gamma (zero for no calls). G>=1. + +Truncate each exact forward matrix entry toward zero to the h=2^-p grid. +Use the transpose of that integer table for its inverse call. Since exact +inverse equals transpose, this is the same entrywise truncation of the +actual inverse. Each stored entry still has absolute value at most one. +Read all instruction sources before writing the destination. Multiply and +sum exactly, keep scalar coefficients exact, then truncate each new data +coordinate once toward zero to the same grid. + +This operation does not increase the absolute value of a coordinate. By +induction each computed bank has norm at most the product of its previous +beta values, hence at most G. This bound includes arbitrary scalar gains, +all helper roles, and self-source queries. It does not assume that a rounded +map is linear or that its stored inverse undoes its stored forward map. + +Let E_i be the bank error on one program side after instruction i. The exact +map contributes at most beta_i E_(i-1). Entry quantization on the computed +input contributes at most gamma_i h G. The final data truncation adds at +most h. Thus + + E_i <= beta_i E_(i-1) + (gamma_i G+1)h. + +Every suffix product of beta values is at most G. Sum both program errors, +using their combined instruction count m. Every returned coordinate of the +endpoint difference therefore has error at most + + E = m G (Gamma G+1) h. (2) + +Choose an integer p>=0 with + + 2^p >= 4 max(1, m G (Gamma G+1)) C(3B)^(dq). + +Then E<=eta/4. This also covers an empty program pair, where m=0 and its +endpoint difference is exactly zero. Equations (1) and (2) prove the +threshold decision and the claimed separation between its two cases. + +## 3. Executable and arithmetic boundary + +`detector.py` uses no exact endpoint or Magnus producer. It takes the program, +word, parameter, input role and output role. It forms each rational Cayley +matrix from the retained tridiagonal basis action, quantizes the entries, +and replays both complete programs with integers. A query computes its old +sum before one final division. A linear assignment uses exact rational +scalar arithmetic before one truncation. Every dirty output is retained. + +For alphabet size s the code stores 2sd^2 matrix-entry slots. The dense +replay pays qd^2 integer matrix products and md coordinate truncations, +plus all linear/query scalar products and additions. Matrix formation, +source parsing, gain/denominator calculation, allocation and returned banks +are additional work. There is no claim that this dense numerical method is +faster than exact rational replay or an admitted native primitive. + +After the word is supplied, the required fractional precision satisfies + + p = O(log C + dq(1+log B) + log(m+1) + + log G + log(Gamma G+1)). + +This is polynomial in the explicit program/word lengths and scalar/parameter +binary input sizes. Exact scalar sums and products give polynomial-size +representations of C, G and Gamma. Integer path matrices have entry size +O(log B); their minors have O(d(1+log B+log d)) bits. The tridiagonal basis +solves use ratios of these minors and polynomially many exact operations. +The stored data have magnitude at most G, so their integers use at most +p+O(log G) bits. Dot products add at most O(log d) bits; exact scalar sums +use coefficient denominators whose product divides C. This bounds the +arithmetic bit sizes in the supplied detector polynomially as well. +This statement is for this detector after a word is given. It is not a new +bit-complexity analysis of the upstream coefficient producer. + +## Evidence and limits + +The verifier uses the exact tridiagonal endpoint and a separately transcribed +dense Gaussian-inverse interpreter only as test oracles. It compares every +returned coordinate with (2), not just the threshold verdict. Equal programs, +exact cancelling grid points and failed identities are separate cases. Tiny +parameters, a scalar discrepancy 2^-80, scalar gains 2^100, dirty returns, +aliased queries and a delayed inverse series test different terms in the +bound. Corrupted code tests remove scalar denominators, parameter denominator +size, cumulative gains or the inverse transpose. + +The guard is deliberately conservative. It is not a least precision, an +IEEE floating-point guarantee, or a proof that an unspecified numerical +library respects these rounding rules. It adds no finite native alphabet, +Clifford relation, physical tape tariff, supplier admission or complete kappa +improvement. The selected frontier and inherited native/analytic obligations +remain unchanged. No independent human or proof-kernel review is claimed. + +## Attribution + +Ali Romman's [PR #5315](https://github.com/CrocSwap/integer-mult-bounds/pull/5315), +consumed at `9bebc267c4608e51fcc94a543b8e0d66077cdfbb`, supplies the rational +orthogonal realization, literal action and tests retained in `vendor/`. +Krzysztof Wójt (@krzysztofwojt) supplies the inverse compiler and shortest-word +proof in [PR #5262](https://github.com/CrocSwap/integer-mult-bounds/pull/5262). +The retained notices credit zxv's +[PR #5235](https://github.com/CrocSwap/integer-mult-bounds/pull/5235), the +dirty-echo/tensor/phase lineage and classical rational-series methods. +Cayley transforms, Hadamard's determinant inequality and forward-error +propagation are classical. This result binds their explicit constants to +this complete register grammar and one literal dyadic consumer. diff --git a/research/orthogonal-witness-precision/README.md b/research/orthogonal-witness-precision/README.md new file mode 100644 index 0000000000..0bd504969b --- /dev/null +++ b/research/orthogonal-witness-precision/README.md @@ -0,0 +1,58 @@ +# A funded numerical detector for orthogonal inverse witnesses + +Exact nonzero rational witnesses can be small. This package proves a lower +bound for their magnitude and gives a complete dyadic replay that detects +the selected endpoint without using its exact value as an oracle. + +For a path of dimension d, q named calls, rational parameter A/B, and product +C of all scalar denominators, every nonzero selected discrepancy has magnitude +at least `1/[C(3B)^(dq)]`. The [proof](PROOF.md) joins this separation to +all matrix-entry quantization, data truncation and scalar amplification. +The detector keeps every role and reads old values on aliased queries. + +`detect(program, word, parameter, input_index, output_index)` returns the +selected zero/nonzero decision, the dyadic endpoint difference, its proved +error and precision, and the full matrix-product/rounding counts. A zero +selected endpoint is not a universal identity certificate. The retained +inverse producer can supply a distinguishing word for a false identity. + +Run with Python 3.12 and its standard library: + +```sh +python3.12 -B scripts/research_package.py --package research/orthogonal-witness-precision +``` + +Both registered isolated, warning-strict modes end with +`PASS_ORTHOGONAL_WITNESS_PRECISION`. Normal runs write no package files. +`verify.py --write-result` regenerates RESULT.json. `--small` keeps the +boundary controls and a smaller random/stress set. + +The finite check covers equal and unequal complete programs, cancelling grid +points, tiny parameters and scalar discrepancies, large scalar gains, aliased +queries, dirty returns and an inverse-series stress family. Exact rational +replay and a separate dense inverse interpreter are test oracles only. The +production detector imports neither the exact endpoint replay nor the +coefficient producer. + +This is a sufficient precision and a specified integer/dyadic computation. +It does not claim optimal guards, IEEE behavior, a native Clifford witness, +a tape implementation, a faster identity test or a complete kappa change. +The source coefficient-generation cost and dense matrix products are paid. +The selected frontier remains unchanged. + +Prepared by Ali Romman with substantial OpenAI Codex assistance; Apache-2.0. +[PR #5315](https://github.com/CrocSwap/integer-mult-bounds/pull/5315) supplies +the orthogonal construction. Krzysztof Wójt's +[PR #5262](https://github.com/CrocSwap/integer-mult-bounds/pull/5262) supplies +the inverse compiler. Retained source notices preserve zxv and the earlier +rational-series/dirty-echo/tensor/phase credit. `SOURCES.json` pins the exact +bytes retained in branch history. Classical determinant and error bounds +retain their credit; no global literature priority is claimed. + +## Open next questions + +For a fixed native-compatible witness, can sparse or exact factor application +reduce this dense replay and its conservative scalar-gain guard? First pin +all native operator relations and the caller's complete error and cost +contract. This package proves finite detectability; it does not supply that +binding or an optimized physical implementation. diff --git a/research/orthogonal-witness-precision/RESULT.json b/research/orthogonal-witness-precision/RESULT.json new file mode 100644 index 0000000000..bab7c61ebd --- /dev/null +++ b/research/orthogonal-witness-precision/RESULT.json @@ -0,0 +1,929 @@ +{ + "status": "PASS", + "cases": [ + { + "label": "commutator", + "nonzero": true, + "bits": 62, + "separation_denominator_bits": 44, + "matrix_products": 36, + "data_roundings": 12, + "dimension": 3 + }, + { + "label": "tiny-parameter", + "nonzero": true, + "bits": 998, + "separation_denominator_bits": 980, + "matrix_products": 36, + "data_roundings": 12, + "dimension": 3 + }, + { + "label": "equal-dirty-sandwich", + "nonzero": false, + "bits": 179, + "separation_denominator_bits": 130, + "matrix_products": 144, + "data_roundings": 44, + "dimension": 4 + }, + { + "label": "deleted-sandwich-0", + "nonzero": true, + "bits": 88, + "separation_denominator_bits": 58, + "matrix_products": 32, + "data_roundings": 20, + "dimension": 2 + }, + { + "label": "deleted-sandwich-1", + "nonzero": true, + "bits": 46, + "separation_denominator_bits": 33, + "matrix_products": 9, + "data_roundings": 10, + "dimension": 1 + }, + { + "label": "deleted-sandwich-2", + "nonzero": true, + "bits": 88, + "separation_denominator_bits": 58, + "matrix_products": 32, + "data_roundings": 20, + "dimension": 2 + }, + { + "label": "deleted-sandwich-3", + "nonzero": true, + "bits": 43, + "separation_denominator_bits": 29, + "matrix_products": 8, + "data_roundings": 10, + "dimension": 1 + }, + { + "label": "deleted-sandwich-4", + "nonzero": true, + "bits": 88, + "separation_denominator_bits": 58, + "matrix_products": 32, + "data_roundings": 20, + "dimension": 2 + }, + { + "label": "deleted-sandwich-5", + "nonzero": true, + "bits": 46, + "separation_denominator_bits": 33, + "matrix_products": 9, + "data_roundings": 10, + "dimension": 1 + }, + { + "label": "deleted-sandwich-6", + "nonzero": true, + "bits": 88, + "separation_denominator_bits": 58, + "matrix_products": 32, + "data_roundings": 20, + "dimension": 2 + }, + { + "label": "deleted-sandwich-7", + "nonzero": true, + "bits": 43, + "separation_denominator_bits": 29, + "matrix_products": 8, + "data_roundings": 10, + "dimension": 1 + }, + { + "label": "tiny-scalar-discrepancy", + "nonzero": true, + "bits": 83, + "separation_denominator_bits": 81, + "matrix_products": 0, + "data_roundings": 1, + "dimension": 1 + }, + { + "label": "large-scalar-gain", + "nonzero": true, + "bits": 414, + "separation_denominator_bits": 8, + "matrix_products": 4, + "data_roundings": 6, + "dimension": 2 + }, + { + "label": "rational-aliased-query", + "nonzero": true, + "bits": 10, + "separation_denominator_bits": 7, + "matrix_products": 1, + "data_roundings": 1, + "dimension": 1 + }, + { + "label": "dirty-return", + "nonzero": true, + "bits": 13, + "separation_denominator_bits": 8, + "matrix_products": 4, + "data_roundings": 2, + "dimension": 2 + }, + { + "label": "selected-grid-1", + "nonzero": true, + "bits": 57, + "separation_denominator_bits": 39, + "matrix_products": 12, + "data_roundings": 20, + "dimension": 2 + }, + { + "label": "cancelled-grid-1", + "nonzero": false, + "bits": 47, + "separation_denominator_bits": 28, + "matrix_products": 12, + "data_roundings": 20, + "dimension": 2 + }, + { + "label": "selected-grid-2", + "nonzero": true, + "bits": 115, + "separation_denominator_bits": 88, + "matrix_products": 20, + "data_roundings": 28, + "dimension": 2 + }, + { + "label": "cancelled-grid-2", + "nonzero": false, + "bits": 81, + "separation_denominator_bits": 53, + "matrix_products": 20, + "data_roundings": 28, + "dimension": 2 + }, + { + "label": "selected-grid-4", + "nonzero": true, + "bits": 228, + "separation_denominator_bits": 183, + "matrix_products": 36, + "data_roundings": 44, + "dimension": 2 + }, + { + "label": "cancelled-grid-4", + "nonzero": false, + "bits": 151, + "separation_denominator_bits": 107, + "matrix_products": 36, + "data_roundings": 44, + "dimension": 2 + }, + { + "label": "random-equal-0", + "nonzero": false, + "bits": 175, + "separation_denominator_bits": 133, + "matrix_products": 128, + "data_roundings": 64, + "dimension": 4 + }, + { + "label": "random-1", + "nonzero": true, + "bits": 43, + "separation_denominator_bits": 32, + "matrix_products": 6, + "data_roundings": 8, + "dimension": 1 + }, + { + "label": "random-2", + "nonzero": true, + "bits": 46, + "separation_denominator_bits": 34, + "matrix_products": 9, + "data_roundings": 10, + "dimension": 1 + }, + { + "label": "random-3", + "nonzero": true, + "bits": 46, + "separation_denominator_bits": 33, + "matrix_products": 8, + "data_roundings": 10, + "dimension": 1 + }, + { + "label": "random-equal-4", + "nonzero": false, + "bits": 268, + "separation_denominator_bits": 212, + "matrix_products": 224, + "data_roundings": 64, + "dimension": 4 + }, + { + "label": "random-5", + "nonzero": true, + "bits": 33, + "separation_denominator_bits": 19, + "matrix_products": 4, + "data_roundings": 7, + "dimension": 1 + }, + { + "label": "random-6", + "nonzero": true, + "bits": 17, + "separation_denominator_bits": 9, + "matrix_products": 1, + "data_roundings": 4, + "dimension": 1 + }, + { + "label": "random-7", + "nonzero": true, + "bits": 34, + "separation_denominator_bits": 23, + "matrix_products": 5, + "data_roundings": 8, + "dimension": 1 + }, + { + "label": "random-equal-8", + "nonzero": false, + "bits": 163, + "separation_denominator_bits": 126, + "matrix_products": 128, + "data_roundings": 40, + "dimension": 4 + }, + { + "label": "random-9", + "nonzero": true, + "bits": 39, + "separation_denominator_bits": 23, + "matrix_products": 5, + "data_roundings": 8, + "dimension": 1 + }, + { + "label": "random-10", + "nonzero": true, + "bits": 74, + "separation_denominator_bits": 54, + "matrix_products": 12, + "data_roundings": 14, + "dimension": 1 + }, + { + "label": "random-11", + "nonzero": true, + "bits": 60, + "separation_denominator_bits": 47, + "matrix_products": 10, + "data_roundings": 12, + "dimension": 1 + }, + { + "label": "random-equal-12", + "nonzero": false, + "bits": 265, + "separation_denominator_bits": 206, + "matrix_products": 224, + "data_roundings": 56, + "dimension": 4 + }, + { + "label": "random-13", + "nonzero": true, + "bits": 54, + "separation_denominator_bits": 44, + "matrix_products": 10, + "data_roundings": 10, + "dimension": 1 + }, + { + "label": "random-14", + "nonzero": true, + "bits": 25, + "separation_denominator_bits": 17, + "matrix_products": 4, + "data_roundings": 5, + "dimension": 1 + }, + { + "label": "random-15", + "nonzero": true, + "bits": 67, + "separation_denominator_bits": 52, + "matrix_products": 10, + "data_roundings": 12, + "dimension": 1 + }, + { + "label": "random-equal-16", + "nonzero": false, + "bits": 123, + "separation_denominator_bits": 92, + "matrix_products": 96, + "data_roundings": 40, + "dimension": 4 + }, + { + "label": "random-17", + "nonzero": true, + "bits": 37, + "separation_denominator_bits": 21, + "matrix_products": 4, + "data_roundings": 11, + "dimension": 1 + }, + { + "label": "random-18", + "nonzero": true, + "bits": 60, + "separation_denominator_bits": 42, + "matrix_products": 8, + "data_roundings": 13, + "dimension": 1 + }, + { + "label": "random-19", + "nonzero": true, + "bits": 35, + "separation_denominator_bits": 27, + "matrix_products": 7, + "data_roundings": 8, + "dimension": 1 + }, + { + "label": "random-equal-20", + "nonzero": false, + "bits": 52, + "separation_denominator_bits": 31, + "matrix_products": 32, + "data_roundings": 24, + "dimension": 4 + }, + { + "label": "random-21", + "nonzero": true, + "bits": 28, + "separation_denominator_bits": 14, + "matrix_products": 2, + "data_roundings": 7, + "dimension": 1 + }, + { + "label": "random-22", + "nonzero": true, + "bits": 52, + "separation_denominator_bits": 36, + "matrix_products": 6, + "data_roundings": 13, + "dimension": 1 + }, + { + "label": "random-23", + "nonzero": true, + "bits": 49, + "separation_denominator_bits": 29, + "matrix_products": 5, + "data_roundings": 10, + "dimension": 1 + }, + { + "label": "random-equal-24", + "nonzero": false, + "bits": 202, + "separation_denominator_bits": 162, + "matrix_products": 160, + "data_roundings": 48, + "dimension": 4 + }, + { + "label": "random-25", + "nonzero": true, + "bits": 46, + "separation_denominator_bits": 29, + "matrix_products": 6, + "data_roundings": 11, + "dimension": 1 + }, + { + "label": "random-26", + "nonzero": true, + "bits": 40, + "separation_denominator_bits": 29, + "matrix_products": 4, + "data_roundings": 8, + "dimension": 1 + }, + { + "label": "random-27", + "nonzero": true, + "bits": 39, + "separation_denominator_bits": 28, + "matrix_products": 5, + "data_roundings": 9, + "dimension": 1 + }, + { + "label": "random-equal-28", + "nonzero": false, + "bits": 214, + "separation_denominator_bits": 148, + "matrix_products": 160, + "data_roundings": 56, + "dimension": 4 + }, + { + "label": "random-29", + "nonzero": true, + "bits": 45, + "separation_denominator_bits": 27, + "matrix_products": 6, + "data_roundings": 8, + "dimension": 1 + }, + { + "label": "random-30", + "nonzero": true, + "bits": 61, + "separation_denominator_bits": 43, + "matrix_products": 9, + "data_roundings": 13, + "dimension": 1 + }, + { + "label": "random-31", + "nonzero": true, + "bits": 61, + "separation_denominator_bits": 40, + "matrix_products": 8, + "data_roundings": 13, + "dimension": 1 + }, + { + "label": "random-equal-32", + "nonzero": false, + "bits": 162, + "separation_denominator_bits": 125, + "matrix_products": 128, + "data_roundings": 40, + "dimension": 4 + }, + { + "label": "random-33", + "nonzero": true, + "bits": 48, + "separation_denominator_bits": 33, + "matrix_products": 4, + "data_roundings": 11, + "dimension": 1 + }, + { + "label": "random-34", + "nonzero": true, + "bits": 32, + "separation_denominator_bits": 22, + "matrix_products": 4, + "data_roundings": 7, + "dimension": 1 + }, + { + "label": "random-35", + "nonzero": true, + "bits": 48, + "separation_denominator_bits": 36, + "matrix_products": 8, + "data_roundings": 13, + "dimension": 1 + }, + { + "label": "random-equal-36", + "nonzero": false, + "bits": 151, + "separation_denominator_bits": 121, + "matrix_products": 128, + "data_roundings": 32, + "dimension": 4 + }, + { + "label": "random-37", + "nonzero": true, + "bits": 43, + "separation_denominator_bits": 31, + "matrix_products": 6, + "data_roundings": 10, + "dimension": 1 + }, + { + "label": "random-38", + "nonzero": true, + "bits": 39, + "separation_denominator_bits": 25, + "matrix_products": 5, + "data_roundings": 9, + "dimension": 1 + }, + { + "label": "random-39", + "nonzero": true, + "bits": 47, + "separation_denominator_bits": 33, + "matrix_products": 7, + "data_roundings": 10, + "dimension": 1 + }, + { + "label": "random-equal-40", + "nonzero": false, + "bits": 129, + "separation_denominator_bits": 98, + "matrix_products": 96, + "data_roundings": 32, + "dimension": 4 + }, + { + "label": "random-41", + "nonzero": true, + "bits": 38, + "separation_denominator_bits": 27, + "matrix_products": 6, + "data_roundings": 11, + "dimension": 1 + }, + { + "label": "random-42", + "nonzero": true, + "bits": 70, + "separation_denominator_bits": 49, + "matrix_products": 8, + "data_roundings": 13, + "dimension": 1 + }, + { + "label": "random-43", + "nonzero": true, + "bits": 39, + "separation_denominator_bits": 27, + "matrix_products": 5, + "data_roundings": 7, + "dimension": 1 + }, + { + "label": "random-equal-44", + "nonzero": false, + "bits": 85, + "separation_denominator_bits": 60, + "matrix_products": 64, + "data_roundings": 24, + "dimension": 4 + }, + { + "label": "random-45", + "nonzero": true, + "bits": 39, + "separation_denominator_bits": 24, + "matrix_products": 5, + "data_roundings": 9, + "dimension": 1 + }, + { + "label": "random-46", + "nonzero": true, + "bits": 26, + "separation_denominator_bits": 15, + "matrix_products": 3, + "data_roundings": 5, + "dimension": 1 + }, + { + "label": "random-47", + "nonzero": true, + "bits": 53, + "separation_denominator_bits": 33, + "matrix_products": 6, + "data_roundings": 10, + "dimension": 1 + }, + { + "label": "random-equal-48", + "nonzero": false, + "bits": 134, + "separation_denominator_bits": 95, + "matrix_products": 96, + "data_roundings": 64, + "dimension": 4 + }, + { + "label": "random-49", + "nonzero": true, + "bits": 39, + "separation_denominator_bits": 24, + "matrix_products": 4, + "data_roundings": 6, + "dimension": 1 + }, + { + "label": "random-50", + "nonzero": true, + "bits": 58, + "separation_denominator_bits": 35, + "matrix_products": 7, + "data_roundings": 11, + "dimension": 1 + }, + { + "label": "random-51", + "nonzero": true, + "bits": 43, + "separation_denominator_bits": 30, + "matrix_products": 6, + "data_roundings": 8, + "dimension": 1 + }, + { + "label": "random-equal-52", + "nonzero": false, + "bits": 208, + "separation_denominator_bits": 156, + "matrix_products": 160, + "data_roundings": 56, + "dimension": 4 + }, + { + "label": "random-53", + "nonzero": true, + "bits": 31, + "separation_denominator_bits": 20, + "matrix_products": 3, + "data_roundings": 7, + "dimension": 1 + }, + { + "label": "random-54", + "nonzero": true, + "bits": 58, + "separation_denominator_bits": 47, + "matrix_products": 11, + "data_roundings": 13, + "dimension": 1 + }, + { + "label": "random-55", + "nonzero": true, + "bits": 37, + "separation_denominator_bits": 24, + "matrix_products": 5, + "data_roundings": 9, + "dimension": 1 + }, + { + "label": "random-equal-56", + "nonzero": false, + "bits": 204, + "separation_denominator_bits": 161, + "matrix_products": 160, + "data_roundings": 56, + "dimension": 4 + }, + { + "label": "random-57", + "nonzero": true, + "bits": 39, + "separation_denominator_bits": 27, + "matrix_products": 5, + "data_roundings": 7, + "dimension": 1 + }, + { + "label": "random-58", + "nonzero": true, + "bits": 82, + "separation_denominator_bits": 68, + "matrix_products": 13, + "data_roundings": 14, + "dimension": 1 + }, + { + "label": "random-59", + "nonzero": true, + "bits": 39, + "separation_denominator_bits": 27, + "matrix_products": 5, + "data_roundings": 6, + "dimension": 1 + }, + { + "label": "random-equal-60", + "nonzero": false, + "bits": 96, + "separation_denominator_bits": 68, + "matrix_products": 64, + "data_roundings": 40, + "dimension": 4 + }, + { + "label": "random-61", + "nonzero": true, + "bits": 17, + "separation_denominator_bits": 9, + "matrix_products": 2, + "data_roundings": 5, + "dimension": 1 + }, + { + "label": "random-62", + "nonzero": true, + "bits": 47, + "separation_denominator_bits": 36, + "matrix_products": 7, + "data_roundings": 11, + "dimension": 1 + }, + { + "label": "random-63", + "nonzero": true, + "bits": 46, + "separation_denominator_bits": 35, + "matrix_products": 8, + "data_roundings": 10, + "dimension": 1 + }, + { + "label": "random-equal-64", + "nonzero": false, + "bits": 264, + "separation_denominator_bits": 209, + "matrix_products": 224, + "data_roundings": 64, + "dimension": 4 + }, + { + "label": "random-65", + "nonzero": true, + "bits": 36, + "separation_denominator_bits": 22, + "matrix_products": 5, + "data_roundings": 6, + "dimension": 1 + }, + { + "label": "random-66", + "nonzero": true, + "bits": 48, + "separation_denominator_bits": 33, + "matrix_products": 8, + "data_roundings": 10, + "dimension": 1 + }, + { + "label": "random-67", + "nonzero": true, + "bits": 33, + "separation_denominator_bits": 24, + "matrix_products": 6, + "data_roundings": 7, + "dimension": 1 + }, + { + "label": "random-equal-68", + "nonzero": false, + "bits": 161, + "separation_denominator_bits": 115, + "matrix_products": 128, + "data_roundings": 56, + "dimension": 4 + }, + { + "label": "random-69", + "nonzero": true, + "bits": 59, + "separation_denominator_bits": 47, + "matrix_products": 10, + "data_roundings": 11, + "dimension": 1 + }, + { + "label": "random-70", + "nonzero": true, + "bits": 34, + "separation_denominator_bits": 24, + "matrix_products": 3, + "data_roundings": 7, + "dimension": 1 + }, + { + "label": "random-71", + "nonzero": true, + "bits": 32, + "separation_denominator_bits": 25, + "matrix_products": 5, + "data_roundings": 6, + "dimension": 1 + }, + { + "label": "random-equal-72", + "nonzero": false, + "bits": 86, + "separation_denominator_bits": 62, + "matrix_products": 64, + "data_roundings": 32, + "dimension": 4 + }, + { + "label": "random-73", + "nonzero": true, + "bits": 29, + "separation_denominator_bits": 20, + "matrix_products": 4, + "data_roundings": 6, + "dimension": 1 + }, + { + "label": "random-74", + "nonzero": true, + "bits": 43, + "separation_denominator_bits": 32, + "matrix_products": 6, + "data_roundings": 10, + "dimension": 1 + }, + { + "label": "random-75", + "nonzero": true, + "bits": 50, + "separation_denominator_bits": 37, + "matrix_products": 7, + "data_roundings": 11, + "dimension": 1 + }, + { + "label": "random-equal-76", + "nonzero": false, + "bits": 154, + "separation_denominator_bits": 125, + "matrix_products": 128, + "data_roundings": 48, + "dimension": 4 + }, + { + "label": "random-77", + "nonzero": true, + "bits": 50, + "separation_denominator_bits": 37, + "matrix_products": 9, + "data_roundings": 11, + "dimension": 1 + }, + { + "label": "random-78", + "nonzero": true, + "bits": 66, + "separation_denominator_bits": 44, + "matrix_products": 8, + "data_roundings": 12, + "dimension": 1 + }, + { + "label": "random-79", + "nonzero": true, + "bits": 46, + "separation_denominator_bits": 33, + "matrix_products": 6, + "data_roundings": 10, + "dimension": 1 + }, + { + "label": "inverse-series-stress", + "nonzero": true, + "bits": 2262, + "separation_denominator_bits": 1951, + "matrix_products": 9248, + "data_roundings": 1139, + "dimension": 17 + } + ], + "zero": 24, + "nonzero": 78, + "rejecting_controls": 7, + "maximum_fractional_bits": 2262, + "stress_lowest_degree_words": 65536, + "digest": "d780ab6579fa44a68cf079e3900438dac309f5ee020778191f5aef645c3b8314" +} diff --git a/research/orthogonal-witness-precision/SOURCES.json b/research/orthogonal-witness-precision/SOURCES.json new file mode 100644 index 0000000000..57e001b0ed --- /dev/null +++ b/research/orthogonal-witness-precision/SOURCES.json @@ -0,0 +1,174 @@ +{ + "schema_version": 1, + "base_commit": "ff3cc58e370d0f678e529246f8c73e8094e18fcf", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "c35482cd9035843b15a634cc8276a7e1e40e8395", + "sha256": "6fe0a099b89aa2aed796a13c3a21dafc63f3388ebf397464e44e0451893b9375" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "f126dd2e2dad2b669e75d1d0d0bd05c600725602", + "sha256": "f7a48bfa2659b88378282a8eee7d9fe52cdf505594124c4d1686b58510fffd72" + }, + { + "path": "research/orthogonal-witness-precision/vendor/orthogonal/PROOF.md", + "usage": "provenance", + "pin": "head:f736ecedbacfa9a86b9082d5387af702f643b6dd:research/orthogonal-witness-precision/vendor/orthogonal/PROOF.md", + "git_blob": "aeaae8bd63c8f7ed2ab1cc9971e2f95bf7ee9a74", + "sha256": "a0a581c0505a1311cf95af5077f634c799075c619717d5e6a726a13335885cec", + "upstream": { + "commit": "9bebc267c4608e51fcc94a543b8e0d66077cdfbb", + "path": "research/orthogonal-inverse-witness/PROOF.md", + "url": "https://github.com/aliromman/integer-mult-bounds/blob/9bebc267c4608e51fcc94a543b8e0d66077cdfbb/research/orthogonal-inverse-witness/PROOF.md" + } + }, + { + "path": "research/orthogonal-witness-precision/vendor/orthogonal/README.md", + "usage": "provenance", + "pin": "head:f736ecedbacfa9a86b9082d5387af702f643b6dd:research/orthogonal-witness-precision/vendor/orthogonal/README.md", + "git_blob": "a77fd2cf0d2953e64893e254e7d6ba5defd58bf0", + "sha256": "a1f9fafcf3f33ee7fbd833bbdcd9308f9e44b0f65d419201864e142473a5609a", + "upstream": { + "commit": "9bebc267c4608e51fcc94a543b8e0d66077cdfbb", + "path": "research/orthogonal-inverse-witness/README.md", + "url": "https://github.com/aliromman/integer-mult-bounds/blob/9bebc267c4608e51fcc94a543b8e0d66077cdfbb/research/orthogonal-inverse-witness/README.md" + } + }, + { + "path": "research/orthogonal-witness-precision/vendor/orthogonal/check_witness.py", + "usage": "provenance", + "pin": "head:f736ecedbacfa9a86b9082d5387af702f643b6dd:research/orthogonal-witness-precision/vendor/orthogonal/check_witness.py", + "git_blob": "ce99710ececee979c8a58e87bea13896c48d340e", + "sha256": "234cab3358e95098ac452f57dd26ad6ed18f3c403e04f07bd62b06fa466d6f1c", + "upstream": { + "commit": "9bebc267c4608e51fcc94a543b8e0d66077cdfbb", + "path": "research/orthogonal-inverse-witness/check_witness.py", + "url": "https://github.com/aliromman/integer-mult-bounds/blob/9bebc267c4608e51fcc94a543b8e0d66077cdfbb/research/orthogonal-inverse-witness/check_witness.py" + } + }, + { + "path": "research/orthogonal-witness-precision/vendor/orthogonal/literal.py", + "usage": "provenance", + "pin": "head:f736ecedbacfa9a86b9082d5387af702f643b6dd:research/orthogonal-witness-precision/vendor/orthogonal/literal.py", + "git_blob": "b8ac1a86c4979749f70b13ecd0f8ae7105a717b1", + "sha256": "19b2fc1fb500fa7c5466868862c0d64c3782177ee83bf05fbcb302129910a758", + "upstream": { + "commit": "9bebc267c4608e51fcc94a543b8e0d66077cdfbb", + "path": "research/orthogonal-inverse-witness/literal.py", + "url": "https://github.com/aliromman/integer-mult-bounds/blob/9bebc267c4608e51fcc94a543b8e0d66077cdfbb/research/orthogonal-inverse-witness/literal.py" + } + }, + { + "path": "research/orthogonal-witness-precision/vendor/orthogonal/vendor/UPSTREAM-PROOF.md", + "usage": "provenance", + "pin": "head:f736ecedbacfa9a86b9082d5387af702f643b6dd:research/orthogonal-witness-precision/vendor/orthogonal/vendor/UPSTREAM-PROOF.md", + "git_blob": "d2433c24ca46a1cf4af481f6ae9b281991cdafac", + "sha256": "de0820379f76fb4ab680c6401c852cc9ea127e447de11ca93a1453471d858f11", + "upstream": { + "commit": "9bebc267c4608e51fcc94a543b8e0d66077cdfbb", + "path": "research/orthogonal-inverse-witness/vendor/UPSTREAM-PROOF.md", + "url": "https://github.com/aliromman/integer-mult-bounds/blob/9bebc267c4608e51fcc94a543b8e0d66077cdfbb/research/orthogonal-inverse-witness/vendor/UPSTREAM-PROOF.md" + } + }, + { + "path": "research/orthogonal-witness-precision/vendor/orthogonal/vendor/UPSTREAM-README.md", + "usage": "provenance", + "pin": "head:f736ecedbacfa9a86b9082d5387af702f643b6dd:research/orthogonal-witness-precision/vendor/orthogonal/vendor/UPSTREAM-README.md", + "git_blob": "1f895da66011f6ae59970cc0331b2fa00840568d", + "sha256": "e43549a712b8aab26b904b4da140b2924f7fee82407c5cdbe362303802456184", + "upstream": { + "commit": "9bebc267c4608e51fcc94a543b8e0d66077cdfbb", + "path": "research/orthogonal-inverse-witness/vendor/UPSTREAM-README.md", + "url": "https://github.com/aliromman/integer-mult-bounds/blob/9bebc267c4608e51fcc94a543b8e0d66077cdfbb/research/orthogonal-inverse-witness/vendor/UPSTREAM-README.md" + } + }, + { + "path": "research/orthogonal-witness-precision/vendor/orthogonal/vendor/algebra.py", + "usage": "provenance", + "pin": "head:f736ecedbacfa9a86b9082d5387af702f643b6dd:research/orthogonal-witness-precision/vendor/orthogonal/vendor/algebra.py", + "git_blob": "a9e9c8d6f19ad8bcec56bd18b59cf6490e22caa2", + "sha256": "684679714e53ed02214c7c060743abf5726ccb8637e35fabe92c8b25bb4d9dc9", + "upstream": { + "commit": "9bebc267c4608e51fcc94a543b8e0d66077cdfbb", + "path": "research/orthogonal-inverse-witness/vendor/algebra.py", + "url": "https://github.com/aliromman/integer-mult-bounds/blob/9bebc267c4608e51fcc94a543b8e0d66077cdfbb/research/orthogonal-inverse-witness/vendor/algebra.py" + } + }, + { + "path": "research/orthogonal-witness-precision/vendor/orthogonal/vendor/dirty-sandwich.json", + "usage": "provenance", + "pin": "head:f736ecedbacfa9a86b9082d5387af702f643b6dd:research/orthogonal-witness-precision/vendor/orthogonal/vendor/dirty-sandwich.json", + "git_blob": "c1254508e7b1ad79c6daf2a98cf1803b102d2078", + "sha256": "b6db99af39224b8321cf2ea1fae2f0205db66ccce9719be6a8378d209db80ede", + "upstream": { + "commit": "9bebc267c4608e51fcc94a543b8e0d66077cdfbb", + "path": "research/orthogonal-inverse-witness/vendor/dirty-sandwich.json", + "url": "https://github.com/aliromman/integer-mult-bounds/blob/9bebc267c4608e51fcc94a543b8e0d66077cdfbb/research/orthogonal-inverse-witness/vendor/dirty-sandwich.json" + } + }, + { + "path": "research/orthogonal-witness-precision/vendor/orthogonal/vendor/fields.py", + "usage": "provenance", + "pin": "head:f736ecedbacfa9a86b9082d5387af702f643b6dd:research/orthogonal-witness-precision/vendor/orthogonal/vendor/fields.py", + "git_blob": "2442625a155e2bcba532981e2aa1cca0cd997881", + "sha256": "831bea6e3b30a44c23a6d344246c1fd12359cdbb5f7975c45dab7b5e2520b942", + "upstream": { + "commit": "9bebc267c4608e51fcc94a543b8e0d66077cdfbb", + "path": "research/orthogonal-inverse-witness/vendor/fields.py", + "url": "https://github.com/aliromman/integer-mult-bounds/blob/9bebc267c4608e51fcc94a543b8e0d66077cdfbb/research/orthogonal-inverse-witness/vendor/fields.py" + } + }, + { + "path": "research/orthogonal-witness-precision/vendor/orthogonal/vendor/syntax.py", + "usage": "provenance", + "pin": "head:f736ecedbacfa9a86b9082d5387af702f643b6dd:research/orthogonal-witness-precision/vendor/orthogonal/vendor/syntax.py", + "git_blob": "5a91dd192181b34dd098fcc62a5015e8623aa1ec", + "sha256": "4c55af1b7d1daabbd1bb6d33768576afcf72bbb3903a6d26087d9527a289cb2d", + "upstream": { + "commit": "9bebc267c4608e51fcc94a543b8e0d66077cdfbb", + "path": "research/orthogonal-inverse-witness/vendor/syntax.py", + "url": "https://github.com/aliromman/integer-mult-bounds/blob/9bebc267c4608e51fcc94a543b8e0d66077cdfbb/research/orthogonal-inverse-witness/vendor/syntax.py" + } + }, + { + "path": "research/orthogonal-witness-precision/vendor/orthogonal/vendor/wrong-order.json", + "usage": "provenance", + "pin": "head:f736ecedbacfa9a86b9082d5387af702f643b6dd:research/orthogonal-witness-precision/vendor/orthogonal/vendor/wrong-order.json", + "git_blob": "3beca6f4b18cb64d7189d3346ebcecc0f8643d01", + "sha256": "e7cb08cb0d4186e9086e7d041db6d49e3fe3a54b2722ded6c08bf919c66ede1f", + "upstream": { + "commit": "9bebc267c4608e51fcc94a543b8e0d66077cdfbb", + "path": "research/orthogonal-inverse-witness/vendor/wrong-order.json", + "url": "https://github.com/aliromman/integer-mult-bounds/blob/9bebc267c4608e51fcc94a543b8e0d66077cdfbb/research/orthogonal-inverse-witness/vendor/wrong-order.json" + } + }, + { + "path": "research/orthogonal-witness-precision/vendor/orthogonal/verify.py", + "usage": "provenance", + "pin": "head:f736ecedbacfa9a86b9082d5387af702f643b6dd:research/orthogonal-witness-precision/vendor/orthogonal/verify.py", + "git_blob": "10eb86e249d2148fb27c49fdf62e784c278f50d4", + "sha256": "b56179cae3dbbd2c869acd2f027c5bc6a255a5cf8d7b4a8ca6873d33f2d78c76", + "upstream": { + "commit": "9bebc267c4608e51fcc94a543b8e0d66077cdfbb", + "path": "research/orthogonal-inverse-witness/verify.py", + "url": "https://github.com/aliromman/integer-mult-bounds/blob/9bebc267c4608e51fcc94a543b8e0d66077cdfbb/research/orthogonal-inverse-witness/verify.py" + } + }, + { + "path": "research/orthogonal-witness-precision/vendor/orthogonal/witness.py", + "usage": "provenance", + "pin": "head:f736ecedbacfa9a86b9082d5387af702f643b6dd:research/orthogonal-witness-precision/vendor/orthogonal/witness.py", + "git_blob": "5ee87c59425099da12ba948a60721d68735038a2", + "sha256": "5387ce6641c7e20e983efa63712f7825d34c790cdb36b564e777d013048dd4e7", + "upstream": { + "commit": "9bebc267c4608e51fcc94a543b8e0d66077cdfbb", + "path": "research/orthogonal-inverse-witness/witness.py", + "url": "https://github.com/aliromman/integer-mult-bounds/blob/9bebc267c4608e51fcc94a543b8e0d66077cdfbb/research/orthogonal-inverse-witness/witness.py" + } + } + ] +} diff --git a/research/orthogonal-witness-precision/TASK.json b/research/orthogonal-witness-precision/TASK.json new file mode 100644 index 0000000000..146f993026 --- /dev/null +++ b/research/orthogonal-witness-precision/TASK.json @@ -0,0 +1,95 @@ +{ + "schema_version": 1, + "task_id": "formal-interface-lemma", + "priority_revision": 7, + "base_commit": "ff3cc58e370d0f678e529246f8c73e8094e18fcf", + "original_card": { + "id": "formal-interface-lemma", + "question": "Can one uncovered interface implication be formalized with exact caller and certificate bindings?", + "starting_points": [ + "docs/research/research-family-status.md", + "certificates/selected-result.json", + "research/gate-operand-parity-lean/README.md", + "research/staged544-certified-endpoint/README.md", + "research/unconditional-batched-crt/README.md" + ], + "methods": [ + "Formalize a missing boundary lemma identified by the selected review.", + "Audit a formal theorem-to-certificate binding independently." + ], + "acceptance_gate": "State the exact formalized proposition and remaining assumptions; avoid duplicate arithmetic formalizations already present.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Inventory the gate-operand parity lemma (#3807) and certified endpoint arithmetic (#3857). Neither is a full multiplication proof. For #4100, audit the compact-switch statement and its hypotheses before formalizing it.", + "scope": "Source-binding orientation only; no scientific replay, theorem acceptance or supplier admission. Budget any heavy replay separately." + }, + "first_experiment": "Write one missing statement with quantified hypotheses, actual caller and existing coverage. A compact-switch lemma is a candidate only after its mathematical contract is reviewed. Establish a bounded proof plan before a separately budgeted proof-assistant build; do not rerun large Lean jobs as orientation.", + "bottleneck_link": "A missing interface proof can reduce the conditional gap even if it does not change kappa.", + "allowed_variations": [ + "Narrow to one formal lemma or one theorem-to-certificate binding." + ], + "scope_change_triggers": [ + "Formalizing already-covered arithmetic and claiming the full multiplication theorem." + ], + "overlap_terms": [ + "hyperplane end", + "formal interface", + "Lean binding", + "3807", + "3857", + "4100", + "gate-operand-parity-lean", + "staged544-certified-endpoint", + "unconditional-batched-crt" + ], + "existing_checks": [ + { + "scope": "PR #3807: scoped gate-operand parity formalization.", + "evidence": "research/gate-operand-parity-lean/README.md", + "remaining": "Exact theorem-to-caller binding and genuinely uncovered interface lemmas.", + "status": "author-checked", + "source_commit": "4c3530f42a6abcc48e7a6bcffd6c901911dc8269", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "PR #3857: certified real-power moment/endpoint arithmetic.", + "evidence": "research/staged544-certified-endpoint/README.md", + "remaining": "Uniform algorithmic implications, not another endpoint digit.", + "status": "author-checked", + "source_commit": "ef4315b8caa605e47a2515004845eb2d2ed71a86", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "PR #4100: compact-switch formalization proposed as future validation.", + "evidence": "research/unconditional-batched-crt/README.md", + "remaining": "Audit the statement and assumptions before a formal proof campaign.", + "status": "author-checked", + "source_commit": "337d04939571a637aeab54a0f58f54fde811663a", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + } + ] + }, + "scope_status": "changed", + "actual_scope": "Prove an explicit rational endpoint separation bound and a complete funded dyadic detector for the given orthogonal witness.", + "scope_change_reason": "The exact witness leaves numerical detectability open. This result supplies a scalar-denominator and Cayley-determinant bound, then pays all scalar gain and coefficient/data rounding in a separate finite-precision consumer.", + "bottleneck_link": "Converts exact witness nonzeroness into a proved finite precision for a concrete replay, without using the exact endpoint as a decision oracle.", + "budget_minutes": 75, + "stop_rule": "Stop at the selected-endpoint detector. No IEEE behavior, optimal precision, new coefficient-producer bit complexity, native relations or complete kappa claim.", + "outcome": "completed", + "evidence": "PROOF.md, detector.py, verify.py, RESULT.json", + "author": "Ali Romman", + "ai_assistance": "Substantial OpenAI Codex assistance for proof, implementation, verification and publication.", + "open_questions": [ + { + "question": "Can a sparse or exact factor application reduce the conservative dense detector guard and replay cost for a fixed native-compatible witness?", + "why_it_matters": "The proved precision is sufficient but deliberately loose, and the dense detector is not a native primitive.", + "first_step": "Pin a caller with all extra operator relations, then compare its complete error and instruction invoice against this bound.", + "blocked_by": "Native alphabet binding, physical costs and an optimized error analysis remain open." + } + ] +} diff --git a/research/orthogonal-witness-precision/VALIDATION.md b/research/orthogonal-witness-precision/VALIDATION.md new file mode 100644 index 0000000000..e28222b611 --- /dev/null +++ b/research/orthogonal-witness-precision/VALIDATION.md @@ -0,0 +1,36 @@ +# Validation record + +Prepared by Ali Romman with substantial OpenAI Codex assistance. Apache-2.0. +Base: `ff3cc58e370d0f678e529246f8c73e8094e18fcf`. +Runtime: CPython 3.12.13, standard library only. + +Both registered isolated, warning-strict normal and optimized commands pass +and reproduce RESULT.json. There are 102 selected-endpoint cases: 24 zero +and 78 nonzero. Every returned coordinate meets the proved coefficient/data +error bound. All but the final stress case also match the retained separate +dense Gaussian-inverse oracle. Seven invalid-domain controls reject. + +Cases include an exact discrepancy 2^-80, a Cayley parameter 2^-80, gains +2^100, true inverse calls, dirty helper returns, aliased queries, eight +sandwich deletions, exact zero grid points and 80 deterministic random +programs. The inverse-series stress has 65,536 lowest-degree words, dimension +17, 2,262 fractional bits, 9,248 dense matrix products and 1,139 data +truncations. These are literal detector counts, not a physical/native tariff. + +Four separate code mutations fail in both normal and optimized modes before +receipt comparison. Omitting scalar denominators or the parameter denominator +violates the exact separation bound. Omitting scalar gains or using a forward +matrix in place of its inverse violates the complete endpoint error bound. +The source files and package remain unchanged by the mutation runs. + +The exact endpoint and dense inverse replay are verification oracles only. +The detector imports neither the endpoint replay nor the coefficient producer. +Its decision uses the explicit budget and its own integer dyadic output. +The proof establishes a sufficient guard after a path word is supplied, not +an optimal precision or a new upstream producer complexity theorem. + +No IEEE backend, independent human/proof-kernel review, native tape replay, +selected cold admission, Lean, Docker or complete kappa calculation was run. +The full-history wrapper is unpassed in the shallow checkout. Direct source +pin ancestry and portable replay are separate publication checks. No source +predecessor or selected-frontier file is changed. diff --git a/research/orthogonal-witness-precision/VERIFY.json b/research/orthogonal-witness-precision/VERIFY.json new file mode 100644 index 0000000000..9956226c02 --- /dev/null +++ b/research/orthogonal-witness-precision/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": 240, + "checks": "Exact endpoint separation, full integer dyadic replay, independent dense exact endpoints, equal and unequal programs, all dirty roles, large scalar gains, tiny denominators/parameters, source bytes and committed receipt." + }, + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-O", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 240, + "checks": "Exact endpoint separation, full integer dyadic replay, independent dense exact endpoints, equal and unequal programs, all dirty roles, large scalar gains, tiny denominators/parameters, source bytes and committed receipt." + } + ] +} diff --git a/research/orthogonal-witness-precision/detector.py b/research/orthogonal-witness-precision/detector.py new file mode 100644 index 0000000000..1c7d7d8f72 --- /dev/null +++ b/research/orthogonal-witness-precision/detector.py @@ -0,0 +1,113 @@ +"""Detect a selected rational Cayley endpoint with a proved dyadic precision. + +Ali Romman, with substantial OpenAI Codex assistance. Apache-2.0. +The retained source and classical determinant bounds are credited in PROOF.md. +""" +from fractions import Fraction as Q +from pathlib import Path +import sys + +sys.path.insert(0, str(Path(__file__).resolve().parent/'vendor/orthogonal')) +from literal import parameters, action +from syntax import validate + + +def need(value, message): + if not value: + raise ValueError(message) + + +def trunc(n, d=1): + return n//d if n >= 0 else -((-n)//d) + + +def budget(program, dimension, parameter): + need(validate(program).characteristic == 0, 'rational grammar required') + parameter = Q(parameter) + need(type(dimension) is int and dimension >= 1 and 0 < parameter <= Q(1,4), 'Cayley domain') + denominator, gain, largest = 1, Q(1), Q(0) + calls = steps = 0 + for side in ('left','right'): + for ins in program[side]: + steps += 1 + if ins['op'] == 'linear': + coefficients = [Q(c) for _,c in ins['terms']] + beta, gamma = max(Q(1),sum(map(abs,coefficients),Q(0))), Q(0) + elif ins['op'] == 'apply': + coefficients = [] + beta, gamma = Q(dimension), Q(dimension) + calls += 1 + else: + coefficients = [Q(ins['coefficient'])] + gamma = abs(coefficients[0])*dimension + beta = 1+gamma + calls += 1 + for c in coefficients: + denominator *= c.denominator + gain *= beta + largest = max(largest,gamma) + separation_denominator = denominator * (3*parameter.denominator)**(dimension*calls) + separation = Q(1,separation_denominator) + error_multiplier = steps*gain*(largest*gain+1) + required = 4*max(Q(1),error_multiplier)*separation_denominator + bits = max(0,required.numerator.bit_length()-required.denominator.bit_length()) + while 1 << bits < required: + bits += 1 + return dict(bits=bits, separation=separation, error=error_multiplier/(1 << bits), + gain=gain, scalar_denominator=denominator, calls=calls, steps=steps, + coefficient_denominator_bits=separation_denominator.bit_length()) + + +def dyadic_matrices(program, word, parameter, bits): + d, scale = len(word)+1, 1 << bits + matrices = {} + for label, band in parameters(program,word,parameter).items(): + columns = [action(band,[Q(i==j) for i in range(d)],1) for j in range(d)] + rows = [[trunc(x.numerator*scale,x.denominator) for x in row] for row in zip(*columns)] + matrices[label,1] = rows + matrices[label,-1] = list(map(list,zip(*rows))) + return matrices + + +def detect(program, word, parameter, input_index, output_index): + need(type(word) in (list,tuple) and all(type(a) is str and a in program['operators'] for a in word), + 'valid path word required') + roles, d = program['roles'], len(word)+1 + need(type(input_index) is int and type(output_index) is int and + 0 <= input_index < len(roles) and 0 <= output_index < len(roles), 'invalid role') + parameter = Q(parameter) + plan = budget(program,d,parameter) + bits, scale = plan['bits'], 1 << plan['bits'] + matrices = dyadic_matrices(program,word,parameter,bits) + endpoints = [] + products = roundings = scalar_products = 0 + for side in ('left','right'): + values = {role:[scale*int(i==input_index and j==d-1) for j in range(d)] + for i,role in enumerate(roles)} + for ins in program[side]: + dst = ins['dst'] + if ins['op'] == 'linear': + rational = [sum((Q(c)*values[src][j] for src,c in ins['terms']),Q(0)) for j in range(d)] + result = [trunc(x.numerator,x.denominator) for x in rational] + scalar_products += d*len(ins['terms']) + else: + src = dst if ins['op'] == 'apply' else ins['src'] + matrix = matrices[ins['operator'],ins['direction']] + dot = [sum(a*b for a,b in zip(row,values[src])) for row in matrix] + products += d*d + if ins['op'] == 'apply': + result = [trunc(x,scale) for x in dot] + else: + c = Q(ins['coefficient']) + result = [trunc(old*scale*c.denominator+c.numerator*x,scale*c.denominator) + for old,x in zip(values[dst],dot)] + scalar_products += d + roundings += d + values[dst] = result + endpoints.append([values[role] for role in roles]) + difference = [[a-b for a,b in zip(left,right)] for left,right in zip(*endpoints)] + value = Q(difference[output_index][0],scale) + need(plan['error'] <= plan['separation']/4, 'unfunded numerical detector') + return dict(nonzero=abs(value)>plan['separation']/2, value=value, endpoint_integers=difference, + plan=plan, matrix_products=products, scalar_products=scalar_products, + data_roundings=roundings, stored_matrix_entries=2*len(program['operators'])*d*d) diff --git a/research/orthogonal-witness-precision/verify.py b/research/orthogonal-witness-precision/verify.py new file mode 100644 index 0000000000..46fddc25e6 --- /dev/null +++ b/research/orthogonal-witness-precision/verify.py @@ -0,0 +1,130 @@ +"""Check separation and every rounded output against exact independent endpoints. + +Ali Romman, with substantial OpenAI Codex assistance. Apache-2.0. +Retained test factories and dense oracle are credited in SOURCES.json. +""" +import argparse +from copy import deepcopy +from fractions import Fraction as Q +import hashlib +import importlib.util +import json +from pathlib import Path +import random +import sys + +ROOT = Path(__file__).resolve().parent +sys.path.insert(0,str(ROOT)) +from detector import budget, detect +from literal import replay +from witness import construct + + +def need(value, message): + if not value: + raise ValueError(message) + + +def reject(call): + try: + call() + except (ValueError,TypeError): + return + raise ValueError('invalid case accepted') + + +def run(small): + for row in json.loads((ROOT/'SOURCES.json').read_text())['files']: + if '/vendor/' in row['path']: + need(hashlib.sha256((ROOT.parents[1]/row['path']).read_bytes()).hexdigest()==row['sha256'], 'source bytes') + spec=importlib.util.spec_from_file_location('_orthogonal_cases',ROOT/'vendor/orthogonal/verify.py') + old=importlib.util.module_from_spec(spec);spec.loader.exec_module(old) + digest=hashlib.sha256();cases=[];zero=nonzero=0 + max_bits=0 + def inspect(p,word=None,parameter=Q(1,4),input_index=0,output_index=0,dense=True,label='case'): + nonlocal zero,nonzero,max_bits + if word is None: + w=construct(p,parameter);word=w['word'];parameter=Q(w['parameter']) + input_index,output_index=w['input'],w['output'] + r=detect(p,word,parameter,input_index,output_index) + exact=replay(p,word,parameter,input_index) + if dense: + w={'word':word,'dimension':len(word)+1,'parameter':str(parameter),'input':input_index} + need(exact==old.dense_replay(p,w),'separate dense exact endpoint') + plan=r['plan'];scale=1 << plan['bits'];eta=plan['separation'] + value=exact[output_index][0] + if value: + need(abs(value)>=eta,'nonzero separation bound') + nonzero+=1 + else:zero+=1 + need(r['nonzero']==bool(value),'dyadic classification') + distance=max(abs(Q(x,scale)-y) for a,b in zip(r['endpoint_integers'],exact) for x,y in zip(a,b)) + need(distance<=plan['error']<=eta/4,'complete data and coefficient error') + need(r['matrix_products']==plan['calls']*(len(word)+1)**2,'dense product invoice') + need(r['data_roundings']==plan['steps']*(len(word)+1),'complete rounding invoice') + max_bits=max(max_bits,plan['bits']) + encoded={'label':label,'nonzero':r['nonzero'],'bits':plan['bits'], + 'separation_denominator_bits':plan['coefficient_denominator_bits'], + 'matrix_products':r['matrix_products'],'data_roundings':r['data_roundings'], + 'dimension':len(word)+1} + digest.update(json.dumps(r['endpoint_integers']).encode());cases.append(encoded) + return r + wrong=json.loads((ROOT/'vendor/orthogonal/vendor/wrong-order.json').read_text()) + inspect(wrong,label='commutator') + inspect(wrong,parameter=Q(1,2**80),label='tiny-parameter') + sandwich=json.loads((ROOT/'vendor/orthogonal/vendor/dirty-sandwich.json').read_text()) + inspect(sandwich,word=['A','B','A'],label='equal-dirty-sandwich') + for j in range(len(sandwich['left'])): + p=deepcopy(sandwich);del p['left'][j];inspect(p,label='deleted-sandwich-'+str(j)) + tiny=old.program();tiny['left']=[old.linear('x',[['x',str(1+Q(1,2**80))]])] + inspect(tiny,label='tiny-scalar-discrepancy') + huge=old.program();huge['left']=[old.apply('x','A',1),old.linear('x',[['x',2**100]])] + huge['right']=[old.linear('x',[['x',2**100]])] + inspect(huge,label='large-scalar-gain') + self_query=old.program();self_query['left']=[old.query('x','x','A',-1,'3/7')] + inspect(self_query,label='rational-aliased-query') + dirty=old.program(['x','h']);dirty['left']=[old.apply('h','B',-1)] + inspect(dirty,label='dirty-return') + for count in (1,2,4): + p=old.grid_roots(count) + inspect(p,label='selected-grid-'+str(count)) + inspect(p,word=['A'],parameter=Q(1,4),label='cancelled-grid-'+str(count)) + rng=random.Random(53155326) + for k in range(8 if small else 80): + p=old.program(['x','h','y']) + for side in ('left','right'): + for _ in range(rng.randint(2,7)): + dst,src=rng.choice(p['roles']),rng.choice(p['roles']);a=rng.choice(p['operators']);sign=rng.choice((-1,1)) + kind=rng.randrange(3) + if kind==0:ins=old.apply(dst,a,sign) + elif kind==1:ins=old.query(dst,src,a,sign,str(Q(rng.randint(-3,3),rng.randint(1,7)))) + else:ins=old.linear(dst,[[src,str(Q(rng.randint(-3,3),rng.randint(1,7)))],[dst,1]]) + p[side].append(ins) + if k%4==0: + p['right']=deepcopy(p['left'])+[old.apply('h','A',1),old.apply('h','A',-1)] + if old.group_difference(p):inspect(p,label='random-'+str(k)) + else:inspect(p,word=['A','B','A'],input_index=k%3,output_index=(k//3)%3,label='random-equal-'+str(k)) + depth=4 if small else 16 + stress=inspect(old.stress(depth),dense=False,label='inverse-series-stress') + controls=0 + for parameter in (Q(0),Q(-1,8),Q(1,2)): + reject(lambda: detect(wrong,['A','B'],parameter,0,0));controls+=1 + for word,i,o in [(['C'],0,0),(['A'],True,0),(['A'],0,2)]: + reject(lambda: detect(wrong,word,Q(1,4),i,o));controls+=1 + bad=deepcopy(wrong);bad['field']=2 + reject(lambda: detect(bad,['A'],Q(1,4),0,0));controls+=1 + return dict(status='PASS',cases=cases,zero=zero,nonzero=nonzero,rejecting_controls=controls, + maximum_fractional_bits=max_bits,stress_lowest_degree_words=2**depth, + digest=digest.hexdigest()) + + +def main(): + ap=argparse.ArgumentParser();ap.add_argument('--small',action='store_true');ap.add_argument('--write-result',action='store_true') + a=ap.parse_args();r=run(a.small) + if not a.small: + if a.write_result:(ROOT/'RESULT.json').write_text(json.dumps(r,indent=2)+'\n') + else:need(r==json.loads((ROOT/'RESULT.json').read_text()),'receipt differs') + print(json.dumps(r,sort_keys=True));print('PASS_ORTHOGONAL_WITNESS_PRECISION') + + +if __name__=='__main__':main()