Certify exact worst bills for adaptive typed row choices

research/adaptive-row-bill/PROOF.md

@@ -0,0 +1,100 @@
+# Adaptive complete row bills
+
+At type i, let R_i be a finite nonempty set of nonnegative rational rows of
+length n. A row must include all child, adapter and restoration charges of its
+declared contract. Each node can choose its row independently. The local toll
+is one. Define T(x)_i = max_{r in R_i} r x. A policy selects one row per type;
+its matrix is A. These are mathematical costs, not physical native operations.
+
+The certificate has exactly two possible conclusions:
+
+1. A rational u >= 1 satisfies u = 1 + T(u). A policy A attains every row:
+   u = 1 + Au. The value u is the exact worst total over all finite depths and
+   adaptive choices. All allowed rows have the common strict contraction
+   bound r u <= q u_i, where q = max_i (u_i-1)/u_i < 1.
+2. A legal policy A has a nonzero rational v >= 0 with Av >= v. Its unit-toll
+   work diverges in at least one type. Thus no finite worst total exists for
+   all types, and no common positive strict contraction weights exist.
+
+## Fixed policy alternative
+
+For M = I-A, eliminate columns without row swaps while each pivot is positive.
+The off-diagonal Schur entries stay nonpositive. If pivot k is nonpositive,
+set v_k=1 and v_j=0 for j>k. Solve the earlier triangular equations for v_i.
+The signs give v>=0. The first k original equations are zero. The k-th original
+equation is the nonpositive pivot, since earlier equations are zero. Every later
+original row is nonpositive, since it sees only off-diagonal entries on the
+support of v. Thus Mv<=0. This proves the second alternative.
+
+If all pivots are positive, substitution preserves nonnegativity. In particular
+u=M^{-1}1 is positive, and Au=u-1>=0 gives u>=1. The weighted maximum norm
+contracts by max_i (Au)_i/u_i<1. It follows that M^{-1}=sum_{j>=0} A^j>=0.
+The vector u is the unit-toll total. This is the classical M-matrix alternative.
+
+## Finite policy improvement
+
+Start with any policy. Apply the fixed policy alternative. A noncontraction
+witness ends the algorithm. Otherwise obtain its total u. For each type, select
+a row that maximizes r u. Keep the old choice at a tie. Change only rows with
+r u > u_i-1. If no row changes, u=1+T(u), as required.
+
+Suppose the next policy B also contracts, with total z. Then
+
+    z-u = (I-B)^{-1}(1+Bu-u) >= 0.
+
+The last vector is nonzero, since some row changed strictly. The inverse contains
+the identity, so at least one coordinate increases strictly. A policy cannot
+recur: its total is unique, while all later totals are at least the preceding
+total and each improvement is strict somewhere. There are only product_i |R_i|
+policies. The uncapped exact algorithm therefore terminates. The implementation
+has a declared 4096-policy default budget; exhaustion emits no certificate.
+No polynomial runtime or small rational-growth bound is claimed.
+
+## Adaptive choices and exact attainment
+
+Let x_0=0 and x_{d+1}=1+T(x_d). Induction on depth proves that x_d is the maximum
+work with d toll levels. Independent row choices are essential: every type may
+use its own maximizing row at every node. More history cannot improve this
+finite-horizon recursion. The positive vector u bounds every x_d from above.
+
+For x,y, nonnegative rows give
+
+    |T(x)_i-T(y)_i| <= max_{r in R_i} r |x-y|.
+
+Thus T is q-Lipschitz in the u-weighted maximum norm. Iteration converges to u.
+The fixed attaining policy has total (I-A)^{-1}1=u, so adaptivity cannot exceed
+this one policy. More precisely, 0<=u-x_d<=q^d u. This also gives an explicit
+finite-depth tail bound for every allowed schedule.
+
+For an unsafe witness, choose c>0 with 1>=cv. Then A^j1>=cv for every j. The
+sum through d toll levels is at least dc v, which diverges on the nonzero
+support of v. A positive weight w with Aw<w is impossible: at an index that
+maximizes v_i/w_i, monotonicity would give v_i< v_i.
+
+## Why the row contract matters
+
+The whole matrices [[0,2],[0,0]] and [[0,0],[2,0]] each have zero square. Their
+independent row menu also permits [[0,2],[2,0]], which has witness (1,1).
+Checking only the displayed whole matrices misses this legal bad combination.
+Conversely, independent row closure can add choices that a correlated physical
+contract forbids. A bad row policy then rejects the relaxation, not that physical
+contract. The same distinction applies to upper-bound rows versus exact costs.
+
+The safe menu in example.json has exact total (5,3), even though one allowed
+row has sum 6/5. The attaining rows are (1/5,1) and (2/5,0). All rows obey
+the common ratio 4/5. The example is a synthetic contract, not a selected
+supplier invoice. It shows the additional decision supported by this tool.
+
+## Credit and limits
+
+This is an exact certificate interface and proof of its implementation, not a
+new general matrix or policy-iteration theorem. Credit classical Bellman policy
+iteration and M-matrix theory. Kozyakin's
+[independent-row-uncertainty theory](https://arxiv.org/abs/1507.00492) gives the
+related spectral finiteness setting. PR5785 supplies the repository's fixed
+matrix interface; PR5892 treats observed forcing; PR6271 treats synchronized
+paid switching. Their results are not re-audited here. No physical row coverage,
+selected compiler applicability, native realization, new kappa or discharge of
+the five selected assumptions follows from this certificate.
+
+Ali Romman, with substantial OpenAI Codex assistance. Apache-2.0.

research/adaptive-row-bill/README.md

@@ -0,0 +1,83 @@
+# Exact adaptive typed bills
+
+A fixed-matrix test does not check every combination of allowed supplier rows.
+This package constructs an exact certificate for a finite nonnegative rational
+menu at each type. It either gives the exact worst unit-toll total under all
+adaptive choices, or gives one legal fixed policy that fails contraction.
+The independent checker uses only row products and inequalities.
+
+The [proof](PROOF.md) shows termination of uncapped policy iteration, exact
+attainment by one stationary policy, a common strict contraction ratio and a
+finite-depth tail bound. This is a scoped certificate implementation and proof.
+It is not a new general matrix theorem, a physical supplier or a new kappa.
+
+The [example](example.json) has exact total (5,3) and common ratio 4/5, despite
+an allowed row sum of 6/5. A separate control has two nilpotent whole modes but
+an unsafe legal row combination. Thus neither a plain row-sum test nor separate
+checks of the original whole modes settle the declared adaptive contract.
+
+## Reproduce
+
+Use CPython 3.12 and the standard library from the repository root:
+
+```sh
+python3.12 -I -B research/adaptive-row-bill/bills.py research/adaptive-row-bill/example.json
+python3.12 -I -O -Werror -B research/adaptive-row-bill/verify.py
+python3.12 -B scripts/research_package.py --package research/adaptive-row-bill
+```
+
+Save a producer certificate and pass it with `--check certificate.json` to check
+it against the problem. The checker checks the problem directly. The producer
+accepts 1..64 types and 1..64 rows per type. Its default is 4096 policy solves;
+`--policy-limit` can set a different positive limit. Exhaustion produces no
+certificate. Certificate rationals have an 8192-bit budget. Exact arithmetic
+can grow; no uniform practical runtime or polynomial complexity is claimed.
+
+The verifier independently enumerates all policies for 2538 finite row families:
+2025 two-type families on the stated three-value grid, 512 three-type binary
+support/complement families, and the example. Permutation determinants check
+all principal minors. Cramer's rule checks every finite total. It checks 12200
+policies, 1629 literal prefix/tail inequalities, four chain sizes through 64,
+and 18 invalid-input or false-certificate controls. There are 181 safe and 2357
+unsafe families. These tests corroborate the written proof; they do not replace
+its all-size argument or independent human review.
+
+## Applicability and overlap
+
+Each row must include all recursive children and all adapter and restoration
+charges. Row choices must be independently legal for each type. A bad policy
+in an upper-bound or independently enlarged menu does not disprove a smaller
+physical contract. The examples are synthetic. No current native supplier,
+compiler, stock, precision or outer budget is recertified. The selected frontier
+and all five selected assumptions are unchanged.
+
+The base is canonical main 7c49fe32c55de02c2c873655c804b16e4c3fef0a, priority 8.
+The required selected-source binding check passed after sparse source files were
+restored. The current record selects PR6030; older numeric text in the priority
+page is historical. The [advance claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/6458)
+records the changed card scope. Live Discussions, open PRs and targeted all-state
+searches were checked before the claim. The full overlap cache found no match
+for its three targeted phrases. Sparse local files, arbitrary historical diffs
+and unpublished work remain limits. No search establishes novelty.
+
+[PR5785](https://github.com/CrocSwap/integer-mult-bounds/pull/5785) supplies the
+fixed-matrix certificate. [PR5892](https://github.com/CrocSwap/integer-mult-bounds/pull/5892)
+already treats observed forcing and reachable types. [PR6271](https://github.com/CrocSwap/integer-mult-bounds/pull/6271)
+treats synchronized paid switching periods. These are different contracts, and
+no predecessor scientific result is counted or audited again.
+
+## Open next questions
+
+The structured questions are in [TASK.json](TASK.json). Bind one current complete
+supplier menu to the row contract, then use its actual compiler and outer bill.
+A separate optimization can reduce the common ratio when that ratio controls a
+real reserve or cutoff. A favorable abstract certificate alone is insufficient.
+
+## Attribution
+
+Prepared for Ali Romman with substantial OpenAI Codex assistance; no subagents.
+Credit classical M-matrix theory, Bellman policy iteration and
+[Kozyakin's independent-row-uncertainty theory](https://arxiv.org/abs/1507.00492).
+Credit Ali Romman's PR5785, Nick Petalas's PR5892 and PR6271, and the retained
+Nick Petalas, David Ganz / Dugongue, Jose Manuel and typed-recursion lineage.
+No predecessor executable is imported. Apache-2.0.

research/adaptive-row-bill/SOURCES.json

@@ -0,0 +1,18 @@
+{
+  "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"
+    }
+  ]
+}

research/adaptive-row-bill/TASK.json

@@ -0,0 +1,105 @@
+{
+  "schema_version": 1,
+  "task_id": "independent-moment",
+  "priority_revision": 8,
+  "base_commit": "7c49fe32c55de02c2c873655c804b16e4c3fef0a",
+  "original_card": {
+    "id": "independent-moment",
+    "question": "Does a changed construction's serialized target/paid invoice independently support its claimed improvement?",
+    "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",
+      "docs/research/recursive-invoice-preflight.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": "Demonstrate independence, source binding, positive cases and semantic failure controls. Name the existing checks and the missing coverage. More digits or another equivalent evaluation of an unchanged root is not by itself new verification coverage.",
+    "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": "Independently recount one changed emitted word and its complete caller, importing no constructor or pricing engine. Include target losses, owned lifetimes, native orientation and extra charges. Check existing #5633/#5708/#5717/#5719 coverage to avoid duplicate audits and preserve its exact head. Stop after the chosen missing implication; a correct root alone is not supplier admission.",
+    "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": [
+      "invoice",
+      "signed moment",
+      "productive target",
+      "independent recount"
+    ],
+    "existing_checks": [
+      {
+        "scope": "PR #4088: mixed local/owner/phase ledger and moment reported.",
+        "evidence": "research/staged544-mixed-fourth-entry/README.md",
+        "remaining": "Independent binding of changed construction to paid histogram, distinct from full admission.",
+        "status": "author-checked",
+        "source_commit": "72d7efc181edb21806a878f174847c96dd410ab0",
+        "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129"
+      },
+      {
+        "scope": "PR #4091: sharp pooled ceiling proposed for fixed THREE/FOUR words and inventory.",
+        "evidence": "research/staged-fourth-mixture-ceiling/README.md",
+        "remaining": "Validate dual, exhaustive pattern scope and exact source equivalence before applying to newer fills.",
+        "status": "author-checked",
+        "source_commit": "a29bdd8f56cd18b805917775cdec09ff935eddc4",
+        "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129"
+      },
+      {
+        "scope": "PR #4067: paid (2,2) to (1,3) exchange and fixed OQ4 host reported.",
+        "evidence": "research/r437-two-window-carrier/README.md",
+        "remaining": "Independent full cost delta; remaining caller/precision/stock obligations are separate.",
+        "status": "author-checked",
+        "source_commit": "a95f11c52e3ca1e4c5171b3c20d8f4b0815aee2e",
+        "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": "Exact worst-case unit-toll bills for finite independent row menus under arbitrary adaptive choices.",
+  "scope_change_reason": "Replace a single emitted-word recount by a reusable finite typed-recurrence certificate. PR5892 already covers observed forcing; this result changes the row-choice contract.",
+  "bottleneck_link": "A complete heterogeneous compiler invoice can have several legal rows per type. A common certificate permits every adaptive choice; a failing legal policy identifies the exact unsafe combination before physical construction.",
+  "budget_minutes": 90,
+  "stop_rule": "Finish the exact certificate, written proof, independent finite enumeration and publication. Do not infer a physical supplier or a kappa gain.",
+  "outcome": "completed",
+  "evidence": "PROOF.md; bills.py; verify.py: 2538 families, 12200 policies, 1629 prefix checks and 18 rejection controls.",
+  "author": "Ali Romman with substantial OpenAI Codex assistance",
+  "ai_assistance": "Substantial OpenAI Codex assistance in proof, implementation, verification and publication. No subagents.",
+  "open_questions": [
+    {
+      "question": "Which complete current supplier contracts permit independent choice of these typed rows?",
+      "why_it_matters": "Only a valid source-to-row binding transfers this certificate to a physical recursive bill.",
+      "first_step": "Serialize one finite menu from actual complete supplier alternatives. Include every child, adapter, restoration and type constraint.",
+      "blocked_by": "No current supplier menu has been bound here."
+    },
+    {
+      "question": "Can a smaller common contraction ratio reduce a compiler reserve or cutoff at the same saving?",
+      "why_it_matters": "The exact worst total gives valid weights but need not minimize the common ratio.",
+      "first_step": "Use exact scaled-row certificates to bracket the best ratio, then bind the improved reserve to one actual compiler.",
+      "blocked_by": "Requires a complete source menu and a concrete consumer of that ratio."
+    }
+  ]
+}

research/adaptive-row-bill/VALIDATION.md

@@ -0,0 +1,33 @@
+# Validation record
+
+Local interpreter: CPython 3.12.13, macOS arm64, standard library only.
+The exact executable was
+`/Users/aliromman/.local/share/uv/python/cpython-3.12-macos-aarch64-none/bin/python3.12`.
+
+The registered ordinary and optimized commands passed. Both emitted the same
+receipt: 2538 families, 12200 policies, 181 safe, 2357 unsafe, 1629 prefix checks,
+and 18 rejecting controls. A separate direct ordinary run also passed.
+The independent oracle uses permutation determinants and Cramer's rule; it
+imports neither the producer's elimination nor its policy decisions.
+
+At scientific commit `76447bc104e91e731ff1ddb663dcf867d7a52f86`, committed-byte
+and owner-execute-mode checks passed for all eight package files. The official
+export and its declared-input integrity check passed. Both scientific commands
+passed from the exported files with empty PATH, no Git checkout and read-only
+files/directories. All nine file hashes and modes, including export metadata,
+remained unchanged. Ordinary and optimized stdout were identical.
+
+The checkout is shallow. Full-history source preflight was not claimed. The
+package is a direct descendant of the declared canonical base; all provenance
+pins resolve at that base. There are no external runtime inputs or side-branch
+Git dependencies. This removes the missing-predecessor clean-checkout issue.
+
+Canonical main was fetched again before submission. Its base, priority and
+selected-record files were unchanged. The initial complete overlap cache covered
+409 open PRs and 6362 Discussion records. Submission checks read later Discussion
+claims and new open PR bodies through PR6466. No matching row-menu certificate
+was found. Sparse local notes and unpublished work remain coverage limits.
+
+Hosted CI is recorded in the PR after the published head is available.
+No independent human review, formal proof-kernel acceptance, selected-supplier
+replay or new kappa is claimed. No fragile workaround is used.