Certify exact dyadic helper-channel capacity with Smith witnesses

research/dyadic-helper-channel-capacity/PROOF.md

@@ -0,0 +1,112 @@
+# Exact dyadic channel capacity at one cut
+
+Let D=Z[1/2]. All modules and matrices below use D. The prefix and suffix
+of a fixed cut are A and B, with B A=M invertible. There is no live owned
+field at the cut. M is a direct sum of the identity on a helper group G and an invertible
+map on its complement. All helpers
+in G have one input chart S and one output chart T. Let F be one common
+cut chart strictly between S and T. Embed its eligible physical fields
+in the full field list.
+
+Let L be the rows v supported at F such that v A has support in G.
+Let R be the columns u supported at F such that B u has support in G.
+Choose full D-module bases L0 and R0, as rows and columns respectively.
+These must be module bases, not arbitrary scaled rational-space bases.
+Set K=L0 R0. Empty modules have capacity zero.
+
+A normalized t-channel interface is a pair of coefficient matrices X,Y
+with X K Y=I_t. Its rows and columns give t dual prefix/suffix channels.
+The maximum such t is exactly the number of nonzero Smith invariant
+factors of K that are units in D. Equivalently,
+
+```text
+capacity_D(K) = min_{odd primes p} rank_(F_p)(K mod p).
+```
+
+This is the classical Smith theorem applied to the helper-cut pairing.
+It does not claim Smith normal form or the field-pairing method as new.
+
+## Proof of the optimum
+
+Clear denominators with a power of two d. Integer row and column operations
+give U(d K)V=diag(s_1,...,s_r,0), with U,V unimodular, positive s_i and
+s_i dividing s_(i+1). Clearing d does not change any unit status in D.
+Let t count the initial powers of two among the s_i. Scaling the first t
+rows of U by d/s_i and taking the first t columns of V gives X K Y=I_t.
+This constructs the full unit block, not only a numerical upper bound.
+
+If t<r, any odd prime divisor p of s_(t+1) divides all later factors.
+Exactly the first t factors remain nonzero modulo p. Thus K has rank t
+there. Any larger identity block would retain its larger rank modulo p,
+which is impossible. If t=r, rational rank supplies the upper bound.
+This also proves the formula over odd primes. An equivalent certificate
+uses the ideal generated by all minors of size t+1: Cauchy-Binet would
+put 1 in a proper ideal if a larger identity block existed. No integer
+factorization is needed to compute or certify the optimum.
+
+The Smith kernel basis is saturated. If U C V is diagonal, C x=0 is
+equivalent to setting the nonzero diagonal coordinates of V^-1 x to zero.
+The remaining columns of V give every D-valued kernel vector. This is why
+rational elimination followed by independent denominator clearing is not
+a substitute for a module basis.
+
+## From the unit block to helper channels
+
+For each selected row v and column u set a=v A and b=B u. Since M is
+identity on G and A is invertible, B A b=b=B u gives A b=u. Therefore
+all cross pairings satisfy a_i b_j=v_i u_j=delta_ij. The row and column
+maps split off a free direct summand at both the boundary and cut.
+Their complements are free over the principal ideal domain D. Complete
+these maps to invertible bases. The source's helper-handoff argument then
+isolates t identity channels simultaneously. ADDs and dyadic-unit SCALEs
+implement the finite bases. The single-channel compiler in PR5611 gives
+an explicit elementary completion; iterative restriction to the remaining
+direct summand gives the block version.
+
+This is algebraic interface capacity. A physical implementation must have
+enough cut carriers and must restore wire order, satisfy common charts,
+retain arbitrary inputs and charge all basis operations. A required
+original helper pivot at the cut is an extra restriction. This theorem
+does not silently remove that restriction from the source constructor.
+
+## A causal counterexample to rational rank
+
+Use three fields and the prefix
+
+```text
+A = [[1,0,1], [0,1,2], [1,2,6]],
+B = [[2,2,-1], [2,5,-2], [-1,-2,1]].
+```
+
+Four ADDs produce A: `x0+=x2`, `x1+=2*x2`, `x2+=x0`, `x2+=2*x1`.
+Reverse them to produce B. Both determinants are 1 and B A=A B=I.
+Take helper coordinates G={0,1} and cut coordinates F={0,1}. The row
+and column conditions are both `z0+2*z1=0`. Saturated bases are
+(2,-1), up to sign. Their pairing is [5]. Rational rank is one, but the
+dyadic capacity is zero: division by 5 is unavailable. Multiplication
+by any power of two cannot repair this defect. This is a causal scalar
+fixture, not a source-bound physical P104 construction or paid invoice.
+
+Conversely K=diag(3,5) has no unit entry, but has Smith factors 1,15 and
+capacity one. Joint combinations can create a unit pairing. Testing
+individual entries is therefore insufficient in the other direction too.
+
+## Algorithm and verification boundary
+
+The algorithm records U,S,V. A nonzero Euclidean remainder strictly
+reduces the absolute pivot. Once its row and column are cleared, an
+entry not divisible by the pivot is brought into that row; the next
+Euclidean pass reduces the pivot. The loop terminates. Each accepted
+pivot divides the remaining submatrix, so the final diagonal is in
+Smith order. All operations preserve integral unimodularity.
+
+The independent check recomputes every determinantal divisor in the
+bounded test domain. It also checks U K V, determinants of U,V and the
+constructive identity block. The written proof covers arbitrary finite
+matrices; the census checks the implementation. It is not a formal proof.
+No new native word, full caller, compiler admission or kappa follows.
+
+Ali Romman with substantial OpenAI Codex assistance. Apache-2.0.
+Credit PR5599/5602 for helper splitting, PR5609 for the field cut pairing,
+PR5611 for dual-pair completion, Nick Petalas PR5115 for row preparation,
+and the classical Smith and Euclidean algorithms.

