From e1f0906c35defdc4704f2b3e5e954c2a62981791 Mon Sep 17 00:00:00 2001 From: Nick Petalas Date: Thu, 22 Oct 2026 23:43:54 +0100 Subject: [PATCH] feat(research): prove the three-value same-phase shear floor --- research/three-spectrum-shear/PROOF.md | 143 +++++++ research/three-spectrum-shear/README.md | 104 +++++ research/three-spectrum-shear/RESULT.json | 459 +++++++++++++++++++++ research/three-spectrum-shear/SOURCES.json | 30 ++ research/three-spectrum-shear/TASK.json | 66 +++ research/three-spectrum-shear/VERIFY.json | 35 ++ research/three-spectrum-shear/exact.py | 107 +++++ research/three-spectrum-shear/verify.py | 198 +++++++++ 8 files changed, 1142 insertions(+) create mode 100644 research/three-spectrum-shear/PROOF.md create mode 100644 research/three-spectrum-shear/README.md create mode 100644 research/three-spectrum-shear/RESULT.json create mode 100644 research/three-spectrum-shear/SOURCES.json create mode 100644 research/three-spectrum-shear/TASK.json create mode 100644 research/three-spectrum-shear/VERIFY.json create mode 100644 research/three-spectrum-shear/exact.py create mode 100644 research/three-spectrum-shear/verify.py diff --git a/research/three-spectrum-shear/PROOF.md b/research/three-spectrum-shear/PROOF.md new file mode 100644 index 0000000000..7f836aa99c --- /dev/null +++ b/research/three-spectrum-shear/PROOF.md @@ -0,0 +1,143 @@ +# Three character values already force six calls + +Let C have character spectrum {1,i,-1}. For any finite complex role space, +let N be square-zero of rank three. Require the complete endpoint + + S(z) = I + (z-1)N, z in {1,i,-1}. + +Every input coordinate, including every helper, is arbitrary and dirty. +Allowed free gates are constant invertible complex role matrices. Each paid +gate applies C or C^-1 to one role. The constants are shared across characters. +The minimum number of paid calls is six. + +This settles Open next question 1 in Richard Hoekstra's PR1318. Its normalization, +direction-span split and target-image loop method are inherited and credited. +The new observation is that the independent-direction exclusion needs only the +two active values i and -1. No fourth character is required. + +## Normalize and split + +At z=1 the product of constant gates must be identity. Absorb the constants into +conjugations to write a k-call word as + + F(z) = R_k(z)...R_1(z), + R_j(z) = I + (z^epsilon_j-1)a_j b_j, + b_j a_j=1, epsilon_j in {+1,-1}. + +These rank-one idempotents need not be self-adjoint. This normalization is the +one in PR1318 and allows arbitrarily many restored dirty helpers. Rank(F-I)<=k +and det F(i)=i^(sum epsilon_j)=1. Thus k>=3 and k is even. Any word with fewer +than six calls must have exactly four, with all signs equal or two of each. + +Put Y=im N and V=span(a_1,...,a_4). Then Y is contained in V, dim Y=3, +and N vanishes on Y. Hence dim V is three or four. If dim V=4, the restriction +N|V factors through V/Y, so rank(N|V)<=1. + +## Independent directions: the new two-value exclusion + +Choose a_j=e_j for j=1,...,4, extending to a basis of the entire role space. +Later factors change only their own rows. Row one of the endpoint forces + + (z^epsilon_1-1)b_1 = (z-1)N_row1. + +If epsilon_1=-1, dividing by z-1 gives N_row1=-z^-1 b_1 at both z=i and -1. +The two scalars differ, so b_1=0, contradicting b_1 a_1=1. Thus epsilon_1=+1. +Apply the same argument to F^-1=S^-1=I-(z-1)N, with the directions in reverse +order. It forces epsilon_4=-1. In particular both all-equal sign patterns are +excluded. The only remaining patterns are ++-- and +-+-. + +For ++-- put g=z-1 and d=b_2 a_1. The first two endpoint rows give + + N_row1=b_1, + N_row2=b_2+g d b_1. + +The values g(i) and g(-1) differ. Hence d b_1=0, so d=0 and N_row2=b_2. +In the first two columns these two rows have determinant +b_1 a_1 * b_2 a_2 - b_1 a_2 * b_2 a_1 = 1. +Thus rank(N|V)>=2, a contradiction. + +For +-+- row two instead gives + + N_row2 = -d b_1 + z^-1(d b_1-b_2). + +Again the two active values force b_2=d b_1. Idempotence gives +1=b_2 a_2=d b_1 a_2, so d is nonzero. Direct multiplication, now as an identity +for every nonzero z, yields + + R_2 R_1 = I+(z-1)M_1, + M_1=(a_1-d a_2)b_1, M_1^2=0, rank M_1=1. + +The inverse word has the same alternating sign pattern. Its first pair +therefore gives R_3^-1 R_4^-1=I+(z-1)M_tilde. Inverting this square-zero +shear gives R_4 R_3=I+(z-1)M_2, where M_2=-M_tilde has rank one and square zero. +Consequently + + F(z)=I+(z-1)(M_1+M_2)+(z-1)^2 M_2 M_1. + +At z=i and -1, divide F(z)-S(z) by z-1 and subtract. This gives M_2 M_1=0 +and then N=M_1+M_2. Its rank is at most two, the final contradiction. +This is the new exclusion that closes the three-value question. + +## Directions spanning Y: the inherited loop method at two active values + +For completeness, the PR1318 target-image argument is written with its actual +sample points. Restrict all factors to Y, where their product is identity. +Every a_j lies in the span of the other three. Otherwise a covector annihilating +the other three detects a nonzero jth rank-one update after an invertible prefix, +contradicting identity on Y. The unique dependency therefore uses all four. +Write a_1=e_1,a_2=e_2,a_3=e_3 and a_4=(c_1,c_2,c_3), with all c_j nonzero. +Let f_j=b_j|Y. From R_3 R_2 R_1=R_4^-1, row one says + + (z^epsilon_1-1)f_1=(z^-epsilon_4-1)c_1 f_4. + +Evaluation at i and -1 forces epsilon_4=-epsilon_1 and f_1=c_1 f_4. +Row two excludes epsilon_2=epsilon_1, since it would give +f_2+(z^epsilon_1-1)(f_2 a_1)f_1=(c_2/c_1)f_1 at two distinct scalars, +forcing both f_2 a_1=0 and f_2 a_1=c_2/c_1. +Thus epsilon_2=-epsilon_1 and f_2=-(c_2/c_1)f_1. +The determinant on Y forces epsilon_3=epsilon_1. The first pair is a shear; +substituting it in R_3 R_2 R_1=R_4^-1 and comparing the two active values gives +f_3=(c_3/c_1)f_1. Rescale the directions and use them as coordinates to obtain + + a_1=e_1, a_2=e_2, a_3=e_3, a_4=e_1-e_2+e_3, + f_1=f_2=f_3=f_4=(1,1,1). + +For each outside input column the remaining covector entries are arbitrary +complex beta_1,...,beta_4. Write B(z) for its outside-to-Y transfer and +H(z)=B(z)/(z-1), t=z^-1. Direct multiplication gives the following inherited +canonical coefficient formulas. + +For +-+-: + + H_1=t beta_1+(1-t)beta_2-(1-t)beta_3-t beta_4, + H_2=-beta_2+(1-t)beta_3+t beta_4, + H_3=t(beta_3-beta_4). + +Equality H(i)=H(-1) forces beta_1=beta_2 and beta_3=beta_4. Every constant +transfer column lies in span(e_1-e_2), which has dimension one. + +For -+-+: + + H_1=-beta_1+(1-t)beta_2-(1-t)beta_3+beta_4, + H_2=t beta_2+(1-t)beta_3-beta_4, + H_3=-beta_3+beta_4. + +Equality forces beta_2=beta_3. Every constant transfer column lies in +span(e_1,e_2-e_3), which has dimension two. Neither pattern can have rank three. +The argument applies to any finite number of outside and helper roles because +the same image bound holds separately for every outside column. + +## Attainment and scope + +For one source x and target y use C on x, then y+=x, then C^-1 on x, +then y-=x. The endpoint is x restored and y+=(C-I)x for arbitrary dirty x,y. +Apply this independently to three pairs: six calls attain the bound. Every +rank-three square-zero N has this canonical shear form after a constant basis +change. The six-call construction therefore covers every N in the theorem. + +This is a scoped written proof. The checker corroborates its two-value +coefficient constraints, canonical image bounds and literal six-call endpoint +using exact Q(i) arithmetic. It is not exhaustive enumeration of arbitrary +complex projectors, a proof-assistant formalization, or a multiplication theorem. +Other phase functions, extra character-dependent gates, clean-input contracts, +physical tariffs and supplier admission are outside the theorem. diff --git a/research/three-spectrum-shear/README.md b/research/three-spectrum-shear/README.md new file mode 100644 index 0000000000..e13c946c22 --- /dev/null +++ b/research/three-spectrum-shear/README.md @@ -0,0 +1,104 @@ +# Three values already force six same-phase calls + +This contribution is produced by Nick Petalas. New work is Apache-2.0. +Independent human and formal proof-kernel review are unclaimed. + +For a phase operator C with spectrum {1,i,-1}, three independent transfers +`y_j += (C-I)x_j` require exactly **six C/C^-1 calls**, even with arbitrary +constant invertible complex role mixing and any finite number of restored +dirty helpers. Equivalently, the complete map `I+(z-1)N` for any rank-three +square-zero N has minimum six in this alphabet. + +This is a scoped algebraic proof with exact finite corroboration. It answers +Open next question 1 in Richard Hoekstra's [PR1318](https://github.com/CrocSwap/integer-mult-bounds/pull/1318), +which proves the four-value floor and leaves the three-value case open. +The new first/last-row argument excludes four independent phase directions +using only i and -1. The inherited target-image loop method needs those same +two active values. [PROOF.md](PROOF.md) gives the complete argument and credits +the inherited normalization, span split and canonical loops. No predecessor +verifier is imported or replayed. No literature-priority claim is made. + +Deleting the -i character therefore does not create the proposed four-call +shortcut. Six direct calls attain the bound with all source, target and helper +columns handled as arbitrary dirty inputs. This does not change a selected +supplier, physical tariff or kappa. Extra character-dependent gates, different +phase functions and clean-input contracts are outside the theorem. + +## Reproduce + +From the repository root, using CPython 3.12 and its standard library: + +```sh +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -W error -B research/three-spectrum-shear/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -W error -O -B research/three-spectrum-shear/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/three-spectrum-shear +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/three-spectrum-shear --check-source-history +``` + +Other machines can substitute their CPython 3.12 interpreter. Expected direct +output is `PASS_THREE_SPECTRUM_SHEAR minimum=6 loops=2 collapse_cases=81 upper_samples=6 controls=9 no_new_kappa`. + +The checker uses exact Q(i) arithmetic. It constructs both four-call canonical +loops on all basis inputs, imposes equality at i and -1 by exact elimination, +and obtains constant-transfer image ranks one and two. It tests the new pair +collapse on 81 explicit rational cases. Six literal eight-role upper endpoints +include two restored dirty spectator roles. The nine controls cover six omitted +calls, the single-active-value boundary, a nonidempotent factor and zero phase. +These are finite checks of the written proof's core, not enumeration of all +complex projectors or all circuits. The all-dimension lower bound is the proof. + +`RESULT.json` is generated by the verifier and binds its mathematical fields to +the package and inherited-input hashes. To regenerate without overwriting it: + +```sh +python3.12 -W error -B research/three-spectrum-shear/verify.py --write /tmp/three-spectrum-result.json +python3.12 -W error -B research/three-spectrum-shear/verify.py --certificate /tmp/three-spectrum-result.json +``` + +Source pin availability, metadata validation and passing CI are distinct from +scientific approval. No native phase/compiler, finite-precision, fixed-tape, +physical hosting, supplier-admission, outer theorem or Lean replay is run. + +## Provenance and overlap + +Base canonical main is `624de9dc66858af0945e5f8a0942488d62280d43`, priority revision 7. +`SOURCES.json` pins the current card, selected record and PR1318 proof/README +bytes. The PR1318 head is `5cc2496bbdae91e1f5d96d2ae340b42d2d776f24`. +The `complex-new-helper-inventory` card is explicitly changed to this open +algebraic interface question; its historical packing experiment is not the +question being answered. The current selected source-binding control passed. + +The [advance claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19134000) +follows live open/merged PR and body searches, distinctive all-main README +searches, active Discussions, recent account submissions and a local question +reservation. Sparse local notes, arbitrary diffs and unpublished work are +coverage limits. Search absence is not a novelty certificate. No matching open +PR was identified by the targeted PR1318/object searches at claim time. + +Credit Richard Hoekstra for PR1318's four-value theorem, canonical loop method, +normalization, upper construction and explicit open question. Retain the +Swapnil Jain/Douglas Colkitt register/restoration lineage and the distinct +context contributions named in PR1318's unchanged NOTICE: Jeremy Diviney +PR836/PR800, David Govea PR720, Sagar Thakrar PR990 and Richard Hoekstra PR1235. +No predecessor source code is copied into this package. + +## Verification implementation limits + +Power-of-Ten rules 3 and 9 have narrow Python-runtime deviations in `exact.py` +and `verify.py`. Fraction objects, matrix entries, JSON parsing and Python +arithmetic dispatch allocate or dispatch dynamically. Matrix order is capped +at eight, loop alphabets and products have fixed finite bounds, and no search +queue or recursion is used. Receipt inputs are trusted committed package files, +not a service input. Inspectable direct arithmetic and exact endpoint checks +compensate for these runtime constraints. A fixed-capacity native arithmetic +engine would be a separate implementation if runtime guarantees were needed. +All functions fit within 60 physical lines. Warning-strict normal/optimized +replays are the available diagnostics; no optional linter is required. + +## Open next questions + +Can a separately paid additional character-dependent gate reduce the complete +three-source transfer bill? First specify the extra phase gate and its tariff, +then exhibit a complete dirty-restoring word. No such extra gate, physical +invoice or supplier is provided here. Extending a search in the same alphabet +cannot beat the proved call floor. diff --git a/research/three-spectrum-shear/RESULT.json b/research/three-spectrum-shear/RESULT.json new file mode 100644 index 0000000000..319c67f450 --- /dev/null +++ b/research/three-spectrum-shear/RESULT.json @@ -0,0 +1,459 @@ +{ + "canonical_loops": [ + { + "H_i": [ + [ + [ + "0", + "-1" + ], + [ + "1", + "1" + ], + [ + "-1", + "-1" + ], + [ + "0", + "1" + ] + ], + [ + [ + "0", + "0" + ], + [ + "-1", + "0" + ], + [ + "1", + "1" + ], + [ + "0", + "-1" + ] + ], + [ + [ + "0", + "0" + ], + [ + "0", + "0" + ], + [ + "0", + "-1" + ], + [ + "0", + "1" + ] + ] + ], + "H_minus_one": [ + [ + [ + "-1", + "0" + ], + [ + "2", + "0" + ], + [ + "-2", + "0" + ], + [ + "1", + "0" + ] + ], + [ + [ + "0", + "0" + ], + [ + "-1", + "0" + ], + [ + "2", + "0" + ], + [ + "-1", + "0" + ] + ], + [ + [ + "0", + "0" + ], + [ + "0", + "0" + ], + [ + "-1", + "0" + ], + [ + "1", + "0" + ] + ] + ], + "constant_image_rank": 1, + "kernel_basis": [ + [ + [ + "1", + "0" + ], + [ + "1", + "0" + ], + [ + "0", + "0" + ], + [ + "0", + "0" + ] + ], + [ + [ + "0", + "0" + ], + [ + "0", + "0" + ], + [ + "1", + "0" + ], + [ + "1", + "0" + ] + ] + ], + "signs": "+-+-" + }, + { + "H_i": [ + [ + [ + "-1", + "0" + ], + [ + "1", + "1" + ], + [ + "-1", + "-1" + ], + [ + "1", + "0" + ] + ], + [ + [ + "0", + "0" + ], + [ + "0", + "-1" + ], + [ + "1", + "1" + ], + [ + "-1", + "0" + ] + ], + [ + [ + "0", + "0" + ], + [ + "0", + "0" + ], + [ + "-1", + "0" + ], + [ + "1", + "0" + ] + ] + ], + "H_minus_one": [ + [ + [ + "-1", + "0" + ], + [ + "2", + "0" + ], + [ + "-2", + "0" + ], + [ + "1", + "0" + ] + ], + [ + [ + "0", + "0" + ], + [ + "-1", + "0" + ], + [ + "2", + "0" + ], + [ + "-1", + "0" + ] + ], + [ + [ + "0", + "0" + ], + [ + "0", + "0" + ], + [ + "-1", + "0" + ], + [ + "1", + "0" + ] + ] + ], + "constant_image_rank": 2, + "kernel_basis": [ + [ + [ + "1", + "0" + ], + [ + "0", + "0" + ], + [ + "0", + "0" + ], + [ + "0", + "0" + ] + ], + [ + [ + "0", + "0" + ], + [ + "1", + "0" + ], + [ + "1", + "0" + ], + [ + "0", + "0" + ] + ], + [ + [ + "0", + "0" + ], + [ + "0", + "0" + ], + [ + "0", + "0" + ], + [ + "1", + "0" + ] + ] + ], + "signs": "-+-+" + } + ], + "claim_type": "scoped proof", + "controls": [ + "omitted_call_1", + "omitted_call_2", + "omitted_call_3", + "omitted_call_4", + "omitted_call_5", + "omitted_call_6", + "single_active_value_is_insufficient", + "nonidempotent_paid_factor", + "zero_character" + ], + "minimum_calls": 6, + "pair_collapse_cases": 81, + "schema": "three-spectrum-shear/v1", + "source_sha256": { + "research/four-spectrum-shear/PROOF.md": "8b5d44eb6d9392499d2745888d6a25ebfe9db28d6fdeec3e6b7e7ca9c0525aeb", + "research/four-spectrum-shear/README.md": "7faee8876263af16f8c52e24a640d876391516dd85f2b5fcb764bdec5fe4ddd6", + "research/three-spectrum-shear/PROOF.md": "6696d89bd6589d76b36958468b7aa7b2fe1e644762c7a54b8bd793a68e2b2faf", + "research/three-spectrum-shear/README.md": "2c31c35233b34635567e8cb496b872c9a2c0e6794d91744f400809744cb19834", + "research/three-spectrum-shear/SOURCES.json": "4c485f6392b3b42c9654b2ece259dd91909abde831a4d525514a0eb1bfeabd17", + "research/three-spectrum-shear/TASK.json": "a0b9923eb7846ed6eca8dcb71ea138f16effd7ac59a53a7428b88f431e0d0314", + "research/three-spectrum-shear/VERIFY.json": "3159ba1fd530f70faec0f2e70fb56e429356f4add497a49fdf44418c0f10451c", + "research/three-spectrum-shear/exact.py": "23d8daddced7f9b4a65ac796eb6d7895115ac1a0f5b5d0a105a5d05e40fb7b4c", + "research/three-spectrum-shear/verify.py": "506cb022109cefdfd62219f8114521405570a02e24ff86810e20a5e59ed08464" + }, + "spectrum": [ + "1", + "i", + "-1" + ], + "two_value_constraints": { + "determinant_patterns": [ + [ + -1, + -1, + -1, + -1 + ], + [ + -1, + -1, + 1, + 1 + ], + [ + -1, + 1, + -1, + 1 + ], + [ + -1, + 1, + 1, + -1 + ], + [ + 1, + -1, + -1, + 1 + ], + [ + 1, + -1, + 1, + -1 + ], + [ + 1, + 1, + -1, + -1 + ], + [ + 1, + 1, + 1, + 1 + ] + ], + "endpoint_patterns": [ + [ + 1, + -1, + 1, + -1 + ], + [ + 1, + 1, + -1, + -1 + ] + ], + "inverse_values": [ + [ + "0", + "-1" + ], + [ + "-1", + "0" + ] + ], + "negative_first_ratios": [ + [ + "0", + "1" + ], + [ + "1", + "0" + ] + ], + "positive_parameters": [ + [ + "-1", + "1" + ], + [ + "-2", + "0" + ] + ] + }, + "upper_endpoint_samples": 6, + "upper_roles": 8 +} diff --git a/research/three-spectrum-shear/SOURCES.json b/research/three-spectrum-shear/SOURCES.json new file mode 100644 index 0000000000..a8d53feacb --- /dev/null +++ b/research/three-spectrum-shear/SOURCES.json @@ -0,0 +1,30 @@ +{ + "schema_version": 1, + "base_commit": "624de9dc66858af0945e5f8a0942488d62280d43", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "c35482cd9035843b15a634cc8276a7e1e40e8395", + "sha256": "6fe0a099b89aa2aed796a13c3a21dafc63f3388ebf397464e44e0451893b9375" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "f126dd2e2dad2b669e75d1d0d0bd05c600725602", + "sha256": "f7a48bfa2659b88378282a8eee7d9fe52cdf505594124c4d1686b58510fffd72" + }, + { + "path": "research/four-spectrum-shear/PROOF.md", + "usage": "input", + "git_blob": "0256fbde98318fe68bc664be06d736fd2989c49e", + "sha256": "8b5d44eb6d9392499d2745888d6a25ebfe9db28d6fdeec3e6b7e7ca9c0525aeb" + }, + { + "path": "research/four-spectrum-shear/README.md", + "usage": "input", + "git_blob": "4174fb24e52002a6be9494bfae07678d3be1ca5b", + "sha256": "7faee8876263af16f8c52e24a640d876391516dd85f2b5fcb764bdec5fe4ddd6" + } + ] +} diff --git a/research/three-spectrum-shear/TASK.json b/research/three-spectrum-shear/TASK.json new file mode 100644 index 0000000000..8cae68cf1f --- /dev/null +++ b/research/three-spectrum-shear/TASK.json @@ -0,0 +1,66 @@ +{ + "schema_version": 1, + "task_id": "complex-new-helper-inventory", + "priority_revision": 7, + "base_commit": "624de9dc66858af0945e5f8a0942488d62280d43", + "original_card": { + "id": "complex-new-helper-inventory", + "question": "Can a new local cost interface change the deficit-to-recursive-cost ratio beyond current packing?", + "starting_points": [ + "docs/research/research-family-status.md", + "research/complex-local-word-ceiling/README.md", + "research/heterogeneous-owner-assembly/README.md", + "certificates/selected-result.json", + "research/selected-k8-unrestricted-ends/README.md" + ], + "methods": [ + "Propose a changed helper inventory and derive an optimistic exact moment.", + "Design a small completed instance and independently verify its endpoint and rank bill." + ], + "acceptance_gate": "A new physically realizable contract outside the frozen catalogue whose per-call profile, screened with ceiling.ceiling(), beats the selected word's packing ceiling; a lower cap does not establish identical circuitry or order attainable optima, and is insufficient to pass the stronger-budget target under this model. 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", + "research/complex-local-word-ceiling/verify.py" + ], + "expected": "PASS_COMPLEX_LOCAL_WORD_CEILING", + "inspect": "Read the selected word's per-call local profile, its packing ceiling and the lever table; run levers.py for the ideal budget of the lever you target.", + "scope": "Positive control and planning budget only; this is not a new construction or full cold replay." + }, + "first_experiment": "Before any synthesis, write the candidate per-call local profile (and centre charge / unpaid coordinates if changed) and screen it with ceiling.ceiling(); reject it if even the ideal ceiling does not beat the selected word's by your stated margin.", + "bottleneck_link": "Packing of the selected word is capped at +0.87% (ceiling model); only a lower local excess spend or a changed coverage law raises the cap.", + "allowed_variations": [ + "Narrow to one changed boundary or helper type with explicit counts.", + "If the coverage law, template or guard changes, derive an applicable fully charged replacement bound instead of applying the incumbent ceiling outside its scope." + ], + "scope_change_triggers": [ + "Mixing only providers already inside the pinned catalogue.", + "Only changing helper terminal subspaces and monotone frames within the fixed scalar word, entrances and cleanup contract already covered by #1995/#2013.", + "Continuing a partial cost improvement while leaving the same unpriced consumer, restoration or central-readout obligation unresolved; refresh the family expansion decision first. Local product-retiming evidence has a narrow scope and is not a ban on changed graphs or contracts." + ], + "overlap_terms": [ + "helper inventory", + "heterogeneous-owner", + "mutable leaver" + ] + }, + "scope_status": "changed", + "actual_scope": "Resolve PR1318 Open next question 1: exact minimum C/C^-1 calls for a rank-three square-zero shear on spectrum {1,i,-1}, with arbitrary constant complex mixing and restored dirty helpers.", + "scope_change_reason": "An explicitly open algebraic prerequisite replaces the card's construction search. Two active spectral values suffice for a new four-call exclusion; no paid-moment improvement is sought.", + "bottleneck_link": "Scoped side result: decides whether deleting one character value can reduce a three-source same-phase transfer from six calls to four. Physical invoices and supplier admission remain separate.", + "budget_minutes": 60, + "stop_rule": "Stop after the first proved three-value exclusion with exact canonical corroboration. Do not extend to other spectra or larger ranks.", + "outcome": "completed", + "evidence": "PROOF.md gives the quantified proof; generated RESULT.json binds exact two-value constraints, two canonical image ranks, 81 pair-collapse probes, six complete upper endpoints and nine controls.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "Can a separately paid additional character-dependent gate reduce the complete three-source transfer bill?", + "why_it_matters": "The six-call floor holds only for one common C/C^-1 phase alphabet; a changed alphabet could escape it.", + "first_step": "Specify one extra phase gate, its allowed use and physical tariff, then exhibit one complete dirty-restoring word before pricing a supplier.", + "blocked_by": "No extra character-dependent gate or physical tariff is supplied here." + } + ] +} diff --git a/research/three-spectrum-shear/VERIFY.json b/research/three-spectrum-shear/VERIFY.json new file mode 100644 index 0000000000..87352216d0 --- /dev/null +++ b/research/three-spectrum-shear/VERIFY.json @@ -0,0 +1,35 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/four-spectrum-shear/PROOF.md", + "research/four-spectrum-shear/README.md" + ], + "commands": [ + { + "argv": [ + "{python}", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 60, + "checks": "Exact three-value coefficient constraints, canonical loop image ranks, pair-collapse probes, complete dirty six-call endpoint, nine scope/failure controls and source-bound generated receipt." + }, + { + "argv": [ + "{python}", + "-W", + "error", + "-O", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 60, + "checks": "Same complete certificate with assertions disabled; boundary and receipt checks remain active." + } + ] +} diff --git a/research/three-spectrum-shear/exact.py b/research/three-spectrum-shear/exact.py new file mode 100644 index 0000000000..e6ecd2f0b7 --- /dev/null +++ b/research/three-spectrum-shear/exact.py @@ -0,0 +1,107 @@ +"""Bounded exact Q(i) matrices for the three-spectrum certificate.""" +from dataclasses import dataclass +from fractions import Fraction + + +@dataclass(frozen=True) +class Q: + r: Fraction = Fraction(0) + i: Fraction = Fraction(0) + + def __add__(self, other): + return Q(self.r + other.r, self.i + other.i) + + def __neg__(self): + return Q(-self.r, -self.i) + + def __sub__(self, other): + return self + -other + + def __mul__(self, other): + return Q(self.r * other.r - self.i * other.i, + self.r * other.i + self.i * other.r) + + def __truediv__(self, other): + norm = other.r * other.r + other.i * other.i + if norm == 0: + raise ZeroDivisionError('zero Gaussian rational') + return Q((self.r * other.r + self.i * other.i) / norm, + (self.i * other.r - self.r * other.i) / norm) + + def __bool__(self): + return bool(self.r or self.i) + + def encode(self): + return [str(self.r), str(self.i)] + + +ZERO, ONE, I = Q(), Q(Fraction(1)), Q(Fraction(0), Fraction(1)) + + +def identity(n): + if not 1 <= n <= 8: + raise ValueError('matrix order must be between 1 and 8') + return [[ONE if r == c else ZERO for c in range(n)] for r in range(n)] + + +def multiply(a, b): + rows, inner, cols = len(a), len(b), len(b[0]) + assert 1 <= rows <= 8 and 1 <= inner <= 8 and 1 <= cols <= 8 + assert all(len(row) == inner for row in a) + return [[sum((a[r][k] * b[k][c] for k in range(inner)), ZERO) + for c in range(cols)] for r in range(rows)] + + +def rref(matrix): + a = [row[:] for row in matrix] + rows, cols = len(a), len(a[0]) + assert 1 <= rows <= 8 and 1 <= cols <= 8 + assert all(len(row) == cols for row in a) + pivots = [] + for col in range(cols): + choices = [r for r in range(len(pivots), rows) if a[r][col]] + if not choices: + continue + pivot = len(pivots) + a[pivot], a[choices[0]] = a[choices[0]], a[pivot] + scale = a[pivot][col] + a[pivot] = [entry / scale for entry in a[pivot]] + for r in range(rows): + if r != pivot: + scale = a[r][col] + a[r] = [a[r][c] - scale * a[pivot][c] for c in range(cols)] + pivots.append(col) + if len(pivots) == rows: + break + return a, pivots + + +def kernel(matrix): + reduced, pivots = rref(matrix) + cols = len(matrix[0]) + basis = [] + for free in range(cols): + if free in pivots: + continue + vector = [ZERO for _ in range(cols)] + vector[free] = ONE + for r, pivot in enumerate(pivots): + vector[pivot] = -reduced[r][free] + basis.append(vector) + return basis + + +def factor(z, sign, direction, covector): + n = len(direction) + if not 1 <= n <= 8 or n != len(covector) or sign not in (-1, 1): + raise ValueError('invalid factor dimension or sign') + if sum((direction[j] * covector[j] for j in range(n)), ZERO) != ONE: + raise ValueError('paid factor must be a rank-one idempotent') + parameter = (z if sign == 1 else ONE / z) - ONE + unit = identity(n) + return [[unit[r][c] + parameter * direction[r] * covector[c] + for c in range(n)] for r in range(n)] + + +def encode_matrix(matrix): + return [[entry.encode() for entry in row] for row in matrix] diff --git a/research/three-spectrum-shear/verify.py b/research/three-spectrum-shear/verify.py new file mode 100644 index 0000000000..39ab0f964d --- /dev/null +++ b/research/three-spectrum-shear/verify.py @@ -0,0 +1,198 @@ +"""Exact corroboration of the new three-value shear obstruction, not a census.""" +import argparse +import hashlib +import itertools +import json +from pathlib import Path +from fractions import Fraction + +from exact import I, ONE, ZERO, Q, encode_matrix, factor, identity, kernel, multiply, rref + +PACKAGE = Path(__file__).resolve().parent +ROOT = PACKAGE.parents[1] + + +def require(predicate, message): + if not predicate: + raise ValueError(message) + + +def column_matrix(vectors): + return [list(row) for row in zip(*vectors)] + + +def canonical_h(z, first_sign): + directions = [(ONE, ZERO, ZERO, ZERO), (ZERO, ONE, ZERO, ZERO), + (ZERO, ZERO, ONE, ZERO), (ONE, -ONE, ONE, ZERO)] + columns = [] + for beta_slot in range(4): + word = identity(4) + for j in range(4): + beta = ONE if j == beta_slot else ZERO + covector = (ONE, ONE, ONE, beta) + word = multiply(factor(z, first_sign * (-1) ** j, + directions[j], covector), word) + require([row[:3] for row in word[:3]] == identity(3), 'loop on Y') + require(word[3] == identity(4)[3], 'outside input restoration') + columns.append([word[r][3] / (z - ONE) for r in range(3)]) + return column_matrix(columns) + + +def loop_certificate(): + records = [] + for first_sign, expected_rank in ((1, 1), (-1, 2)): + at_i, at_minus = canonical_h(I, first_sign), canonical_h(-ONE, first_sign) + difference = [[at_i[r][c] - at_minus[r][c] for c in range(4)] + for r in range(3)] + basis = kernel(difference) + projected = multiply(at_i, column_matrix(basis)) + require(len(rref(projected)[1]) == expected_rank, 'constant image rank') + expected_basis = ([[ONE, ONE, ZERO, ZERO], [ZERO, ZERO, ONE, ONE]] + if first_sign == 1 else + [[ONE, ZERO, ZERO, ZERO], [ZERO, ONE, ONE, ZERO], + [ZERO, ZERO, ZERO, ONE]]) + require(len(basis) == len(expected_basis), 'constraint nullity') + require(multiply(difference, column_matrix(expected_basis)) == + [[ZERO] * len(expected_basis) for _ in range(3)], 'beta constraints') + records.append({'signs': '+-+-' if first_sign == 1 else '-+-+', + 'H_i': encode_matrix(at_i), 'H_minus_one': encode_matrix(at_minus), + 'kernel_basis': encode_matrix(basis), + 'constant_image_rank': expected_rank}) + return records + + +def paired_collapse(): + cases = 0 + for d_int, u_int, v_int in itertools.product((-1, 1, 2), repeat=3): + d, u, v = Q(Fraction(d_int)), Q(Fraction(u_int)), Q(Fraction(v_int)) + b1 = [ONE, ONE / d, u, v] + b2 = [d * x for x in b1] + a1, a2 = identity(4)[:2] + shear_direction = [a1[j] - d * a2[j] for j in range(4)] + require(sum((b1[j] * shear_direction[j] for j in range(4)), ZERO) == ZERO, + 'square-zero collapse') + for z in (I, -ONE, Q(Fraction(2))): + word = multiply(factor(z, -1, a2, b2), factor(z, 1, a1, b1)) + expected = identity(4) + for r in range(4): + for c in range(4): + expected[r][c] += (z - ONE) * shear_direction[r] * b1[c] + require(word == expected, 'literal paired collapse') + cases += 1 + return cases + + +def upper_word(z, omitted=None): + word = identity(8) + for source in range(3): + a1 = identity(8)[source] + a2 = a1[:] + a2[source + 3] = -ONE + for offset, (sign, direction) in enumerate(((1, a1), (-1, a2))): + if source * 2 + offset != omitted: + word = multiply(factor(z, sign, direction, a1), word) + return word + + +def expected_upper(z): + word = identity(8) + for source in range(3): + word[source + 3][source] = z - ONE + return word + + +def two_value_constraints(): + active = (I, -ONE) + negative_ratio = [-(ONE / z) for z in active] + inverse_values = [ONE / z for z in active] + g = [z - ONE for z in active] + require(negative_ratio[0] != negative_ratio[1], 'negative first-call exclusion') + require(inverse_values[0] != inverse_values[1], 'alternating row constraint') + require(g[0] != g[1], 'positive pair row constraint') + signs = [list(pattern) for pattern in itertools.product((-1, 1), repeat=4) + if sum(pattern) % 4 == 0] + require(len(signs) == 8, 'four-call determinant patterns') + surviving = [s for s in signs if s[0] == 1 and s[-1] == -1] + require(surviving == [[1, -1, 1, -1], [1, 1, -1, -1]], 'endpoint sign screen') + for count in (3, 5): + require(not any(sum(s) % 4 == 0 for s in + itertools.product((-1, 1), repeat=count)), 'odd determinant') + return {'negative_first_ratios': [x.encode() for x in negative_ratio], + 'inverse_values': [x.encode() for x in inverse_values], + 'positive_parameters': [x.encode() for x in g], + 'determinant_patterns': signs, 'endpoint_patterns': surviving} + + +def controls(): + rejected = [] + for omitted in range(6): + require(upper_word(I, omitted) != expected_upper(I), 'omitted-call control') + rejected.append(f'omitted_call_{omitted + 1}') + # At one active value the first-row two-value argument has no exclusion. + require(len(rref([[ONE, -(ONE / I)]])[1]) == 1, 'binary interpolation control') + require(len(rref([[ONE, -(ONE / I)], [ONE, ONE]])[1]) == 2, + 'two active values restore exclusion') + rejected.append('single_active_value_is_insufficient') + try: + factor(I, 1, [ONE, ZERO], [ZERO, ONE]) + except ValueError: + rejected.append('nonidempotent_paid_factor') + else: + raise ValueError('nonidempotent factor was accepted') + try: + _ = ONE / ZERO + except ZeroDivisionError: + rejected.append('zero_character') + else: + raise ValueError('zero character was accepted') + return rejected + + +def source_hashes(): + manifest = json.loads((PACKAGE / 'SOURCES.json').read_text()) + hashes = {} + for row in manifest['files']: + if row['usage'] == 'input': + data = (ROOT / row['path']).read_bytes() + digest = hashlib.sha256(data).hexdigest() + require(digest == row['sha256'], 'predecessor input bytes changed') + hashes[row['path']] = digest + for name in ('README.md', 'PROOF.md', 'TASK.json', 'SOURCES.json', + 'VERIFY.json', 'exact.py', 'verify.py'): + path = PACKAGE / name + hashes[path.relative_to(ROOT).as_posix()] = hashlib.sha256(path.read_bytes()).hexdigest() + return hashes + + +def certificate(): + samples = (ONE, I, -ONE, -I, Q(Fraction(2)), Q(Fraction(1, 2), Fraction(1, 2))) + for z in samples: + require(upper_word(z) == expected_upper(z), 'complete eight-role upper endpoint') + return {'schema': 'three-spectrum-shear/v1', 'claim_type': 'scoped proof', + 'minimum_calls': 6, 'spectrum': ['1', 'i', '-1'], + 'two_value_constraints': two_value_constraints(), + 'canonical_loops': loop_certificate(), 'pair_collapse_cases': paired_collapse(), + 'upper_endpoint_samples': len(samples), 'upper_roles': 8, + 'controls': controls(), 'source_sha256': source_hashes()} + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument('--write', type=Path, help='write a new generated receipt exclusively') + parser.add_argument('--certificate', type=Path, default=PACKAGE / 'RESULT.json') + args = parser.parse_args() + result = certificate() + canonical = json.dumps(result, sort_keys=True, indent=2) + '\n' + if args.write: + with args.write.open('x') as stream: + stream.write(canonical) + else: + loaded = json.loads(args.certificate.read_text()) + require(json.dumps(loaded, sort_keys=True, indent=2) + '\n' == canonical, + 'receipt differs, including value types or source hashes') + print('PASS_THREE_SPECTRUM_SHEAR minimum=6 loops=2 collapse_cases=81 ' + 'upper_samples=6 controls=9 no_new_kappa') + + +if __name__ == '__main__': + main()