diff --git a/research/cayley-path-exact-denominator/PROOF.md b/research/cayley-path-exact-denominator/PROOF.md new file mode 100644 index 0000000000..6076fd3875 --- /dev/null +++ b/research/cayley-path-exact-denominator/PROOF.md @@ -0,0 +1,203 @@ +# Exact denominators of skew-path Cayley blocks + +Produced by Nick Petalas. Apache-2.0. + +## Claim and source boundary + +This is a scoped written algebraic proof with finite exact corroboration. +It sharpens the arithmetic separation step in Ali Romman's +[PR #5339](https://github.com/CrocSwap/integer-mult-bounds/pull/5339), source +head `26fe40cbca6972a0e392e9248a9cb8a84368530b`. The predecessor supplies +the complete rational register grammar and the funded error implication in +its proof, sections 1 and 2. Those results are premises here. Its scientific +replay is not the deliverable and was not rerun. + +The new result is the exact common denominator of each labelled path matrix, +including its necessary cancellation, and the resulting smaller sufficient +precision. It does not settle the predecessor's native-compatible execution +question or discharge a selected multiplication-framework assumption. + +## 1. One connected block + +Let K be the skew adjacency matrix of an n-vertex path. Its upper +off-diagonal entries are +1 and its lower ones are -1. Put + + O = (b I - a K)^(-1) (b I + a K), + +where a,b are positive coprime integers. Let den(O) be the least positive +integer h for which hO is an integer matrix. Define + + D_0 = 1, D_1 = b, + D_n = b D_(n-1) + a^2 D_(n-2). + +Then, for every n >= 1, + + den(O) = D_n / gcd(D_n, 2b). (1) + +The same formula holds for O inverse. Signs on individual path edges do not +change it. One optional closed form is + + D_n = sum_(0 <= k <= floor(n/2)) binom(n-k,k) a^(2k) b^(n-2k). + +These continuant and path-matching identities are classical. The exact +cancellation and its application to this witness interface are the step +established here; global literature priority is unclaimed. + +### Proof of the denominator formula + +Write M=bI-aK. Expansion along the last row gives det(M)=D_n. The recurrence +and positive a,b show D_n>0. Modulo a it gives D_n congruent to b^n. +Consequently gcd(D_n,a)=1. + +Since bI+aK=2bI-M, + + O = 2b adj(M)/D_n - I. + +Every numerator is divisible by h=gcd(D_n,2b). Hence multiplying O by +D_n/h gives an integer matrix. This proves that den(O) divides D_n/h. + +For n>=2, the far-corner cofactor has absolute value a^(n-1). This follows +by successively expanding the minor obtained by deleting the last row and +first column. It is triangular along the unique path. Thus the off-diagonal +corner entry of O has absolute value + + 2b a^(n-1) / D_n. + +Its reduced denominator is exactly D_n/gcd(D_n,2b), because a and D_n are +coprime. Any common denominator must clear that one entry. This proves (1). +For n=1, K=0 and O=I; (1) gives b/gcd(b,2b)=1 as required. + +Real skew symmetry gives O inverse = O transpose, so the denominator is +unchanged. For arbitrary signed unit path edges there is a diagonal matrix +S with entries in {+1,-1} such that K_signed=S K S. Conjugation by S +changes only entry signs, preserving the least common denominator. This +completes the proof. + +## 2. Label runs and primitive scaling + +The source uses t=A/B in reduced form and + + O_label(t) = (I-t K_label/2)^(-1) (I+t K_label/2). + +Set g=gcd(A,2B), a=A/g and b=2B/g. Apply (1) to these coprime parameters. +Applying it directly to A,2B without cancelling g can give a false answer. +For example t=2/9 has a=1,b=9. A two-vertex block has denominator 41, +whereas the unscaled expression incorrectly gives 82. + +Edges not carrying the selected label are absent in K_label. Its connected +components are the consecutive runs of selected edges, together with +isolated vertices. A run of ell edges has n=ell+1 vertices. The matrix and +its Cayley transform are block diagonal in these components. Therefore + + Q_label = lcm_(components c) [D_(n_c)/gcd(D_(n_c),2b)] (2) + +is the exact denominator of the entire label matrix and its inverse. +An isolated vertex contributes 1. Repeated component sizes contribute once +to the least common multiple. Distinct component denominators need not +divide one another, so replacing the lcm by a maximum is unsound. + +At t=1/4, runs of two and one edges have denominators 33 and 65. Their +joint denominator is 2145. Two separate two-edge runs have denominator 33, +rather than 33 squared. These are denominator statements, not physical +component-sharing or free native-call claims. + +## 3. The complete register lattice and separation + +Retain the source grammar over Q. Every role is returned. Assignments read +old source values. Instructions are rational linear assignments, applications +of named O_label or its inverse, and + + dst += c O_label^(+/-1) src, + +including src=dst. Across both programs, let C be the product of the positive +reduced denominators of every scalar-coefficient occurrence, exactly as in +the predecessor. Let the q named-call occurrences have labels a_1,...,a_q. +Define + + H = C product_(j=1,...,q) Q_(a_j). (3) + +For every integral input bank, every returned difference coordinate has +denominator dividing H. Equivalently, the full rational linear bank map +has entries in H^(-1) Z. No role is assumed to be clean or discarded. +For inputs with common denominator U, replace H by UH. + +To prove this, maintain a common denominator on each program side. At a +linear instruction multiply by the product of that instruction's scalar +denominators. At an application multiply by Q_label. At a query multiply +by Q_label and the coefficient denominator. The old destination and source, +including an alias, use the denominator before this multiplication. Unchanged +registers can be represented with the enlarged denominator too. Induction +proves the claim for each side. The product of the two side denominators +clears their difference and is (3). + +In particular the predecessor's selected integral basis input satisfies + + f != 0 implies |f| >= eta_new = 1/H. (4) + +The integer H is a valid common denominator, not necessarily the least +denominator of a complete program. Compositions, cancellations and unused +directions can reduce it. Matrix-level sharpness in (1) does not imply +that (3), (4), or the final numerical precision is sharp. + +## 4. Smaller sufficient grid with the same error contract + +Use the predecessor's exact bank gains beta_i>=1 and entry-error gains +gamma_i. Write G=product beta_i, Gamma=max gamma_i, and m for the combined +instruction count. An empty product has G=1, and Gamma=0 when there are no +instructions. The cited error implication is + + |fhat-f| <= E 2^(-p), E=m G (Gamma G+1), + +for entrywise truncation of forward tables toward zero, transposed tables +for inverse calls, and one toward-zero data truncation per new coordinate. +All old-value and scalar-gain hypotheses remain in force. The only change +required in that implication is the sufficient choice + + 2^p >= 4 max(1,E) H. (5) + +Equations (4) and (5) give error at most eta_new/4. Threshold eta_new/2 +therefore distinguishes a zero selected endpoint from a nonzero one. +A zero at this input/output/parameter tuple is not a universal identity test. + +For the original reduced A/B, each exact Q_label divides +det(2B I-A K_label). The predecessor bounds that determinant by (3B)^d. +Thus (3) never exceeds its coarse C(3B)^(dq). No claim asserts that H +divides that coarse numeric upper bound. + +### A strict, fully specified fixture + +Take t=1/4 and a path of nine vertices. Its eight edge labels, in spatial +order, are a,b,a,b,a,b,a,b. Each label has four two-vertex components, so +Q_a=Q_b=65. On one role apply b,a,b,a,b,a,b,a in chronological order. +Compare with the empty program. On input e_8 the coordinate-zero difference +is (16/65)^8. Reaching vertex zero in eight calls requires taking the +leftward edge at every call, so there is exactly one contributing route. + +Here C=1, q=m=8, G=9^8, Gamma=9, and + + E=8*9^8*(9*9^8+1)=133417453941706320. + +The old H bound is 12^72 and the new one is 65^8. The least integer p +satisfying each version of the same sufficient inequality is respectively +318 and 108. The reduction is exactly 210 fractional bits. The verifier +executes both dyadic grids and checks every returned coordinate against the +cited error budget. This is an explicit local guard improvement, not a +least-precision result or a performance measurement. + +## 5. Scope and credit + +The written proof covers every finite signed path and the stated rational +register grammar. Finite corroboration covers only the enumerated domains. +No source scientific census is rerun, and no predecessor theorem is audited. +No native Clifford binding, production precision policy, complete physical +cost, stock, tape, recursive compiler admission, new kappa, selected-frontier +change or complete multiplication theorem is established. Independent human +and formal proof-kernel review are unclaimed. + +Credit Ali Romman #5339 for the separation/error consumer and #5315 for the +rational orthogonal witness, Krzysztof Wojt #5262 for the complete inverse +compiler and shortest-word theorem, zxv #5235 for the retained certificate +lineage, and all predecessor notices for dirty-echo/tensor/phase and +rational-series work. Cayley transforms, continuants, adjugates and integer +lattice separation are classical. The exact-denominator specialization, +precision refinement, proof and verifier were produced by Nick Petalas. diff --git a/research/cayley-path-exact-denominator/README.md b/research/cayley-path-exact-denominator/README.md new file mode 100644 index 0000000000..04c9b56716 --- /dev/null +++ b/research/cayley-path-exact-denominator/README.md @@ -0,0 +1,83 @@ +# Exact Cayley path denominators and a smaller sufficient grid + +This scoped algebraic proof determines the exact least common denominator of +every signed path Cayley block. It improves one arithmetic step in Ali +Romman's [PR #5339](https://github.com/CrocSwap/integer-mult-bounds/pull/5339). +For coprime positive a,b and an n-vertex connected path, + +```text +D_0 = 1, D_1 = b, D_n = b D_(n-1) + a^2 D_(n-2) +den((bI-aK)^(-1)(bI+aK)) = D_n/gcd(D_n,2b). +``` + +The inverse has the same denominator. Disconnected label runs combine by +least common multiple. The far-corner matrix entry proves minimality. +[PROOF.md](PROOF.md) proves the formula for every finite signed path and +substitutes it into the predecessor's complete rational-register separation +and error implication. No predecessor scientific replay or audit is performed. + +In a specified nine-dimensional alternating-label example with eight calls, +the same sufficient precision inequality drops from **318 to 108 fractional +bits**, a reduction of 210. This is a guard improvement, not least precision, +a runtime measurement, native admission or a new multiplication exponent. + +## Reproduce + +From the repository root, using CPython 3.12 and only its standard library: + +```sh +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/cayley-path-exact-denominator +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/cayley-path-exact-denominator/verify.py +``` + +A different CPython 3.12 path can replace this machine's interpreter path. +The registered commands run the warning-strict verifier in normal and +optimized modes. Expected scientific marker: +`PASS_CAYLEY_PATH_EXACT_DENOMINATOR`. + +The verifier compares the formula with dense rational inversion, enumerates +signed supports, checks complete dirty-input bank maps, executes both dyadic +grids in the strict example, and exercises rejection controls. It emits a +generated stdout receipt bound to all seven package file hashes. It writes +no files. [VALIDATION.md](VALIDATION.md) records domains and execution limits. + +## Limitations + +The exact per-matrix denominator need not be the least common denominator +of a composed program. The new sufficient grid need not be optimal. The +funded detector's error theorem is credited to #5339. Its general arithmetic +kernel, native compatibility, physical costs and upstream coefficient +producer are not audited here. The written theorem is unbounded in path +size; the finite checker limits matrices to dimension 32 and tests the +explicit smaller domains in VALIDATION.md. + +No selected caller, production precision policy, physical supplier, new +kappa, selected-frontier change or complete multiplication theorem is +claimed. Independent human and formal proof-kernel review are unclaimed. + +## Open next questions + +- Can program-level cancellation reduce the lattice H below the product of + the exact per-call denominators? Start with one literal inverse-pair word + and retain all scalar and dirty-return effects. Matrix-level minimality + does not settle this question. +- Can this arithmetic refinement lower a bound for a native-compatible + witness with a complete paid error contract? First pin its actual operator + relations and caller. That binding and its physical cost remain open. + +## Related open work + +The live publication search found no open PR studying these skew-path Cayley +denominators or this orthogonal-witness precision bound. Historical #5315, +#5339 and #5352 are credited predecessors, not open work. Search coverage +and its sparse-local limitation are recorded in TASK.json. + +## Credit + +This contribution was produced by Nick Petalas. Credit Ali Romman #5339 for +the separation/error consumer and its open optimization question, and #5315 +for the rational orthogonal realization; Krzysztof Wojt #5262 for the inverse +compiler and shortest-word theorem; zxv #5235 and the retained +dirty-echo/tensor/phase and rational-series lineage. Cayley transforms, +continuants, adjugates and integer lattice separation are classical. No +global literature-priority claim is made. Apache-2.0. diff --git a/research/cayley-path-exact-denominator/SOURCES.json b/research/cayley-path-exact-denominator/SOURCES.json new file mode 100644 index 0000000000..a55a86a5d4 --- /dev/null +++ b/research/cayley-path-exact-denominator/SOURCES.json @@ -0,0 +1,30 @@ +{ + "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/orthogonal-witness-precision/PROOF.md", + "usage": "input", + "git_blob": "36d4c06875c7346e437227a4206f0eb474c53e76", + "sha256": "762ef04f95edc3a55347d5f58a166cde77a100e9331326e180cffa9eef88eaaa" + }, + { + "path": "research/orthogonal-witness-precision/README.md", + "usage": "input", + "git_blob": "0bd504969b70f7eb97f74b7bd84754adb2b18e08", + "sha256": "e41efda1fc15fcaf188359578c60fb24ce57068c56f08fc510cc44695d7534b4" + } + ] +} diff --git a/research/cayley-path-exact-denominator/TASK.json b/research/cayley-path-exact-denominator/TASK.json new file mode 100644 index 0000000000..79d033c2ab --- /dev/null +++ b/research/cayley-path-exact-denominator/TASK.json @@ -0,0 +1,106 @@ +{ + "schema_version": 1, + "task_id": "uniform-transfer-audit", + "priority_revision": 8, + "base_commit": "19fdb086ea96af9a9f87936a2b888e10af4ed810", + "original_card": { + "id": "uniform-transfer-audit", + "question": "Can one of the selected record's five inherited assumptions be proved at its actual caller?", + "starting_points": [ + "docs/research/current-priorities.md", + "docs/research/research-family-status.md", + "certificates/selected-result.json", + "docs/research/pr-intake-evidence/pr5599-completion/PROOF-REVIEW.md" + ], + "methods": [ + "Construct and independently check one source-bound instance of the stated first experiment.", + "Seek an exact counterexample or target-specific complete-budget obstruction to that same proposed change." + ], + "acceptance_gate": "Identify the proposition and what would change downstream; do not equate a finite replay with a universal proof.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_selected_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Read revision 8, the selected review and live exact-source handoffs. Then follow this card's bounded first_experiment.", + "scope": "Source-bound orientation only, not a supplier replay or theorem proof." + }, + "first_experiment": "Choose one assumption ID (native_all_columns, owned_erasure, compiler, precision_tape, analytic_recovery), one quantified implication and exact dependency closure. Check current handoffs, including #5625 row reentry and #5707 root-prefix lowering, without treating their partial scope as the whole theorem. Prove or falsify that implication with a caller-bound argument; stop at the chosen obligation. Finite tests or root digits do not discharge an all-size statement.", + "bottleneck_link": "Judge the actual current supplier contract and complete signed target/paid bill; frozen-profile ceilings require an applicability proof.", + "allowed_variations": [ + "One exact source head, helper/cut region or quantified proposition and changed hypothesis; check live handoffs first. Different seeds are not different scopes." + ], + "scope_change_triggers": [ + "Changing source head, helper/cut domain, operation alphabet or caller boundary without recording the new scope.", + "Treating an archived proposal or local numerical pass as complete supplier admission." + ], + "overlap_terms": [ + "native_all_columns", + "owned_erasure", + "compiler", + "precision_tape", + "analytic_recovery" + ], + "existing_checks": [ + { + "scope": "PR #4100: proposed unconditional construction and finite checks, without independent acceptance.", + "evidence": "research/unconditional-batched-crt/README.md", + "remaining": "Independent proof audit of one caller-bound all-size implication; all other premises remain explicit.", + "status": "author-checked", + "source_commit": "337d04939571a637aeab54a0f58f54fde811663a", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "Selected PR5599: complete helper-subspace construction and independent caller replay; five framework assumptions remain.", + "evidence": "docs/research/pr-intake-evidence/pr5599-completion/PROOF-REVIEW.md", + "remaining": "The next experiment must identify uncovered source-specific work. Successor archive intake does not transfer this admission.", + "status": "reviewed", + "source_commit": "09dd0965711ca7eeb169057a420abab1c9052137", + "selected_record_sha256": "2a0220e866417774606e0f991e41b9c1d26b1f43b97857238cf478dbc7d330b5" + } + ] + }, + "scope_status": "changed", + "actual_scope": "Exact common denominators of rational signed-path Cayley blocks, label-run lcm composition, and a smaller sufficient endpoint-detection grid.", + "scope_change_reason": "The current all-size assumption card is changed to a scoped arithmetic refinement of PR5339. It does not audit a predecessor or discharge a selected assumption.", + "bottleneck_link": "This is a local precision side result: exact denominator structure can lower sufficient arithmetic precision while preserving a fully charged error contract. No actual selected caller is bound.", + "budget_minutes": 60, + "stop_rule": "Ship the first verified denominator/precision improvement; leave program-level cancellation and native binding open.", + "outcome": "completed", + "evidence": "PROOF.md gives the all-path argument; verify.py independently inverts finite rational matrices and executes the strict dyadic fixture.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "Can program-level cancellation reduce H below the product of exact per-call denominators?", + "why_it_matters": "The product remains a sufficient bound and can overpay inverse cancellation.", + "first_step": "Pin one inverse-pair register word and derive its exact full bank lattice, including every scalar and dirty return.", + "blocked_by": "Per-matrix denominator sharpness does not imply composed-word sharpness." + }, + { + "question": "Does a native-compatible witness obtain a smaller complete paid precision bill from this refinement?", + "why_it_matters": "A local guard reduction alone cannot admit a physical supplier.", + "first_step": "Pin its native relations, actual caller and rounding/error/cost contract before substituting the exact Q values.", + "blocked_by": "No native binding or physical execution contract is supplied." + } + ], + "environment": { + "python": "3.12.15", + "implementation": "CPython", + "platform": "macOS-27.0.1-arm64-arm-64bit", + "dependencies": "Python standard library only" + }, + "coordination": { + "source": "PR #5339", + "source_author": "aliromman", + "source_head": "26fe40cbca6972a0e392e9248a9cb8a84368530b", + "claim_url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19219089", + "checked_at_utc": "2026-10-27T14:46:16.706076+00:00", + "upstream_commit": "19fdb086ea96af9a9f87936a2b888e10af4ed810", + "priority_revision": 8, + "overlap_coverage": "Live open PR lists; own 200 most recent PRs; last 40 handoff comments and active Discussions; full-main distinctive README searches; merged searches for denominator, continuant and orthogonal witness; PR5315/5339/5352 bodies. Cached card scan covers 310 open PRs and 5460 Discussion records but omits 7916 sparse local notes. No absence-of-matches novelty claim.", + "source_head_bytes_match": true + } +} diff --git a/research/cayley-path-exact-denominator/VALIDATION.md b/research/cayley-path-exact-denominator/VALIDATION.md new file mode 100644 index 0000000000..4b43fda08a --- /dev/null +++ b/research/cayley-path-exact-denominator/VALIDATION.md @@ -0,0 +1,70 @@ +# Verification contract + +The written result is a scoped algebraic proof. The checks corroborate the +new denominator formula and precision substitution, not predecessor results. +The two source Markdown files are authenticated by their manifest hashes. +No predecessor code is imported or executed. + +## Finite domains + +- Connected blocks use every reduced A/B with 4<=B<=28 and + 1<=A<=floor(B/4), at every dimension 1 through 9. Dense Fraction inversion + checks the whole matrix's least denominator and the far-corner witness. + An independent binomial sum checks the continuant recurrence. +- Signed supports use all edge tuples in {-1,0,1}^(n-1), for n=1 through 6, + at parameters 1/4, 2/9 and 3/13. Every full inverse is compared with the + transpose, and its exact common denominator is checked too. +- All one- and two-instruction words over six explicitly listed instruction + fixtures are checked on all ten independent input columns. They include + rational linear combinations, repeated terms, a zero coefficient, named + forward/inverse applications, an ordinary query and a self-source query. + Every role is retained. The denominator bound is checked on the whole bank + and its difference from the identity program. +- The nine-dimensional guard fixture runs the exact eight-call program and + its integer/dyadic replays at both prescribed grids. Every returned + coordinate is checked against the same source error budget. +- Controls reject four invalid parameters and three invalid edge inputs. + Separate arithmetic controls distinguish an omitted gcd, omitted primitive + scaling, product versus lcm, maximum versus lcm, and omitted scalar factors. + +Counts and package hashes come from the generated stdout receipt. No receipt +is written by hand or committed. All replay outputs and elapsed-time logs +belong outside the checkout. + +## Commands + +```sh +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/cayley-path-exact-denominator/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -O -W error -B research/cayley-path-exact-denominator/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/cayley-path-exact-denominator +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/cayley-path-exact-denominator --check-source-history +``` + +Hosted execution is separate from these local checks and from independent +scientific review. The PR body records current local timings and CI status. +No proof assistant, selected scientific cold replay, physical native caller, +upstream coefficient producer or general optimized detector is run. + +## Code inspection and bounded deviations + +The verifier uses structured control flow without recursion. Its largest +matrix is capped at dimension 32. All enumeration ranges are fixed above; +the register programs are private tuples with at most two instructions in +the census, and eight in the guard example. All functions fit within 60 +physical lines. Meaningful requirements are explicit exceptions and remain +enabled with Python optimization. Source inputs and outputs are read-only. +No callbacks, code generation, reflection or subprocesses occur. + +Rule 3, allocation after initialization, requires a managed-runtime deviation +for Python Fraction, integer and list allocation. The scope is this finite +standalone checker. Matrix buffers contain at most 32 rows and 64 augmented +columns. Rational parameters have at most 256 denominator bits, connected +determinants at most 32 times the parameter-size order, and the only replay +grids are bounded by 4096 bits. The fixed fixture coefficients and iteration +counts bound live arithmetic sizes. Python/library allocation internals are +not instrumented. Direct normal/optimized runs exercise the capacity controls. +If a production caller is added, its resource contract needs separate design. + +Rule 10 uses the repository's Python package replay plus isolated +warning-strict normal and optimized execution. No repository-wide static +analysis configuration is changed for this isolated research package. diff --git a/research/cayley-path-exact-denominator/VERIFY.json b/research/cayley-path-exact-denominator/VERIFY.json new file mode 100644 index 0000000000..60f77644e5 --- /dev/null +++ b/research/cayley-path-exact-denominator/VERIFY.json @@ -0,0 +1,37 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/orthogonal-witness-precision/PROOF.md", + "research/orthogonal-witness-precision/README.md" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Exact connected and signed-support denominators, full dirty-register lattices, both dyadic grids and rejection controls." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "The same mathematical checks with assertions disabled; explicit requirements remain active." + } + ] +} diff --git a/research/cayley-path-exact-denominator/verify.py b/research/cayley-path-exact-denominator/verify.py new file mode 100644 index 0000000000..3390e42258 --- /dev/null +++ b/research/cayley-path-exact-denominator/verify.py @@ -0,0 +1,326 @@ +"""Exact Cayley path denominators. Produced by Nick Petalas. Apache-2.0.""" + +from fractions import Fraction +from hashlib import sha256 +from itertools import product +import json +from math import comb, gcd, lcm +from pathlib import Path + + +MAX_DIMENSION = 32 +PACKAGE = Path(__file__).resolve().parent + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def scaled_parameter(parameter): + require(type(parameter) is Fraction, "parameter must be a Fraction") + require(0 < parameter <= Fraction(1, 4), "parameter outside (0,1/4]") + require(parameter.denominator.bit_length() <= 256, "parameter capacity") + common = gcd(parameter.numerator, 2 * parameter.denominator) + return parameter.numerator // common, 2 * parameter.denominator // common + + +def continuant(n, a, b): + require(type(n) is int and 0 <= n <= MAX_DIMENSION, "dimension capacity") + require(type(a) is int and type(b) is int and a > 0 and b > 0, + "positive integer parameters required") + require(gcd(a, b) == 1, "parameters must be coprime") + require(max(a.bit_length(), b.bit_length()) <= 257, "integer capacity") + previous, current = 0, 1 + for _ in range(n): + previous, current = current, b * current + a * a * previous + return current + + +def block_denominator(n, parameter): + a, b = scaled_parameter(parameter) + require(type(n) is int and 1 <= n <= MAX_DIMENSION, "positive block dimension required") + determinant = continuant(n, a, b) + return determinant // gcd(determinant, 2 * b) + + +def path_denominator(edges, parameter): + require(type(edges) is tuple and len(edges) < MAX_DIMENSION, "edge capacity") + require(all(type(x) is int and x in (-1, 0, 1) for x in edges), + "edges must be signed unit edges or absent") + scaled_parameter(parameter) + denominator, size = 1, 1 + for edge in edges: + if edge: + size += 1 + else: + denominator = lcm(denominator, block_denominator(size, parameter)) + size = 1 + return lcm(denominator, block_denominator(size, parameter)) + + +def inverse(matrix): + n = len(matrix) + require(1 <= n <= MAX_DIMENSION and all(len(row) == n for row in matrix), + "square matrix capacity") + rows = [[Fraction(x) for x in row] + [Fraction(i == j) for j in range(n)] + for i, row in enumerate(matrix)] + for column in range(n): + pivot = next((i for i in range(column, n) if rows[i][column]), None) + require(pivot is not None, "singular matrix") + rows[column], rows[pivot] = rows[pivot], rows[column] + divisor = rows[column][column] + rows[column] = [x / divisor for x in rows[column]] + for i in range(n): + if i != column: + factor = rows[i][column] + rows[i] = [x - factor * y for x, y in zip(rows[i], rows[column])] + return [row[n:] for row in rows] + + +def dense_cayley(edges, parameter): + # The comparison uses I-tK/2 directly, without continuants or scaling. + path_denominator(edges, parameter) + n = len(edges) + 1 + matrix = [[Fraction(i == j) for j in range(n)] for i in range(n)] + for i, edge in enumerate(edges): + matrix[i][i + 1] = -parameter * edge / 2 + matrix[i + 1][i] = parameter * edge / 2 + solved = inverse(matrix) + return [[2 * solved[i][j] - (i == j) for j in range(n)] for i in range(n)] + + +def common_denominator(matrix): + return lcm(*(x.denominator for row in matrix for x in row)) + + +def matvec(matrix, vector): + require(len(matrix) == len(vector), "matrix/vector dimension mismatch") + return [sum((x * y for x, y in zip(row, vector)), Fraction(0)) for row in matrix] + + +def check_connected(): + count = 0 + for denominator in range(4, 29): + for numerator in range(1, denominator // 4 + 1): + if gcd(numerator, denominator) != 1: + continue + parameter = Fraction(numerator, denominator) + a, b = scaled_parameter(parameter) + for n in range(1, 10): + determinant = continuant(n, a, b) + closed = sum(comb(n - k, k) * a ** (2 * k) * b ** (n - 2 * k) + for k in range(n // 2 + 1)) + require(determinant == closed, "continuant matching formula") + require(gcd(determinant, a) == 1, "corner coprimality") + matrix = dense_cayley((1,) * (n - 1), parameter) + expected = block_denominator(n, parameter) + require(common_denominator(matrix) == expected, "connected denominator") + if n > 1: + require(matrix[0][-1].denominator == expected, "corner minimality") + count += 1 + return count + + +def check_signed_supports(): + count = 0 + for parameter in (Fraction(1, 4), Fraction(2, 9), Fraction(3, 13)): + for n in range(1, 7): + for edges in product((-1, 0, 1), repeat=n - 1): + matrix = dense_cayley(edges, parameter) + expected = path_denominator(edges, parameter) + require(common_denominator(matrix) == expected, "signed support denominator") + backwards = inverse(matrix) + require(backwards == [list(row) for row in zip(*matrix)], + "Cayley inverse must be its transpose") + require(common_denominator(backwards) == expected, "inverse denominator") + count += 1 + return count + + +def instructions(): + # Private fixtures have two independent roles and this fixed tuple grammar. + return ( + ("linear", 0, ((0, Fraction(1, 2)), (1, Fraction(-2, 3)))), + ("linear", 1, ((0, Fraction(0)), (0, Fraction(5, 7)))), + ("apply", 0, 0, 1), ("apply", 1, 1, -1), + ("query", 0, 1, 0, 1, Fraction(2, 5)), + ("query", 1, 1, 1, -1, Fraction(-3, 11)), + ) + + +def product_denominators(coefficients): + coefficients = tuple(coefficients) + require(len(coefficients) <= 16, "coefficient capacity") + result = 1 + for coefficient in coefficients: + result *= coefficient.denominator + return result + + +def exact_program(program, matrices, denominators, initial): + require(len(program) <= 8 and len(initial) == 2, "fixture program capacity") + require(all(ins in instructions() for ins in program), "unknown fixture instruction") + registers = [row[:] for row in initial] + bound = 1 + for ins in program: + kind, dst = ins[:2] + if kind == "linear": + terms = ins[2] + result = [sum((c * registers[src][j] for src, c in terms), Fraction(0)) + for j in range(len(registers[dst]))] + bound *= product_denominators(c for _, c in terms) + else: + src = dst if kind == "apply" else ins[2] + label, direction = ins[2:4] if kind == "apply" else ins[3:5] + matrix = matrices[label] + if direction == -1: + matrix = [list(row) for row in zip(*matrix)] + value = matvec(matrix, registers[src]) + bound *= denominators[label] + if kind == "query": + coefficient = ins[5] + bound *= coefficient.denominator + result = [old + coefficient * new + for old, new in zip(registers[dst], value)] + else: + result = value + registers[dst] = result + require(all(bound % x.denominator == 0 for row in registers for x in row), + "returned dirty-role denominators must divide the bound") + return registers, bound + + +def check_registers(): + parameter, word = Fraction(1, 4), (0, 1, 0, 1) + edges = [tuple(int(x == label) for x in word) for label in range(2)] + matrices = [dense_cayley(edge, parameter) for edge in edges] + denominators = [path_denominator(edge, parameter) for edge in edges] + programs = [(ins,) for ins in instructions()] + list(product(instructions(), repeat=2)) + count = 0 + for program in programs: + # Every column of the complete bank map, including every dirty input. + for column in range(10): + initial = [[Fraction(column == 5 * role + j) for j in range(5)] + for role in range(2)] + returned, bound = exact_program(program, matrices, denominators, initial) + require(all(bound % (new - old).denominator == 0 + for row, oldrow in zip(returned, initial) + for new, old in zip(row, oldrow)), "endpoint difference lattice") + count += 1 + return {"programs": len(programs), "independent_input_columns": count} + + +def truncate_ratio(numerator, denominator): + require(denominator > 0, "positive truncation denominator required") + return (1 if numerator >= 0 else -1) * (abs(numerator) // denominator) + + +def rounded_apply_sequence(matrices, order, bits, initial): + require(0 <= bits <= 4096 and len(order) <= 32, "dyadic replay capacity") + scale = 1 << bits + tables = [[[truncate_ratio(x.numerator * scale, x.denominator) for x in row] + for row in matrix] for matrix in matrices] + values = [int(x * scale) for x in initial] + for label in order: + values = [truncate_ratio(sum(x * y for x, y in zip(row, values)), scale) + for row in tables[label]] + return [Fraction(x, scale) for x in values] + + +def check_guard_fixture(): + parameter, word = Fraction(1, 4), (0, 1) * 4 + edges = [tuple(int(x == label) for x in word) for label in range(2)] + matrices = [dense_cayley(edge, parameter) for edge in edges] + require([path_denominator(edge, parameter) for edge in edges] == [65, 65], + "alternating path denominators") + order = (1, 0) * 4 + initial = [Fraction(j == 8) for j in range(9)] + exact = initial + for label in order: + exact = matvec(matrices[label], exact) + require(exact[0] == Fraction(16, 65) ** 8, "unique shortest propagation path") + gain = 9 ** 8 + error_factor = 8 * gain * (9 * gain + 1) + old_lattice, new_lattice = 12 ** 72, 65 ** 8 + old_bits = (4 * error_factor * old_lattice - 1).bit_length() + new_bits = (4 * error_factor * new_lattice - 1).bit_length() + require((old_bits, new_bits) == (318, 108), "sufficient precision fixture") + for bits, lattice in ((old_bits, old_lattice), (new_bits, new_lattice)): + computed = rounded_apply_sequence(matrices, order, bits, initial) + error = Fraction(error_factor, 1 << bits) + require(error <= Fraction(1, 4 * lattice), "funded error allowance") + require(all(abs(x - y) <= error for x, y in zip(computed, exact)), + "actual complete returned-vector error") + require(abs(computed[0]) > Fraction(1, 2 * lattice), "nonzero verdict") + return {"dimension": 9, "calls": 8, "coarse_bits": old_bits, + "refined_bits": new_bits, "saved_bits": old_bits - new_bits, + "endpoint": str(exact[0])} + + +def check_controls(): + count = 0 + for parameter in (Fraction(0), Fraction(-1, 4), Fraction(1, 3), 0.25): + try: + block_denominator(2, parameter) + except ValueError: + count += 1 + else: + raise ValueError("invalid parameter accepted") + for edges in ((2,), (True,), (1,) * MAX_DIMENSION): + try: + path_denominator(edges, Fraction(1, 4)) + except ValueError: + count += 1 + else: + raise ValueError("invalid edges accepted") + parameter = Fraction(1, 4) + actual = common_denominator(dense_cayley((1, 1), parameter)) + require(actual != continuant(3, 1, 8), "omitted gcd mutation must fail") + count += 1 + # The deliberately unscaled b=18,a=2 formula gives 82 instead of 41. + require(common_denominator(dense_cayley((1,), Fraction(2, 9))) != + (18 * 18 + 2 * 2) // gcd(18 * 18 + 2 * 2, 36), + "omitted primitive scaling mutation must fail") + count += 1 + require(path_denominator((1, 1, 0, 1, 1), parameter) == 33, + "repeated runs use lcm, not product") + require(path_denominator((1, 1, 0, 1), parameter) == 2145, + "unequal runs use lcm, not maximum") + count += 2 + scaled = [[x / 7 for x in row] for row in dense_cayley((1,), parameter)] + require(any(65 % x.denominator != 0 for row in scaled for x in row), + "scalar denominator omission must fail") + count += 1 + return count + + +def authenticate_inputs(): + root = PACKAGE.parent.parent + sources = json.loads((PACKAGE / "SOURCES.json").read_text()) + rows = sources["files"] + require(len(rows) <= 16, "source manifest capacity") + for row in rows: + if row["usage"] == "input": + require(sha256((root / row["path"]).read_bytes()).hexdigest() == row["sha256"], + "source hash mismatch: " + row["path"]) + + +def main(): + authenticate_inputs() + result = {"schema": "cayley-path-exact-denominator/v1", + "connected_matrices": check_connected(), + "signed_support_matrices": check_signed_supports(), + "register_fixtures": check_registers(), + "guard_fixture": check_guard_fixture(), + "rejection_and_boundary_controls": check_controls()} + names = ("README.md", "PROOF.md", "TASK.json", "SOURCES.json", "VERIFY.json", + "VALIDATION.md", "verify.py") + result["package_sha256"] = {name: sha256((PACKAGE / name).read_bytes()).hexdigest() + for name in names} + print(json.dumps(result, indent=2, sort_keys=True)) + print("PASS_CAYLEY_PATH_EXACT_DENOMINATOR") + + +if __name__ == "__main__": + main()