Prove exact helper capacity under odd-denominator budgets (no κ)

research/odd-budget-helper-capacity/PROOF.md

@@ -0,0 +1,129 @@
+# Exact helper capacity with prescribed odd denominators
+
+This scoped algebraic result was produced by Nick Petalas. Apache-2.0.
+
+## Contract and theorem
+
+Let D=Z[1/2]. Let K be any finite m-by-n matrix over D. Fix positive odd
+integers a,b. A t-channel boundary is a pair of rational matrices
+
+```text
+X in Mat(t,m,Q),  Y in Mat(n,t,Q),  X K Y = I_t,
+a X over D,       b Y over D.
+```
+
+These are denominator divisibility budgets. They do not bound coefficient
+magnitudes, dyadic precision, operation count or native availability.
+In particular, a bound on the numerical size of a denominator is a different
+contract. The t=0 boundary is allowed.
+
+Choose a normalized dyadic Smith chart
+
+```text
+U K V = diag(h_1,...,h_r,0),
+U in GL_m(D), V in GL_n(D),
+0 < h_1 | h_2 | ... | h_r, all h_i odd.
+```
+
+Such a chart exists by the classical integer Smith theorem after clearing a
+power-of-two denominator and absorbing powers of two into U. The factors h_i
+are the positive odd parts of the ordinary integer Smith factors.
+
+**The maximum t is the number of h_i dividing ab.** By divisibility order
+these are an initial segment. Equivalently, for 1 <= t <= r a t-channel
+boundary exists exactly when h_t divides ab. For t>r it is impossible.
+
+Consequently, for 1 <= t <= r, the least positive odd q permitting qX and
+qY over D is
+
+```text
+q_t = product over odd primes p of p^ceil(v_p(h_t)/2).
+```
+
+More strongly, every feasible common q is a multiple of q_t. For t=0 use
+q_0=1; for t>r no q works. With a dyadic suffix only, b=1, the exact
+one-sided denominator requirement is h_t | a. With a=b=1 the theorem
+reduces to Ali Romman's #5615 criterion. That case and Smith reduction
+are credited predecessors, not new results here.
+
+## Attainment
+
+Let h_t divide ab and take the first t rows and columns of the Smith chart.
+Define
+
+```text
+X[i,:] = (b/h_i) U[i,:],
+Y[:,i] = V[:,i]/b,             1 <= i <= t.
+```
+
+Then XKY=I_t entry by entry. Also aX has rows (ab/h_i)U[i,:], hence is
+dyadic, and bY consists of columns of V. This constructs all channels
+simultaneously. It needs no unproved lifting of a residue-ring solution.
+The symmetric denominator formula follows by applying this construction
+with a=b=q_t.
+
+## Necessity, including rectangular maps and prime powers
+
+Write A=aX and B=bY. The endpoint implies AKB=ab I_t. Substitute the
+Smith chart and absorb its dyadic inverse factors into A and B. It suffices
+to consider
+
+```text
+A' S B' = ab I_t, S=diag(h_1,...,h_r,0),
+A',B' over D.
+```
+
+The rational rank of S gives t<=r. Suppose h_t does not divide ab. Choose
+an odd prime p with v_p(h_t)>e=v_p(ab), and let k be the number of h_i
+with v_p(h_i)<=e. Divisibility order gives k<t. The remaining entries of
+S, including its zero entries, are divisible by p^(e+1).
+
+Work in R=Z_(p), the rationals whose reduced denominators are not divisible
+by p. The first k rows of B' form a k-by-t matrix. Since k<t, its rational
+kernel contains a nonzero vector. Multiply that vector by a rational
+scalar so every coordinate has nonnegative p-valuation and at least one
+has valuation zero. The resulting vector c belongs to R^t, is primitive
+at p, and is killed by those first k rows exactly.
+
+It follows that S B' c belongs to p^(e+1) R^m: the first k coordinates
+are zero, and each remaining nonzero diagonal coordinate has that
+divisibility. Multiplying by A' preserves the inclusion. But ab c has
+at least one coordinate of valuation exactly e. This contradicts
+A' S B' c=ab c. Thus h_t must divide ab.
+
+This argument permits arbitrary rectangular A',B' and arbitrary dyadic
+mixing. Reduction only modulo p would miss obstructions when p divides
+ab. The primitive-kernel step is why the full prime valuations matter.
+No determinant-only bound or rational-rank relaxation substitutes for it.
+
+## Example and use
+
+For odd factors (1,27,675), the first, second and third common-denominator
+requirements are respectively 1,9,45. A common q=15 admits only one
+channel, even though it includes both relevant odd primes. The asymmetric
+budgets (a,b)=(9,3) admit two, while (9,75) admit three. In every case
+the boundary matrices above attain the count, even after non-diagonal
+invertible dyadic basis changes.
+
+The new result quantifies the finite exact-division debt when a helper
+cut fails the dyadic unit criterion. It does not imply that either boundary
+map is legal in a native word. If the proposed boundary needs dyadic
+bases, productive target completions, ownership or physical carriers,
+those conditions still require separate proofs. Odd-scalar support in
+another package is not an automatic admission of these maps.
+
+## Evidence limits and credit
+
+The proof covers every finite dyadic matrix and every positive odd budget.
+The executable accepts supplied, checked Smith charts with at most six
+rows/columns, 256-bit input entries, and odd factors/budgets below 2^20.
+Its finite witnesses and independent residue-ring oracle corroborate this
+new contract. They do not prove the universal quantifiers or replay any
+predecessor's scientific suite.
+
+Credit Ali Romman #5615 for the saturated helper-cut pairing interface,
+with #5599/#5602 helper splitting, #5609 cut pairings, #5611 completion,
+Nick Petalas #5115 row preparation and their retained native/controller/
+compiler lineage. Smith normal form, localization and elementary valuation
+arithmetic are classical. No literature-wide priority for those methods,
+physical supplier, new kappa or complete multiplication theorem is claimed.

