Repository navigation
Conversation
This was referenced Oct 27, 2026
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Summary
Prove the exact price six for demand
(2,1,1)overZ/4whenE_10,E_21,E_02andP_0cost one and every other directed gate type costs 100. This resolves the concrete cheap-cycle case in lee-phys #5163, Open next question 1. The source is preserved and every original dirty input is restored. All nonzero coefficients, arbitrary interleavings and repetitions are allowed, with no workspace or free basis changes.Claim type: scoped written proof with an exact finite certificate. The new word adapts child-first preparation to separated source insertions. A written incoming-row/unit-insertion argument excludes every cheaper word at every positive vector width. The finite certificate independently excludes all words of length at most five. No new kappa, physical caller, full multiplication theorem or selected-frontier change is claimed.
This contribution was produced by Nick Petalas. Credit lee-phys #5163 for the question, destination-price theorem and unit-arrival argument; Krzysztof Wójt #5045 for nonunit source counts and repeated-insertion constructions; Ross Richardson #3121/#3063 for edge-priced forest synthesis and dirt restoration; Nick Petalas #4916; Cinna Davis #1944/#1968; Anthony #774; Oscar Fennell #759; Tekalign #3130 and the retained lineage. Predecessor results are cited, not audited or replayed as this contribution. Independent human and formal proof-kernel review are unclaimed.
Evidence
Before: #5163 solves destination-only prices and explicitly leaves independently priced directed edges open. After: one suggested cheap-cycle instance has a complete attaining word, a universal lower-bound proof and an exact short-word exclusion.
Local warning-strict normal and optimized CPython checks both pass:
2d215b3748c3bec4ccd7984c4da5e172c54844e6. Official export integrity/input coverage and both read-only Git-free normal/optimized replays pass; all seven export files remain unchanged.From the contribution checkout root:
Any CPython 3.12 installation can replace that local interpreter. Only the standard library is needed. Expected markers are
PASS_Z4_DIRECTED_CYCLE_FANOUT,PASS_REGISTERED_RESEARCH_PACKAGEandPASS_RESEARCH_COMMIT_BYTES.Limitations and unrun obligations
Only this fixed abstract price matrix is solved. The full directed-price envelope, physical coefficient preparation, source access, routing, native frames, precision/tape, storage and supplier/outer admission remain open or unpriced. No Lean, Docker or selected scientific cold replay was run. Every registered command ran locally; no mathematical check is deferred solely to CI.
Scientific base is freshly fetched canonical main
19fdb086ea96af9a9f87936a2b888e10af4ed810, priority revision eight, unchanged at submission refresh. TASK.json explicitly changesbit-helper-contractto this algebraic side question. The advance CLAIM, live fanout thread, open/all-state account and topic searches, batch reservations and all-main README searches were checked. Entry cache coverage was 310 open PRs and 5,456 Discussion records. Arbitrary historical diffs and unpublished work remain outside novelty coverage.Open next questions
Related open work
Research: nonconsecutive commuting C3 fanout schedule #1865 studies commuting shared-source C3 fanout intervals in a fixed scalar word. This PR solves a
Z/4independently directed abstract tariff; no shared word profile or kappa is compared.Copied-information floor of the selected centre path #3120 studies copied-information rank of the selected centre endpoint. This PR computes no centre rank and supplies no selected physical caller.
research: centre sink duality, dependent-triple braid sparsity (|B| <= 12), and circle-cancellation sharing ceilings #3147 studies centre incidence, sink duality and sharing ceilings. Its native object and invoice differ from this three-row ring-valued tariff; no shared numerical quantity is compared.
Prove connected restored source-XOR words need 2(n-1) calls (no new κ) #5935 proves a connected-restoration lower bound for source-XOR words over fields. This PR has a preserved source, a nonidentity fanout endpoint and nonunit coefficients over
Z/4; it computes no shared numerical quantity.The completion refresh inspected all 13 other open PRs from this account created since the advance CLAIM. None studies this independently priced
Z/4demand or computes its minimum. No additional mathematical computations were run to compare those contributions.CI notes
Both hosted checks passed at contribution head
2d215b3748c3bec4ccd7984c4da5e172c54844e6in run 40523755100:planin 5m9s andreplay (research/z4-directed-cycle-fanout)in 1m19s. Run metadata confirms the exact head and completed success. Hosted replay certifies the registered package checks, including normal and optimized commands; independent human and formal proof-kernel review remain unclaimed. All reported local checks also passed.Merge Danger
Door: two-way. Blast radius: isolated. Six new files in one opt-in research package; no shared implementations, predecessor credits, frozen inputs or selected records change.