Prove unbounded dyadic acquisition at rational rank one (no new κ)

research/sparse-dyadic-normalization/PROOF.md

@@ -0,0 +1,135 @@
+# Sparse dyadic normalization at rational rank one
+
+Let R = Z[1/2]. One arbitrary scalar x is observed through the mandatory
+coefficient a > 0 and selected eligible coefficients b_i in Z. The decoder
+must have the form
+
+    x = c_0 (a x) + sum_{i in J} c_i (b_i x),   c_i in R,
+
+as an identity for every x. Each acquired menu entry i has its declared
+positive cost w_i. The mandatory observation is already present and is not
+included in this incremental charge. No other observation or arbitrary new
+linear combination is available for free.
+
+## 1. Exact scalar criterion
+
+Such a decoder exists if and only if
+
+    gcd(a, (b_i)_{i in J}) is a power of two.
+
+For necessity, clear a common power-of-two denominator from a proposed decoder
+identity at x = 1. The integer gcd must divide that power of two. For
+sufficiency, integer Bezout coefficients express the positive gcd g as a
+combination of the observed coefficients. If g is a power of two, dividing
+those coefficients by g gives an allowed decoder. This also handles an empty
+selection, zero menu entries and negative menu entries. The condition is on
+the odd part of the gcd, not on rational rank or on whether one entry is a
+dyadic unit.
+
+The identity is valid over any R-module. Necessity already holds when x ranges
+over R. This is not a statement for fields in which every odd prime is inverted.
+Rational observation coefficients whose denominators are powers of two reduce
+to the same integer criterion by clearing a common power of two.
+
+## 2. Exact encoding of a finite weighted cover problem
+
+Take any finite universe U, distinct odd primes p_u for its elements, and an
+indexed menu of subsets S_i of U. Repeated subsets and the empty subset are
+allowed. Define
+
+    a = product_{u in U} p_u,
+    b_i = product_{u in U minus S_i} p_u.
+
+Empty products are one. For every selected index set J, unique prime
+factorization gives the exact identity
+
+    gcd(a, (b_i)_{i in J}) = product_{u not in union_{i in J} S_i} p_u.
+
+Indeed, p_u divides a and every selected b_i precisely when no selected S_i
+contains u. All coefficients are positive squarefree divisors of the same odd
+integer a. Therefore J permits dyadic decoding if and only if its sets cover
+U. Feasibility, every feasible index set, all positive additive costs, all
+optimum costs and every optimum index set are preserved exactly. If no cover
+exists, no allowed acquisition menu decodes. If U is empty, the mandatory
+unit coefficient already decodes and the optimum incremental charge is zero.
+
+Thus the menu-selection problem contains arbitrary finite weighted Set Cover
+already at rational rank one. This is an exact finite optimization encoding;
+no new complexity-theory classification or approximation lower bound is
+needed for the obstruction claimed here.
+
+## 3. Sharp unbounded acquisition count with rank unchanged
+
+For any integer n >= 1, choose n distinct odd primes and let S_i = {i}. Then
+
+    a = p_1 ... p_n,   b_i = a / p_i.
+
+Every menu entry is necessary. If entry i is missing, every available observed
+coefficient is divisible by p_i. Clearing dyadic denominators would force
+p_i to divide a power of two, which is impossible. All n entries suffice
+because the gcd is one, so the exact minimum incremental acquisition count
+is n. For arbitrary positive prices the exact optimum is sum_i w_i.
+
+The observation matrix has one column and rational rank one before any
+acquisition, after every partial acquisition, and after completion. The
+rational decoder (a x)/a therefore sees no rank deficit, while the constrained
+dyadic decoder can require arbitrarily many acquisitions. The cheapest
+unrestricted added observation would be x itself and would require one
+acquisition; it is not in the declared singleton menu when n >= 2.
+
+For example, a = 105 and the menu is 35, 21, 15. Every two-entry selection
+leaves one odd prime in the gcd. All three decode with the literal identity
+
+    -105 + 2*35 + 21 + 15 = 1.
+
+This is the first delivered obstruction. No larger construction is pursued.
+
+## 4. Connection and limits
+
+Ali Romman's [PR #5789](https://github.com/CrocSwap/integer-mult-bounds/pull/5789)
+explicitly distinguishes rational rank certificates from dyadic completion
+and legal delivery. The new step is the sparse eligible-menu acquisition
+obstruction, not another rank certificate or an audit of that tool. Bezout,
+prime factorization and weighted Set Cover are classical ingredients.
+
+The result concerns the existence of a decoder under a declared menu. It
+does not construct a physical source, prove that any current caller realizes
+these coefficients, price coefficient synthesis, constrain intermediate
+magnitudes, restore dirty helpers, or admit an integer-multiplication supplier.
+In particular it is not an n-call lower bound for unrestricted circuits, free
+mixing of unacquired rows, nonlinear decoders, or a changed coefficient ring.
+It changes no selected frontier or inherited framework assumption.
+
+## 5. What the executable checks
+
+The all-n result above is a written proof. The independent executable
+corroborates a finite domain. It constructs menu coefficients from subset
+complements, computes gcds with the standard-library integer oracle, produces
+Bezout coefficients with a separate bounded Euclidean algorithm, and replays
+the decoder at three exact rational scalar inputs. It compares optimum costs
+with literal subset-union enumeration for every price tuple in {1,2,3}^m.
+
+The complete menu domain is 0 <= |U| <= 3, 0 <= m <= 3, with every ordered
+menu, including repetitions. Separately it checks every selection of the
+singleton family for 1 <= n <= 12 and a modular missing-prime obstruction for
+each infeasible selection. Signed, zero, non-squarefree and dyadic-unit
+boundaries, invalid inputs, forged coefficients and rational-only decoding
+controls are included. The report enumerates its actual counts and binds all
+six package files by SHA256. It is generated on stdout, never hand-written.
+
+## 6. Verification implementation bounds
+
+The executable has no recursion, external dependencies or file writes. It
+reads only the six package files for its generated hash receipt. Fixed test
+domains bound every enumeration. The decoder permits at most 16 optional rows
+of at most 4096 bits each. Extended Euclid has at most twice the larger input
+bit length plus two iterations, since every two divisions at least halve the
+positive remainder. Functions stay below 60 physical lines.
+
+Python's integer and Fraction operations allocate dynamically. This is a
+managed-runtime deviation from fixed-allocation rules, bounded here by the
+finite domains and input limits. Iterative Bezout coefficient growth is bounded
+by a product of at most 17 input magnitudes. Negative controls intentionally
+pass one of a fixed set of direct functions as a callback. Production checking
+does not use dynamic dispatch. Explicit ValueError checks remain enabled under
+-O. No compiler, external linter, proof kernel, Lean or Docker is required.