research/dyadic-helper-channel-capacity/README.md

@@ -0,0 +1,64 @@
+# Exact dyadic capacity of a helper cut
+
+This scoped interface theorem computes the maximum simultaneous unit
+pairings over D=Z[1/2]. For full dyadic bases of the eligible prefix and
+suffix modules, form K. Its capacity is the number of Smith invariant
+factors that are powers of two, or the minimum rank modulo an odd prime.
+The algorithm returns both an attaining unit block and an upper-bound
+certificate. Complete kappa is unchanged.
+
+[PROOF.md](PROOF.md) gives the optimum and its helper-handoff application.
+[capacity.py](capacity.py) computes the Smith transformations, saturated
+kernel bases and unit block. [verify.py](verify.py) checks them by an
+independent gcd-of-minors calculation. [RESULT.json](RESULT.json) records
+2,401 exhaustive integer 2-by-2 matrices and 75 rectangular dyadic cases
+through 5-by-5, the causal controls and five rejecting controls.
+
+The causal prefix/suffix fixture has rational pairing rank one but
+capacity zero because K=[5]. The converse fixture K=diag(3,5) has capacity
+one although no entry is a unit. These prevent both rank-only false
+positives and entry-only false negatives in helper searches.
+
+## Reproduce
+
+Python 3.12 and the standard library suffice:
+
+```sh
+python3 -B scripts/research_package.py --package research/dyadic-helper-channel-capacity
+```
+
+Both modes must print `PASS_DYADIC_HELPER_CHANNEL_CAPACITY`. The launcher
+must print `PASS_REGISTERED_RESEARCH_PACKAGE`. Inputs are authenticated
+before science. No Git or network is used by the scientific replay.
+
+## Scope, source and credit
+
+Base: canonical main `6cf7a683f447b9f1e2333791907fd92be5009a63`, priority 7.
+The pinned [PR5602](https://github.com/CrocSwap/integer-mult-bounds/pull/5602)
+proof supplies the causal helper interface. The
+[claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/5125#discussioncomment-19184494)
+is separate from active physical cut searches. Current guidance and the
+selected record were rechecked. Remote pages were complete; local notes
+were sparse. No exhaustive novelty claim is made.
+
+Credit Ali Romman's [PR5599](https://github.com/CrocSwap/integer-mult-bounds/pull/5599),
+PR5602, [PR5609](https://github.com/CrocSwap/integer-mult-bounds/pull/5609)
+and [PR5611](https://github.com/CrocSwap/integer-mult-bounds/pull/5611),
+Nick Petalas's [PR5115](https://github.com/CrocSwap/integer-mult-bounds/pull/5115),
+and their retained source lineage. Smith reduction and the Euclidean
+algorithm are classical. The new contribution is their exact application
+to the full dyadic helper pairing, with constructive and obstruction
+certificates. Ali Romman with substantial OpenAI Codex assistance;
+Apache-2.0. No independent human or proof-kernel acceptance is claimed.
+
+Physical carriers, wire permutations, common frames, scalar work, growth,
+all native maps, ownership, the caller and compiler costs remain payable.
+No current P104 cut census, complete selected replay or outer funding run
+was performed. The synthetic causal fixture is not a physical supplier.
+
+## Open next questions
+
+Apply this criterion to one source cut that has positive rational rank
+but no known dyadic unit pairing. Use saturated kernel bases and publish
+its Smith certificate before optimizing a circuit. A physical gain then
+needs a permitted carrier and the complete revised paid/target invoice.

research/dyadic-helper-channel-capacity/RESULT.json

@@ -0,0 +1,17 @@
+{
+  "causal_capacity": 0,
+  "causal_pairing": [
+    [
+      5
+    ]
+  ],
+  "causal_rational_rank": 1,
+  "exhaustive_2_by_2": 2401,
+  "joint_capacity": 1,
+  "joint_factors": [
+    1,
+    15
+  ],
+  "rectangular_dyadic": 75,
+  "rejected_inputs": 5
+}

research/dyadic-helper-channel-capacity/SOURCES.json

@@ -0,0 +1,24 @@
+{
+  "schema_version": 1,
+  "base_commit": "6cf7a683f447b9f1e2333791907fd92be5009a63",
+  "files": [
+    {
+      "path": "certificates/selected-result.json",
+      "usage": "provenance",
+      "git_blob": "fc3d4ba105e1f097d0d7d051a308281e86ab1446",
+      "sha256": "66974efdced4083c00025f97d95d83909a226cdf801edb9301c195c6641f6903"
+    },
+    {
+      "path": "docs/research/agent-task-catalog.json",
+      "usage": "provenance",
+      "git_blob": "f126dd2e2dad2b669e75d1d0d0bd05c600725602",
+      "sha256": "f7a48bfa2659b88378282a8eee7d9fe52cdf505594124c4d1686b58510fffd72"
+    },
+    {
+      "path": "research/p104-coupled-helper-bases/PROOF.md",
+      "usage": "input",
+      "git_blob": "168733f6c486d689e58de15c6c34ce1b5ae6b12d",
+      "sha256": "d9049aa75f065c3c21b0f55246c433c643584bca8969f2f382a83c425c4a2927"
+    }
+  ]
+}

research/dyadic-helper-channel-capacity/TASK.json

@@ -0,0 +1,100 @@
+{
+  "schema_version": 1,
+  "task_id": "formal-interface-lemma",
+  "priority_revision": 7,
+  "base_commit": "6cf7a683f447b9f1e2333791907fd92be5009a63",
+  "original_card": {
+    "id": "formal-interface-lemma",
+    "question": "Can one uncovered interface implication be formalized with exact caller and certificate bindings?",
+    "starting_points": [
+      "docs/research/research-family-status.md",
+      "certificates/selected-result.json",
+      "research/gate-operand-parity-lean/README.md",
+      "research/staged544-certified-endpoint/README.md",
+      "research/unconditional-batched-crt/README.md"
+    ],
+    "methods": [
+      "Formalize a missing boundary lemma identified by the selected review.",
+      "Audit a formal theorem-to-certificate binding independently."
+    ],
+    "acceptance_gate": "State the exact formalized proposition and remaining assumptions; avoid duplicate arithmetic formalizations already present.",
+    "first_step": {
+      "command": [
+        "python3",
+        "-B",
+        "scripts/research_baseline.py"
+      ],
+      "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY",
+      "inspect": "Inventory the gate-operand parity lemma (#3807) and certified endpoint arithmetic (#3857). Neither is a full multiplication proof. For #4100, audit the compact-switch statement and its hypotheses before formalizing it.",
+      "scope": "Source-binding orientation only; no scientific replay, theorem acceptance or supplier admission. Budget any heavy replay separately."
+    },
+    "first_experiment": "Write one missing statement with quantified hypotheses, actual caller and existing coverage. A compact-switch lemma is a candidate only after its mathematical contract is reviewed. Establish a bounded proof plan before a separately budgeted proof-assistant build; do not rerun large Lean jobs as orientation.",
+    "bottleneck_link": "A missing interface proof can reduce the conditional gap even if it does not change kappa.",
+    "allowed_variations": [
+      "Narrow to one formal lemma or one theorem-to-certificate binding."
+    ],
+    "scope_change_triggers": [
+      "Formalizing already-covered arithmetic and claiming the full multiplication theorem."
+    ],
+    "overlap_terms": [
+      "hyperplane end",
+      "formal interface",
+      "Lean binding",
+      "3807",
+      "3857",
+      "4100",
+      "gate-operand-parity-lean",
+      "staged544-certified-endpoint",
+      "unconditional-batched-crt"
+    ],
+    "existing_checks": [
+      {
+        "scope": "PR #3807: scoped gate-operand parity formalization.",
+        "evidence": "research/gate-operand-parity-lean/README.md",
+        "remaining": "Exact theorem-to-caller binding and genuinely uncovered interface lemmas.",
+        "status": "author-checked",
+        "source_commit": "4c3530f42a6abcc48e7a6bcffd6c901911dc8269",
+        "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129"
+      },
+      {
+        "scope": "PR #3857: certified real-power moment/endpoint arithmetic.",
+        "evidence": "research/staged544-certified-endpoint/README.md",
+        "remaining": "Uniform algorithmic implications, not another endpoint digit.",
+        "status": "author-checked",
+        "source_commit": "ef4315b8caa605e47a2515004845eb2d2ed71a86",
+        "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129"
+      },
+      {
+        "scope": "PR #4100: compact-switch formalization proposed as future validation.",
+        "evidence": "research/unconditional-batched-crt/README.md",
+        "remaining": "Audit the statement and assumptions before a formal proof campaign.",
+        "status": "author-checked",
+        "source_commit": "337d04939571a637aeab54a0f58f54fde811663a",
+        "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129"
+      }
+    ]
+  },
+  "scope_status": "changed",
+  "actual_scope": "Exact maximum simultaneous unit pairings for a fixed dyadic helper-cut matrix.",
+  "scope_change_reason": "Constructive algebraic capacity and exact certificates replace the generic formalization card. No formal-kernel claim.",
+  "bottleneck_link": "The criterion prevents rational-rank overcounting and entry-test undercounting of productive helper channels.",
+  "budget_minutes": 60,
+  "stop_rule": "Prove the exact capacity, expose causal false-positive and joint false-negative examples, and independently check all certificate fields.",
+  "outcome": "completed",
+  "evidence": "PROOF.md, capacity.py, RESULT.json",
+  "author": "Ali Romman with substantial OpenAI Codex assistance",
+  "ai_assistance": "Substantial OpenAI Codex assistance.",
+  "open_questions": [
+    {
+      "question": "Does a current source cut gain a channel under the full dyadic criterion?",
+      "why_it_matters": "An additional productive target can improve the full signed moment.",
+      "first_step": "Check current claims, compute saturated kernels and their Smith pairing certificate at one candidate cut.",
+      "blocked_by": "Actual physical carriers, scalar cost and growth, native semantics and full caller funding."
+    }
+  ],
+  "coordination": {
+    "claim": "https://github.com/CrocSwap/integer-mult-bounds/discussions/5125#discussioncomment-19184494",
+    "main": "6cf7a683f447b9f1e2333791907fd92be5009a63",
+    "priority_revision": 7
+  }
+}

research/dyadic-helper-channel-capacity/VERIFY.json

@@ -0,0 +1,34 @@
+{
+  "schema_version": 1,
+  "status": "ready",
+  "python": "3.12",
+  "requirements": [],
+  "inputs": [
+    "research/p104-coupled-helper-bases/PROOF.md"
+  ],
+  "commands": [
+    {
+      "argv": [
+        "{python}",
+        "-W",
+        "error",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 60,
+      "checks": "Pinned causal interface, exhaustive Smith certificates, all determinantal divisors, constructive unit blocks, causal and false-certificate controls."
+    },
+    {
+      "argv": [
+        "{python}",
+        "-W",
+        "error",
+        "-B",
+        "-O",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 60,
+      "checks": "Pinned causal interface, exhaustive Smith certificates, all determinantal divisors, constructive unit blocks, causal and false-certificate controls."
+    }
+  ]
+}