From 376db3265f7c0418f6d95209fbf4eee5700417b0 Mon Sep 17 00:00:00 2001 From: Nick Petalas Date: Tue, 27 Oct 2026 11:31:12 +0000 Subject: [PATCH] feat(research): prove optimal heterogeneous Smith axis order --- research/smith-axis-order/PROOF.md | 172 ++++++++++++++ research/smith-axis-order/README.md | 114 +++++++++ research/smith-axis-order/SOURCES.json | 28 +++ research/smith-axis-order/TASK.json | 125 ++++++++++ research/smith-axis-order/VERIFY.json | 34 +++ research/smith-axis-order/circuit.py | 204 ++++++++++++++++ research/smith-axis-order/verify.py | 314 +++++++++++++++++++++++++ 7 files changed, 991 insertions(+) create mode 100644 research/smith-axis-order/PROOF.md create mode 100644 research/smith-axis-order/README.md create mode 100644 research/smith-axis-order/SOURCES.json create mode 100644 research/smith-axis-order/TASK.json create mode 100644 research/smith-axis-order/VERIFY.json create mode 100644 research/smith-axis-order/circuit.py create mode 100644 research/smith-axis-order/verify.py diff --git a/research/smith-axis-order/PROOF.md b/research/smith-axis-order/PROOF.md new file mode 100644 index 0000000000..67cdce71d6 --- /dev/null +++ b/research/smith-axis-order/PROOF.md @@ -0,0 +1,172 @@ +# Optimal axis order for heterogeneous Smith tensors + +This contribution was produced by Nick Petalas. New material is Apache-2.0. +Credit Dugongue / David Ganz, PR [#5815](https://github.com/CrocSwap/integer-mult-bounds/pull/5815) +at `f0fcda576df410dc15cd5b8183d4f74d284eba2b`, for the Gaussian integral +Smith word and its complete two-pass addition-precision accounting, especially +consumer-construction.md C2–C8. Tensor products, valuation arithmetic and +adjacent-exchange proofs are classical. No literature-wide priority is claimed. + +## 1. Changed premise and exact tariff + +Put pi=1+i, and fix n>=1 nonnegative integers a_1,...,a_n. Define + +```text +S = [[i,0],[1,1]], T = [[1,-i],[0,1]], +C_a = S diag(1,pi^a) T = [[i,1],[1,pi^a-i]], +F_a = tensor_j C_(a_j), N=2^n. +``` + +The Gaussian factor in #5815 is C_2. We allow unequal gaps a_j. This changes +the tensor being computed; we do not claim an order improvement for its +identical C_2 axes. Input coordinates are arbitrary Gaussian integers. The +endpoint is every coordinate of F_a x modulo pi^P, for an integer P>=0. +Normalization by pi^-B instead gives the same calculation with raw modulus +P=p+B, whenever this raw modulus is nonnegative. + +We permit independent axis permutations sigma for the T gather and tau for +the S delivery, at fixed coordinate indices. There are no axis swaps of the +data. Each scalar ADD performed at q residue digits costs exactly q in this +tariff, including q=0. The theorem minimizes the sum of this mass over **both** +passes. It does not minimize shifts, phases, routing, allocation, truncation, +cleanup, bit time, or all implementations of F_a. + +## 2. A legal modular word for every pair of orders + +Work in an owned copy of the input, initially reduced modulo pi^P. After +gathering a set A of axes, a coordinate u has precision + +```text +q(u,A) = (P - sum_(j in A) a_j u_j)_+. +``` + +For the next axis j, a low/high pair differs only at bit j and has common +current precision q. Execute + +```text +low <- low - i*high mod pi^q +high <- high mod pi^(q-a_j)_+ +``` + +The subtraction precedes truncation. Later T axes do not change the already +processed bits. Therefore each discarded error, on reaching the diagonal +tensor factor, receives at least the valuation sum that paid for its loss. +If that sum is >=P, the entire coordinate may be replaced by zero. This +proves the gather invariant and correctness of truncation by induction. + +After all T axes, a coordinate represents pi^e z, where +e=sum_j a_j u_j and z is known modulo pi^(P-e)_+. We need not physically +multiply all diagonal entries into a common-precision array. + +During delivery let B be the remaining axes. A pair at axis j in B has tags +e and e+a_j, where e=sum_(h in B minus {j}) a_h u_h. Its represented values +are pi^e z_0 and pi^(e+a_j) z_1. With q=(P-e)_+, execute + +```text +z_1 <- z_0 + pi^a_j * z_1 mod pi^q +z_0 <- i*z_0 mod pi^q +give both coordinates tag e and precision q. +``` + +These are precisely S applied to the represented pair. The old z_1 needs +only (q-a_j)_+ digits. When q-a_j<0, its missing contribution is already +zero modulo pi^q. The new z_0 phase follows the addition. At the end all +tags are zero and all precisions are P. Thus this word computes every +required output for arbitrary inputs, for every sigma and tau. Original +inputs are preserved. This ordinary modular word uses the declared owned +truncation/erasure contract; it is not a reversible implementation. + +## 3. Exact mass formula + +For a set A of axes define the rational average + +```text +H(A) = 2^(-|A|) sum_(U subset A) (P - sum_(j in U) a_j)_+. +``` + +For a gather order sigma, let A_m contain its first m axes, including A_0 +empty. Among its N/2 pairs at the next stage, each processed bit pattern +occurs equally often, so + +```text +M_T(sigma) = (N/2) sum_(m=0)^(n-1) H(A_m). +``` + +For delivery order tau, the ADD at a stage depends only on axes remaining +after that stage. Their sets, read backwards, are the prefixes of reverse(tau). +The same counting gives the exact identity + +```text +M_S(tau) = M_T(reverse(tau)). +``` + +All actual stage masses are integers: a stage uses at most n-1 averaging +bits, which are paid by the factor N/2. The formula counts every scalar pair +of both passes, rather than only the diagonal bank or one pass. + +## 4. Adjacent exchange and all equality cases + +Take adjacent gather axes with gaps a,b after an arbitrary prefix A. Let +X=sum_(j in A) a_j U_j, where U_j are independent uniform binary bits, and +write f(t)=max(t,0). The first stage cost is unchanged by the exchange; +every later stage has the same prefix set. The difference of the two +normalized gather sums is exactly + +```text +D(a,b | A) = (1/2) E[ f(P-X-a) - f(P-X-b) ]. +``` + +If a>=b, every summand is <=0. If a>b and P>b, the event with all prefix +bits zero has positive probability and gives a strictly negative summand. +If P<=b, both summands vanish for every X>=0. Hence for a>b the exchange +is strict exactly when P>b. + +Define clipped gaps b_j=min(a_j,P). An order has minimum gather mass **if +and only if** its clipped gaps are nonincreasing. Sufficiency follows by +sorting all adjacent inversions; swaps within a clipped tie have zero cost. +For necessity, any sequence that is not nonincreasing has an adjacent +increase in its clipped gaps. Swapping that pair strictly decreases cost, +by the preceding calculation. This includes P=0 and arbitrary zero gaps. + +The exact delivery minimizers are the orders with clipped gaps +nondecreasing, by Section 3. The two order choices are independent, so +these conditions characterize every minimizing pair (sigma,tau). + +In particular, sort the actual gaps descending for gather and ascending +for delivery. If a_[1]>=...>=a_[n] is that sorted list, the exact optimum is + +```text +M_min = N sum_(m=0)^(n-1) + 2^(-m) sum_(U subset {1,...,m}) (P-sum_(j in U) a_[j])_+. +``` + +Once the orders are chosen, this is an explicit finite formula, with no +search over permutations. The written theorem has no executable size limit. + +## 5. First strict improvement + +For gaps (1,4) and P=3, use the same fixed four-coordinate target throughout. + +```text +gather gaps (1,4), delivery gaps (4,1): 11+11 = 22 +gather gaps (4,1), delivery gaps (1,4): 9+ 9 = 18 +``` + +Both words have eight nominal scalar ADD positions; a zero-precision ADD +contributes zero mass. The optimized word saves four residue-digit ADD +units. Its literal modular execution and independent dense tensor outputs +agree. This is an exact component-work comparison, not a runtime speedup. + +Equal gaps make every order tie. More generally, gaps >=P are all tied even +if their actual values differ. Ordering heterogeneous physical axes can +change movement costs, which this theorem does not absorb into its tariff. + +## 6. Evidence boundary + +The verifier exhausts its declared small profiles and orders, separately +enumerates actual stage pairs, checks the exchange identity and all equality +cases, and compares the new heterogeneous modular word with direct dense +tensor multiplication. Odd moduli are checked through their Gaussian parity +lattice. These checks corroborate this written proof. No predecessor result +or verifier is replayed or audited. No selected source, supplier admission, +five framework assumption, or complete multiplication theorem is changed. diff --git a/research/smith-axis-order/README.md b/research/smith-axis-order/README.md new file mode 100644 index 0000000000..073834437c --- /dev/null +++ b/research/smith-axis-order/README.md @@ -0,0 +1,114 @@ +# Exact optimal ordering of heterogeneous Smith axes + +This contribution was produced by Nick Petalas. New material is Apache-2.0. + +**Scoped proof with finite corroboration; no new kappa.** For a tensor of +integral factors `C_a = [[i,1],[1,(1+i)^a-i]]`, arbitrary Gaussian-integer +inputs, and every raw residue precision P>=0, the minimum complete two-pass +addition-precision mass is attained by descending valuation gaps in the +triangular gather and ascending gaps in delivery. Every optimal order is +classified by sorting the clipped gaps `min(a,P)` in those directions. + +The first strict example has gaps (1,4) and P=3: the same four-coordinate +tensor costs **18 instead of 22** residue-digit ADD units. Both words have +eight nominal ADD positions. This is an exact arithmetic-work comparison, +not a measured runtime or an admitted supplier. + +[PROOF.md](PROOF.md) gives the all-size modular word, full two-pass formula, +adjacent-exchange identity, equality cases and proof. [circuit.py](circuit.py) +implements the new heterogeneous circuit and ordering; [verify.py](verify.py) +uses independent coordinate-pair accounting, dense tensor multiplication and +Gaussian parity-lattice congruence checks. It imports no predecessor code. + +## Relation to the source and current priorities + +Credit Dugongue / David Ganz's [PR #5815](https://github.com/CrocSwap/integer-mult-bounds/pull/5815), +exact head `f0fcda576df410dc15cd5b8183d4f74d284eba2b`, for the integral Gaussian +Smith circuit, propagated moduli, complete two-pass accounting, and the +parameter-efficiency continuation. In particular, consumer-construction.md +C2–C8 supplies the starting word. Tensor factorization, valuation arithmetic +and adjacent exchanges are classical; no literature-wide priority is claimed. + +The new step changes identical Gaussian gaps a=2 to **unequal supplied +gaps** and optimizes the entire order class, including delivery. Identical +Gaussian gaps tie, so this adds no ordering gain to #5815's existing word. +No earlier implementation or mathematical result was audited or replayed. + +This is a declared side result from the formal-interface-lemma card, rather +than a formal-kernel or selected-caller proof. It can guide a heterogeneous +ordinary tensor backend once such a backend's complete physical bill is +supplied. The selected .00310045 result and five assumptions retain their +status. Main was refreshed at `de5ec2e7a6074068452f45b1a191b5c72832df4a`, +priority revision 8. The source limitations and live overlap searches are in +[TASK.json](TASK.json) and [SOURCES.json](SOURCES.json). + +## Reproduce + +From the worktree root, using CPython 3.12 and its standard library: + +```sh +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/smith-axis-order/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/smith-axis-order +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/smith-axis-order --check-source-history +``` + +Any CPython 3.12 path may replace the shown interpreter. The direct verifier +ends `PASS_SMITH_AXIS_ORDER`; registered verification also runs optimized +Python. To save a generated, package-hash-bound receipt, pass +`--receipt /path/outside-the-checkout/receipt.json` to the direct verifier. +Default execution writes no files. Counts are printed from actual enumeration. + +## Local evidence + +- All 153,405 physical-axis orders across 2,259 profile/precision cases pass; + all 593,730 adjacent-exchange identities pass. Profiles are nondecreasing + multisets of 1–5 gaps in 0–4, precisions 0–8, with every physical-axis + permutation including repeated-gap permutations. +- 18,648 basis endpoints and 4,320 arbitrary-input endpoints agree with a + direct dense tensor oracle: all ordered profiles in 0–2 through four axes, + precisions 0–5, and the optimal/opposite order pairings. +- 357 complete finite-ring input cases cover gaps 0,1,2,4 in one axis and + (1,4) in two axes, at precisions 0–2. Thirteen malformed inputs reject; + six semantic controls cover strictness, clipped ties, corrupted output, + early truncation and omitted delivery. + +The counts are finite corroboration of the separate written proof. These are +not independent human review or formal proof-kernel results. + +## Limits and engineering inspection + +The executable accepts 1–8 axes, gaps and precision in 0–64, and Gaussian +input components of height at most 10^6. The proof covers all finite n and +nonnegative integer gaps and precisions. Finite tests cover smaller ranges; +they do not establish the universal theorem by themselves. + +The tariff is the sum of operand precision for all ADDs in both declared +triangular passes. Phase, scale, truncation, owned storage, cleanup, access, +physical layout and full compiler costs remain separate. Axis scheduling +does not permute coordinates in this indexed circuit, but a physical tape +host still needs its access bill. Owned truncation is permitted; reversible +truncation is a different contract. No Lean, Docker, supplier cold replay or +complete rounded multiplier was run. Independent human and formal +proof-kernel review are unclaimed. + +All loops have finite bounds from at most eight axes and 256 coordinates; +verification domains are fixed. There is no recursion or network dependency. +Python allocation and arbitrary-precision integers are explicit managed-runtime +deviations from fixed allocation: live arrays are bounded by 256 coordinates, +and tensor valuation exponents by 512. The verifier's largest dense matrix +has 256 Gaussian entries. Local module loading and the sorting key are bounded +dispatch deviations. Relevant diagnostics, ordinary and optimized replays, +boundary rejections and committed-byte checks are recorded in the PR. + +## Open next questions + +1. **Unequal per-axis ADD prices.** Which order minimizes the bill when axes + have different physical prices? It matters when routing or coefficient + work varies by axis. Start with the two-axis exchange formula, now weighted + by those prices, and look for context-dependent comparisons. A universal + sorting rule is unproved. +2. **One actual heterogeneous backend.** Does an existing caller produce + unequal Smith gaps whose complete physical bill benefits from this order? + Start with one explicitly supplied tensor factorization and source-bound + input/output grids. Actual routing, scales, truncation, cleanup and consumer + costs block a supplier or kappa conclusion. diff --git a/research/smith-axis-order/SOURCES.json b/research/smith-axis-order/SOURCES.json new file mode 100644 index 0000000000..35421d7b8a --- /dev/null +++ b/research/smith-axis-order/SOURCES.json @@ -0,0 +1,28 @@ +{ + "schema_version": 1, + "base_commit": "de5ec2e7a6074068452f45b1a191b5c72832df4a", + "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" + } + ], + "external_context": [ + { + "repository": "CrocSwap/integer-mult-bounds", + "pull_request": 5815, + "head": "f0fcda576df410dc15cd5b8183d4f74d284eba2b", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/5815", + "path": "research/gaussian-exceptional-correction/consumer-construction.md", + "usage": "Bibliographic context only; C2-C8 cited, no code import, replay or source-byte acceptance dependency. The new factor, word and proof are fully restated in PROOF.md." + } + ] +} diff --git a/research/smith-axis-order/TASK.json b/research/smith-axis-order/TASK.json new file mode 100644 index 0000000000..ec260374cb --- /dev/null +++ b/research/smith-axis-order/TASK.json @@ -0,0 +1,125 @@ +{ + "schema_version": 1, + "task_id": "formal-interface-lemma", + "priority_revision": 8, + "base_commit": "de5ec2e7a6074068452f45b1a191b5c72832df4a", + "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_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": "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": "Exact globally minimizing axis orders and all equality cases for the complete two-pass ADD-precision mass of supplied heterogeneous Gaussian-integer Smith tensors; scoped proof with finite exact corroboration.", + "scope_change_reason": "The formal-interface card is changed to an algebraic parameter-efficiency side result. PR5815 supplies an identical-gap ordinary tensor word; this contribution changes the supplied tensor to unequal nonnegative gaps and optimizes its axis orders. It does not audit that predecessor or formalize a selected-caller assumption.", + "bottleneck_link": "Complete ordinary-response precision work is a supplier cost. This minimizes the entire two-pass ADD component for a new heterogeneous tensor interface; source instantiation and every other physical cost remain separate.", + "budget_minutes": 60, + "stop_rule": "Stop at the first verified strict ordering improvement; leave unequal physical prices and actual-caller instantiation as open questions.", + "outcome": "completed", + "evidence": "PROOF.md; circuit.py; verify.py. First exact fixture: 22 -> 18 ADD-precision units at gaps (1,4), raw precision 3. Full finite counts are generated by verify.py.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "Which order minimizes addition-precision mass with unequal per-axis physical prices?", + "why_it_matters": "Routing and coefficient work can price different axes differently.", + "first_step": "Insert axis weights into the adjacent two-axis exchange formula and test context dependence.", + "blocked_by": "No general optimal ordering criterion proved for unequal prices." + }, + { + "question": "Does an actual heterogeneous backend realize a favorable complete physical bill using this order?", + "why_it_matters": "The equal Gaussian tensor gives ties, so current supplier benefit requires a genuinely heterogeneous interface.", + "first_step": "Supply one exact heterogeneous factorization and its input/output grids, then charge routing, scales, truncation and cleanup.", + "blocked_by": "No actual source-bound heterogeneous caller or full compiler bill is supplied." + } + ], + "claim_type": "scoped proof with finite corroboration", + "claim_url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19215669", + "source_question": "PR #5815: ordinary Gaussian tensor parameter-efficiency continuation; changed identical-axis hypothesis to supplied heterogeneous valuation gaps.", + "source_pr": 5815, + "source_head": "f0fcda576df410dc15cd5b8183d4f74d284eba2b", + "upstream_refresh": { + "commit": "de5ec2e7a6074068452f45b1a191b5c72832df4a", + "priority_revision": 8, + "checked_at": "2026-10-27T11:28:38.562807+00:00" + }, + "overlap": { + "live_open_prs": "Initial required 100 records, then full 400-limit list; 437 records in complete cached overlap snapshot. Candidate Gaussian PR bodies #5813, #5815, #5821, #5825 and #5880 read.", + "account_history": "Latest 200 PRs plus explicit source-PR search; this target is not a follow-up to this account's recent PRs. #5880 targets reversible overwrite storage from #5821, a different question.", + "source_distribution": "No earlier claim in the batch uses #5815; earlier #5794 question abandoned before research after another lock was found. Both locks retained.", + "main_search": "Searched all origin/main research READMEs for axis ordering, heterogeneous Smith, valuation sorting and formula/object terms; searched merged and open PRs. No identical result found.", + "limitations": "Search is not a literature-wide novelty proof. Cached local working-tree note coverage omits sparse packages; direct origin/main grep covers all matching README blobs. Unpublished work may overlap." + }, + "environment": { + "implementation": "CPython", + "python": "3.12.15", + "platform": "macOS-27.0.1-arm64-arm-64bit", + "interpreter": "/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12", + "dependencies": "standard library only" + } +} diff --git a/research/smith-axis-order/VERIFY.json b/research/smith-axis-order/VERIFY.json new file mode 100644 index 0000000000..e67d2d9ff2 --- /dev/null +++ b/research/smith-axis-order/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": 180, + "checks": "Exact all-order minima, exchange identity, equality characterization, arbitrary-input dense heterogeneous tensor endpoints, odd Gaussian moduli, strict fixture, semantic controls and malformed input rejections." + }, + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-O", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 180, + "checks": "The same complete scientific domain with optimization enabled; no verifier acceptance relies on Python assertions." + } + ] +} diff --git a/research/smith-axis-order/circuit.py b/research/smith-axis-order/circuit.py new file mode 100644 index 0000000000..09c074483f --- /dev/null +++ b/research/smith-axis-order/circuit.py @@ -0,0 +1,204 @@ +"""Heterogeneous integral Smith tensor; exact Gaussian residue arithmetic. + +All arrays are owned scratch. Erasure and physical routing are outside the +addition-precision tariff. No predecessor implementation is imported. +""" + +from fractions import Fraction + +Gaussian = tuple[int, int] +MAX_AXES = 8 +MAX_PRECISION = 64 +MAX_GAP = 64 + + +def validate(gaps: tuple[int, ...], precision: int) -> None: + if not isinstance(gaps, tuple) or not 1 <= len(gaps) <= MAX_AXES: + raise ValueError("expected 1..8 axes as a tuple") + if type(precision) is not int or not 0 <= precision <= MAX_PRECISION: + raise ValueError("precision must be an integer in 0..64") + if any(type(gap) is not int or not 0 <= gap <= MAX_GAP for gap in gaps): + raise ValueError("gaps must be integers in 0..64") + + +def validate_order(order: tuple[int, ...], width: int) -> None: + if not isinstance(order, tuple) or len(order) != width: + raise ValueError("order must have one entry per axis") + if any(type(axis) is not int for axis in order): + raise ValueError("axis indices must be integers") + if sorted(order) != list(range(width)): + raise ValueError("order must be a permutation") + + +def mul(left: Gaussian, right: Gaussian) -> Gaussian: + a, b = left + c, d = right + return a * c - b * d, a * d + b * c + + +def pi_power(exponent: int) -> Gaussian: + # At most 8*64 valuation units in a tensor coordinate. + if type(exponent) is not int or not 0 <= exponent <= MAX_AXES * MAX_GAP: + raise ValueError("invalid valuation exponent") + value = (1, 0) + for _ in range(exponent): + value = mul(value, (1, 1)) + return value + + +def residue(value: Gaussian, precision: int) -> Gaussian: + """A fundamental parallelogram representative modulo (1+i)**precision.""" + modulus = pi_power(precision) + a, b = modulus + x, y = value + norm = a * a + b * b + quotient = ((x * a + y * b) // norm, (y * a - x * b) // norm) + removed = mul(quotient, modulus) + return x - removed[0], y - removed[1] + + +def gather_mass(gaps: tuple[int, ...], precision: int, order: tuple[int, ...]) -> int: + validate(gaps, precision) + validate_order(order, len(gaps)) + demands = [precision] + total = 0 + for position, axis in enumerate(order): + total += (1 << (len(gaps) - position - 1)) * sum(demands) + demands += [max(0, demand - gaps[axis]) for demand in demands] + return total + + +def optimal_orders( + gaps: tuple[int, ...], precision: int +) -> tuple[tuple[int, ...], tuple[int, ...]]: + validate(gaps, precision) + gather = tuple(sorted(range(len(gaps)), key=lambda axis: -gaps[axis])) + return gather, tuple(reversed(gather)) + + +def optimal_mass(gaps: tuple[int, ...], precision: int) -> int: + gather, _ = optimal_orders(gaps, precision) + return 2 * gather_mass(gaps, precision, gather) + + +def is_optimal_order( + gaps: tuple[int, ...], precision: int, order: tuple[int, ...] +) -> bool: + validate(gaps, precision) + validate_order(order, len(gaps)) + clipped = [min(gaps[axis], precision) for axis in order] + return all( + left >= right for left, right in zip(clipped[:-1], clipped[1:], strict=True) + ) + + +def exchange_delta( + prefix_gaps: tuple[int, ...], a: int, b: int, precision: int +) -> Fraction: + """Normalized gather difference for orders (a,b) and (b,a).""" + validate(prefix_gaps + (a, b), precision) + remaining = [precision] + for gap in prefix_gaps: + remaining += [max(0, demand - gap) for demand in remaining] + return Fraction( + sum(max(0, value - a) - max(0, value - b) for value in remaining), + 2 * len(remaining), + ) + + +def check_inputs( + gaps: tuple[int, ...], + precision: int, + gather: tuple[int, ...], + delivery: tuple[int, ...], + values: tuple[Gaussian, ...], +) -> None: + validate(gaps, precision) + validate_order(gather, len(gaps)) + validate_order(delivery, len(gaps)) + if not isinstance(values, tuple) or len(values) != 1 << len(gaps): + raise ValueError("input must contain exactly 2**n Gaussian integers") + for value in values: + if ( + not isinstance(value, tuple) + or len(value) != 2 + or any(type(part) is not int or abs(part) > 10**6 for part in value) + ): + raise ValueError( + "Gaussian coordinates must be integer pairs of height <=10**6" + ) + + +def gather_pass( + gaps: tuple[int, ...], precision: int, order: tuple[int, ...], work: list[Gaussian] +) -> tuple[list[int], int]: + demands = [precision] * len(work) + mass = 0 + for axis in order: + bit = 1 << axis + for low in range(len(work)): + if low & bit: + continue + high = low | bit + q = demands[low] + if q != demands[high]: + raise ArithmeticError("gather pair precision mismatch") + # a <- a-i*b before discarding digits of b. + a, b = work[low], work[high] + work[low] = residue((a[0] + b[1], a[1] - b[0]), q) + demands[high] = max(0, q - gaps[axis]) + work[high] = residue(b, demands[high]) + mass += q + return demands, mass + + +def delivery_pass( + gaps: tuple[int, ...], + precision: int, + order: tuple[int, ...], + work: list[Gaussian], + demands: list[int], +) -> int: + tags = [ + sum(gap for axis, gap in enumerate(gaps) if index & (1 << axis)) + for index in range(len(work)) + ] + mass = 0 + for axis in order: + bit = 1 << axis + scale = pi_power(gaps[axis]) + for low in range(len(work)): + if low & bit: + continue + high = low | bit + q = max(0, precision - tags[low]) + if ( + tags[high] != tags[low] + gaps[axis] + or demands[low] != q + or demands[high] != max(0, q - gaps[axis]) + ): + raise ArithmeticError("delivery tag/precision mismatch") + a = work[low] + b = mul(scale, work[high]) + work[high] = residue((a[0] + b[0], a[1] + b[1]), q) + work[low] = residue((-a[1], a[0]), q) + tags[high] = tags[low] + demands[high] = q + mass += q + if any(tags) or any(q != precision for q in demands): + raise ArithmeticError("incomplete delivery") + return mass + + +def execute( + gaps: tuple[int, ...], + precision: int, + gather: tuple[int, ...], + delivery: tuple[int, ...], + values: tuple[Gaussian, ...], +) -> tuple[tuple[Gaussian, ...], int]: + check_inputs(gaps, precision, gather, delivery, values) + work = [residue(value, precision) for value in values] + demands, first_mass = gather_pass(gaps, precision, gather, work) + second_mass = delivery_pass(gaps, precision, delivery, work, demands) + return tuple(work), first_mass + second_mass diff --git a/research/smith-axis-order/verify.py b/research/smith-axis-order/verify.py new file mode 100644 index 0000000000..65bd3884b1 --- /dev/null +++ b/research/smith-axis-order/verify.py @@ -0,0 +1,314 @@ +"""Exact finite corroboration of the ordering proof; standard library only.""" + +import argparse +from fractions import Fraction +from hashlib import sha256 +from importlib.util import module_from_spec, spec_from_file_location +from itertools import combinations_with_replacement, permutations, product +import json +from math import comb +from pathlib import Path + +spec = spec_from_file_location( + "smith_axis_circuit", Path(__file__).with_name("circuit.py") +) +if spec is None or spec.loader is None: + raise ImportError("cannot load the package-local circuit") +circuit = module_from_spec(spec) +spec.loader.exec_module(circuit) +execute = circuit.execute +exchange_delta = circuit.exchange_delta +gather_mass = circuit.gather_mass +is_optimal_order = circuit.is_optimal_order +optimal_mass = circuit.optimal_mass +optimal_orders = circuit.optimal_orders + + +def require(condition: bool, message: str) -> None: + if not condition: + raise ArithmeticError(message) + + +def literal_mass( + gaps: tuple[int, ...], + precision: int, + order: tuple[int, ...], + delivery: bool = False, +) -> int: + """Independent enumeration of every actual pair at every stage.""" + total = 0 + for position, axis in enumerate(order): + relevant = order[position + 1 :] if delivery else order[:position] + for coordinate in range(1 << len(gaps)): + if coordinate & (1 << axis) == 0: + debt = sum(gaps[j] for j in relevant if coordinate & (1 << j)) + total += max(0, precision - debt) + return total + + +def ordering_checks() -> dict[str, int]: + counts = {"profiles_with_precision": 0, "orders": 0, "exchanges": 0} + for width in range(1, 6): + for gaps in combinations_with_replacement(range(5), width): + # Repeated gaps are still distinct physical axes; check all n! orders. + orders = tuple(permutations(range(width))) + for precision in range(9): + gather, delivery = optimal_orders(gaps, precision) + expected = literal_mass(gaps, precision, gather) + require(optimal_mass(gaps, precision) == 2 * expected, "optimal total") + require( + literal_mass(gaps, precision, delivery, True) == expected, + "delivery reversal", + ) + counts["profiles_with_precision"] += 1 + for order in orders: + actual = literal_mass(gaps, precision, order) + require( + actual == gather_mass(gaps, precision, order), "mass formula" + ) + require(actual >= expected, "suboptimal sorted gather") + require( + (actual == expected) + == is_optimal_order(gaps, precision, order), + "equality classification", + ) + counts["orders"] += 1 + for index in range(width - 1): + swapped = list(order) + swapped[index : index + 2] = reversed( + swapped[index : index + 2] + ) + delta = Fraction( + actual - gather_mass(gaps, precision, tuple(swapped)), + 1 << (width - 1), + ) + prefix = tuple(gaps[j] for j in order[:index]) + require( + delta + == exchange_delta( + prefix, + gaps[order[index]], + gaps[order[index + 1]], + precision, + ), + "exchange identity", + ) + counts["exchanges"] += 1 + return counts + + +def reference_pi(exponent: int) -> tuple[int, int]: + # Independent binomial expansion, rather than the interpreter's recurrence. + return ( + sum(comb(exponent, j) * (-1) ** (j // 2) for j in range(0, exponent + 1, 2)), + sum( + comb(exponent, j) * (-1) ** ((j - 1) // 2) + for j in range(1, exponent + 1, 2) + ), + ) + + +def reference_product(left: tuple[int, int], right: tuple[int, int]) -> tuple[int, int]: + real = left[0] * right[0] - left[1] * right[1] + imag = left[1] * right[0] + left[0] * right[1] + return real, imag + + +def dense_kernel(gaps: tuple[int, ...]) -> tuple[tuple[tuple[int, int], ...], ...]: + factors = [] + for gap in gaps: + value = reference_pi(gap) + factors.append((((0, 1), (1, 0)), ((1, 0), (value[0], value[1] - 1)))) + matrix = [] + for row in range(1 << len(gaps)): + entries = [] + for column in range(1 << len(gaps)): + value = (1, 0) + for axis, factor in enumerate(factors): + value = reference_product( + value, factor[(row >> axis) & 1][(column >> axis) & 1] + ) + entries.append(value) + matrix.append(tuple(entries)) + return tuple(matrix) + + +def congruent(left: tuple[int, int], right: tuple[int, int], precision: int) -> bool: + """Independent parity-lattice criterion for divisibility by pi**P.""" + real, imag = left[0] - right[0], left[1] - right[1] + scale = 1 << (precision // 2) + if real % scale or imag % scale: + return False + return precision % 2 == 0 or (real // scale - imag // scale) % 2 == 0 + + +def dense_action(matrix: tuple, values: tuple) -> tuple: + output = [] + for row in matrix: + terms = [ + reference_product(coefficient, value) + for coefficient, value in zip(row, values, strict=True) + ] + output.append((sum(term[0] for term in terms), sum(term[1] for term in terms))) + return tuple(output) + + +def endpoint_case( + gaps: tuple[int, ...], + precision: int, + values: tuple, + matrix: tuple, + gather: tuple[int, ...], + delivery: tuple[int, ...], +) -> None: + expected = dense_action(matrix, values) + actual, mass = execute(gaps, precision, gather, delivery, values) + require( + all(congruent(a, b, precision) for a, b in zip(actual, expected, strict=True)), + "heterogeneous tensor endpoint", + ) + require( + mass + == literal_mass(gaps, precision, gather) + + literal_mass(gaps, precision, delivery, True), + "literal emitted tariff", + ) + + +def endpoint_checks() -> dict[str, int]: + counts = {"basis_endpoints": 0, "arbitrary_endpoints": 0, "exhaustive_inputs": 0} + for width in range(1, 5): + for gaps in product(range(3), repeat=width): + matrix = dense_kernel(gaps) + length = 1 << width + basis = [ + tuple((int(index == column), 0) for index in range(length)) + for column in range(length) + ] + arbitrary = [ + tuple( + ((index * 7 + seed * 3) % 13 - 6, (index * index + seed) % 11 - 5) + for index in range(length) + ) + for seed in range(3) + ] + for precision in range(6): + gather, delivery = optimal_orders(gaps, precision) + for first, second in ((gather, delivery), (delivery, gather)): + for vector in basis: + endpoint_case(gaps, precision, vector, matrix, first, second) + counts["basis_endpoints"] += 1 + for vector in arbitrary: + endpoint_case(gaps, precision, vector, matrix, first, second) + counts["arbitrary_endpoints"] += 1 + for gaps in ((0,), (1,), (2,), (4,), (1, 4)): + matrix = dense_kernel(gaps) + for precision in range(3): + representatives = tuple( + product( + range(1 << ((precision + 1) // 2)), range(1 << (precision // 2)) + ) + ) + gather, delivery = optimal_orders(gaps, precision) + for vector in product(representatives, repeat=1 << len(gaps)): + endpoint_case(gaps, precision, vector, matrix, gather, delivery) + counts["exhaustive_inputs"] += 1 + return counts + + +def strict_fixture_endpoints() -> int: + gaps, precision = (1, 4), 3 + matrix = dense_kernel(gaps) + gather, delivery = optimal_orders(gaps, precision) + vectors = [tuple((int(j == k), 0) for j in range(4)) for k in range(4)] + vectors += [ + ((3, -2), (5, 7), (-1, 4), (6, -8)), + ((-9, 11), (0, 1), (1, 0), (12, -13)), + ] + for vector in vectors: + for first, second in ((gather, delivery), (delivery, gather)): + endpoint_case(gaps, precision, vector, matrix, first, second) + return 2 * len(vectors) + + +def controls() -> dict[str, object]: + gaps, precision = (1, 4), 3 + gather, delivery = optimal_orders(gaps, precision) + good = literal_mass(gaps, precision, gather) + literal_mass( + gaps, precision, delivery, True + ) + bad = literal_mass(gaps, precision, delivery) + literal_mass( + gaps, precision, gather, True + ) + require((good, bad) == (18, 22), "strict improving fixture") + require(not is_optimal_order(gaps, precision, delivery), "wrong-direction control") + require(is_optimal_order((4, 7), 3, (0, 1)), "clipped equality control") + require(not congruent((0, 0), (1, 0), 3), "corrupt endpoint accepted") + correct, _ = execute((4,), 3, (0,), (0,), ((0, 0), (1, 0))) + require(not congruent(correct[0], (0, 0), 3), "early truncation witness") + require(good != gather_mass(gaps, precision, gather), "omitted delivery control") + invalid = [ + ((), 1, (), ()), + ((-1,), 1, (0,), (0,)), + ((65,), 1, (0,), (0,)), + ((True,), 1, (0,), (0,)), + ((1,), -1, (0,), (0,)), + ((1,), 65, (0,), (0,)), + ((1,), True, (0,), (0,)), + ((1,), 1, (1,), (0,)), + ((1, 2), 1, (0, 0), (0, 1)), + ((1,), 1, (0,), (True,)), + ] + rejected = 0 + for profile, p, first, second in invalid: + try: + execute(profile, p, first, second, ((0, 0), (0, 0))) + except ValueError: + rejected += 1 + else: + raise ArithmeticError("malformed input accepted") + for vector in (((0, 0),), ((True, 0), (0, 0)), ((10**6 + 1, 0), (0, 0))): + try: + execute((1,), 1, (0,), (0,), vector) + except ValueError: + rejected += 1 + else: + raise ArithmeticError("malformed Gaussian input accepted") + return { + "malformed_inputs_rejected": rejected, + "semantic_controls": 6, + "strict_fixture_endpoints": strict_fixture_endpoints(), + "fixture": { + "gaps": gaps, + "precision": precision, + "original_mass": bad, + "optimal_mass": good, + }, + } + + +def main() -> None: + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--receipt", type=Path) + args = parser.parse_args() + result = { + "claim_type": "scoped proof with finite corroboration", + "ordering": ordering_checks(), + "endpoints": endpoint_checks(), + "controls": controls(), + } + package = Path(__file__).resolve().parent + result["package_sha256"] = { + path.name: sha256(path.read_bytes()).hexdigest() + for path in sorted(package.iterdir()) + if path.is_file() + } + payload = json.dumps(result, indent=2, sort_keys=True) + "\n" + if args.receipt is not None: + args.receipt.write_text(payload) + print(payload, end="") + print("PASS_SMITH_AXIS_ORDER") + + +if __name__ == "__main__": + main()