diff --git a/research/cyclic-source-root-stock/PROOF.md b/research/cyclic-source-root-stock/PROOF.md new file mode 100644 index 0000000000..507b174ac6 --- /dev/null +++ b/research/cyclic-source-root-stock/PROOF.md @@ -0,0 +1,200 @@ +# Exact root stock for a repeated cyclic source order + +This is a scoped proof in the arbitrary-dirty binary connector model. The +finite replay corroborates it; the universal quantifiers come from this proof. + +## The contract and the theorem + +There are n immutable sources x_j, arbitrary dirty roots z_p, and one distinct +arbitrary dirty target y_m for every nonzero mask m in F2^n. The requested map is + + y_m += A_m(sum_j m_j B_j x_j). + +All roots and sources must restore. Every B_j and A_m occurs exactly twice. +The source projection of the chronological word is fixed to + + w_n = 0,1,...,n-1,0,1,...,n-1. + +Source/output ports may vary per occurrence. Arbitrarily many invertible +scalar binary root frames are permitted. For the lower bound their cost is +relaxed away. The upper construction emits and charges actual root XORs. +No target feedback, source mutation, extra child call, clean full row or +matrix-valued mixing inside a root is admitted. Every complete child preserves +other rows, restores its private scratch, and meets its required frame and +head-return contract. All data and root rows are excluded from child scratch. +Targets remain unobserved until the full batch completes. The A_m and B_j are +arbitrary compatible linear maps; singular, rectangular and noncommuting maps +are allowed. Special identities between fixed maps are outside generic necessity. + +**Theorem.** The minimum number of roots for this fixed source order is + + k(n) = 1 for 1 <= n <= 3, + 2 for n = 4, + n-1 for n >= 5. + +More precisely, for n>=5, a binary reader-support code H containing the all-ones +vector is feasible if and only if codim(H)<=1. This does not determine the +minimum over other source orders. For example, conorholds's PR2182 already +attains n-3 roots for n>=4 using a different source word. + +## The credited root-code reduction + +We use Arham Tahir's PR2795 feasibility criterion, built on conorholds's +normalized source axes in PR2182 and Mason Hale's mandatory-mask method in +PR2282. This is a cited predecessor result, not a rechecked deliverable. +Here is the notation needed for this application. + +In normalized coordinates, the two occurrences of source j inject the same +nonzero axis v_j. Otherwise the arbitrary independent source response would +remain in the restored roots. Let V have these columns and put H=rowspace(V). +Let q_t be the parity vector of source labels in the prefix through cut t, and +D(w)={q_s+q_t}. The two readouts of one A_m must have the same incoming-dirt +covector r, so their source mask is + + m = h AND d, h=rV in H, d=q_s+q_t in D(w). + +The exact unrestricted-frame feasibility criterion is + + {h AND d : h in H, d in D(w)} = F2^n. (1) + +The all-ones mask forces ones in H and ones in D(w). Also dim(H)<=k when there +are k roots. Sufficiency is constructive using paid binary frame changes. +The explicit upper program below realizes the particular code used here +without invoking the predecessor compiler. + +## Repeated order gives exactly the cyclic arcs + +Identify source positions with the cycle C_n. The parity of a contiguous +substring of w_n is a cyclic arc, the empty set, or the full set. A substring +longer than n has the same parity as the complementary shorter cyclic arc, +since a full traversal contributes ones. Every proper nonempty arc occurs as +a substring within the two traversals. Therefore D(w_n) consists exactly of +all cyclic arcs, including empty and full. For n>=1 its size is n(n-1)+2. + +This derivation is specific to the repeated order. Arbitrary paired source +words do not have the same difference set. + +## A rank-two quotient forces a missing mask + +Suppose n>=5 and a feasible H has codimension at least two. Choose a surjective +linear map phi:F2^n -> F2^2 that vanishes on H. Write a_i=phi(e_i). Since +ones belongs to H, + + sum_i a_i=0. (2) + +If i,j are nonadjacent positions of C_n and a_i,a_j are distinct and nonzero, +consider m=ones+e_i+e_j. Any arc d containing the support of m is one of +ones, ones+e_i, ones+e_j. It cannot omit both isolated zero positions, because +the complement of an arc is an arc. Consequently any h with h AND d=m is one +of + + m, ones+e_i, ones+e_j. + +Their images under phi are a_i+a_j, a_i and a_j, respectively. All three are +nonzero. None belongs to H, contradicting (1). Thus feasibility requires that +positions with distinct nonzero a_i values are adjacent in C_n. + +There cannot be three different nonzero values among the a_i: representatives +of all three would form a triangle, absent from C_n for n>=4. Surjectivity +therefore forces exactly two distinct nonzero values a,b. They are linearly +independent over F2. By (2), each occurs an even number of times, hence at +least twice. Every a-position must be adjacent to every b-position. Selecting +two of each would give a K2,2 subgraph, a four-cycle. A cycle C_n for n>=5 has +no such subgraph. This contradiction proves codim(H)<=1 and k>=n-1. + +The proof supplies an explicit missing mask for every rank-two quotient; +it is not an extrapolation from a finite source-count census. + +## Every eligible hyperplane is feasible + +Let H=ker(u dot -) with nonzero u and u dot ones=0. For any m in H, choose h=m +and d=ones. If m is outside H, then + + u dot (ones+m)=1. + +Hence some position j with m_j=0 has u_j=1. Put h=m+e_j and d=ones+e_j. +Then h belongs to H, d is a cyclic arc, and h AND d=m. Thus every hyperplane +containing ones is feasible. Full space is feasible as well. Combined with +the obstruction, this proves the stated classification for n>=5. + +## An explicit attaining dirty-root program + +For n>=5, take k=n-1 roots and the code H={h:h_0=h_1}. Inject B0 and B1 at +root zero and inject B_j at root j-1 for j>=2. Repeat these exact ports in +the second source traversal. All roots restore after the two traversals. + +For each nonzero m, choose the following h and two source cuts s,t. + +- If m_0=m_1, take h=m and (s,t)=(0,n). +- Otherwise let j be the missing position in {0,1}; take h=m+e_j and + (s,t)=(j+1,j+n). + +In the first case q_s+q_t=ones. In the second it is ones+e_j. Both give +h AND (q_s+q_t)=m. The reader covector in the k roots is + + r=(h_0,h_2,h_3,...,h_(n-1)). + +It is nonzero. Choose the first nonzero position p of r. To read A_m at +one of its cuts, execute z_p+=z_q for every other position q in support(r), +read A_m from z_p, then undo those XORs in reverse order. This restores the +entire root vector after each readout block. Both readouts see exactly the +same root-dirt combination and cancel it. The residual is precisely the +requested A_m applied to the B_j responses. All target blocks can coexist +at their designated source cuts because targets are distinct and every +readout block leaves the roots unchanged. + +This argument retains A_m B_j in the correct order. It never commutes the +maps or assumes clean dirt. Root shears act only between equal-sized root +rows; arbitrary compatible source and output dimensions are allowed. + +The exact child incidence is 2n B calls and 2(2^n-1) A calls. Each output +pays 4(wt(r)-1) root XORs across its two readouts. Summing over all nonzero +m gives + + sum_m wt(r) = 3*2^(n-2)+(n-2)*2^(n-1), + root XOR count = (2n-5)*2^n+4. (3) + +The first term counts masks having either low bit set. The other terms count +each independent higher bit. Every mask except zero contributes the minus +one in wt(r)-1. These are attaining counts for this program, not an optimal +transfer tariff. + +Let c_Bj(p), c_Am(p), and c_X(p,q) be complete actual-port call prices, including +required access, updates, private-scratch cleanup, head returns and frames. +Let I pay admission, root reservation, scheduling and any initial layout; +P pay reusable preparation; D pay actual instruction storage, reads and +dispatch. With p_m the pivot above, the complete abstract bill is + + I+P+D + 2 sum_j c_Bj(port_j) + 2 sum_m c_Am(p_m) + + 4 sum_m sum_(q in support(r_m), q!=p_m) c_X(p_m,q). + +Reserve (n-1)L dirty root cells, all source/target rows, and each child's +separate private scratch. The instruction template is O(n*2^n) records and +is generated from the explicit mask/cut formulas. No control generation, +head movement, preparation or physical hosting cost is assigned zero. +An actual recursive caller and its profitability remain unknown. + +## Small exceptions + +At n<=3, every mask is a cyclic arc, so H= and one root suffice. +An active source and nonzero requested output require at least one root. +For n=4, D(w_4) omits exactly 0101 and 1010. A one-dimensional code containing +ones is , so it fails. The two-dimensional code spanned by 0101 and +1010 succeeds: all arc masks use h=ones; the two missing masks use h=m and +d=ones. This also explains why the no-four-cycle step must exclude n=4. +The verifier emits actual two-root readout blocks for this exception. + +## Verification boundary + +The written proof is uniform in n and positive row size. The replay checks +all 3,290 codes containing ones at n=1..7; every rank-two quotient killing +ones at n=5..9, totaling 85,818; cyclic-arc equality and literal dirty-root +programs at n=1..10; and all 236 single-operation omissions at n=5. The +n=5,6 quotient witnesses also undergo direct full kernel/difference checking. +These are original fixed-order instances, not predecessor minima replays. +The root program uses free response symbols and separate A_m image spaces, +so root dirt, target dirt and noncommutative map order remain explicit. + +No physical implementation, complete recursive invoice, supplier admission, +new kappa, arbitrary-word root minimum or full multiplication theorem follows. +Independent human and formal proof-kernel review are unclaimed. diff --git a/research/cyclic-source-root-stock/README.md b/research/cyclic-source-root-stock/README.md new file mode 100644 index 0000000000..22473e5485 --- /dev/null +++ b/research/cyclic-source-root-stock/README.md @@ -0,0 +1,118 @@ +# Sharp dirty-root stock for repeated cyclic source order + +A scoped proof gives the exact root minimum for the fixed source projection +`B0 ... B(n-1) B0 ... B(n-1)` in the arbitrary-dirty binary connector model. +Every source and every nonzero-mask output is called exactly twice. With +unrestricted paid scalar binary frames and per-occurrence ports, the minimum +is **n-1 roots for every n>=5**. The small minima are one root at n=1,2,3 and +two at n=4. + +The [proof](PROOF.md) applies Arham Tahir's PR2795 root-code criterion to a new +fixed-order question. A rank-two quotient would force two nonadjacent positions +with different nonzero labels. Their complementary mask is unreachable. +Avoiding that witness would require a four-cycle inside a longer cycle. +Conversely, every parity hyperplane containing ones is feasible. Thus for +n>=5 the feasible reader codes are exactly full space and those hyperplanes. + +Source order alone can consume extra dirty stock despite identical child +incidence. Conorholds's PR2182 uses a different source word and already attains +n-3 roots for n>=4. This package classifies the repeated-order family; it does +not improve or replay that predecessor construction. + +The explicit upper program pays 2n source calls, 2(2^n-1) output readouts, +and `(2n-5)*2^n+4` full-row root XORs for n>=5. At n=5 it has four roots, +10 source calls, 62 readouts and 164 root XORs. Every readout computes one +root combination, reads it, and uncomputes it. The proof gives complete +actual-port price expressions and reserves all arbitrary dirt. This is a +root-stock optimum, not a transfer-cost optimum or a profitable supplier. +No new kappa or selected-frontier change is claimed. + +## Reproduce + +From the worktree root, with the standard library only: + +```sh +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -W error -B research/cyclic-source-root-stock/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/cyclic-source-root-stock +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/cyclic-source-root-stock --check-source-history +``` + +The manifest runs both normal and optimized warning-strict verifiers. Expected: + +```text +PASS_CYCLIC_SOURCE_ROOT_STOCK codes=3290 quotients=85818 omissions=236 roots=n-1_for_n>=5 +``` + +The exact replay covers all 3,290 codes containing ones at n=1..7 and all +85,818 surjective rank-two quotients killing ones at n=5..9. At n=5,6 each +quotient's missing mask is separately checked against its entire kernel and +prefix-difference set. Literal forward/inverse dirty programs and cyclic-arc +identities cover n=1..10. All 236 operation omissions at n=5 reject, as do nine +invalid argument cases; the n=4 four-cycle exception is a positive control. +Universal scope comes from the written proof, rather than those finite counts. + +[RESULT.json](RESULT.json) is generated by `verify.py --emit`, not handwritten. +It binds the six local source/metadata files and records the enumerated results. +The default replay recomputes the receipt and compares JSON with types retained. +From an exported package, `python3.12 -I -O -W error -B verify.py` needs no Git, +network, solver or predecessor executable. A new receipt must first be emitted +to the external run directory and compared before publication. + +## Scope, credit and provenance + +This contribution was produced by Nick Petalas. Apache-2.0. Independent human +and formal proof-kernel review are unclaimed. + +Credit Arham Tahir / PR2795 for the exact root-code feasibility criterion; +conorholds / PR2182 for normalized source axes, the multi-root contract and +its differently ordered attaining star; Mason Hale / PR2282 for mandatory-mask +methods; Ross Richardson / PR934/PR943 for the dirty connector and prefix model; +and Douglas Colkitt / PR1185 and the retained common-factor/commutator lineage. +Their exact main-tree README blobs are pinned as provenance in SOURCES.json. +No predecessor implementation is imported. Classical linear algebra and the +elementary cycle facts are not claimed as new mathematics. + +Card `connector-alphabet-change` has explicitly changed scope to an original +source-order/root-stock theorem. It is a self-contained interface side result, +not completion of a selected-supplier handoff. Canonical base is +`624de9dc66858af0945e5f8a0942488d62280d43`, priority revision 7; the selected +conditional kappa remains 0.00302015. The card's prescribed positive control +passed before this fixed-order investigation. No historical scientific audit +or selected cold replay is this contribution's deliverable. + +Entry overlap covered 411 open PRs and 3,919 Discussion/comment/reply records. +The sparse helper searched 117 of 6,319 main-tree notes; separate distinctive +all-main README and merged-term searches supplemented it. Live claims and this +account's recent submissions were checked. Unpublished work and arbitrary code +diffs remain coverage limits; absence of a match does not certify novelty. +The [advance claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19134262) +records the exact target. + +## Open next questions + +- Can a specified other double-permutation order have a closed-form root + minimum? Begin with one changed source order and its exact difference set. + The obstruction here relies on the cyclic-arc support and does not transfer + automatically. No larger root-code search is justified without that question. +- Can a real recursive caller expose this repeated source order and benefit + from reordering its children? Start with the caller's full chronology, stable + ports and live-root ledger. Physical access, scheduling, restoration and + completed consumer costs are missing, so no adoption benefit is established. + +## Code bounds + +The verifier has no recursion, external processes or mutable shared state. +Source count is capped at ten; RREF inventory dimension at six; quotient words +at nine. At most 2,825 code sets are retained at once, each with at most 128 +masks; compiled programs are capped at 45,000 records. Functions are under +60 physical lines. Always-enabled `require` checks retain all conditions under +`-O`; warning-strict normal/optimized registered runs check the actual artifact. + +Power-of-Ten rule 3 has a managed-runtime deviation in verify.py. Python's +integers, sets, tuples and JSON allocate during enumeration. The fixed domains, +streamed quotient inventory, bounded program size and 100,000-byte receipt +limit bound live allocations. No fixed-pool implementation or byte-exact runtime +heap bound is claimed. If the replay caps expand, first reassess these bounds +or introduce fixed-capacity storage. Rules 8 and 9 use ordinary direct Python +functions; standard-library iterators and JSON dispatch have fixed targets and +bounded inputs. No unavailable compiler diagnostic is claimed as run. diff --git a/research/cyclic-source-root-stock/RESULT.json b/research/cyclic-source-root-stock/RESULT.json new file mode 100644 index 0000000000..2104545c59 --- /dev/null +++ b/research/cyclic-source-root-stock/RESULT.json @@ -0,0 +1,238 @@ +{ + "result": { + "boundary_rejections": 9, + "claim_type": "scoped proof with finite exact corroboration", + "code_census": [ + { + "codes": 1, + "feasible_by_dimension": [ + 0, + 1 + ], + "minimum": 1, + "n": 1 + }, + { + "codes": 2, + "feasible_by_dimension": [ + 0, + 1, + 1 + ], + "minimum": 1, + "n": 2 + }, + { + "codes": 5, + "feasible_by_dimension": [ + 0, + 1, + 3, + 1 + ], + "minimum": 1, + "n": 3 + }, + { + "codes": 16, + "feasible_by_dimension": [ + 0, + 0, + 1, + 7, + 1 + ], + "minimum": 2, + "n": 4 + }, + { + "codes": 67, + "feasible_by_dimension": [ + 0, + 0, + 0, + 0, + 15, + 1 + ], + "minimum": 4, + "n": 5 + }, + { + "codes": 374, + "feasible_by_dimension": [ + 0, + 0, + 0, + 0, + 0, + 31, + 1 + ], + "minimum": 5, + "n": 6 + }, + { + "codes": 2825, + "feasible_by_dimension": [ + 0, + 0, + 0, + 0, + 0, + 0, + 63, + 1 + ], + "minimum": 6, + "n": 7 + } + ], + "constructions": [ + { + "n": 1, + "readouts": 2, + "root_shears": 0, + "roots": 1, + "source_calls": 2 + }, + { + "n": 2, + "readouts": 6, + "root_shears": 0, + "roots": 1, + "source_calls": 4 + }, + { + "n": 3, + "readouts": 14, + "root_shears": 0, + "roots": 1, + "source_calls": 6 + }, + { + "n": 4, + "readouts": 30, + "root_shears": 36, + "roots": 2, + "source_calls": 8 + }, + { + "n": 5, + "readouts": 62, + "root_shears": 164, + "roots": 4, + "source_calls": 10 + }, + { + "n": 6, + "readouts": 126, + "root_shears": 452, + "roots": 5, + "source_calls": 12 + }, + { + "n": 7, + "readouts": 254, + "root_shears": 1156, + "roots": 6, + "source_calls": 14 + }, + { + "n": 8, + "readouts": 510, + "root_shears": 2820, + "roots": 7, + "source_calls": 16 + }, + { + "n": 9, + "readouts": 1022, + "root_shears": 6660, + "roots": 8, + "source_calls": 18 + }, + { + "n": 10, + "readouts": 2046, + "root_shears": 15364, + "roots": 9, + "source_calls": 20 + } + ], + "interval_checks": [ + { + "masks": 2, + "n": 1 + }, + { + "masks": 4, + "n": 2 + }, + { + "masks": 8, + "n": 3 + }, + { + "masks": 14, + "n": 4 + }, + { + "masks": 22, + "n": 5 + }, + { + "masks": 32, + "n": 6 + }, + { + "masks": 44, + "n": 7 + }, + { + "masks": 58, + "n": 8 + }, + { + "masks": 74, + "n": 9 + }, + { + "masks": 92, + "n": 10 + } + ], + "omission_rejections": 236, + "quotient_census": [ + { + "n": 5, + "rank_two_quotients": 210 + }, + { + "n": 6, + "rank_two_quotients": 930 + }, + { + "n": 7, + "rank_two_quotients": 3906 + }, + { + "n": 8, + "rank_two_quotients": 16002 + }, + { + "n": 9, + "rank_two_quotients": 64770 + } + ] + }, + "schema": "cyclic-source-root-stock/v1", + "sources_sha256": { + "PROOF.md": "6a3235505fb4bdab925930e8c6b4358000e9b1ecae24ad8a7839635bd191c1ae", + "README.md": "9ba1ded6ff11c7a319a8626deec96156ac679dfa96b53571ad4f485ca4ab2286", + "SOURCES.json": "2fab2f56d4e028b3cc04f1f22b4ea50bd41b19beda2d5f00c268d9a2db6ca7a1", + "TASK.json": "b05cc8eb6a28a21f07996626c8b468dac422a7c902e9291a6422ece624c2ee78", + "VERIFY.json": "f5db8220e2d4b2e1f453e23469246ef25cd5be4328320effaa5b2ff29684683f", + "verify.py": "698957e201bfbdd694d24c81b4a5691cabaed79be7425158e4cbd02da875593d" + } +} diff --git a/research/cyclic-source-root-stock/SOURCES.json b/research/cyclic-source-root-stock/SOURCES.json new file mode 100644 index 0000000000..82ae89b236 --- /dev/null +++ b/research/cyclic-source-root-stock/SOURCES.json @@ -0,0 +1,42 @@ +{ + "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/eight-source-root-code/README.md", + "usage": "provenance", + "git_blob": "ce5d5add72a7b57bb17cc339d9fda4bb0592160c", + "sha256": "8a9100409033acfc0ede9fa260c0172c958e5103a244b1de97b7e132659038d0" + }, + { + "path": "research/scalable-dirty-connectors/README.md", + "usage": "provenance", + "git_blob": "dc3f9202735a5d55e95e34e64746f4afb74bfba6", + "sha256": "3484f6454736045ea4a6ab6e67710cce9a238ada28d61d694aed4c4b017c78d5" + }, + { + "path": "research/seven-source-root-minimum/README.md", + "usage": "provenance", + "git_blob": "2fac5ab937d94856e55fd753d067f2f6f8ada111", + "sha256": "17554797cf3a8752ef3f8b65b0d7fc9e98f7f99f3afb5dbb1b0952fbf9f1fd58" + }, + { + "path": "research/universal-connector-boundary/README.md", + "usage": "provenance", + "git_blob": "d277f7c5830b1f2bc42e1ff41ab86e7d7564929f", + "sha256": "23415f7829ab8d80a783142f10f7d31abbce84579362769984680af3df954476" + } + ] +} diff --git a/research/cyclic-source-root-stock/TASK.json b/research/cyclic-source-root-stock/TASK.json new file mode 100644 index 0000000000..b56194c331 --- /dev/null +++ b/research/cyclic-source-root-stock/TASK.json @@ -0,0 +1,76 @@ +{ + "schema_version": 1, + "task_id": "connector-alphabet-change", + "priority_revision": 7, + "base_commit": "624de9dc66858af0945e5f8a0942488d62280d43", + "original_card": { + "id": "connector-alphabet-change", + "question": "Does one explicit extension of the connector alphabet offer a favorable completed budget?", + "starting_points": [ + "docs/research/research-family-status.md", + "research/universal-connector-boundary/README.md", + "certificates/selected-result.json" + ], + "methods": [ + "Construct and charge a legal extra operation on a minimal instance.", + "Prove a target-specific bound after adding one specified operation family." + ], + "acceptance_gate": "State which fixed-alphabet premise changes and charge its implementation; do not declare it free. 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/universal-connector-boundary/verify.py" + ], + "expected": "PASS_UNIVERSAL_CONNECTOR_BOUNDARY", + "inspect": "Reproduce the 945-pairing control, then read Exact interface to list the allowed calls.", + "scope": "Positive control / source-bound orientation only; this is not a new construction or full cold replay." + }, + "first_experiment": "Add exactly one legally priced operation and test a tiny dirty-input instance before enumerating larger cases.", + "bottleneck_link": "A new legal connector operation could change recursive interface cost; a larger census in the same alphabet is a separate side result.", + "allowed_variations": [ + "Choose one additional operation and a small source count for its first counterexample." + ], + "scope_change_triggers": [ + "Keeping the alphabet and only increasing the source count; record this as a changed assignment.", + "Extending a source-count census without naming a supplier/interface decision it could change; audit #2973 pruning concerns before relying on the affected predecessor exclusions." + ], + "overlap_terms": [ + "universal connector", + "source-toggle", + "connector alphabet" + ] + }, + "scope_status": "changed", + "actual_scope": "Exact dirty-root minimum for the fixed source word 0,1,...,n-1,0,1,...,n-1 with two calls per generic binary source/output map and unrestricted paid scalar root frames.", + "scope_change_reason": "Replace an alphabet-extension experiment by an original source-order/root-stock theorem using the credited root-code criterion. This is a scoped interface side result, not a selected-supplier improvement.", + "bottleneck_link": "Child incidence alone does not control dirty-root stock. A repeated source order forces n-1 roots for n>=5, whereas a credited differently ordered star attains n-3. Actual caller access and complete cost remain unknown.", + "budget_minutes": 60, + "stop_rule": "Stop at the first written exact root-stock theorem with bounded exact corroboration; package that result without extending source-order or transfer-cost scope.", + "outcome": "completed", + "evidence": "PROOF.md gives the universal fixed-order classification and a paid upper program. verify.py enumerates new fixed-order code and quotient domains, literal endpoints, and omission controls; generated RESULT.json binds local source hashes.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "Does one specified other double-permutation source order have a closed-form root minimum?", + "why_it_matters": "It could distinguish source-order effects on dirty stock without a new arbitrary-word census.", + "first_step": "Specify one changed order and derive its exact prefix-difference support.", + "blocked_by": "The cyclic-arc obstruction does not apply to general orders; no new expansion is claimed." + }, + { + "question": "Does an actual recursive caller expose the repeated order and benefit from reordering?", + "why_it_matters": "A root-stock obstruction matters to the multiplier only through an actual completed caller.", + "first_step": "Pin one caller and list chronological child ports, live roots and restoration obligations.", + "blocked_by": "No physical caller, complete access/consumer bill or supplier admission is supplied." + } + ], + "claim_url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19134262", + "overlap": { + "open_prs": 411, + "discussion_records": 3919, + "local_notes_searched": 117, + "local_notes_in_head": 6319, + "limits": "Sparse note omissions supplemented by distinctive all-main README and merged-term searches; arbitrary diffs and unpublished work not covered." + } +} diff --git a/research/cyclic-source-root-stock/VERIFY.json b/research/cyclic-source-root-stock/VERIFY.json new file mode 100644 index 0000000000..851a489ae2 --- /dev/null +++ b/research/cyclic-source-root-stock/VERIFY.json @@ -0,0 +1,32 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [], + "commands": [ + { + "argv": [ + "{python}", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 180, + "checks": "Recompute the new fixed-order code and quotient domains, literal arbitrary-dirty endpoints, source/readout incidence and every n=5 operation omission; compare source-bound receipt." + }, + { + "argv": [ + "{python}", + "-O", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 180, + "checks": "Retain the same exact evidence and rejection checks with optimized Python." + } + ] +} diff --git a/research/cyclic-source-root-stock/verify.py b/research/cyclic-source-root-stock/verify.py new file mode 100644 index 0000000000..1493ce96e7 --- /dev/null +++ b/research/cyclic-source-root-stock/verify.py @@ -0,0 +1,286 @@ +#!/usr/bin/env python3 +"""Exact corroboration of the fixed cyclic-source root-stock theorem.""" + +import argparse +import hashlib +import itertools +import json +from pathlib import Path + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def dimension(n): + require(type(n) is int and 1 <= n <= 10, "source count must be 1..10") + + +def span(basis): + require(len(basis) <= 10, "basis exceeds replay capacity") + result = [0] + for vector in basis: + result += [value ^ vector for value in result] + return frozenset(result) + + +def differences(n): + dimension(n) + prefixes = [0] + for label in list(range(n)) * 2: + prefixes.append(prefixes[-1] ^ (1 << label)) + return {left ^ right for left in prefixes for right in prefixes} + + +def arcs(n): + dimension(n) + result = {0, (1 << n) - 1} + for start in range(n): + mask = 0 + for length in range(1, n): + mask |= 1 << ((start + length - 1) % n) + result.add(mask) + return result + + +def all_subspaces(d): + """Unique binary RREF bases, with every rank included, for d <= 6.""" + require(type(d) is int and 0 <= d <= 6, "RREF dimension must be 0..6") + for rank in range(d + 1): + for pivots in itertools.combinations(range(d), rank): + free = [(row, col) for row, pivot in enumerate(pivots) + for col in range(pivot + 1, d) if col not in pivots] + for assignments in range(1 << len(free)): + basis = [1 << pivot for pivot in pivots] + for index, (row, col) in enumerate(free): + if (assignments >> index) & 1: + basis[row] |= 1 << col + yield span(basis) + + +def code_census(): + rows = [] + expected_codes = [1, 2, 5, 16, 67, 374, 2825] + expected_minimum = [1, 1, 1, 2, 4, 5, 6] + for n in range(1, 8): + ones = (1 << n) - 1 + ds = differences(n) + seen = set() + feasible_by_dimension = [0] * (n + 1) + for subspace in all_subspaces(n - 1): + code = frozenset(subspace | {value ^ ones for value in subspace}) + require(code not in seen, "duplicate code in complete inventory") + seen.add(code) + covered = {h & d for h in code for d in ds} + if len(covered) == 1 << n: + feasible_by_dimension[len(code).bit_length() - 1] += 1 + minimum = next(k for k, count in enumerate(feasible_by_dimension) if count) + require(len(seen) == expected_codes[n - 1], "incomplete code domain") + require(minimum == expected_minimum[n - 1], "wrong root minimum") + if n >= 5: + require(feasible_by_dimension[n - 1:] == [(1 << (n - 1)) - 1, 1], + "hyperplane classification differs") + rows.append({"n": n, "codes": len(seen), "minimum": minimum, + "feasible_by_dimension": feasible_by_dimension}) + return rows + + +def quotient(vector, columns): + result = 0 + for index, column in enumerate(columns): + if (vector >> index) & 1: + result ^= column + return result + + +def quotient_census(): + """Every surjective rank-two quotient killing ones, n=5..9.""" + rows = [] + for n in range(5, 10): + count = 0 + for prefix in itertools.product(range(4), repeat=n - 1): + last = 0 + for value in prefix: + last ^= value + columns = prefix + (last,) + if len(set(columns) - {0}) < 2: + continue + count += 1 + pairs = [(i, j) for i in range(n) for j in range(i + 1, n) + if (j - i) not in (1, n - 1) and columns[i] and columns[j] + and columns[i] != columns[j]] + require(bool(pairs), "rank-two cyclic obstruction has no witness") + i, j = pairs[0] + ones = (1 << n) - 1 + missing = ones ^ (1 << i) ^ (1 << j) + for candidate in (missing, missing ^ (1 << i), missing ^ (1 << j)): + require(quotient(candidate, columns) != 0, "invalid quotient witness") + if n <= 6: + kernel = [h for h in range(1 << n) if quotient(h, columns) == 0] + require(all((h & d) != missing for h in kernel for d in differences(n)), + "direct coverage accepts a claimed missing mask") + require(count == 4 ** (n - 1) - 3 * 2 ** (n - 1) + 2, + "wrong surjective quotient domain") + rows.append({"n": n, "rank_two_quotients": count}) + return rows + + +def reader(n, mask): + dimension(n) + require(type(mask) is int and 0 < mask < 1 << n, "invalid output mask") + if n >= 5: + h = mask + if (mask & 1) == ((mask >> 1) & 1): + cuts = (0, n) + else: + absent = 0 if not (mask & 1) else 1 + h |= 1 << absent + cuts = (absent + 1, absent + n) + return (h & 1) | ((h >> 2) << 1), cuts + axes = [1] * n if n <= 3 else [1, 2, 1, 2] + prefixes = [0] + for label in list(range(n)) * 2: + prefixes.append(prefixes[-1] ^ (1 << label)) + for r in range(1, 2 if n <= 3 else 4): + h = sum(((r & axis).bit_count() % 2) << j for j, axis in enumerate(axes)) + for left in range(2 * n + 1): + for right in range(left + 1, 2 * n + 1): + if h & (prefixes[left] ^ prefixes[right]) == mask: + return r, (left, right) + raise ValueError("small attaining code lacks a mask") + + +def program(n): + dimension(n) + roots = 1 if n <= 3 else 2 if n == 4 else n - 1 + ports = [0] * n if n <= 3 else [0, 1, 0, 1] if n == 4 else [0, 0] + list(range(1, n - 1)) + schedule = [[] for _ in range(2 * n + 1)] + for mask in range(1, 1 << n): + covector, cuts = reader(n, mask) + support = [j for j in range(roots) if (covector >> j) & 1] + require(bool(support), "zero reader cannot serve a nonzero output") + pivot = support[0] + block = [("X", pivot, j) for j in support[1:]] + block += [("A", mask, pivot)] + block += [("X", pivot, j) for j in reversed(support[1:])] + for cut in cuts: + schedule[cut].extend(block) + word = [] + for cut, blocks in enumerate(schedule): + word.extend(blocks) + if cut < 2 * n: + label = cut % n + word.append(("B", label, ports[label])) + require(len(word) <= 2 * n + 2 * ((1 << n) - 1) + 4 * (roots - 1) * ((1 << n) - 1), + "compiled word exceeds its finite invoice") + return roots, word + + +def endpoint(n, roots, word): + """Free linear response symbols retain arbitrary root dirt and map order.""" + dimension(n) + require(1 <= roots <= n and len(word) <= 45000, "program exceeds replay capacity") + z = [1 << j for j in range(roots)] + # Each target has its own A_m image space; bit roots+n is its untouched dirt. + dirt = 1 << (roots + n) + y = [dirt] * (1 << n) + for kind, left, right in word: + if kind == "X": + z[left] ^= z[right] + elif kind == "B": + z[right] ^= 1 << (roots + left) + elif kind == "A": + y[left] ^= z[right] + else: + raise ValueError("unknown operation") + return (z == [1 << j for j in range(roots)] + and y == [dirt ^ (mask << roots) for mask in range(1 << n)]) + + +def construction_checks(): + rows = [] + for n in range(1, 11): + roots, word = program(n) + require(endpoint(n, roots, word), "wrong dirty endpoint") + require(endpoint(n, roots, list(reversed(word))), "inverse endpoint differs") + sources = [left for kind, left, _ in word if kind == "B"] + require(sources == list(range(n)) * 2, "source order changed") + outputs = [0] * (1 << n) + for kind, left, _ in word: + if kind == "A": + outputs[left] += 1 + require(outputs == [0] + [2] * ((1 << n) - 1), "readout incidence changed") + shears = sum(kind == "X" for kind, _, _ in word) + if n >= 5: + require(shears == (2 * n - 5) * (1 << n) + 4, "wrong explicit shear bill") + rows.append({"n": n, "roots": roots, "source_calls": len(sources), + "readouts": sum(outputs), "root_shears": shears}) + roots, word = program(5) + for index in range(len(word)): + require(not endpoint(5, roots, word[:index] + word[index + 1:]), + "single omitted operation escaped") + return rows, len(word) + + +def boundary_controls(): + rejected = 0 + for invalid in (0, 11, -1, True, 5.0): + try: + program(invalid) + except ValueError: + rejected += 1 + require(rejected == 5, "source-count validation failed") + for mask in (0, 32, -1, True): + try: + reader(5, mask) + except ValueError: + rejected += 1 + require(rejected == 9, "mask validation failed") + # C4 contains K2,2: alternating quotient columns are a real exception. + columns = (1, 2, 1, 2) + kernel = [h for h in range(16) if quotient(h, columns) == 0] + require(len({h & d for h in kernel for d in differences(4)}) == 16, + "four-cycle exception lost") + return rejected + + +def compute(): + interval_checks = [] + for n in range(1, 11): + ds = differences(n) + require(ds == arcs(n), "prefix differences are not exactly cyclic arcs") + require(len(ds) == n * (n - 1) + 2, "wrong cyclic-arc count") + interval_checks.append({"n": n, "masks": len(ds)}) + constructions, omissions = construction_checks() + return {"claim_type": "scoped proof with finite exact corroboration", + "interval_checks": interval_checks, "code_census": code_census(), + "quotient_census": quotient_census(), "constructions": constructions, + "omission_rejections": omissions, "boundary_rejections": boundary_controls()} + + +def receipt(): + root = Path(__file__).resolve().parent + files = ("verify.py", "README.md", "PROOF.md", "TASK.json", "SOURCES.json", "VERIFY.json") + hashes = {name: hashlib.sha256((root / name).read_bytes()).hexdigest() for name in files} + return {"schema": "cyclic-source-root-stock/v1", "sources_sha256": hashes, "result": compute()} + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--emit", action="store_true", help="print a generated receipt instead of comparing it") + args = parser.parse_args() + actual = receipt() + if args.emit: + print(json.dumps(actual, sort_keys=True, indent=2)) + return + expected_path = Path(__file__).resolve().with_name("RESULT.json") + require(expected_path.stat().st_size <= 100000, "receipt exceeds capacity") + expected = json.loads(expected_path.read_text()) + require(json.dumps(expected, sort_keys=True) == json.dumps(actual, sort_keys=True), + "source-bound receipt differs") + print("PASS_CYCLIC_SOURCE_ROOT_STOCK codes=3290 quotients=85818 omissions=236 roots=n-1_for_n>=5") + + +if __name__ == "__main__": + main()