research/odd-budget-helper-capacity/README.md

@@ -0,0 +1,93 @@
+# Exact helper capacity under odd-denominator budgets
+
+Scoped written algebraic proof with exact finite corroboration, produced by
+Nick Petalas. For a dyadic helper-cut pairing K with positive odd Smith
+factors h_1 | ... | h_r and prescribed positive odd integers a,b,
+
+```text
+max { t : X K Y=I_t, aX and bY dyadic } = #{ i : h_i divides ab }.
+least common odd denominator for t channels = product_p p^ceil(v_p(h_t)/2).
+```
+
+Every feasible common denominator is a multiple of the displayed integer.
+This extends Ali Romman's [#5615](https://github.com/CrocSwap/integer-mult-bounds/pull/5615)
+dyadic-only boundary, the case a=b=1. It measures the finite exact-division
+debt needed to remove that obstruction. These are denominator divisibility
+budgets, not numerical denominator-size or norm budgets. No new kappa,
+physical supplier or selected-frontier change is claimed.
+
+For factors (1,27,675), the exact common-denominator thresholds are 1,9,45.
+A common denominator 15 still admits just one channel. Budgets (9,3) admit
+two and (9,75) admit three. [PROOF.md](PROOF.md) proves the criterion in every
+finite rectangular dimension with a prime-local kernel argument and explicit
+attaining maps. [capacity.py](capacity.py) validates a supplied dyadic Smith
+chart and constructs those maps and a prime obstruction.
+
+## Evidence and reproduction
+
+The [verifier](verify.py) checks non-diagonal dyadic charts, every pair from a
+finite budget menu, least-common-denominator attainers and indispensable primes.
+A separate exhaustive residue-ring factorization oracle searches right factors
+and every left row modulo 9. Complete scalar searches include deeper prime
+powers at 3 and 5. A control excludes a two-channel boundary missed by
+determinant divisibility alone. Invalid charts, budgets and altered witnesses
+must reject. No predecessor scientific code or census is imported or rerun.
+
+Run from the repository root with CPython 3.12 and its standard library:
+
+```sh
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -W error -B research/odd-budget-helper-capacity/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -O -W error -B research/odd-budget-helper-capacity/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/odd-budget-helper-capacity
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/odd-budget-helper-capacity --check-source-history
+```
+
+Another CPython 3.12 path may be substituted. The verifier prints a computed
+JSON receipt with `PASS_ODD_BUDGET_HELPER_CAPACITY`, counts and SHA256 hashes
+of all eight package files and its declared proof input. It writes no files.
+The runner prints `PASS_REGISTERED_RESEARCH_PACKAGE`; the committed-byte
+preflight prints `PASS_RESEARCH_COMMIT_BYTES`. Checks remain active with `-O`.
+Exact measured coverage and local command times are in the PR body.
+
+[SOURCES.json](SOURCES.json) binds the catalogue, selected record and credited
+proof input to base e54523517d0f03e58352e647c403a5af3e525a57. The catalogue
+context is older than selected #7000; the source-bound baseline was used for
+orientation. The changed card scope is in [TASK.json](TASK.json).
+
+## Limitations
+
+The universal theorem has a written proof. The executable accepts supplied
+Smith charts with at most six rows/columns, 256-bit dyadic input entries and
+positive odd factors and budgets below 2^20. It does not compute Smith charts.
+Runtime bounds and deviations are in [SAFETY.md](SAFETY.md).
+
+This supplies no actual selected prefix/suffix modules, physical carriers,
+common charts, legal productive-target completions, dirty restoration or an
+implementation of the odd divisions. Basis synthesis, coefficient magnitude,
+precision, storage, movement and the complete paid/target and outer invoice
+remain unpriced. The five framework assumptions retain their status. Selected
+cold replay, native execution, Lean and Docker were not run. Independent human
+and formal proof-kernel review are unclaimed.
+
+## Open next questions
+
+1. At one named source cut with a failed dyadic pairing, what odd denominator
+   is necessary and implementable under its exact scalar service? Extract full
+   saturated modules and a Smith chart first, then price the boundary maps and
+   restore every arbitrary input. Source availability and the complete physical
+   bill are the missing obligations.
+2. Can an attaining boundary satisfy a prescribed coefficient norm or growth
+   bound? Begin with the three-factor example and a stated norm budget.
+   Denominator feasibility alone supplies no magnitude guarantee.
+
+## Credit and scope
+
+The new bounded-denominator criterion, maps, prime-power proof and checker were
+produced by Nick Petalas. Credit Ali Romman #5615 for the helper-cut interface,
+#5599/#5602 helper splitting, #5609 pairing, #5611 completion, Nick Petalas #5115
+row preparation and their retained native/controller/compiler lineage. Smith
+normal form, localization and valuation arithmetic are classical. No
+literature-wide priority for these methods is claimed. New work is Apache-2.0;
+predecessor files and credit are unchanged.
+
+[Advance claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19542451).

