Disprove the universal Omega cut and prove the dyadic error asymptotic (no κ)

research/dyadic-omega-counterexample/README.md

@@ -0,0 +1,145 @@
+# The dyadic formal error peak has leading constant two
+
+**Exact counterexample and scoped written proof; No new κ.** In the unchanged
+balanced dirty word, the proposed universal Omega cut does not maximize
+accumulated independent completed-leaf errors. At 128 factors a later scratch
+readout has total formal channel mass **26,144**, versus **26,028** at Omega.
+The same mechanism gives a family of counterexamples at every dyadic size
+from 128 onward, and an asymptotically sharp all-cut upper bound:
+
+\[
+E_\infty(2^h)\le 2\cdot4^h-3^h,
+\qquad \lim_{h\to\infty}\frac{E_\infty(2^h)}{4^h}=2.
+\]
+
+The old fixed Omega cut has leading constant 11/6. This is a result about
+formal free-algebra error mass, not a multiplication speed improvement or
+physical rounding lower bound. The complete argument is in [PROOF.md](PROOF.md).
+It uses credited source lemmas; neither human independent review nor a formal
+proof kernel is claimed. Finite checks corroborate, rather than prove, the
+all-height statements.
+
+## Exact result and chronology
+
+For height h>=2, use the positive word on n=2^h factors; number registers
+x=0, y=1, z_j=j+1. Read z_2 at completed-leaf count
+`4^h-(4^(h-2)+2)/3`. Its exact total channel mass is
+
+    K_h = (47*4^h - 68*3^h + 48*2^h - 20)/24.
+
+Subtracting the fixed Omega mass gives
+`4^h/8-3^h+2^(h+1)-1`, positive for every h>=7. At h=7:
+
+| Readout | Completed leaves | Register | Nonzero channels | Total mass |
+| --- | ---: | ---: | ---: | ---: |
+| New cut | 16042 | 3 | 15594 | 26144 |
+| Omega | 15018 | 8 | 14891 | 26028 |
+
+[WITNESS.json](WITNESS.json) includes both full profiles and SHA256 digests of
+**every signed channel polynomial**, including zero channels. The first error
+budget at which this new profile wins is 15479. At budget 29 the old cut still
+wins, 176 versus 175: the new cut is not a replacement universal profile.
+
+A deeper version of the same cut family approaches leading constant two.
+The upper bound pairs a forward prefix with its complementary inverse prefix,
+and charges their combined mass to complete-call exit supports. Section 6 of
+the proof gives explicit finite formulas and the limiting argument. We do not
+claim the first possible counterexample, an exact finite-height global
+maximum, or a maximizing cut for every error budget.
+
+## Source pins, novelty and credit
+
+Base and checkpoint canonical main:
+`7c49fe32c55de02c2c873655c804b16e4c3fef0a`.
+[SOURCES.json](SOURCES.json) pins all five live inputs by SHA256 and Git blob,
+and the selected certificate/task catalogue as historical provenance.
+The selected accepted value at this base is 0.003125804, from #6030's audited
+source `772dd10a5859a1d15f4851feb371519789213ad8`; it is unchanged.
+
+- Chafik Boukhalfa's #628 supplies the balanced reserved-depth dirty word.
+- Philippe Van Velzen (`philippeVV`), #2177, original head
+  `2cbbb48d3b580e018312278c97b63817de963be7`, supplies the single-error and
+  prefix/exit lemmas, finite accumulated-error census, and conjecture C1.
+  Its substantial Claude assistance and predecessor credit remain intact.
+- ywz65, #2735, original head `90a507b39063cfaebdf92794fcb9d18f358439a6`,
+  proves the fixed Omega profile and complete-call support recurrences,
+  explicitly leaving C1 open. That fixed-cut theorem is unaffected.
+- Adam Gall's #2067 supplies endpoint channel counts. Retain the earlier
+  transport lineage credited by #2177, including woklerx, Charles Bethin
+  (#1416), Arham Tahir (#1374) and Hanson Sun (#1085).
+- The overlap review also considered #5938, #6668 and #6770. Their
+  single-channel/count or interval-transport scopes differ from the sum over
+  all independent errors in a chronological prefix here; they are not inputs.
+
+The new contribution is the C1 counterexample, its exact all-height family,
+and the matching leading asymptotic for global formal total mass. No copied
+source verifier or recurrence engine is used. The primary replay extracts only
+an authenticated predecessor leaf generator for an explicit order comparison;
+its own word and polynomial engines remain separate. The forward replay uses
+neither that generator nor the primary engine.
+
+Prepared for **@CubeJerry**, with substantial **OpenAI Codex assistance** in
+mathematics, code, verification and writing. All new files are Apache-2.0.
+No delegated agents or independent human review are represented.
+
+## Reproduce
+
+Python 3.12, standard library only, from the repository root:
+
+```sh
+python3 -I -B scripts/research_package.py --package research/dyadic-omega-counterexample
+```
+
+Expected: `PASS_REGISTERED_RESEARCH_PACKAGE research/dyadic-omega-counterexample outcome=completed`,
+with `PASS_DYADIC_OMEGA_COUNTEREXAMPLE`, `PASS_FORWARD_OMEGA_COUNTEREXAMPLE`, and
+`PASS_COLD_OPTIMIZED_AND_TAMPER_CONTROLS`. The package authenticates its five
+source inputs. A Git-free export runs the three registered commands directly;
+provenance/metadata validation through the repository hook additionally uses Git.
+
+The bounded replay checks:
+
+- 134 literal source-order comparisons; 32 full profile comparisons through
+  height 8; 28 literal generalized-family cases; 4950 integer
+  recurrence/formula pairs through height 100.
+- A separately written **forward** interpreter of all 16,384 witness leaves,
+  using reversed literal lists for inverses and integer-encoded words rather
+  than backward tuple words. Both complete signed polynomial digests match.
+  Another 1954 paired-prefix/readout cases check the upper-bound mechanism
+  through height 4, including scratch-bound equality.
+- Ten primary and four forward controls, including wrong inverse order,
+  omitted restoration, endpoint/wrong-register substitutions, independent
+  versus shared opposite errors, and altered typed/profile/digest receipts.
+- Cold Git-free replay under optimized Python (`-O`) with warnings treated
+  as errors, then actual corruption of each source input and the witness,
+  all required to fail. This is a portability/failure-detection check,
+  not a third independent mathematical implementation.
+
+[VALIDATION.md](VALIDATION.md) records the executed checks and their limits.
+[TASK.json](TASK.json) records the changed scope, seed, local claim,
+search/overlap coverage and stopping rule; [VERIFY.json](VERIFY.json) registers
+exact commands. Sparse archive search and live term searches are not an
+exhaustive novelty certificate. No repository-wide historical scientific
+replay is needed or claimed for this isolated result.
+
+## Scope and inherited assumptions
+
+Errors are distinct formal symbols injected **after completed leaves**.
+Factors are free and noncommuting; the source's prefix and exit lemmas and
+exact scratch restoration are retained. Mass bounds operator error for
+contractive factors by the triangle inequality; simultaneous realization
+by native operators or rounding is not proved. The package does not cover
+internal leaf intermediates, numerical inverses, aliasing, a rounded caller,
+or precision/tape costs. All five selected assumptions remain:
+`native_all_columns`, `owned_erasure`, `compiler`, `precision_tape`,
+`analytic_recovery`. C1 is a separate conjecture, not a selected assumption.
+
+## Open next questions
+
+1. Determine exact finite-height maxima and error-budget tradeoffs. A useful
+   next step is a proved phase recurrence preserving complete channel profiles
+   and collisions; a mass-only exploratory recurrence is insufficient.
+2. Connect this formal envelope to one pinned native rounding implementation,
+   including inverse phases, restoration, boundaries and tape costs, before
+   pricing any effect at the selected multiplication caller.
+
+The finished result requires neither question to be settled. **No new κ.**

research/dyadic-omega-counterexample/SOURCES.json

@@ -0,0 +1,48 @@
+{
+  "schema_version": 1,
+  "base_commit": "7c49fe32c55de02c2c873655c804b16e4c3fef0a",
+  "files": [
+    {
+      "path": "certificates/selected-result.json",
+      "usage": "provenance",
+      "git_blob": "d59b5035e7b4cbaa9d688a1d32dd0d6eb79c466a",
+      "sha256": "9b8d0eea95b3bf0dfcb7938a732a6439b87a2685dec2a5ab9e525b3b34debbfa"
+    },
+    {
+      "path": "docs/research/agent-task-catalog.json",
+      "usage": "provenance",
+      "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec",
+      "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81"
+    },
+    {
+      "path": "research/leaf-destination-transport-bound/PROOF.md",
+      "usage": "input",
+      "git_blob": "ff752af80689686a4d8732f4697accecface37ae",
+      "sha256": "c7ac98425cac43065cb146bb87c21ac490de7497c9d577074c03a8234397d2ad"
+    },
+    {
+      "path": "research/leaf-destination-transport-bound/PROOF3.md",
+      "usage": "input",
+      "git_blob": "b08078b6968cb251d0fe28b0e69fb279edf32bac",
+      "sha256": "3d29811586a624633a960733fb23899fbfa8fc04aa59a7b2975614f4ec5e873a"
+    },
+    {
+      "path": "research/leaf-destination-transport-bound/check2.py",
+      "usage": "input",
+      "git_blob": "446842aaa233624a19f192db36df4a1660a4b1da",
+      "sha256": "e4c7e04f421a62905c1f9a35caf0559cebde8c9dca4a5053fd46ab950222cc08"
+    },
+    {
+      "path": "research/leaf-destination-transport-bound/omega.py",
+      "usage": "input",
+      "git_blob": "a8205f03c4e51329ee2dd3f1ab7a6deb38fb8d03",
+      "sha256": "f17d03e94daa1ca0292c136d194e456fe4faf37aa0881b444d0c00b4656abc56"
+    },
+    {
+      "path": "research/leaf-omega-profile/README.md",
+      "usage": "input",
+      "git_blob": "5d8b2ed9ecca470d946092814827c36e4f8c7aef",
+      "sha256": "0bb9e452a29a4bd5490ac8153273f8acad1c79147b7f485b38b9bbc48acc4d47"
+    }
+  ]
+}

research/dyadic-omega-counterexample/TASK.json

@@ -0,0 +1,120 @@
+{
+  "schema_version": 1,
+  "task_id": "uniform-transfer-audit",
+  "priority_revision": 8,
+  "base_commit": "7c49fe32c55de02c2c873655c804b16e4c3fef0a",
+  "original_card": {
+    "id": "uniform-transfer-audit",
+    "question": "Can one of the selected record's five inherited assumptions be proved at its actual caller?",
+    "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"
+    ],
+    "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": "Identify the proposition and what would change downstream; do not equate a finite replay with a universal proof.",
+    "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": "Choose one assumption ID (native_all_columns, owned_erasure, compiler, precision_tape, analytic_recovery), one quantified implication and exact dependency closure. Check current handoffs, including #5625 row reentry and #5707 root-prefix lowering, without treating their partial scope as the whole theorem. Prove or falsify that implication with a caller-bound argument; stop at the chosen obligation. Finite tests or root digits do not discharge an all-size statement.",
+    "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": [
+      "native_all_columns",
+      "owned_erasure",
+      "compiler",
+      "precision_tape",
+      "analytic_recovery"
+    ],
+    "existing_checks": [
+      {
+        "scope": "PR #4100: proposed unconditional construction and finite checks, without independent acceptance.",
+        "evidence": "research/unconditional-batched-crt/README.md",
+        "remaining": "Independent proof audit of one caller-bound all-size implication; all other premises remain explicit.",
+        "status": "author-checked",
+        "source_commit": "337d04939571a637aeab54a0f58f54fde811663a",
+        "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129"
+      },
+      {
+        "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": "Test PR2177 Conjecture C1 for independent completed-leaf errors in the unchanged balanced dirty word; give an exact dyadic counterexample and a written all-height asymptotic bound.",
+  "scope_change_reason": "After the revision-8 selection and live overlap review, narrowed the precision audit to the explicitly open historical C1 conjecture in #2177/#2735. This is not an audit or discharge of the selected record's precision_tape assumption at its caller.",
+  "bottleneck_link": "Precision-side result: a proposed universal interior cut underestimates formal accumulated leaf-error mass. The new all-cut upper bound and matching leading asymptotic replace that conjectural estimate within the dirty-word model. No complete numerical compiler, supplier admission or improvement in kappa follows.",
+  "budget_minutes": 120,
+  "stop_rule": "One deterministic dyadic phase-structure investigation, heights 0..8 for candidate discovery; stop the global-optimality search after finding and independently replaying a strict witness. Extend only the same complementary-cut mechanism to an all-height family and upper bound. Freeze the mathematical scope before the final 30 minutes of the 120-minute budget; no unrelated search or parameter sweep.",
+  "outcome": "completed",
+  "evidence": "PROOF.md gives C1 counterexamples for h>=7, a source-derived upper bound, and E_infinity(2^h)/4^h -> 2. WITNESS.json records 26144 versus 26028 at n=128. verify.py and forward_check.py use different word generation, propagation directions and monomial encodings; they match complete signed channel digests. portable_check.py checks optimized Git-free replay and actual input/receipt corruption.",
+  "author": "@CubeJerry",
+  "ai_assistance": "Prepared for @CubeJerry with substantial OpenAI Codex assistance in source review, mathematics, implementation, testing and writing. No delegated agents, independent human review or proof-kernel acceptance is claimed.",
+  "open_questions": [
+    {
+      "question": "What is the exact finite-height maximum, and which cuts maximize each error budget?",
+      "why_it_matters": "The new family fixes the asymptotic leading constant but does not replace C1 with a universal maximizing profile; at budget 29 the old cut still wins.",
+      "first_step": "Develop a proved finite-state phase recurrence that retains complete profiles or a certified dominance relation, then test all cuts and both orientations at small heights.",
+      "blocked_by": "A proof that the state representation preserves every channel collision and the tradeoffs between error budgets; the exploratory mass recurrence is not such a certificate."
+    },
+    {
+      "question": "How does this formal error envelope enter an actual rounded compiler at the selected caller?",
+      "why_it_matters": "Formal free-algebra mass is only an upper error envelope; actual precision cost and attainability determine whether this affects the multiplication construction.",
+      "first_step": "Pin one native operator realization and its per-leaf rounding model, including inverse phases, internal intermediates, boundary values and restoration, before pricing a complete caller.",
+      "blocked_by": "No such native rounding or tape model is supplied by this package; all five selected framework assumptions remain."
+    }
+  ],
+  "track": "adversarial-audit",
+  "track_integer": 64,
+  "selection_seed": "00000000000000000000000000000064",
+  "claim": {
+    "created_utc": "2026-11-06T11:56:00Z",
+    "expected_finish_utc": "2026-11-06T13:51:00Z",
+    "method": "Complementary forward/inverse phase cuts; exact free-algebra replay. No randomized sampling.",
+    "coordination": "Local claim: no pinned sprint issue found; connected tools do not expose Discussions posting. Read Discussions #1163/#1166 and active discussion list; do not create a reservation issue."
+  },
+  "overlap": {
+    "candidates": [
+      "Net completion-tax application (#6769/#6771, recently covered)",
+      "Independent-leaf interior accumulation (chosen; C1 open in #2177/#2735)",
+      "Restored-helper compression contract (#6760, recently covered)"
+    ],
+    "sources": "Current priority and family files; PR ledger; live all-state PR searches for Omega/channel, C1/leaf, Omega/counterexample and 26144; #2177, #2735, #5938, #6668 and #6770.",
+    "limits": "Sparse offline search read 7 notes and omitted 8910 paths; live term searches and handoff review reduce overlap risk but are not an exhaustive novelty certificate.",
+    "distinct_result": "#2735 proves the fixed Omega profile and leaves C1 open. #6668 concerns maximal single-channel counts; #6770 concerns interval register transport. This package counts every independent error over a chronological prefix and disproves C1."
+  },
+  "checkpoint": {
+    "at_utc": "2026-11-06T12:34:13Z",
+    "canonical_main": "7c49fe32c55de02c2c873655c804b16e4c3fef0a",
+    "result": "Pre-publication canonical main unchanged after fetch; revision 8, selected certificate, guidance and frozen inputs unchanged. Live overlap rechecked; no same-scope result found in the documented term searches."
+  },
+  "coverage": {
+    "literal_profiles": "32 full profiles for Y/Z at heights 0..8 and new/Omega at heights 2..8",
+    "general_family": "28 literal (h,m) pairs for 2<=h<=8, 1<=m<h; 4950 exact recurrence/formula pairs through h=100",
+    "forward_witness": "All 16384 leaves, both specified readouts, complete signed channel-polynomial digests",
+    "upper_bound_corroboration": "1954 paired-prefix/readout cases at heights 0..4, both orientations; written proof is the all-height evidence",
+    "search_limit": "No assertion of earliest possible counterexample, exact finite maximum, exhaustive parameter search, or universal profile."
+  }
+}