diff --git a/research/z4-directed-cycle-fanout/PROOF.md b/research/z4-directed-cycle-fanout/PROOF.md new file mode 100644 index 0000000000..beb32bf293 --- /dev/null +++ b/research/z4-directed-cycle-fanout/PROOF.md @@ -0,0 +1,73 @@ +# Six is the exact directed-cycle price + +Let R=Z/4, w>=1 and take arbitrary independent a,b,c,p in R^w. The dirty +rows start at a,b,c. The disjoint source p cannot be written. The gate +E_ij(alpha) adds alpha A_j into A_i, for distinct dirty rows i,j; P_i(beta) +adds beta p into A_i. Every nonzero coefficient is allowed. The gate types +E_10, E_21, E_02 and P_0 cost one; the remaining five types cost 100. +Prices are stationary and coefficient-independent. No other operations, +workspace, observations or free basis changes are available. Words are fixed, +finite and may have arbitrary repetitions and interleavings. The required +endpoint is (a+2p,b+p,c+p,p) on every input. + +## Attainment + +Execute chronologically + +```text +E_21(-1), E_10(-1), P_0(1), E_10(1), P_0(1), E_21(1). +``` + +The first two gates leave (a,b-a,c-b). After the first insertion and next +ADD they are (a+p,b+p,c-b). The last insertion and ADD give +(a+2p,b+p,c+p). Every gate costs one; the complete price is six. The source +never changes. The identities hold coordinatewise at every positive width, +retaining all original dirt. + +## No word can cost less + +Track the three-by-three matrix M of original dirt coefficients. Every +prefix is invertible, because each ADD has its negated-coefficient inverse +and insertions leave M unchanged. The endpoint requires M=I. + +Recall the incoming-row return argument of #5045/#5163. A row cannot receive +exactly one nonzero ADD. Before its unique incoming ADD its dirt row is e_i. +If that gate is E_ij(alpha), restoration with no later incoming ADD requires +alpha m_j=0, where m_j is row j of the invertible prefix M. Right multiplication +by M inverse gives alpha e_j=0, hence alpha=0, a contradiction. This counts +total arrivals at a row, not individual directed edges. + +Suppose a word costs less than six. It uses only price-one gates, so every +source insertion is into row zero. Let t be the number of insertions. Rows +one and two each have a nonzero final source coefficient and no insertion +of their own. Each must receive an ADD, hence at least two by the return +argument. + +If t=0, every source coefficient remains zero, which is impossible. If +t>=2, its price is at least t+2+2>=6, a contradiction. + +For t=1, write beta for the inserted coefficient. The final source column +is beta v, since every subsequent gate is R-linear. Its row-one coefficient +is 1, so beta is a unit. If row zero receives no ADD, its final source +coefficient is beta, which cannot equal the required nonunit 2. Row zero +therefore receives at least one ADD, and hence at least two. The price is +at least 1+2+2+2=7, again a contradiction. This exhausts t and proves the +minimum six. The proof requires no width bound or special dirty input. + +## Separate finite certificate + +Represent rows by a three-by-four matrix of coefficients of (a,b,c,p). +The start is [I|0] and the target is [I|(2,1,1)]. The twelve cheap generators +include all three nonzero coefficients on each cheap gate type, so the +alphabet is closed under inversion. + +The verifier enumerates the complete radius-two ball about the start and +radius-three ball about the target. They contain 99 and 613 matrices and +have empty intersection. A word of length at most five has a split with +prefix length at most two and suffix length at most three. Its split matrix +would lie in both balls. Price-100 gates cannot occur in a cheaper word. +The six-gate word supplies the matching upper certificate. + +This finite computation independently corroborates the written lower bound +after the coefficient-matrix reduction. The result is an abstract tariff, +not a physical implementation, supplier or multiplication theorem. diff --git a/research/z4-directed-cycle-fanout/README.md b/research/z4-directed-cycle-fanout/README.md new file mode 100644 index 0000000000..fcb3cc2f01 --- /dev/null +++ b/research/z4-directed-cycle-fanout/README.md @@ -0,0 +1,104 @@ +# Exact nonunit dirty fanout on a cheap directed cycle + +This contribution was produced by Nick Petalas. Apache-2.0. + +For demand `(2,1,1)` over `Z/4`, the exact price is **six** when source +insertion into row zero and the directed ADD cycle `0 -> 1 -> 2 -> 0` +cost one, while all other source insertions and ADD directions cost 100. +Every nonzero coefficient has its gate's price. All three inputs are +arbitrary dirty rows; the disjoint source is preserved. There is no workspace. + +This is a **scoped written proof with an exact finite certificate**, answering +the concrete cheap-cycle case suggested in Open next question 1 of +[lee-phys, PR #5163](https://github.com/CrocSwap/integer-mult-bounds/pull/5163). +That predecessor determines destination-only prices and leaves independent +directed prices open. Its result is cited, rather than replayed as the +contribution. The new chronological word is + +```text +E_21(-1), E_10(-1), P_0(1), E_10(1), P_0(1), E_21(1) +(a,b,c,p) -> (a+2p,b+p,c+p,p). +``` + +Here `E_ij(c)` adds `c A_j` into `A_i`, and `P_i(c)` adds `c p` into `A_i`. +Every gate costs one. The word uses a path inside the cycle; the third cheap +edge remains available to competitors. [PROOF.md](PROOF.md) proves the +endpoint at every positive width and excludes every cheaper word, with +arbitrary repetitions, interleavings and nonzero coefficients. This supplies +one exactly solved independent-edge instance, not an arbitrary-price formula. +No new kappa, physical caller or selected-frontier change is claimed. + +## Evidence and reproduction + +Complete cheap-word balls of radii two and three contain 99 and 613 literal +three-by-four coefficient matrices, and are disjoint. Every word of length +at most five would give an intersection, since all inverses are available. +A separate scalar interpreter checks all 256 four-scalar inputs and their +inverse executions. Nineteen controls cover six gate deletions, six sign +changes, invalid gates and capacity limits. All nine directed gate types +have their prices checked. Each successful invocation prints a generated +receipt bound to all package-file SHA256 hashes. No receipt is handwritten. + +From the repository root, using CPython 3.12 and only its standard library: + +```sh +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/z4-directed-cycle-fanout/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -O -W error -B research/z4-directed-cycle-fanout/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/z4-directed-cycle-fanout +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/z4-directed-cycle-fanout --check-source-history +``` + +Any CPython 3.12 installation can replace the local path. Expected markers +are `PASS_Z4_DIRECTED_CYCLE_FANOUT`, `PASS_REGISTERED_RESEARCH_PACKAGE` and +`PASS_RESEARCH_COMMIT_BYTES`. Normal and optimized runs retain all checks. + +## Sources and scope + +Scientific base is canonical main `19fdb086ea96af9a9f87936a2b888e10af4ed810`, +priority revision eight. Selected-source orientation passed with +`PASS_RESEARCH_BASELINE_BINDINGS_ONLY`; it was metadata orientation. +TASK.json changes the historical `bit-helper-contract` card to this algebraic +side question. There is no G20 implementation claim. + +Credit lee-phys #5163 for the question, destination-price theorem and unit-arrival +argument; Krzysztof Wójt [#5045](https://github.com/CrocSwap/integer-mult-bounds/pull/5045) +for nonunit source-count classification and repeated-insertion words; and +Ross Richardson [#3121](https://github.com/CrocSwap/integer-mult-bounds/pull/3121) +and #3063 for edge-priced forest synthesis and dirt restoration. The new word +adapts established child-first preparation to separated source insertions. +Nick Petalas #4916, Cinna Davis #1944/#1968, Anthony #774, Oscar Fennell #759 +and Tekalign #3130 retain the earlier lineage. Classical matrix identities +are not claimed as new methods. Predecessor proof text is provenance-pinned; +no predecessor executable is imported or scientifically replayed. + +Entry overlap covered 310 open PRs and 5,456 Discussion records in the reported +cache, live handoff and fanout threads, account submissions, all-main README +terms and distinctive merged-PR searches. Only one recent account target came +from #5163; its equal-nonunit question differs from this unit-containing +independently priced instance. Unpublished work and arbitrary diffs remain +outside novelty coverage. + +Independent human and formal proof-kernel review are unclaimed. Physical +coefficient preparation, native frames, movement, precision, tape, storage and +the full supplier invoice remain unpriced. No multiplication theorem, Lean, +Docker or selected scientific cold replay is supplied. + +## Implementation limits + +There is no recursion, external process, network or output file. Words have +at most 64 gates; matrices have twelve residues; search radius is at most +three with a checked 1,000-state capacity. Functions have fewer than sixty +lines. Python managed allocation is a deviation from Power of Ten's fixed +allocation rule, confined to these bounded matrices and searches. The +compensating controls reject larger radii and words. A larger search needs +separately reviewed capacities. Warning-strict normal and optimized checks +exercise the limits. No shared implementation is changed. + +## Open next questions + +1. Determine the full directed-price envelope for this demand. Start with + directional subset cuts and a complete Pareto search. The present proof + solves one price matrix and does not enumerate that envelope. +2. Price one physical realization before using the word in a supplier. + Specify coefficient access, routing, native frames and restoration. + Those complete physical prices are missing from the abstract model. diff --git a/research/z4-directed-cycle-fanout/SOURCES.json b/research/z4-directed-cycle-fanout/SOURCES.json new file mode 100644 index 0000000000..fde7c08ce7 --- /dev/null +++ b/research/z4-directed-cycle-fanout/SOURCES.json @@ -0,0 +1,36 @@ +{ + "schema_version": 1, + "base_commit": "19fdb086ea96af9a9f87936a2b888e10af4ed810", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "581f8d87008354eb5b869f7ed9de1317ad837ce8", + "sha256": "2a0220e866417774606e0f991e41b9c1d26b1f43b97857238cf478dbc7d330b5" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec", + "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81" + }, + { + "path": "research/local-ring-row-fanout/README.md", + "usage": "provenance", + "git_blob": "a65ecdb615300c6b4357eadadb52b46cfbc363ba", + "sha256": "4f167d526d889089717b9ba273bc7d048efe4ec1e02cdd91456543e7fc9703fb" + }, + { + "path": "research/two-row-nonunit-fanout/README.md", + "usage": "provenance", + "git_blob": "ea27d3919102a2e66ab4d3ed9170edafee633a06", + "sha256": "8aba08fc4a0c049ffaa20f12ca96bbfc582f853ed063a2f694a6bf853c637313" + }, + { + "path": "research/dirty-anchor-edge-tariffs/README.md", + "usage": "provenance", + "git_blob": "16aa73e36b791fd4c025011123b8101dd4a1c2d6", + "sha256": "dae5277016949f17bc55191e34a5f9470475b94ed679c843217973711ce2a341" + } + ] +} diff --git a/research/z4-directed-cycle-fanout/TASK.json b/research/z4-directed-cycle-fanout/TASK.json new file mode 100644 index 0000000000..f8c33bd275 --- /dev/null +++ b/research/z4-directed-cycle-fanout/TASK.json @@ -0,0 +1,83 @@ +{ + "schema_version": 1, + "task_id": "bit-helper-contract", + "priority_revision": 8, + "base_commit": "19fdb086ea96af9a9f87936a2b888e10af4ed810", + "original_card": { + "id": "bit-helper-contract", + "question": "Can a changed G20 helper path or independent-target split improve the complete BIT moment without losing its physical endpoint?", + "starting_points": [ + "docs/research/current-priorities.md", + "docs/research/research-family-status.md", + "certificates/selected-result.json", + "docs/research/pr-intake-evidence/pr5599-completion/PROOF-REVIEW.md", + "research/g20-helper-split/README.md", + "research/g20-conjugation-admission/README.md" + ], + "methods": [ + "Construct and independently check one source-bound instance of the stated first experiment.", + "Seek an exact counterexample or target-specific complete-budget obstruction to that same proposed change." + ], + "acceptance_gate": "A full boundary contract and paid profile; unchanged scalar counts alone are insufficient. A scoped local result may be retained without a complete supplier. Expanding it into further construction rounds requires the family-level budget and obligation gate in research-family-status.md; an optimistic passing relaxation alone is not acceptance.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_selected_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Read revision 8, the selected review and live exact-source handoffs. Then follow this card's bounded first_experiment.", + "scope": "Source-bound orientation only, not a supplier replay or theorem proof." + }, + "first_experiment": "First read #5679/#5708 and their audits as pending component proposals. Choose one uncovered helper group/cut on an exact word; compare arbitrary-input native action, targets, owned storage, both orientations and full signed bill. Stop if the gain is only a scalar count or repaid by lost targets. Do not rerun the frozen #5609 common-frame domain without changing its hypothesis.", + "bottleneck_link": "Judge the actual current supplier contract and complete signed target/paid bill; frozen-profile ceilings require an applicability proof.", + "allowed_variations": [ + "One exact source head, helper/cut region or quantified proposition and changed hypothesis; check live handoffs first. Different seeds are not different scopes." + ], + "scope_change_triggers": [ + "Changing source head, helper/cut domain, operation alphabet or caller boundary without recording the new scope.", + "Treating an archived proposal or local numerical pass as complete supplier admission." + ], + "overlap_terms": [ + "G20", + "helper split", + "5679", + "5708", + "independent target" + ], + "existing_checks": [ + { + "scope": "Selected PR5599: complete helper-subspace construction and independent caller replay; five framework assumptions remain.", + "evidence": "docs/research/pr-intake-evidence/pr5599-completion/PROOF-REVIEW.md", + "remaining": "The next experiment must identify uncovered source-specific work. Successor archive intake does not transfer this admission.", + "status": "reviewed", + "source_commit": "09dd0965711ca7eeb169057a420abab1c9052137", + "selected_record_sha256": "2a0220e866417774606e0f991e41b9c1d26b1f43b97857238cf478dbc7d330b5" + } + ] + }, + "scope_status": "changed", + "actual_scope": "Exact price six for Z/4 demand (2,1,1), three dirty rows, one preserved source, unit-price directed cycle and P0, all other gate types priced 100.", + "scope_change_reason": "Take explicit cheap-cycle Open next question 1 of lee-phys PR5163 as an algebraic side result; no G20 word or supplier admission is claimed.", + "bottleneck_link": "Nonunit demands can invalidate unit-forest prices. One exactly solved directed instance supplies a small benchmark for routing and restoration accounting, without a supplier claim.", + "budget_minutes": 60, + "stop_rule": "Stop at the first verified original exact minimum or a documented search failure.", + "outcome": "completed", + "evidence": "Six-call all-cheap word; written all-width lower bound; disjoint complete balls of sizes 99 and 613; 256 literal forward/inverse cases; 19 controls.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "What is the complete directed-price envelope for demand (2,1,1) over Z/4?", + "why_it_matters": "One price matrix does not classify independent edge tariffs.", + "first_step": "Retain directed subset cuts and enumerate Pareto word counts.", + "blocked_by": "No all-price lower-bound classification is supplied." + }, + { + "question": "Can a physical caller realize this abstract six-call word at favorable complete prices?", + "why_it_matters": "An abstract tariff is not a supplier improvement.", + "first_step": "Specify source access, routing, coefficient preparation, native frames and restoration.", + "blocked_by": "No physical caller and price contract is supplied." + } + ] +} diff --git a/research/z4-directed-cycle-fanout/VERIFY.json b/research/z4-directed-cycle-fanout/VERIFY.json new file mode 100644 index 0000000000..12b0180a94 --- /dev/null +++ b/research/z4-directed-cycle-fanout/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": 120, + "checks": "Literal endpoint and inverse; complete radius-two/radius-three exclusion; all scalar dirty inputs; omission, sign, invalid-input and capacity controls." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Literal endpoint and inverse; complete radius-two/radius-three exclusion; all scalar dirty inputs; omission, sign, invalid-input and capacity controls." + } + ] +} diff --git a/research/z4-directed-cycle-fanout/verify.py b/research/z4-directed-cycle-fanout/verify.py new file mode 100644 index 0000000000..4e339b45c1 --- /dev/null +++ b/research/z4-directed-cycle-fanout/verify.py @@ -0,0 +1,133 @@ +#!/usr/bin/env python3 +"""Exact Z/4 dirty-fanout endpoint and complete short-word exclusion.""" +import hashlib +import itertools +import json +from pathlib import Path + +IDENTITY = (1, 0, 0, 0, 0, 1, 0, 0, 0, 0, 1, 0) +TARGET = (1, 0, 0, 2, 0, 1, 0, 1, 0, 0, 1, 1) +PAIRS = ((1, 0), (2, 1), (0, 2), (0, 3)) +GENERATORS = tuple((i, j, c) for i, j in PAIRS for c in (1, 2, 3)) +WORD = ((2, 1, 3), (1, 0, 3), (0, 3, 1), + (1, 0, 1), (0, 3, 1), (2, 1, 1)) + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def valid_gate(gate): + require(isinstance(gate, tuple) and len(gate) == 3, 'gate shape') + require(all(type(x) is int for x in gate), 'integer gate entries') + i, j, c = gate + require(0 <= i < 3 and 0 <= j <= 3 and i != j, 'gate roles') + require(1 <= c <= 3, 'nonzero canonical coefficient') + + +def gate_price(gate): + valid_gate(gate) + return 1 if gate[:2] in PAIRS else 100 + + +def apply_gate(state, gate): + """Literal three-by-four coefficient matrix, without packed arithmetic.""" + valid_gate(gate) + require(len(state) == 12 and all(type(x) is int and 0 <= x < 4 + for x in state), 'matrix residues') + i, j, c = gate + source = state[4*j:4*j+4] if j < 3 else (0, 0, 0, 1) + row = tuple((state[4*i+k] + c*source[k]) % 4 for k in range(4)) + return state[:4*i] + row + state[4*i+4:] + + +def execute(word, state=IDENTITY): + require(isinstance(word, tuple) and len(word) <= 64, 'word capacity') + for gate in word: + state = apply_gate(state, gate) + return state + + +def ball(start, radius): + require(type(radius) is int and 0 <= radius <= 3, 'radius capacity') + seen, frontier = {start}, {start} + for _ in range(radius): + next_frontier = {apply_gate(s, g) for s in frontier for g in GENERATORS} + next_frontier.difference_update(seen) + seen.update(next_frontier) + require(len(seen) <= 1000, 'state capacity') + frontier = next_frontier + return seen + + +def digest(states): + return hashlib.sha256(b''.join(bytes(s) for s in sorted(states))).hexdigest() + + +def scalar_execution(values, word): + """Independent evaluation on four actual scalars, including the source.""" + require(len(values) == 4, 'scalar shape') + out = list(values) + for i, j, c in word: + out[i] = (out[i] + c*out[j]) % 4 + return tuple(out) + + +def expect_rejection(function, argument): + try: + function(argument) + except ValueError: + return 1 + raise ValueError('invalid input accepted') + + +def main(): + require(execute(WORD) == TARGET, 'complete endpoint') + require(sum(map(gate_price, WORD)) == 6, 'complete price') + require(len(GENERATORS) == 12 and len(set(GENERATORS)) == 12, 'alphabet') + inverse = tuple((i, j, 4-c) for i, j, c in reversed(WORD)) + require(execute(inverse, TARGET) == IDENTITY, 'inverse endpoint') + forward, backward = ball(IDENTITY, 2), ball(TARGET, 3) + require(not forward.intersection(backward), 'word of cost at most five') + literal_cases = 0 + for inputs in itertools.product(range(4), repeat=4): + a, b, c, p = inputs + expected = ((a+2*p) % 4, (b+p) % 4, (c+p) % 4, p) + output = scalar_execution(inputs, WORD) + require(output == expected, 'literal dirty endpoint') + require(scalar_execution(output, inverse) == inputs, 'literal inverse') + literal_cases += 1 + controls = 0 + for k in range(len(WORD)): + require(execute(WORD[:k]+WORD[k+1:]) != TARGET, 'deletion survived') + i, j, c = WORD[k] + changed = WORD[:k] + ((i, j, 4-c),) + WORD[k+1:] + require(execute(changed) != TARGET, 'wrong sign survived') + controls += 2 + for gate in ((0, 0, 1), (0, 3, 0), (0, 3, 4), (False, 3, 1), (3, 0, 1)): + controls += expect_rejection(gate_price, gate) + controls += expect_rejection(ball_radius_control, 4) + controls += expect_rejection(execute, WORD*11) + for i, j in itertools.permutations(range(3), 2): + require(gate_price((i, j, 1)) == (1 if (i, j) in PAIRS else 100), + 'directed price') + for i in range(3): + require(gate_price((i, 3, 1)) == (1 if i == 0 else 100), 'source price') + package = Path(__file__).resolve().parent + hashes = {p.name: hashlib.sha256(p.read_bytes()).hexdigest() + for p in sorted(package.iterdir()) if p.is_file()} + receipt = {'status': 'PASS_Z4_DIRECTED_CYCLE_FANOUT', 'minimum_price': 6, + 'word': WORD, 'ball_sizes': [len(forward), len(backward)], + 'ball_hashes': [digest(forward), digest(backward)], + 'literal_inputs': literal_cases, 'controls': controls, + 'package_sha256': hashes} + print(json.dumps(receipt, sort_keys=True)) + + +def ball_radius_control(radius): + return ball(IDENTITY, radius) + + +if __name__ == '__main__': + main()