research/odd-budget-helper-capacity/SAFETY.md

@@ -0,0 +1,62 @@
+# Executable bounds and inspection
+
+Produced by Nick Petalas. Apache-2.0.
+
+The executable validates supplied dyadic Smith charts. It computes no Smith
+form and imports no predecessor algorithm. The only external input is the
+pinned proof text, read for authentication. Scientific checks use no subprocess,
+network, floating-point arithmetic, recursion or source-file mutation.
+
+## Bounds
+
+Input matrices have one through six rows/columns. Each reduced numerator and
+denominator has at most 256 bits. Entries must be dyadic; U,V must be square
+with dyadic-unit determinant. The full Smith identity and positive odd
+chain are checked. Odd factors/budgets are at most 2^20-1. Matrix loops have
+at most six iterations, products at most 6^3 terms and elimination six pivots.
+Intermediate exact arithmetic is bounded by these input sizes.
+
+Trial division visits at most 511 odd candidates through the factor's square
+root, with at most twenty divisions per candidate. Budget products are below
+2^40; the valuation loop has forty-one slots. The common-denominator function
+accepts at most six factors. Production functions are below sixty physical
+lines. Contract failures raise explicit exceptions and remain active with -O.
+
+The independent modulo-nine oracle visits at most 9^4 right factors and 9^2
+left rows per two-channel system; the one-channel bounds are 9^2 each. The
+largest live image has 81 tuples. The scalar oracle has at most 125^2 pairs
+per system. Every verifier domain is a literal bounded range or finite product.
+Each registered command has a 120-second timeout. Local timings are in the PR.
+
+## Managed-runtime deviations
+
+Rule: Power of Ten 3, fixed allocation.
+Location: both Python files during exact arithmetic and exhaustive checks.
+Reason: CPython integers, Fractions and tuple construction allocate dynamically;
+fixed-allocation execution is unavailable in this runtime.
+Scope: this bounded single-process certificate command.
+Compensating control: explicit matrix, bit, factor, budget and enumeration caps;
+no growing work queue or retained candidate-factorization list. Sources are the
+eight committed files and one hash-authenticated declared proof.
+Verification: normal/optimized checks exercise input-capacity rejection, complete
+residue domains and witness contracts.
+Follow-up: larger constants require a fresh arithmetic/memory analysis; a
+fixed-allocation deployment needs a separate backend.
+
+Rule: Power of Ten 9, indirect calls.
+Location: verify.py expect_rejection.
+Reason: this bounded test helper receives three explicit candidate functions.
+Scope: invalid-input controls only, with no externally supplied call target.
+Compensating control: each site names construct, matrix or common_denominator.
+Verification: every control must raise; a positive boundary must pass.
+Follow-up: inspect any added call target explicitly.
+
+Rule: Power of Ten 10, diagnostics.
+Location: the two standalone Python files and package commands.
+Reason: this standard-library package has no compiled backend or required
+separate project Python type-checker.
+Scope: these new files only.
+Compensating control: warning-strict normal/optimized runtime, source compilation,
+available static diagnostics, source pins and committed-byte/history checks.
+Verification: exact commands and outcomes are in the PR body.
+Follow-up: keep these checks; any native backend needs its own analyzers.

research/odd-budget-helper-capacity/SOURCES.json

@@ -0,0 +1,24 @@
+{
+  "schema_version": 1,
+  "base_commit": "e54523517d0f03e58352e647c403a5af3e525a57",
+  "files": [
+    {
+      "path": "certificates/selected-result.json",
+      "usage": "provenance",
+      "git_blob": "75d77b328ea02ded535e7f23aee5b1e55d0bb1a8",
+      "sha256": "154c3d30455d778fd3343b6b4851f0fa4665f0f7625b0adb3675e2bafbbf6bf1"
+    },
+    {
+      "path": "docs/research/agent-task-catalog.json",
+      "usage": "provenance",
+      "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec",
+      "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81"
+    },
+    {
+      "path": "research/dyadic-helper-channel-capacity/PROOF.md",
+      "usage": "input",
+      "git_blob": "c97a6edce3070414c81f0ef6e6c099ebb17f3a90",
+      "sha256": "b258a217f2cd0fc48461285fe8ae24de26b0c5963668d9d8f0955fc6e759e929"
+    }
+  ]
+}