diff --git a/research/two-row-nonunit-fanout/PROOF.md b/research/two-row-nonunit-fanout/PROOF.md new file mode 100644 index 0000000000..1bd3b47624 --- /dev/null +++ b/research/two-row-nonunit-fanout/PROOF.md @@ -0,0 +1,180 @@ +# Exact two-row dirty-fanout tariff with comparable demands + +Krzysztof Wójt, with substantial OpenAI Codex assistance. Apache-2.0. + +This is a written algebraic proof. The executable corroborates finite cases; +neither finite testing nor this package supplies a physical supplier or new κ. + +## Contract and notation + +Keep the contract of Nick Petalas's #4916, restricted to **two** rows, but +allow nonunit and zero target coefficients. Let R be any ring with 1 ≠ 0, +not necessarily finite or commutative. The arbitrary independent inputs are +`a_0,a_1,p ∈ R^w`, with w ≥ 1. The disjoint common source p is preserved. +The required endpoint is + + A_0 = a_0 + λ_0 p, A_1 = a_1 + λ_1 p. + +A finite, fixed straight-line word may use only + + P_i(β): A_i ← A_i + β p, price μ_i > 0, + E_i(α): A_i ← A_i + α A_(1-i), price c_i > 0. + +Thus c_i prices the ADD **into** i. Coefficients multiply on the left. +Prices are stationary, finite, complete, and independent of coefficients; +they may be arbitrary positive real numbers. Every call is charged, including +coefficient preparation and inverse application as stipulated by that model. +There are no other rows, free row transformations, clearing, intermediate +observations, input-dependent choices or separately erased original dirt. +An inverse word, when requested, must be paid separately. + +Write `x ≼ y` when `x ∈ Ry`, equivalently x = r y for some r ∈ R. +Assume the two principal **left** ideals are comparable: + + λ_0 ≼ λ_1 or λ_1 ≼ λ_0. + +This is a condition on the two demands, not on every ideal of R. It includes +every pair in Z/p^k (p prime, k ≥ 1), every pair in a left chain ring, and +some pairs in noncommutative rings. Incomparable demand pairs are excluded. + +## The tariff + +For i ∈ {0,1} put j = 1-i. Define the direct price + + D = [λ_0 ≠ 0] μ_0 + [λ_1 ≠ 0] μ_1, + +the single-insertion price + + { μ_i if λ_j = 0, + S_i = { μ_i + 2 c_j if λ_j ≠ 0 and λ_j ≼ λ_i, + { μ_i + 2(c_i+c_j) otherwise, + +and the repeated-insertion price + + T_i = 2 μ_i + 2 c_j. + +**Theorem.** Over all words in this contract, the exact minimum is + + OPT = min(D, S_0, S_1, T_0, T_1). + +This includes the zero-demand boundary: OPT = 0 if both demands vanish. +The formula solves every two-row nonunit instance over Z/p^k for every +positive price vector, rather than only a fixed modulus or price matrix. + +For two nonzero demands with λ_j not in Rλ_i, comparability gives λ_i ∈ Rλ_j. +The only extra options beyond direct insertion and the valid forest rooted +at j are + + 2 μ_i + 2 c_j and μ_i + 2(c_i+c_j). + +They respectively pay a second source insertion or reversible mixing in +both directions. Their difference is μ_i - 2 c_i: the cheaper method +changes at μ_i = 2 c_i. A forest whose parent demand cannot generate its +child demand is not an attaining construction. + +## Lower bound for arbitrary interleavings + +Zero-coefficient calls can be deleted, since prices are positive. Work with +a word containing no such calls. Set p = 0 and project onto the two original +dirt symbols. Its matrix starts and ends at I_2. Every E_i is an elementary +invertible matrix with inverse E_i(-α); P_i does not change this matrix. +The all-input contract implies matrix equality by testing a single input +coordinate equal to 1 and the other inputs equal to zero. No rank-over-a-field +assumption is used. + +**Directional return lemma.** Each ADD direction occurs either zero times +or at least twice. For example, if the upper direction occurred exactly +once with nonzero coefficient α, every other dirt operation would be lower +triangular. Combining adjacent lower elementary matrices would give + + L(x) U(α) L(y). + +Its upper-right entry is α over any ring, so it cannot be I_2. Interchanging +the two rows gives the other direction. Source calls can be ignored for +this argument, because they do not change dirt coefficients. + +If the target is nonzero, some P_i occurs. Classify by the rows receiving +source insertions: + +1. **Both rows receive an insertion.** The bill is at least μ_0+μ_1 ≥ D. + +2. **Only row i receives insertions, at least twice.** If λ_j ≠ 0, some + E_j must occur: otherwise row j never acquires any p coefficient. + The directional return lemma requires at least two E_j, so the bill is + at least T_i. If λ_j = 0, the bill is at least μ_i = S_i. + +3. **There is exactly one insertion, at row i.** If λ_j = 0 its price alone + gives S_i. Otherwise there are at least two E_j. If λ_j ≼ λ_i, this + already gives the required S_i lower bound. If λ_j is not in Rλ_i, + there must also be an E_i: without that direction, the sole insertion + coefficient must equal λ_i, and row j's final source coefficient is a + sum of left multiples of λ_i, hence belongs to Rλ_i. The contradiction + and the return lemma force at least two E_i, giving μ_i+2(c_i+c_j)=S_i. + +Every possible word therefore costs at least the minimum of the five +displayed numbers. This argument allows arbitrarily many calls, arbitrary +coefficients (including zero divisors), cancellations and interleavings. +It does not require Edmonds' branching theorem. + +## Attaining words + +All words below are in chronological execution order. They preserve the +common source and return the full dirt matrix to I_2. + +**Direct:** insert λ_i p at each row whose demand is nonzero. Cost D. + +**Single insertion, divisible direction:** if λ_j = r λ_i, execute + + E_j(-r), P_i(λ_i), E_j(r). + +The endpoint at j is `(a_j-r a_i)+r(a_i+λ_i p) = a_j+λ_j p`. +If λ_j = 0, a lone P_i(λ_i) suffices. Zero-coefficient calls may be omitted. +This attains S_i in its first two cases (or a smaller, already-covered +direct price when both demands vanish). + +**Two insertions at i:** for any pair of demands, execute + + E_j(-1), P_i(λ_j), E_j(1), P_i(λ_i-λ_j). + +The middle pair transports λ_j p after cancelling a_i; the final insertion +sets row i's demand to λ_i. Its price is T_i. This construction uses no +division. If a source coefficient is zero, it can be omitted; the lower +bound still applies to the resulting word. + +**Single insertion, reverse divisibility:** in the remaining case λ_j ≠ 0 +and λ_j not in Rλ_i, comparability supplies b with λ_i = b λ_j. Execute + + E_i(1-b), E_j(-1), P_i(λ_j), E_j(1), E_i(b-1). + +The first two ADDs are the inverse of the last two ADDs. Immediately after +the insertion the source coefficient column is λ_j e_i. The last two ADDs +send e_i to b e_i + e_j, giving exactly `(λ_i,λ_j)` in row order (i,j). +Hence arbitrary dirt is restored and the price is S_i. No commutation of +b with λ_j has been used. In this remaining case b ≠ 1, so all four ADDs +are nonzero. Literal inversion reverses any word and negates every gate +coefficient, with the same tariff. + +For each expression in the lower envelope there is thus a legal word of +at most that price. Together with the lower bound, this proves equality. + +## Consequences and discriminators + +- For unit demands both divisibility directions hold. The T_i options and + unnecessary reverse-mixing options are dominated, recovering exactly + the two-row specialization of #4916's rooted-forest law. +- The credited #4916 boundary over Z/4 with `(λ_0,λ_1)=(2,1)`, μ=(1,9) + and c=(1,1) has D=10, S_0=5, S_1=11, T_0=4, T_1=20: OPT=4. +- With the same demands, μ=(100,1000) and c=(1,1), OPT=104 is instead + attained with one source insertion and four ADDs. Paying two source + insertions costs 202. A rule allowing only valid forests and repeated + source insertions therefore misses a real optimal regime. +- If λ_0=0, λ_1≠0, direct cost is μ_1; using row 0 as a temporary dirty + source recipient may still be cheaper. Its original dirt must return. +- In a noncommutative ring the test is left divisibility. Replacing it by + right divisibility can incorrectly enable the three-call word. The + executable includes an explicit 2×2 binary-matrix counterexample. + +The universal result rests on this proof. Finite exact shortest paths check +the implementation and its bounded instances; they are not its universal +premise. More rows, incomparable demand ideals and actual physical tariff +matrices require separate results. diff --git a/research/two-row-nonunit-fanout/README.md b/research/two-row-nonunit-fanout/README.md new file mode 100644 index 0000000000..ea27d39191 --- /dev/null +++ b/research/two-row-nonunit-fanout/README.md @@ -0,0 +1,135 @@ +# Exact two-row nonunit dirty-fanout tariffs + +For two arbitrary dirty rows and a preserved common source, this proves the +exact cost for **every pair of demands with comparable principal left ideals**, +including all demands over Z/p^k. The five-term price formula covers arbitrary +positive, stationary, coefficient-independent source and directed-ADD prices. +It includes zero demands and noncommutative coefficient rings. + +This answers the structural two-row part of Nick Petalas's +[#4916 handoff](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19134896). +The predecessor's unit-demand theorem and its Z/4 optimum-four example are +retained and credited. The new result is an all-price theorem with attaining +words, including a regime in which one source insertion and four ADDs beat +both valid forests and repeated source insertion. No new κ is claimed. + +## Contract and result + +Write the required outputs as `A_i = a_i + λ_i p`. Each original `a_i` and +the disjoint source p is arbitrary; p is preserved. Allowed calls are +`P_i(β): A_i += β p`, price μ_i, and `E_i(α): A_i += α A_(1-i)`, price c_i. +Coefficients multiply on the left. There are exactly two rows, no extra +workspace, free basis changes, clearing or intermediate observers. + +For j=1-i, let `x ≼ y` mean `x ∈ Ry`. Assume `λ_0 ≼ λ_1` or `λ_1 ≼ λ_0`. +Define + +```text +D = [λ_0 != 0] μ_0 + [λ_1 != 0] μ_1 +S_i = μ_i if λ_j = 0 + μ_i + 2 c_j if λ_j != 0 and λ_j ≼ λ_i + μ_i + 2(c_i+c_j) otherwise +T_i = 2 μ_i + 2 c_j + +OPT = min(D, S_0, S_1, T_0, T_1). +``` + +The [proof](PROOF.md) counts source insertions and uses a two-row return +lemma: a nonzero ADD direction cannot occur exactly once if arbitrary dirt +must return. It then constructs every price option. This elementary proof +does not invoke the predecessor's disjoint-branching theorem. + +For Z/4 demands `(2,1)`, μ=(1,9), c=(1,1), the credited optimum is four, +using two source insertions at the cheap row. With μ=(100,1000) and the +same demands/ADD prices, the optimum is 104: one insertion and four ADDs. +Repeated insertion costs 202. The two constructions trade off at μ_i=2c_i; +neither can be omitted from the general optimum. + +## Exact evidence + +- **522 independent shortest-path runs:** all demand pairs over Z/2, Z/3, + Z/4, Z/5, Z/8 and Z/9, for all 81 price vectors in `{1,2,3}^4` plus six + asymmetric vectors. All **17,313 optimum comparisons** agree. The oracle + visits 179,845 settled affine states and scans 5,080,872 transitions in + total; these are sums over runs, not distinct global states. +- **2,591 attaining words:** all comparable pairs over seven modular rings, + F2[e]/e² and M2(F2), checked on all three formal input columns and their + inverses (7,773 column checks). The 58 incomparable pairs are rejected. + Literal complete dirty/source domains add **4,800** execution/inverse checks. +- Controls cover the already-known nonunit boundary, the new mixing regime, + omitted preparation, unreturned dirt, wrong mixing sign, wrong coefficient + order, left/right ideals, zero demands, a zero-demand temporary anchor, + and ten malformed/out-of-scope inputs. + +`shortest_path.py` directly explores exact six-coefficient affine states with +every legal nonzero modular coefficient. It imports no tariff code, applies +no depth cap, and stops only when all target distances are settled. Its +returned paths are also replayed by the primary literal interpreter. A +separate supporting agent implemented this oracle; the primary agent reviewed +and integrated it. This is automatic corroboration, not independent human +acceptance. The universal theorem rests on the written proof. + +`RESULT.json` is generated and binds the local proof/code/metadata bytes and +the pinned predecessor README. It excludes timings. Normal and optimized +verification compare the full typed receipt; bool/int changes are unequal. +The direct checker loads exact source bytes without consulting `.pyc` files. + +## Reproduce + +Python 3.12 and the standard library suffice. From the repository root: + +```sh +python3.12 -B scripts/research_package.py --package research/two-row-nonunit-fanout --check-only +python3.12 -B scripts/research_package.py --package research/two-row-nonunit-fanout +python3.12 -I -W error -B research/two-row-nonunit-fanout/verify.py +python3.12 -I -O -W error -B research/two-row-nonunit-fanout/verify.py +python3.12 -B scripts/check_research_commit.py --package research/two-row-nonunit-fanout --check-source-history +``` + +The direct marker is `PASS_TWO_ROW_NONUNIT_FANOUT`; each registered command +has a 120-second cap. To generate a new receipt after an intentional source +change, use `verify.py --write-receipt NEW_PATH`; it refuses to overwrite any +existing output. Do not hand-edit the receipt. + +Scientific base is canonical main `f259dabc7d70e0db8d6d36bfda888f008bbfecc1`, +priority revision 7. Exact source pins and the explicit changed task scope are +in [SOURCES.json](SOURCES.json) and [TASK.json](TASK.json). The +[canonical investigation](https://github.com/CrocSwap/integer-mult-bounds/discussions/5030) +records the claim and publication. The selected-source orientation passed; +that is a metadata binding check, not a selected operator replay. + +## Scope and limitations + +The proof permits arbitrary rings with comparable demand left ideals and +positive real tariffs. The reference code uses explicit finite rings and +positive rational tariffs. The finite shortest-path census is only the six +named modular rings and price vectors. More rows and incomparable demand +ideals are not solved. No complete physical tariff matrix, native caller, +frame/hosting/precision/tape implementation, compiler or outer admission is +provided. No Lean, selected scientific cold replay, independent human review +or full multiplication theorem is claimed. Selected κ remains 0.00302015. + +## Open next questions + +1. **Incomparable demands.** Start with `(2,3)` over Z/6 and one asymmetric + price matrix. A general one-insertion orbit/cost criterion is missing; + the reverse-divisibility construction need not exist. +2. **Three dirty output rows.** Start with `(2,1,1)` over Z/4 and one full + price matrix, deriving a word and cut bound before a larger search. + Shared temporary use can evade the two-direction classification. +3. **An actual caller.** Charge every source access, coefficient, frame, + movement, lifetime, restoration and precision operation. That missing + physical invoice blocks any inference of a recursive supplier gain. + +The structured relevance, first steps and blockers are also in TASK.json. +This contribution stops at the proved two-row algebraic result. + +## Credit + +Prepared by Krzysztof Wójt (@krzysztofwojt) with substantial OpenAI Codex +assistance in derivation, implementation, verification and writing. Apache-2.0. +Credit Nick Petalas #4916 for the unit-ring extension, explicit nonunit +handoff and optimum-four example; Ross Richardson #3121/#3063 for directed +XOR tariffs and the dirty-output model; Cinna Davis #1944/#1968, Anthony +#774, Oscar Fennell #759, Tekalign #3130 and the retained fanout lineage. +No predecessor executable or full census is rerun as a new contribution. diff --git a/research/two-row-nonunit-fanout/RESULT.json b/research/two-row-nonunit-fanout/RESULT.json new file mode 100644 index 0000000000..d01ad30da0 --- /dev/null +++ b/research/two-row-nonunit-fanout/RESULT.json @@ -0,0 +1,58 @@ +{ + "bindings": { + "input_sha256": { + "research/unit-ring-dirty-fanout/README.md": "70764fb3def04ba1b0a51e95cb023358fdaed5100d2440feecbaab0e85a9a5fe" + }, + "local_sha256": { + "PROOF.md": "d177967c73bd5e755c5f70964d5542420e23e36cad81c57452a222e50e356f77", + "README.md": "8aba08fc4a0c049ffaa20f12ca96bbfc582f853ed063a2f694a6bf853c637313", + "SOURCES.json": "2edde3776d9e803f38080e17af6295c9b334db9cfbc616e0559f6386a27816e4", + "TASK.json": "c4e8c5d518fbc972c8ffacc4cc38e9867dfa40b4af95773327047a56c547625d", + "VERIFY.json": "75e391681fabf9e79f102ad1921b0ec7528ad341d67ef642e815114af54083c4", + "shortest_path.py": "86bb9247cf2715b5a1556f25036982599f5b01cd3a0b2f8b0e6f8a8a00d19f9e", + "tariff.py": "82e0a63176df61512293580afb47ac6c7db1cad4060451499b3b3a8885fe117b", + "verify.py": "8431b5b2bad063f161e28ff4791fe9b07ddf8464dc55286604a30a6918795ef0" + } + }, + "construction": { + "candidate_words": 2591, + "coefficient_columns_with_inverse": 7773, + "comparable_pairs": 449, + "incomparable_pairs": 58, + "literal_dirty_states_with_inverse": 4800, + "rings": 9 + }, + "controls": { + "invalid_input_controls": 10, + "semantic_controls": [ + "credited_Z4_optimum_four", + "mixing_beats_forests_and_repeat", + "omitted_preparation", + "unreturned_dirt", + "wrong_mixing_sign", + "wrong_noncommutative_ratio", + "left_versus_right_ideal", + "zero_demands", + "zero_demand_temporary_anchor" + ] + }, + "new_kappa": false, + "schema": "two-row-nonunit-fanout/v1", + "shortest_paths": { + "moduli": [ + 2, + 3, + 4, + 5, + 8, + 9 + ], + "ordered_optimum_sha256": "3e2b739c72d1d372d65db7b1faaa948abe48fc2a1f7abc3adc4032511b3ede1f", + "price_vectors_per_modulus": 87, + "replayed_oracle_paths": 32, + "searches": 522, + "settled_states": 179845, + "target_cost_comparisons": 17313, + "transition_scans": 5080872 + } +} diff --git a/research/two-row-nonunit-fanout/SOURCES.json b/research/two-row-nonunit-fanout/SOURCES.json new file mode 100644 index 0000000000..1e38385ce2 --- /dev/null +++ b/research/two-row-nonunit-fanout/SOURCES.json @@ -0,0 +1,24 @@ +{ + "schema_version": 1, + "base_commit": "f259dabc7d70e0db8d6d36bfda888f008bbfecc1", + "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/unit-ring-dirty-fanout/README.md", + "usage": "input", + "git_blob": "70ce8559a0d35a5e2e9c47f0885c8042b22bb0ef", + "sha256": "70764fb3def04ba1b0a51e95cb023358fdaed5100d2440feecbaab0e85a9a5fe" + } + ] +} diff --git a/research/two-row-nonunit-fanout/TASK.json b/research/two-row-nonunit-fanout/TASK.json new file mode 100644 index 0000000000..3b49b9bc16 --- /dev/null +++ b/research/two-row-nonunit-fanout/TASK.json @@ -0,0 +1,91 @@ +{ + "schema_version": 1, + "task_id": "bit-helper-contract", + "priority_revision": 7, + "base_commit": "f259dabc7d70e0db8d6d36bfda888f008bbfecc1", + "original_card": { + "id": "bit-helper-contract", + "question": "Can one precisely specified helper-mixing word satisfy a replacement for the inherited H2/K interface?", + "starting_points": [ + "docs/research/research-family-status.md", + "research/r439-bsection-stars-seed01/README.md", + "research/r439-copy-path-sharing-barrier/README.md" + ], + "methods": [ + "Derive a replacement interface lemma and price its implementation.", + "Seek an exact dirty-input or chronological-cut counterexample to the proposed replacement." + ], + "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", + "research/r439-bsection-stars-seed01/verify.py" + ], + "expected": "PASS_R439_BSECTION_STARS", + "inspect": "Compare the two false H2/K flags with the unchanged paid profile in its README.", + "scope": "Positive control / source-bound orientation only; this is not a new construction or full cold replay." + }, + "first_experiment": "Write one replacement H2/K implication for a single helper-star operation, then try to falsify it on dirty inputs.", + "bottleneck_link": "A legitimate replacement could admit a cheaper bit circuit; scalar savings alone do not alter the selected moment.", + "allowed_variations": [ + "Choose one helper-star or quartet instance; narrow to one boundary implication." + ], + "scope_change_triggers": [ + "Changing only source count or scalar addition count without an interface argument." + ], + "overlap_terms": [ + "H2_D_frame0_targets_from_helpers", + "K_equals_D", + "helper-star" + ] + }, + "scope_status": "changed", + "actual_scope": "Exact all-price two-row dirty-fanout optimum for demands generating comparable principal left ideals, including every pair over Z/p^k; constructive words and independent finite shortest paths.", + "scope_change_reason": "Handoff-first override: merged PR4916 explicitly leaves the structural nonunit-demand tariff open. Its unit-demand theorem and single Z/4 example are credited predecessors. This is an algebraic interface side result, not an H2/K admission or a new supplier.", + "bottleneck_link": "Complete source and dirty-output mixing prices must distinguish repeated source insertion from reversible row mixing when demand ratios do not exist. This resolves that abstract two-row choice; no actual physical tariff matrix, recursive paid-profile gain or kappa improvement is inferred.", + "budget_minutes": 240, + "stop_rule": "Stop after one exact comparable-demand tariff theorem and bounded independent checks, or a counterexample. Do not expand to more rows, incomparable demands or physical implementation during this contribution.", + "outcome": "completed", + "evidence": "PROOF.md proves the five-term price envelope for arbitrary rings with comparable demand left ideals and arbitrary positive real prices. RESULT.json binds 522 exact modular shortest-path runs, 17313 optimum comparisons, 2591 attaining words, 4800 literal dirty-state/inverse checks and explicit semantic/domain controls. The finite checks corroborate the implementation, not the universal quantifiers.", + "author": "Krzysztof Wójt (@krzysztofwojt)", + "ai_assistance": "Substantial OpenAI Codex assistance in derivation, implementation, checking and writing. A separate Luna worker implemented the finite Dijkstra oracle without importing the tariff formula; the primary agent reviewed it and integrated the comparisons. This is not independent human or proof-kernel verification.", + "coordination_url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/5030", + "handoff_url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19134896", + "predecessor": { + "pr": 4916, + "author": "Nick Petalas", + "head": "459a1d9984e8c5bf09257a409863e63282c282e6", + "retained_input": "research/unit-ring-dirty-fanout/README.md", + "credit": "Unit-demand ring extension and credited Z/4 optimum-four example; Ross Richardson #3121/#3063 and the predecessor dirty-fanout lineage remain credited." + }, + "entry_overlap": { + "open_prs": 320, + "open_prs_at": "2026-10-23T06:48:29.704913+00:00", + "discussion_records": 4130, + "discussions_at": "2026-10-23T06:49:29.966122+00:00", + "local_notes": 6710, + "complete_reported_pagination_and_local_inventory": true, + "limits": "Titles/bodies/comments and top-level README/TASK/ledger scope; arbitrary diffs and unpublished work are not covered. Live predecessor, newest handoffs and new PRs were rechecked before claiming." + }, + "open_questions": [ + { + "question": "What is the exact two-row tariff for incomparable demand left ideals?", + "why_it_matters": "The five-term attainment argument uses reverse divisibility when direct transport fails; this may be unavailable over nonlocal rings.", + "first_step": "Use demands (2,3) over Z/6 with an asymmetric source tariff and compare an independently found word with a source-insertion lower bound.", + "blocked_by": "A general single-insertion orbit criterion and its directional gate cost are not supplied here." + }, + { + "question": "Which additional mechanisms arise with three dirty output rows and nonunit demands?", + "why_it_matters": "A third row can share temporary source insertions and mixing; the two-direction return classification no longer exhausts the possibilities.", + "first_step": "Fix the Z/4 demand (2,1,1) and one complete price matrix; derive a discriminating word and cut bound before any larger search.", + "blocked_by": "No multi-row nonunit attainment theorem or complete optimality certificate is provided." + }, + { + "question": "Can an actual caller provide the coefficient-independent complete tariffs assumed by this theorem?", + "why_it_matters": "Abstract gate counts alone do not establish a recursive supplier saving.", + "first_step": "Choose one actual common-source caller and charge source access, coefficient application, frames, movement, lifetime, restoration and precision for every allowed gate.", + "blocked_by": "No physical tariff matrix or complete caller invoice is supplied." + } + ] +} diff --git a/research/two-row-nonunit-fanout/VERIFY.json b/research/two-row-nonunit-fanout/VERIFY.json new file mode 100644 index 0000000000..ca4efeac5a --- /dev/null +++ b/research/two-row-nonunit-fanout/VERIFY.json @@ -0,0 +1,28 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/unit-ring-dirty-fanout/README.md" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Exact five-term tariff, all attaining endpoints/inverses, independent Dijkstra optimum comparisons, noncommutative/domain controls and typed source-bound receipt" + }, + { + "argv": ["{python}", "-I", "-O", "-W", "error", "-B", "{package}/verify.py"], + "timeout_seconds": 120, + "checks": "The same complete checks with Python assertions disabled" + } + ] +} diff --git a/research/two-row-nonunit-fanout/shortest_path.py b/research/two-row-nonunit-fanout/shortest_path.py new file mode 100644 index 0000000000..4d01757b3a --- /dev/null +++ b/research/two-row-nonunit-fanout/shortest_path.py @@ -0,0 +1,339 @@ +"""Exact shortest-path oracle for two-row dirty fanout over Z/qZ. + +This module intentionally implements the finite state graph directly. It does +not import a tariff formula or any other project code. + +Rows are flattened as ``(a00, a01, p0, a10, a11, p1)``. An ``add`` edge +performs one elementary row operation; a ``source`` edge changes exactly one +row's coefficient of the distinguished source ``p``. Every nonzero residue +is an available coefficient, including the additive inverse of every gate +coefficient. Positive edge prices make Dijkstra's algorithm exact. The search +has no depth bound: it expands complete legal outgoing transitions from each +settled state and stops only after all q^2 pure-translation targets settle. + +Attribution: "Krzysztof Wójt with substantial OpenAI Codex assistance" +License: Apache-2.0 +""" + +from __future__ import annotations + +import heapq +import time +from typing import Tuple, Union + + +State = Tuple[int, int, int, int, int, int] +Action = Union[Tuple[str, int, int], Tuple[str, int, int, int]] +Demand = Tuple[int, int] + +_START: State = (1, 0, 0, 0, 1, 0) + + +def _validate_inputs( + modulus: int, + source_prices: tuple[int, int], + add_prices: tuple[int, int], + include_paths: bool, +) -> None: + if type(modulus) is not int: + raise TypeError("modulus must be an int (bool is not accepted)") + if modulus < 2: + raise ValueError("modulus must be at least 2") + if type(source_prices) is not tuple or len(source_prices) != 2: + raise TypeError("source_prices must be a 2-tuple of positive ints") + if type(add_prices) is not tuple or len(add_prices) != 2: + raise TypeError("add_prices must be a 2-tuple of positive ints") + for name, prices in (("source_prices", source_prices), ("add_prices", add_prices)): + for price in prices: + if type(price) is not int: + raise TypeError(f"{name} entries must be ints (bool is not accepted)") + if price <= 0: + raise ValueError(f"{name} entries must be positive") + if type(include_paths) is not bool: + raise TypeError("include_paths must be bool") + + +def _apply_action(state: State, action: Action, modulus: int) -> State: + """Apply one already validated operation, returning a fresh exact state.""" + kind = action[0] + if kind == "source": + _, dst, beta = action + offset = 3 * dst + 2 + result = list(state) + result[offset] = (result[offset] + beta) % modulus + return tuple(result) # type: ignore[return-value] + + _, dst, src, alpha = action + dst_offset = 3 * dst + src_offset = 3 * src + result = list(state) + for column in range(3): + result[dst_offset + column] = ( + state[dst_offset + column] + alpha * state[src_offset + column] + ) % modulus + return tuple(result) # type: ignore[return-value] + + +def _operation_price( + action: Action, + source_prices: tuple[int, int], + add_prices: tuple[int, int], +) -> int: + if action[0] == "source": + return source_prices[action[1]] + return add_prices[action[1]] + + +def _target_state(demand: Demand) -> State: + return (1, 0, demand[0], 0, 1, demand[1]) + + +def _replay_path( + modulus: int, + source_prices: tuple[int, int], + add_prices: tuple[int, int], + path: tuple[Action, ...], +) -> tuple[State, int]: + """Independently replay a returned operation sequence and sum its prices.""" + state = _START + total = 0 + for action in path: + if not isinstance(action, tuple) or not action: + raise AssertionError("path contains a malformed action") + if action[0] == "source": + if len(action) != 3: + raise AssertionError("source action must be ('source', dst, beta)") + _, dst, beta = action + if type(dst) is not int or dst not in (0, 1): + raise AssertionError("source destination must be row 0 or 1") + if type(beta) is not int or beta % modulus == 0: + raise AssertionError("source coefficient must be nonzero modulo q") + normalized: Action = ("source", dst, beta % modulus) + elif action[0] == "add": + if len(action) != 4: + raise AssertionError("add action must be ('add', dst, src, alpha)") + _, dst, src, alpha = action + if ( + type(dst) is not int + or type(src) is not int + or dst not in (0, 1) + or src not in (0, 1) + or dst == src + ): + raise AssertionError("add rows must be distinct members of {0, 1}") + if type(alpha) is not int or alpha % modulus == 0: + raise AssertionError("add coefficient must be nonzero modulo q") + normalized = ("add", dst, src, alpha % modulus) + else: + raise AssertionError(f"unknown path action: {action[0]!r}") + state = _apply_action(state, normalized, modulus) + total += _operation_price(normalized, source_prices, add_prices) + return state, total + + +def shortest_prices( + modulus: int, + source_prices: tuple[int, int], + add_prices: tuple[int, int], + *, + include_paths: bool = False, +) -> dict[str, object]: + """Return exact optimum prices for every translation demand pair. + + The finite graph has at most ``modulus**6`` row-coefficient states. A + state is settled with its exact shortest distance; every available nonzero + coefficient is considered for both source additions and both directed + row additions. Since every supplied price is positive, ordinary Dijkstra + is valid even when the modulus is composite and some nonzero coefficients + are not units. + + ``costs`` maps ``(lambda0, lambda1)`` to its exact integer optimum. When + ``include_paths`` is true, ``paths`` maps the same keys to operation tuples + accepted by the internal exact replay checker. + """ + _validate_inputs(modulus, source_prices, add_prices, include_paths) + + operations: list[tuple[Action, int]] = [] + for dst in (0, 1): + for beta in range(1, modulus): + action: Action = ("source", dst, beta) + operations.append((action, source_prices[dst])) + src = 1 - dst + for alpha in range(1, modulus): + action = ("add", dst, src, alpha) + operations.append((action, add_prices[dst])) + + target_demands: tuple[Demand, ...] = tuple( + (lambda0, lambda1) + for lambda0 in range(modulus) + for lambda1 in range(modulus) + ) + target_by_state = {_target_state(demand): demand for demand in target_demands} + remaining = set(target_demands) + + distances: dict[State, int] = {_START: 0} + predecessors: dict[State, tuple[State, Action]] | None = ( + {} if include_paths else None + ) + settled: set[State] = set() + settled_costs: dict[Demand, int] = {} + heap: list[tuple[int, State]] = [(0, _START)] + + transition_scans = 0 + successful_relaxations = 0 + heap_pushes = 1 + stale_heap_pops = 0 + started = time.perf_counter() + + while remaining: + distance, state = heapq.heappop(heap) + if distance != distances.get(state): + stale_heap_pops += 1 + continue + if state in settled: + stale_heap_pops += 1 + continue + settled.add(state) + + demand = target_by_state.get(state) + if demand is not None and demand in remaining: + settled_costs[demand] = distance + remaining.remove(demand) + + # Expanding every settled state's complete operation list means the + # search has no depth or branch cap. We stop after all target distances + # are final; states beyond the largest settled target distance cannot + # improve any requested answer. + for action, edge_price in operations: + transition_scans += 1 + successor = _apply_action(state, action, modulus) + candidate = distance + edge_price + previous = distances.get(successor) + if previous is None or candidate < previous: + distances[successor] = candidate + if predecessors is not None: + predecessors[successor] = (state, action) + heapq.heappush(heap, (candidate, successor)) + successful_relaxations += 1 + heap_pushes += 1 + + elapsed = time.perf_counter() - started + result: dict[str, object] = { + "modulus": modulus, + "costs": {demand: settled_costs[demand] for demand in target_demands}, + "stats": { + "target_count": len(target_demands), + "settled_targets": len(settled_costs), + "settled_states": len(settled), + "discovered_states": len(distances), + "transition_scans": transition_scans, + "successful_relaxations": successful_relaxations, + "heap_pushes": heap_pushes, + "stale_heap_pops": stale_heap_pops, + "max_target_cost": max(settled_costs.values()), + "elapsed_seconds": elapsed, + }, + } + + if include_paths: + if predecessors is None: + raise RuntimeError("path predecessors were not recorded") + paths: dict[Demand, tuple[Action, ...]] = {} + for demand in target_demands: + state = _target_state(demand) + reversed_path: list[Action] = [] + while state != _START: + previous, action = predecessors[state] + reversed_path.append(action) + state = previous + paths[demand] = tuple(reversed(reversed_path)) + result["paths"] = paths + + return result + + +def _self_test() -> None: + # With q=2 and ADD prices well above every direct-source route, the direct + # one-operation-per-nonzero-demand construction is a positive control. + # A route that transfers a source coefficient between rows requires at + # least two expensive ADDs to restore both first-two-column coefficients. + control = shortest_prices(2, (1, 2), (100, 100), include_paths=True) + expected = {(0, 0): 0, (1, 0): 1, (0, 1): 2, (1, 1): 3} + if control["costs"] != expected: + raise AssertionError( + f"q=2 direct-cost control failed: {control['costs']!r} != {expected!r}" + ) + control_paths = control["paths"] + if not isinstance(control_paths, dict): + raise AssertionError("q=2 control did not return paths") + for demand, expected_cost in expected.items(): + final_state, replayed_cost = _replay_path( + 2, (1, 2), (100, 100), control_paths[demand] + ) + if final_state != _target_state(demand): + raise AssertionError(f"q=2 path missed target {demand}: {final_state!r}") + if replayed_cost != expected_cost: + raise AssertionError( + f"q=2 path for {demand} costs {replayed_cost}, expected {expected_cost}" + ) + + composite = shortest_prices(4, (25, 26), (1, 1), include_paths=True) + composite_costs = composite["costs"] + composite_paths = composite["paths"] + if not isinstance(composite_costs, dict) or not isinstance(composite_paths, dict): + raise AssertionError("q=4 composite control did not return costs and paths") + for demand, path in composite_paths.items(): + final_state, replayed_cost = _replay_path(4, (25, 26), (1, 1), path) + if final_state != _target_state(demand): + raise AssertionError(f"q=4 path missed target {demand}: {final_state!r}") + if replayed_cost != composite_costs[demand]: + raise AssertionError( + f"q=4 path for {demand} costs {replayed_cost}, " + f"expected {composite_costs[demand]}" + ) + + summaries = [ + (2, (1, 2), (100, 100)), + (3, (25, 26), (1, 1)), + (4, (25, 26), (1, 1)), + (5, (25, 26), (1, 1)), + ] + print("positive control q=2 direct costs and path replay: PASS") + print("composite q=4 all-demand path replay: PASS") + for modulus, source_prices, add_prices in summaries: + result = shortest_prices(modulus, source_prices, add_prices) + costs = result["costs"] + stats = result["stats"] + if not isinstance(costs, dict) or len(costs) != modulus**2: + raise AssertionError( + f"q={modulus} returned {len(costs) if isinstance(costs, dict) else 'no'} " + f"demand costs; expected {modulus**2}" + ) + if not isinstance(stats, dict): + raise AssertionError(f"q={modulus} did not return search statistics") + print( + f"q={modulus}: targets={stats['settled_targets']}, " + f"settled={stats['settled_states']}, " + f"discovered={stats['discovered_states']}, " + f"scans={stats['transition_scans']}, " + f"max_cost={stats['max_target_cost']}, " + f"time={stats['elapsed_seconds']:.3f}s" + ) + + for bad_args in ( + (True, (1, 1), (1, 1)), + (1, (1, 1), (1, 1)), + (2, (True, 1), (1, 1)), + (2, (1, 1), (0, 1)), + ): + try: + shortest_prices(*bad_args) # type: ignore[arg-type] + except (TypeError, ValueError): + pass + else: + raise AssertionError(f"invalid inputs were accepted: {bad_args!r}") + print("input validation controls: PASS") + + +if __name__ == "__main__": + _self_test() diff --git a/research/two-row-nonunit-fanout/tariff.py b/research/two-row-nonunit-fanout/tariff.py new file mode 100644 index 0000000000..f4d2860ae7 --- /dev/null +++ b/research/two-row-nonunit-fanout/tariff.py @@ -0,0 +1,194 @@ +"""Construct exact two-row fanout optima for comparable finite-ring demands. + +The theorem is in PROOF.md and covers arbitrary rings and positive real +prices. This executable uses explicit finite rings and positive rational +prices. Krzysztof Wójt, substantial OpenAI Codex assistance; Apache-2.0. +""" + +from dataclasses import dataclass +from fractions import Fraction +from typing import Callable + + +@dataclass(frozen=True) +class Ring: + name: str + size: int + zero: int + one: int + add: Callable[[int, int], int] + mul: Callable[[int, int], int] + neg: Callable[[int], int] + + def element(self, value: int) -> int: + if type(value) is not int or not 0 <= value < self.size: + raise ValueError("coefficient is not a canonical ring element") + return value + + def quotient(self, target: int, parent: int) -> int | None: + """Return r with target = r * parent, never parent * r.""" + self.element(target) + self.element(parent) + return next((r for r in range(self.size) + if self.mul(r, parent) == target), None) + + +def modular_ring(modulus: int) -> Ring: + if type(modulus) is not int or modulus < 2: + raise ValueError("modulus must be an integer at least two") + return Ring(f"Z/{modulus}", modulus, 0, 1, + lambda a, b: (a + b) % modulus, + lambda a, b: (a * b) % modulus, + lambda a: -a % modulus) + + +def binary_matrix_ring() -> Ring: + """M_2(F_2), row-major bits, used to expose left/right order.""" + def product(a: int, b: int) -> int: + result = 0 + for i in range(2): + for j in range(2): + entry = 0 + for k in range(2): + entry ^= ((a >> (2*i+k)) & 1) & ((b >> (2*k+j)) & 1) + result |= entry << (2*i+j) + return result + return Ring("M2(F2)", 16, 0, 9, lambda a, b: a ^ b, product, lambda a: a) + + +def binary_dual_ring() -> Ring: + """F_2[e]/e^2; a + b*e is encoded by a + 2*b.""" + def product(a: int, b: int) -> int: + constant = (a & 1) & (b & 1) + linear = (((a >> 1) & (b & 1)) ^ ((a & 1) & (b >> 1))) << 1 + return constant | linear + return Ring("F2[e]/e^2", 4, 0, 1, lambda a, b: a ^ b, product, lambda a: a) + + +@dataclass(frozen=True) +class Prices: + source: tuple[Fraction, Fraction] + add: tuple[Fraction, Fraction] + + def __post_init__(self) -> None: + for pair in (self.source, self.add): + if not isinstance(pair, tuple) or len(pair) != 2: + raise ValueError("prices must be two-element tuples") + if any(type(x) not in (int, Fraction) or x <= 0 for x in pair): + raise ValueError("prices must be positive exact rationals") + + +@dataclass(frozen=True) +class Gate: + kind: str + dst: int + coefficient: int + + +@dataclass(frozen=True) +class Plan: + name: str + price: Fraction + word: tuple[Gate, ...] + + +def word_price(word: tuple[Gate, ...], prices: Prices) -> Fraction: + total = Fraction(0) + for gate in word: + if type(gate.dst) is not int or gate.dst not in (0, 1): + raise ValueError("gate destination must be 0 or 1") + if gate.kind == "source": + total += prices.source[gate.dst] + elif gate.kind == "add": + total += prices.add[gate.dst] + else: + raise ValueError("unknown gate kind") + return total + + +def inverse(word: tuple[Gate, ...], ring: Ring) -> tuple[Gate, ...]: + return tuple(Gate(g.kind, g.dst, ring.neg(ring.element(g.coefficient))) + for g in reversed(word)) + + +def demand_quotients(ring: Ring, demand: tuple[int, int]) -> tuple[int | None, ...]: + if not isinstance(demand, tuple) or len(demand) != 2: + raise ValueError("demand must be a pair") + for element in demand: + ring.element(element) + ratios = (ring.quotient(demand[1], demand[0]), + ring.quotient(demand[0], demand[1])) + if all(r is None for r in ratios): + raise ValueError("incomparable principal left ideals are outside scope") + return ratios + + +def lower_envelope(ring: Ring, demand: tuple[int, int], prices: Prices) -> Fraction: + """The five-term theorem, independently of the chosen attaining word.""" + ratios = demand_quotients(ring, demand) + values = [sum((prices.source[i] for i in (0, 1) + if demand[i] != ring.zero), Fraction(0))] + for i in (0, 1): + j = 1-i + if demand[j] == ring.zero: + single = prices.source[i] + elif ratios[i] is not None: + single = prices.source[i] + 2*prices.add[j] + else: + single = prices.source[i] + 2*(prices.add[i] + prices.add[j]) + values.extend((single, 2*prices.source[i] + 2*prices.add[j])) + return min(values) + + +def candidates(ring: Ring, demand: tuple[int, int], prices: Prices) -> tuple[Plan, ...]: + ratios = demand_quotients(ring, demand) + plans = [] + + def retain(name: str, gates: list[Gate]) -> None: + word = tuple(g for g in gates if g.coefficient != ring.zero) + plans.append(Plan(name, word_price(word, prices), word)) + + retain("direct", [Gate("source", i, demand[i]) for i in (0, 1)]) + for i in (0, 1): + j = 1-i + retain(f"repeat-{i}", [ + Gate("add", j, ring.neg(ring.one)), Gate("source", i, demand[j]), + Gate("add", j, ring.one), + Gate("source", i, ring.add(demand[i], ring.neg(demand[j]))), + ]) + ratio = ratios[i] + if ratio is not None: + retain(f"transport-{i}", [Gate("add", j, ring.neg(ratio)), + Gate("source", i, demand[i]), Gate("add", j, ratio)]) + reverse_ratio = ratios[j] + if reverse_ratio is not None: + last = ring.add(reverse_ratio, ring.neg(ring.one)) + retain(f"mix-{i}", [ + Gate("add", i, ring.neg(last)), Gate("add", j, ring.neg(ring.one)), + Gate("source", i, demand[j]), Gate("add", j, ring.one), + Gate("add", i, last), + ]) + return tuple(plans) + + +def optimal_plan(ring: Ring, demand: tuple[int, int], prices: Prices) -> Plan: + best = min(candidates(ring, demand, prices), + key=lambda plan: (plan.price, len(plan.word), plan.name)) + if best.price != lower_envelope(ring, demand, prices): + raise RuntimeError("attaining word disagrees with the proved lower envelope") + return best + + +def execute(ring: Ring, word: tuple[Gate, ...], initial: tuple[int, int, int]) -> tuple[int, ...]: + if not isinstance(initial, tuple) or len(initial) != 3: + raise ValueError("state must contain two rows and the preserved source") + state = [ring.element(value) for value in initial] + for gate in word: + if type(gate.dst) is not int or gate.dst not in (0, 1): + raise ValueError("gate destination must be 0 or 1") + coefficient = ring.element(gate.coefficient) + if gate.kind not in ("source", "add"): + raise ValueError("unknown gate kind") + src = 2 if gate.kind == "source" else 1-gate.dst + state[gate.dst] = ring.add(state[gate.dst], ring.mul(coefficient, state[src])) + return tuple(state) diff --git a/research/two-row-nonunit-fanout/verify.py b/research/two-row-nonunit-fanout/verify.py new file mode 100644 index 0000000000..5ebff2b2ca --- /dev/null +++ b/research/two-row-nonunit-fanout/verify.py @@ -0,0 +1,245 @@ +#!/usr/bin/env python3 +"""Exact bounded corroboration, separate graph oracle, and byte bindings. + +Krzysztof Wójt; substantial OpenAI Codex assistance. Apache-2.0. +""" + +import argparse +import hashlib +import itertools +import json +from pathlib import Path +import sys +import types +from fractions import Fraction + + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] +BOUND_FILES = ( + "README.md", "PROOF.md", "TASK.json", "SOURCES.json", "VERIFY.json", + "tariff.py", "shortest_path.py", "verify.py", +) + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def load_source(name, filename): + """Execute these exact .py bytes, without consulting a bytecode cache.""" + module = types.ModuleType(name) + module.__file__ = str(HERE / filename) + sys.modules[name] = module + exec(compile((HERE / filename).read_bytes(), module.__file__, "exec"), module.__dict__) + return module + + +def bindings(): + local = {name: hashlib.sha256((HERE/name).read_bytes()).hexdigest() + for name in BOUND_FILES} + manifest = json.loads((HERE/"SOURCES.json").read_text()) + inputs = [row for row in manifest["files"] if row["usage"] == "input"] + expected = "research/unit-ring-dirty-fanout/README.md" + require([row["path"] for row in inputs] == [expected], "unexpected live source set") + for row in inputs: + digest = hashlib.sha256((ROOT/row["path"]).read_bytes()).hexdigest() + require(digest == row["sha256"], "predecessor source bytes changed") + return {"local_sha256": local, "input_sha256": {r["path"]: r["sha256"] for r in inputs}} + + +def check_ring(ring): + elements = range(ring.size) + require(ring.zero != ring.one, "zero ring is excluded") + for a in elements: + require(ring.add(a, ring.zero) == a and ring.add(ring.zero, a) == a, + "additive identity") + require(ring.mul(a, ring.one) == a and ring.mul(ring.one, a) == a, + "multiplicative identity") + require(ring.add(a, ring.neg(a)) == ring.zero, "additive inverse") + for b in elements: + require(0 <= ring.add(a, b) < ring.size and 0 <= ring.mul(a, b) < ring.size, + "operation closure") + require(ring.add(a, b) == ring.add(b, a), "additive commutativity") + for c in elements: + require(ring.add(ring.add(a, b), c) == ring.add(a, ring.add(b, c)), + "additive associativity") + require(ring.mul(ring.mul(a, b), c) == ring.mul(a, ring.mul(b, c)), + "multiplicative associativity") + require(ring.mul(a, ring.add(b, c)) == + ring.add(ring.mul(a, b), ring.mul(a, c)), "left distributivity") + require(ring.mul(ring.add(a, b), c) == + ring.add(ring.mul(a, c), ring.mul(b, c)), "right distributivity") + + +def endpoint_matches(t, ring, word, demand): + # Every gate uses left coefficients and is right-module linear. These + # three columns suffice; literal finite dirt is checked separately. + for column in range(3): + state = tuple(ring.one if k == column else ring.zero for k in range(3)) + got = t.execute(ring, word, state) + target = (ring.add(state[0], ring.mul(demand[0], state[2])), + ring.add(state[1], ring.mul(demand[1], state[2])), state[2]) + if got != target or t.execute(ring, t.inverse(word, ring), got) != state: + return False + return True + + +def check_constructions(t): + rings = [t.modular_ring(q) for q in (2, 3, 4, 5, 6, 8, 9)] + rings += [t.binary_dual_ring(), t.binary_matrix_ring()] + counts = {"rings": len(rings), "comparable_pairs": 0, "incomparable_pairs": 0, + "candidate_words": 0, "coefficient_columns_with_inverse": 0, + "literal_dirty_states_with_inverse": 0} + prices = t.Prices((Fraction(7, 3), Fraction(31, 5)), (Fraction(5, 7), Fraction(13, 11))) + for ring in rings: + check_ring(ring) + for demand in itertools.product(range(ring.size), repeat=2): + comparable = any(ring.quotient(demand[i], demand[1-i]) is not None + for i in (0, 1)) + if not comparable: + try: + t.optimal_plan(ring, demand, prices) + except ValueError as exc: + require("incomparable" in str(exc), "wrong domain rejection") + else: + raise ValueError("incomparable demand accepted") + counts["incomparable_pairs"] += 1 + continue + counts["comparable_pairs"] += 1 + for plan in t.candidates(ring, demand, prices): + require(endpoint_matches(t, ring, plan.word, demand), + f"wrong full endpoint: {ring.name}, {demand}, {plan.name}") + require(plan.price == t.word_price(plan.word, prices), "wrong word price") + counts["candidate_words"] += 1 + counts["coefficient_columns_with_inverse"] += 3 + plan = t.optimal_plan(ring, demand, prices) + require(plan.price == t.lower_envelope(ring, demand, prices), "wrong envelope") + fixtures = [(t.modular_ring(4), (2, 1), t.Prices((1, 9), (1, 1))), + (t.modular_ring(4), (2, 1), t.Prices((100, 1000), (1, 1))), + (t.modular_ring(8), (0, 2), t.Prices((1, 20), (1, 2))), + (t.binary_dual_ring(), (2, 1), t.Prices((1, 9), (1, 1))), + (t.binary_matrix_ring(), (11, 1), t.Prices((1, 20), (10, 1)))] + for ring, demand, prices in fixtures: + plan = t.optimal_plan(ring, demand, prices) + for state in itertools.product(range(ring.size), repeat=3): + target = (ring.add(state[0], ring.mul(demand[0], state[2])), + ring.add(state[1], ring.mul(demand[1], state[2])), state[2]) + got = t.execute(ring, plan.word, state) + require(got == target, "literal dirty endpoint") + require(t.execute(ring, t.inverse(plan.word, ring), got) == state, "literal inverse") + counts["literal_dirty_states_with_inverse"] += 1 + return counts + + +def check_shortest_paths(t, oracle): + price_vectors = sorted(set(itertools.product((1, 2, 3), repeat=4)) | { + (1, 9, 1, 1), (100, 1000, 1, 1), (1, 100, 100, 1), + (100, 1, 1, 100), (9, 4, 7, 1), (4, 9, 1, 7), + }) + counts = {"moduli": [2, 3, 4, 5, 8, 9], "price_vectors_per_modulus": len(price_vectors), + "searches": 0, "target_cost_comparisons": 0, "settled_states": 0, + "transition_scans": 0, "replayed_oracle_paths": 0} + digest = hashlib.sha256() + for q in counts["moduli"]: + ring = t.modular_ring(q) + for vector in price_vectors: + prices = t.Prices(vector[:2], vector[2:]) + result = oracle.shortest_prices(q, vector[:2], vector[2:]) + require(result["stats"]["settled_targets"] == q*q, "incomplete oracle search") + for demand, price in sorted(result["costs"].items()): + plan = t.optimal_plan(ring, demand, prices) + require(plan.price == price, f"shortest-path discrepancy {q, vector, demand}") + digest.update(json.dumps([q, vector, demand, price], separators=(",", ":")).encode()+b"\n") + counts["target_cost_comparisons"] += 1 + counts["searches"] += 1 + counts["settled_states"] += result["stats"]["settled_states"] + counts["transition_scans"] += result["stats"]["transition_scans"] + for vector in ((1, 9, 1, 1), (100, 1000, 1, 1)): + result = oracle.shortest_prices(4, vector[:2], vector[2:], include_paths=True) + for demand, path in result["paths"].items(): + word = tuple(t.Gate(a[0], a[1], a[-1]) for a in path) + require(endpoint_matches(t, t.modular_ring(4), word, demand), "oracle path endpoint") + require(t.word_price(word, t.Prices(vector[:2], vector[2:])) == result["costs"][demand], + "oracle path price") + counts["replayed_oracle_paths"] += 1 + counts["ordered_optimum_sha256"] = digest.hexdigest() + return counts + + +def check_controls(t, oracle): + passed = [] + ring = t.modular_ring(4) + repeat = t.optimal_plan(ring, (2, 1), t.Prices((1, 9), (1, 1))) + mixed = t.optimal_plan(ring, (2, 1), t.Prices((100, 1000), (1, 1))) + require(repeat.price == 4 and repeat.name == "repeat-0", "credited nonunit boundary") + require(mixed.price == 104 and mixed.name == "mix-0", "new mixing regime") + require(min(100+1000, 1000+2, 2*100+2) > mixed.price, + "forest-and-repeat-only counterexample lost") + passed.extend(("credited_Z4_optimum_four", "mixing_beats_forests_and_repeat")) + require(not endpoint_matches(t, ring, repeat.word[1:], (2, 1)), "omitted preparation accepted") + require(not endpoint_matches(t, ring, mixed.word[:-1], (2, 1)), "unreturned dirt accepted") + wrong_sign = (t.Gate("add", 0, ring.neg(mixed.word[0].coefficient)),) + mixed.word[1:] + require(not endpoint_matches(t, ring, wrong_sign, (2, 1)), "wrong sign accepted") + passed.extend(("omitted_preparation", "unreturned_dirt", "wrong_mixing_sign")) + noncomm = t.binary_matrix_ring() + require(noncomm.mul(1, 11) == 3 and noncomm.mul(11, 1) == 1, "noncommuting fixture") + wrong = (t.Gate("add", 1, 1), t.Gate("source", 0, 11), t.Gate("add", 1, 1)) + require(not endpoint_matches(t, noncomm, wrong, (11, 1)), "wrong multiplication order accepted") + require(noncomm.quotient(2, 1) is None and noncomm.mul(1, 2) == 2, + "left/right ideal discriminator lost") + passed.extend(("wrong_noncommutative_ratio", "left_versus_right_ideal")) + require(t.optimal_plan(ring, (0, 0), t.Prices((1, 9), (1, 1))).price == 0, + "zero demands should have an empty word") + zero_anchor = t.optimal_plan(ring, (0, 1), t.Prices((1, 9), (1, 1))) + require(zero_anchor.price == 4 and endpoint_matches(t, ring, zero_anchor.word, (0, 1)), + "zero-demand anchor was incorrectly excluded") + passed.extend(("zero_demands", "zero_demand_temporary_anchor")) + invalid = [lambda: t.modular_ring(True), lambda: t.modular_ring(1), + lambda: t.Prices((True, 1), (1, 1)), lambda: t.Prices((0, 1), (1, 1)), + lambda: t.Prices((1.0, 1), (1, 1)), + lambda: t.optimal_plan(ring, (True, 1), t.Prices((1, 1), (1, 1))), + lambda: t.optimal_plan(t.modular_ring(6), (2, 3), t.Prices((1, 1), (1, 1))), + lambda: t.execute(ring, (t.Gate("clear", 0, 1),), (0, 0, 0)), + lambda: t.execute(ring, (t.Gate("add", True, 1),), (0, 0, 0)), + lambda: oracle.shortest_prices(4, (True, 1), (1, 1))] + for operation in invalid: + try: + operation() + except (ValueError, TypeError): + continue + raise ValueError("invalid-domain control was accepted") + return {"semantic_controls": passed, "invalid_input_controls": len(invalid)} + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--write-receipt", type=Path, help="write a new receipt; never overwrite") + args = parser.parse_args() + bound = bindings() + receipt_path = HERE/"RESULT.json" + previous = None + if args.write_receipt is None: + previous = json.loads(receipt_path.read_text()) + require(previous.get("bindings") == bound, "receipt source hashes differ") + elif args.write_receipt.exists(): + raise ValueError("receipt output already exists") + t = load_source("two_row_tariff", "tariff.py") + oracle = load_source("two_row_shortest_path", "shortest_path.py") + report = {"schema": "two-row-nonunit-fanout/v1", "bindings": bound, + "construction": check_constructions(t), "shortest_paths": check_shortest_paths(t, oracle), + "controls": check_controls(t, oracle), "new_kappa": False} + canonical = json.dumps(report, sort_keys=True, indent=2) + "\n" + if args.write_receipt is not None: + with args.write_receipt.open("x", encoding="utf-8") as stream: + stream.write(canonical) + else: + require(canonical == json.dumps(previous, sort_keys=True, indent=2)+"\n", + "typed receipt content differs from the exact replay") + print("PASS_TWO_ROW_NONUNIT_FANOUT", json.dumps({k: v for k, v in report.items() + if k not in ("bindings", "schema")}, sort_keys=True)) + + +if __name__ == "__main__": + main()