research/sparse-dyadic-normalization/README.md

@@ -0,0 +1,89 @@
+# Rational rank one does not bound sparse dyadic acquisition
+
+Claim type: scoped algebraic obstruction with finite corroboration.
+For every n >= 1 there is one scalar source, one mandatory observation and
+an n-entry eligible menu whose exact minimum incremental acquisition count is
+n, although the rational observation rank is one throughout.
+
+Take distinct odd primes p_i, mandatory coefficient a = product_i p_i, and
+eligible coefficients b_i = a/p_i. Every entry is necessary and all suffice.
+The three-entry example observes 105x and may acquire 35x, 21x, 15x. Its exact
+decoder is -105x + 2*35x + 21x + 15x = x. Any missing entry leaves an odd-prime
+obstruction to all coefficients in Z[1/2].
+
+More generally, any finite weighted Set Cover instance embeds exactly by
+setting b_i = product of the primes outside set S_i. The feasible selections,
+their complete declared acquisition charges, every optimum and infeasibility
+are preserved. [PROOF.md](PROOF.md) gives the criterion, construction and
+scope. No new complexity-theory classification is claimed.
+
+This answers an eligible-menu version of the rational-versus-dyadic boundary
+in Ali Romman's [PR #5789](https://github.com/CrocSwap/integer-mult-bounds/pull/5789).
+Its rational-rank implementation is cited, not replayed or audited. The
+contribution concerns a constrained acquisition interface; no current physical
+caller is asserted to realize this synthetic menu.
+
+## Reproduce
+
+From the repository root, using CPython 3.12 and only its standard library:
+
+```sh
+PY=/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12
+"$PY" -W error -B research/sparse-dyadic-normalization/verify.py
+"$PY" -W error -B -O research/sparse-dyadic-normalization/verify.py
+"$PY" -B scripts/research_package.py --package research/sparse-dyadic-normalization
+"$PY" -B scripts/check_research_commit.py --package research/sparse-dyadic-normalization --check-source-history
+```
+
+Any CPython 3.12 path can replace the local interpreter path. The direct marker
+is `PASS_SPARSE_DYADIC_NORMALIZATION`. Each direct invocation emits actual
+enumeration counts and a generated SHA256 receipt for all six package files,
+without writing outputs into the checkout. The registered commands run the
+normal and optimized checks separately. The source-history preflight requires
+the package to be committed first.
+
+The executable covers all ordered menus of at most three subsets of a universe
+of size at most three, including duplicate and empty sets, and all positive
+integer prices in {1,2,3}. It independently checks subset coverage, integer
+gcd, constructed Bezout decoding and literal scalar outputs. It also checks
+all selections in the singleton family through n=12, plus failure and boundary
+controls. Finite execution corroborates the proof; it does not prove the
+unbounded theorem by enumeration.
+
+## Limitations
+
+Acquisition means selecting one declared observation. Mixing an unacquired
+row, inventing a coefficient-one observation or using an odd denominator is
+outside the interface. Coefficient production, magnitude, basis changes,
+dirty-state restoration, source realization and a complete physical invoice
+remain unpriced. The result supplies no new kappa, physical supplier, selected
+frontier update, complete multiplication theorem or proof-kernel validation.
+
+The formal-interface card was changed to an informal eligible-menu obstruction
+because the cited rational tool explicitly leaves dyadic/physical completion
+open. The selected-baseline orientation passed. The implementation contains no
+predecessor code or live external input. SOURCES.json pins only historical
+orientation and card provenance; TASK.json records the contextual predecessor
+head and guide hash. Current tool limits in that PR are not hypotheses of the
+unbounded theorem.
+
+## Open next questions
+
+- Find a named physical cut with several odd-prime losses and a priced eligible
+  menu. First derive its coefficients from the actual producer and consumer.
+  Without this source adapter the result is an algebraic interface obstruction.
+- Identify a useful restriction on physical eligible menus that makes minimum
+  acquisition tractable or bounded. First test whether prime-loss sets are
+  nested, disjoint, or subject to a proved bounded-incidence condition. Generic
+  rational rank supplies none of these hypotheses.
+
+TASK.json records relevance, first steps and blockers for both questions.
+
+## Credit
+
+This contribution was produced by Nick Petalas. Credit Ali Romman #5789 for
+the rational-certificate interface and its explicit completion boundary.
+Bezout identities, ideal localization, prime factorization and weighted Set
+Cover are classical. The new contribution is their exact sparse acquisition
+encoding and sharp unbounded rank-one family in this interface. Apache-2.0.
+Independent human and formal proof-kernel review are unclaimed.

