diff --git a/research/sharp-rank-conditioning/PROOF.md b/research/sharp-rank-conditioning/PROOF.md new file mode 100644 index 0000000000..5d8fe7d1c3 --- /dev/null +++ b/research/sharp-rank-conditioning/PROOF.md @@ -0,0 +1,137 @@ +# Sharp conditioning price of signed rank transport + +This proof was produced by Nick Petalas. Apache-2.0. + +## Statement + +Use Jeremy Diviney's PR #836 model and signed rank potential, with a finite +group G, W independent arbitrary-input roles, a symmetric subadditive metric +r on G, arbitrary invertible complex scalar mixing and paid left row +multiplications by h of price c >= r(h). A free group call has r(h)=0. +Every prefix S is invertible in Mat_W(C[G]). Its faithful left regular matrix +is denoted A(S), and K(S)=||A(S)||_2 ||A(S)^(-1)||_2 >= 1. + +For every paid call on row i, immediately before that call, + + |Delta Phi| <= c (K(S)+K(S)^(-1))/2. (1) + +The constant in (1) is sharp at every real K >= 1, already for two roles +and G=C2. Sharpness is local: it does not assert that a complete cheaper +endpoint exists. + +If a complete endpoint has constant metric m_j on the formal support of +each input column j, put M=sum_j m_j. If its paid prices sum to s>0, then + + M <= sum_k c_k (K(S_k)+K(S_k)^(-1))/2. (2) + +In particular, if M>s, at least one paid prefix satisfies + + K(S_k) >= M/s + sqrt((M/s)^2-1). (3) + +For M=9 and eight unit-price calls, this is + + K(S_k) >= (9+sqrt(17))/8 > 41/25. + +The rational lower comparison is strict because sqrt(17)>103/25, +as 17*625=10625>10609=103^2. PR #836's norm-product diagnostic gives +only K(S_k)>=9/8 through its stated K_i<=K(S_k) comparison. The new +threshold is a necessary condition in the same finite-group formal model. + +## The spectral inequality + +For any invertible finite complex matrix A and unit vector e, put + + R=e*AA*e, L=e*(AA*)^(-1)e, + a=sigma_min(A)^2, b=sigma_max(A)^2. + +Here stars mean conjugate transposes, and e* denotes the row corresponding +to the column e. In a spectral basis, R and L are weighted averages of +lambda and lambda^(-1) on [a,b], using the same nonnegative weights summing +to one. Since (lambda-a)(lambda-b)<=0, + + lambda+ab/lambda <= a+b, + R+ab L <= a+b, + 4ab R L <= (R+ab L)^2 <= (a+b)^2. + +Taking square roots gives the classical Kantorovich bound + + ||e*A||_2 ||A^(-1)e||_2 <= (K+K^(-1))/2. (4) + +Indeed the first norm squared is R and the second is L, since +A^(-*)A^(-1)=(AA*)^(-1). Equality for a= M/s. Solving the +quadratic gives (3). The finite word has finitely many paid prefixes, so +the maximum exists. Dirty restored columns may have m_j=0; they are still +independent inputs in the full regular matrix. + +## A family attaining the local constant + +Let G={1,t}, t^2=1, and r(1)=0,r(t)=1. For v>=1 put + + a=(v+v^(-1))/2, b=(v-v^(-1))/2, + B=[[a,b],[b,a]], D=diag([1],[t]), + S=D B D=[[a[1],b[t]],[b[t],a[1]]]. + +This is a legal prefix: two row-t calls and one invertible scalar mixer +produce it. All role inputs remain independent; no clean state is used. +Its inverse has a on the diagonal and -b[t] off the diagonal, because +a^2-b^2=1. In the faithful regular representation, D is orthogonal and +B has positive eigenvalues v and 1/v, each repeated twice after lifting. +Thus K(S)=v^2. Before multiplying the first row by [t], the two nonzero +pairings on that row are a^2 at 1 and -b^2 at t. The call therefore gains + + Delta Phi=a^2+b^2=(v^2+v^(-2))/2=(K+K^(-1))/2. + +This proves equality in (1) for every K>=1 by taking v=sqrt(K). The +exact executable fixtures use rational v; irrational parameters belong +to the written theorem, not the finite rational enumeration. The same +prefix has Phi=-2b^2, and the next prefix has Phi=1. It has no promised +full constant-rank endpoint. Neither its gain nor its conditioning is +evidence for an eight-call solution. + +## Scope and predecessor credit + +PR #836, Jeremy Diviney, supplies the signed rank potential, its transport +identity, endpoint normalization and original nonunitary search diagnostic. +Those are cited inputs; this package does not replay the predecessor word +examples or audit their counts. Nir Ailon supplies the retained +forward/inverse-potential context. Credit eumemic #288, Swapnil Jain and +the retained register/frame lineage; littleBro #680/#705 supplies the +predecessor's finite Clifford context. No predecessor code is imported. + +The result uses finite groups, complex coefficients and full invertible +arbitrary-input words. An infinite-group extension, restricted-input clean +ancillas, nonfaithful concrete representations, a physical word, complete +supplier, paid physical invoice, compiler, precision/tape, stock, analytic +recovery and a multiplication exponent are outside scope. Independent +human and formal proof-kernel review are unclaimed. diff --git a/research/sharp-rank-conditioning/README.md b/research/sharp-rank-conditioning/README.md new file mode 100644 index 0000000000..09a3e6e1f9 --- /dev/null +++ b/research/sharp-rank-conditioning/README.md @@ -0,0 +1,117 @@ +# Sharp spectral conditioning for signed rank transport + +This contribution was produced by Nick Petalas. Apache-2.0. + +**Claim type: scoped written proof, with exact finite corroboration.** In +Jeremy Diviney's [PR #836](https://github.com/CrocSwap/integer-mult-bounds/pull/836) +formal register model over a finite group, a paid row call of price c has + + |Delta Phi| <= c (K+1/K)/2, + +where K is the spectral condition number of the faithful regular prefix. +The constant is sharp for every K>=1, already on two roles over C2. +The new step applies the classical Kantorovich inequality to the actual +coefficient row and inverse column, then constructs a legal equality family. + +For the complete rank-nine endpoint with eight unit-price calls, at least +one paid prefix must consequently have + + K >= (9+sqrt(17))/8 > 1.64, + +strengthening the predecessor's stated necessary 9/8 spectral bound. +The complete weighted price condition is in [PROOF.md](PROOF.md). +Neither local equality nor this necessary condition constructs the cheaper +endpoint. No new kappa, physical supplier or selected-frontier change follows. + +## Evidence and reproduction + +From the repository root, with CPython 3.12 and the standard library: + +```sh +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/sharp-rank-conditioning/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/sharp-rank-conditioning +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/sharp-rank-conditioning --check-source-history +``` + +Other machines can substitute their CPython 3.12 executable. Both normal and +optimized commands are registered. The direct check prints +`PASS_SHARP_RANK_CONDITIONING` in a generated JSON receipt binding every +package file and the cited source proof by SHA256. It writes no files and +works in the official Git-free export with its declared proof input. +No receipt is handwritten. + +The finite check covers all 80 distinct rational parameters v=p/q with +1<=q<=p<=16. Each equality witness has its full four-dimensional regular +inverse checked by rational elimination and both two-dimensional Fourier +blocks checked separately. A complete orthogonal eigenbasis certifies its +exact spectral condition number. Literal row permutation and inversion +give the new increment, including its negative starting potential. The +unitary boundary v=1 is also checked separately. + +Another 64 rational matrices in dimensions one through eight have prescribed +singular values and independent rational inverses. All 288 row/inverse-column +inequalities pass; eight scalar-dimension rows attain equality. Nine rejection +controls cover invalid bounds, parameters, capacity, singularity and replacing +the inverse by the transpose. Four semantic checks separate a false unitary +bound, a squared-condition substitution, the old threshold and the strict +rational comparison. These are finite real-rational fixtures; the complex, +all-dimension theorem rests on the written spectral argument. + +## Scope and credit + +Credit Jeremy Diviney #836 for the signed rank potential, exact transport, +endpoint law and nonunitary search question; Nir Ailon for the retained +forward/inverse-potential context; eumemic #288, Swapnil Jain and the retained +register/frame lineage; littleBro #680/#705 for the predecessor's finite +Clifford context. The Kantorovich inequality and spectral theorem are +classical. The contribution is this sharp application and its attaining +formal family, without a claim of general literature priority. + +The predecessor proof is cited and source-bound; no predecessor executable, +example or count is replayed. The original `bit-new-register-model` card is +explicitly changed to this complex conditioning side result in +[TASK.json](TASK.json). Base main is +`19fdb086ea96af9a9f87936a2b888e10af4ed810`, priority revision 8. +The [advance claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19220081) +records the scope before substantial work. Published PRs, recent account +submissions, claims and distinctive main/merged searches were inspected. +The cached card scan reported 324 open PRs and 5,489 Discussion records, +with complete remote pagination, but only 224 of 8,136 main note paths +materialized locally. Searches do not prove novelty or cover unpublished work. + +The theorem requires finite groups and the full invertible independent-input +boundary. Infinite groups, clean restricted inputs, nonfaithful concrete +representations and a complete eight-call construction are outside scope. +Physical costs, native realization, compiler, stock, precision/tape, analytic +recovery and the multiplication theorem remain unrun obligations. No selected +cold replay, Lean, Docker, independent human or formal proof-kernel review is +claimed. All five selected framework assumptions retain their status. + +## Open next questions + +Can a complete rank-nine endpoint with eight unit calls attain this necessary +conditioning floor? Start with one fixed formal word and track exact endpoint +equations together with every signed gain. The local equality family does not +supply the full endpoint; this is the main blocker to an attainment claim. +The structured question and its relevance are in TASK.json. + +## Implementation bounds + +The verifier has no recursion, subprocesses, network, dynamic code evaluation +or shared mutable state. Numerical loops have fixed finite domains: dimensions +at most eight, 80 witness parameters, 64 matrices, at most 24 rotations per +matrix and nine invalid-input cases. All functions fit within 60 physical +lines. Explicit exceptions keep every invariant active under optimization. +Six package files and one proof input are each capped at 256 KiB. + +Power of Ten rule 3 deviation: CPython and Fraction allocate during the bounded +offline calculation. Live matrices have at most 8-by-8 entries; rational +rotations have denominators 5 or 13 and at most 24 factors, singular values +are integers 1..4, and witness numerators/denominators are at most 16. +These fixed capacities bound live storage and coefficient heights; runtime +allocation itself is not instrumented. A native implementation would need +fixed storage before claiming that property. Rule 9 deviation: eight local +zero-argument callbacks encode the bounded invalid-input controls; production +mathematical paths use direct calls. Rule 10 diagnostics are warning-strict +normal/optimized replay and AST inspection; no separate static type analyzer +is configured or run for this isolated package. diff --git a/research/sharp-rank-conditioning/SOURCES.json b/research/sharp-rank-conditioning/SOURCES.json new file mode 100644 index 0000000000..f78f7458db --- /dev/null +++ b/research/sharp-rank-conditioning/SOURCES.json @@ -0,0 +1,24 @@ +{ + "schema_version": 1, + "base_commit": "19fdb086ea96af9a9f87936a2b888e10af4ed810", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "581f8d87008354eb5b869f7ed9de1317ad837ce8", + "sha256": "2a0220e866417774606e0f991e41b9c1d26b1f43b97857238cf478dbc7d330b5" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec", + "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81" + }, + { + "path": "research/signed-rank-transport/PROOF.md", + "usage": "input", + "git_blob": "4b51a0eb6610201715803a7f63abc5a8bb220f13", + "sha256": "ba756060ce6ae6445bfb5917523081b6c370292d4acecfbd19437b30b1d1d941" + } + ] +} diff --git a/research/sharp-rank-conditioning/TASK.json b/research/sharp-rank-conditioning/TASK.json new file mode 100644 index 0000000000..9cbb2355ec --- /dev/null +++ b/research/sharp-rank-conditioning/TASK.json @@ -0,0 +1,84 @@ +{ + "schema_version": 1, + "task_id": "bit-new-register-model", + "priority_revision": 8, + "base_commit": "19fdb086ea96af9a9f87936a2b888e10af4ed810", + "original_card": { + "id": "bit-new-register-model", + "question": "Can an explicitly larger or nonabelian register model escape the scoped three-register obstruction?", + "starting_points": [ + "docs/research/research-family-status.md", + "research/bit-three-register-lower-bound/README.md", + "certificates/selected-result.json", + "research/bit-gl3-mixed-targets-length10/README.md", + "docs/research/community-efficient1000-review.md" + ], + "methods": [ + "Construct the smallest exact identity in a newly specified legal operation alphabet.", + "Derive a target-specific relaxation bound for that same explicit alphabet." + ], + "acceptance_gate": "Name the changed hypothesis, all counted roles and a uniform identity; finite column tests alone do not certify it. A scoped local result may be retained without a complete supplier. Expanding it into further construction rounds requires the family-level budget and obligation gate in research-family-status.md; an optimistic passing relaxation alone is not acceptance.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_selected_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Resolve the current selected review, separate complex/ordinary BIT/admitted BIT/outer budgets, and compare the card against live handoffs before starting. Historical ceilings require exact source/model equivalence.", + "scope": "Source-binding orientation only; not a scientific replay or all-size proof. Materialize selected inputs if this checkout is sparse." + }, + "first_experiment": "First compare the alphabet, role count and length with the fully replayed #1974 census and #2027 mixed-root tariff. Identify a changed premise and a legal native implementation; then price one smallest completed instance before searching larger words.", + "bottleneck_link": "A small-width completed saving changes the bit primitive; a finite-address identity alone is insufficient.", + "allowed_variations": [ + "Choose a fixed larger register count or a specified nonabelian operation family." + ], + "scope_change_triggers": [ + "Remaining inside the already-excluded three-register abelian model.", + "Repeating the two-register GL3 census or a covered three-register length without changing a hypothesis; a formal group-algebra word without native conversion is a partial result." + ], + "overlap_terms": [ + "three-register", + "nonabelian", + "group algebra" + ] + }, + "scope_status": "changed", + "actual_scope": "Sharp paid rank-potential increment at a specified faithful regular spectral condition number, with a stronger necessary prefix condition and attaining two-role C2 family.", + "scope_change_reason": "The card asks for a larger binary register mechanism; this is a complex formal-model conditioning obstruction extending the explicit nonunitary search question of PR836.", + "bottleneck_link": "The current supplier bottleneck is distinct. A sharp conditioning obstruction screens formal nonunitary register searches before physical and recursive-cost work; it does not alter the selected construction.", + "budget_minutes": 60, + "stop_rule": "Package the first verified strict conditioning refinement; do not search for an eight-call word or expand the group family.", + "outcome": "completed", + "evidence": "PROOF.md proves the sharp Kantorovich application. verify.py checks 80 rational local equality witnesses, 64 rational matrices and 288 row inequalities, nine rejection controls and four semantic comparisons.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "Can a full rank-nine endpoint with eight unit calls attain the new necessary conditioning floor?", + "why_it_matters": "Local sharpness need not survive the cancellations needed for a complete endpoint. A further obstruction or a complete word would change the search.", + "first_step": "Track signed gains and exact full endpoint equations together for one fixed eight-call formal word, allowing nonunitary scalar mixers.", + "blocked_by": "The present equality family has no complete rank-nine endpoint and supplies no physical implementation." + } + ], + "claim_type": "scoped proof", + "predecessors": [ + { + "pr": 836, + "author": "Jeremy Diviney", + "login": "jeremydiviney", + "source_commit": "7ae9124f59694bb1e5acf2ae99c65e63c115b2f4" + } + ], + "claim_url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19220081", + "preserved_checkout": { + "branch": null, + "state": "detached HEAD", + "commit": "19fdb086ea96af9a9f87936a2b888e10af4ed810" + }, + "upstream_refresh": { + "commit": "19fdb086ea96af9a9f87936a2b888e10af4ed810", + "priority_revision": 8, + "checked_at": "2026-10-27T15:12:20Z" + } +} diff --git a/research/sharp-rank-conditioning/VERIFY.json b/research/sharp-rank-conditioning/VERIFY.json new file mode 100644 index 0000000000..f42a74bc27 --- /dev/null +++ b/research/sharp-rank-conditioning/VERIFY.json @@ -0,0 +1,36 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/signed-rank-transport/PROOF.md" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 60, + "checks": "Exact rational C2 equality family, independently inverted regular and Fourier matrices, prescribed-spectrum matrix row inequalities, threshold and invalid-input controls." + }, + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-O", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 60, + "checks": "The identical exact checks under optimization; all invariants use explicit exceptions." + } + ] +} diff --git a/research/sharp-rank-conditioning/verify.py b/research/sharp-rank-conditioning/verify.py new file mode 100644 index 0000000000..01c7d8bd15 --- /dev/null +++ b/research/sharp-rank-conditioning/verify.py @@ -0,0 +1,210 @@ +#!/usr/bin/env python3 +"""Exact finite corroboration, produced by Nick Petalas. Apache-2.0.""" +from fractions import Fraction as F +import hashlib +import json +from pathlib import Path +import sys + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def eye(n): + require(1 <= n <= 8, "dimension limit") + return [[F(i == j) for j in range(n)] for i in range(n)] + + +def transpose(a): + return [list(row) for row in zip(*a)] + + +def multiply(a, b): + n = len(a) + require(1 <= n <= 8 and len(b) == n, "matrix dimensions") + require(all(len(row) == n for row in a + b), "square matrices") + return [[sum(a[i][k] * b[k][j] for k in range(n)) + for j in range(n)] for i in range(n)] + + +def inverse(a): + n = len(a) + require(1 <= n <= 8, "inverse dimension") + m = [list(row) + unit for row, unit in zip(a, eye(n))] + for j in range(n): + pivot = next((i for i in range(j, n) if m[i][j]), None) + require(pivot is not None, "singular matrix") + m[j], m[pivot] = m[pivot], m[j] + divisor = m[j][j] + m[j] = [x / divisor for x in m[j]] + for i in range(n): + if i != j: + coefficient = m[i][j] + m[i] = [x - coefficient * y for x, y in zip(m[i], m[j])] + return [row[n:] for row in m] + + +def envelope(k): + require(type(k) is F and k >= 1, "condition number must be Fraction >= 1") + return (k + 1 / k) / 2 + + +def coefficient_matrix(a, b): + return [[[a, F(0)], [F(0), a]], [[F(0), b], [b, F(0)]]] + + +def regular(s): + return [[s[x ^ y][i][j] for y in range(2) for j in range(2)] + for x in range(2) for i in range(2)] + + +def coefficients(a): + return [[[a[2 * x + i][j] for j in range(2)] for i in range(2)] + for x in range(2)] + + +def pairings(s, inv, row): + values = [s[g][row][j] * inv[g][j][row] + for j in range(2) for g in range(2)] + require(sum(values) == 1, "actual inverse row normalization") + return values + + +def potential(s, inv): + return sum(s[1][i][j] * inv[1][j][i] + for i in range(2) for j in range(2)) + + +def witness(v): + require(type(v) is F and 1 <= v <= 16, "witness parameter limit") + a, b = (v + 1 / v) / 2, (v - 1 / v) / 2 + s = coefficient_matrix(a, b) + inv = coefficient_matrix(a, -b) + dense = regular(s) + require(inverse(dense) == regular(inv), "independent dense inverse") + for sign in (-1, 1): + block = [[s[0][i][j] + sign * s[1][i][j] for j in range(2)] + for i in range(2)] + expected = [[inv[0][i][j] + sign * inv[1][i][j] for j in range(2)] + for i in range(2)] + require(inverse(block) == expected, "Fourier inverse") + # Unnormalized eigenvectors have norm squared two and form a basis. + d = [[1, 0, 0, 0], [0, 0, 0, 1], + [0, 0, 1, 0], [0, 1, 0, 0]] + basis = [[1, 0, 1, 0], [1, 0, -1, 0], + [0, 1, 0, 1], [0, 1, 0, -1]] + u = multiply(d, basis) + require(multiply(transpose(u), u) == [[2 * x for x in row] for row in eye(4)], + "spectral basis") + diagonal = [v, v, 1 / v, 1 / v] + require(multiply(dense, u) == [[u[i][j] * diagonal[j] for j in range(4)] + for i in range(4)], "exact spectrum") + before = pairings(s, inv, 0) + require(before == [a * a, 0, 0, -b * b], "signed pairing support") + call = eye(4) + call[0], call[2] = call[2], call[0] + after = coefficients(multiply(call, dense)) + after_inv = coefficients(inverse(multiply(call, dense))) + delta = potential(after, after_inv) - potential(s, inv) + require(delta == a * a + b * b == envelope(v * v), "sharp increment") + require(potential(s, inv) == -2 * b * b and potential(after, after_inv) == 1, + "literal potential values") + return delta + + +def rotation(n, seed): + u = eye(n) + for k in range(3 * n): + i, j = k % n, (k + 1) % n + if i == j: + continue + c, s = (F(3, 5), F(4, 5)) if (k + seed) % 2 else (F(5, 13), F(12, 13)) + r = eye(n) + r[i][i], r[j][j], r[i][j], r[j][i] = c, c, -s, s + u = multiply(r, u) + require(multiply(u, transpose(u)) == eye(n), "orthogonal fixture") + return u + + +def matrix_fixtures(): + matrices, rows, equality_rows = 0, 0, 0 + for n in range(1, 9): + for seed in range(8): + u, v = rotation(n, seed), rotation(n, seed + 3) + spectrum = [F(1 + (i + seed) % 4) for i in range(n)] + scaled = [[u[i][j] * spectrum[j] for j in range(n)] for i in range(n)] + a = multiply(scaled, transpose(v)) + inv = inverse(a) + require(multiply(a, inv) == eye(n), "dense inverse fixture") + low, high = min(spectrum) ** 2, max(spectrum) ** 2 + for i in range(n): + r = sum(x * x for x in a[i]) + l = sum(inv[j][i] ** 2 for j in range(n)) + require(4 * low * high * r * l <= (low + high) ** 2, + "Kantorovich fixture") + rows += 1 + equality_rows += (4 * low * high * r * l == (low + high) ** 2) + matrices += 1 + return {"matrices": matrices, "rows": rows, "equality_rows": equality_rows} + + +def controls(): + bad = [lambda: envelope(F(0)), lambda: envelope(F(1, 2)), + lambda: envelope(True), lambda: envelope(2), + lambda: witness(F(17)), lambda: witness(F(0)), + lambda: inverse([[F(0)]]), lambda: eye(9)] + rejected = 0 + for action in bad: + try: + action() + except ValueError: + rejected += 1 + else: + raise ValueError("invalid input accepted") + s = coefficient_matrix(F(5, 4), F(3, 4)) + try: + pairings(s, s, 0) + except ValueError: + rejected += 1 + else: + raise ValueError("false inverse accepted") + require(envelope(F(2)) > 1, "unitary-only false bound rejected") + require(envelope(F(2)) < envelope(F(4)), "squared condition confusion") + require(envelope(F(9, 8)) < F(9, 8), "old 9/8 threshold is strictly weaker") + require(envelope(F(41, 25)) < F(9, 8), "strict rational threshold") + return {"invalid_inputs_rejected": rejected, "semantic_controls": 4} + + +def bounded_bytes(path): + require(path.stat().st_size <= 262144, "file capacity") + return path.read_bytes() + + +def main(): + require(len(sys.argv) == 1, "no command line arguments") + parameters = sorted({F(p, q) for q in range(1, 17) for p in range(q, 17)}) + total = F(0) + for v in parameters: + total += witness(v) + require(witness(F(1)) == 1, "unitary boundary") + result = {"status": "PASS_SHARP_RANK_CONDITIONING", + "witness_parameters": len(parameters), "increment_sum": str(total), + "matrix_fixtures": matrix_fixtures(), "controls": controls()} + package = Path(__file__).resolve().parent + names = ("README.md", "PROOF.md", "TASK.json", "SOURCES.json", "VERIFY.json", "verify.py") + result["sha256"] = {name: hashlib.sha256(bounded_bytes(package / name)).hexdigest() + for name in names} + sources = json.loads(bounded_bytes(package / "SOURCES.json")) + source = next(row for row in sources["files"] if row["usage"] == "input") + expected_path = "research/signed-rank-transport/PROOF.md" + require(source["path"] == expected_path, "exact mathematical source path") + digest = hashlib.sha256(bounded_bytes(package.parents[1] / expected_path)).hexdigest() + require(digest == source["sha256"], "cited proof source identity") + result["source_sha256"] = digest + print(json.dumps(result, sort_keys=True, indent=2)) + + +if __name__ == "__main__": + main()