research/sparse-dyadic-normalization/SOURCES.json

@@ -0,0 +1,18 @@
+{
+  "schema_version": 1,
+  "base_commit": "de5ec2e7a6074068452f45b1a191b5c72832df4a",
+  "files": [
+    {
+      "path": "certificates/selected-result.json",
+      "usage": "provenance",
+      "git_blob": "581f8d87008354eb5b869f7ed9de1317ad837ce8",
+      "sha256": "2a0220e866417774606e0f991e41b9c1d26b1f43b97857238cf478dbc7d330b5"
+    },
+    {
+      "path": "docs/research/agent-task-catalog.json",
+      "usage": "provenance",
+      "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec",
+      "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81"
+    }
+  ]
+}

research/sparse-dyadic-normalization/TASK.json

@@ -0,0 +1,127 @@
+{
+  "schema_version": 1,
+  "task_id": "formal-interface-lemma",
+  "priority_revision": 8,
+  "base_commit": "de5ec2e7a6074068452f45b1a191b5c72832df4a",
+  "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_selected_baseline.py"
+      ],
+      "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY",
+      "inspect": "Resolve the current selected review, separate complex/ordinary BIT/admitted BIT/outer budgets, and compare the card against live handoffs before starting. Historical ceilings require exact source/model equivalence.",
+      "scope": "Source-binding orientation only; not a scientific replay or all-size proof. Materialize selected inputs if this checkout is sparse."
+    },
+    "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 weighted prime-cover encoding for selecting scalar observations admitting a Z[1/2] decoder; sharp unbounded acquisition count at rational rank one.",
+  "scope_change_reason": "The user requests original research rather than audit. PR5789 explicitly leaves dyadic completion and physical delivery outside rational rank; this changes formalization to a self-contained informal sparse-menu obstruction.",
+  "bottleneck_link": "Rational rank alone cannot price which eligible observations must be acquired for a dyadic decoder. This side result prevents zero-cost sparse-completion assumptions; it supplies no physical supplier.",
+  "budget_minutes": 60,
+  "stop_rule": "Ship the first verified prime-cover obstruction and rank-one family; stop extending after its bounded replay passes.",
+  "outcome": "completed",
+  "evidence": "PROOF.md gives the arbitrary-size proof. verify.py independently enumerates subset covers, computes integer gcd and Bezout decoders, checks weighted optima and literal exact scalar outputs.",
+  "author": "Nick Petalas",
+  "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.",
+  "open_questions": [
+    {
+      "question": "Does a named physical cut realize a nontrivial prime-loss menu?",
+      "why_it_matters": "Only a source adapter can turn this synthetic obstruction into a physical acquisition bill.",
+      "first_step": "Derive coefficients and eligible observations from one actual producer/consumer cut.",
+      "blocked_by": "No source-bound physical cut or complete restoration cost is supplied."
+    },
+    {
+      "question": "Which proved physical menu restrictions make minimum acquisition tractable or bounded?",
+      "why_it_matters": "The generic rank-one interface preserves arbitrary finite weighted cover problems.",
+      "first_step": "Test a source-derived menu for nested, disjoint or bounded-incidence prime-loss sets.",
+      "blocked_by": "Physical menu restrictions and coefficient-generation costs are unknown."
+    }
+  ],
+  "claim_type": "scoped algebraic obstruction with finite corroboration",
+  "claim_url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19216201",
+  "predecessor": {
+    "pr": 5789,
+    "author": "Ali Romman",
+    "head": "c282c77bf89c001816c241a013e16441a649936e",
+    "guide_path": "docs/research/rational-rank-certificates.md",
+    "guide_sha256": "6f2ce4b63b58379e674dd23c403098219211727dbd9ec190b4134ad6f691efd6",
+    "usage": "Context and question source only. No predecessor executable or theorem is needed for the self-contained proof."
+  },
+  "environment": {
+    "python": "3.12.15",
+    "platform": "macOS-27.0.1-arm64-arm-64bit",
+    "dependencies": "standard library only"
+  },
+  "finite_evidence": {
+    "menus": 689,
+    "menu_selections": 5054,
+    "weighted_menus": 16609,
+    "literal_decodings": 4530,
+    "sharp_family_sizes": 12,
+    "sharp_family_selections": 8190,
+    "rejection_controls": 15,
+    "boundary_controls": 4,
+    "semantic_controls": 3
+  }
+}