Prove an exact integer dirty-fanout shortening gap (no κ)

research/integer-fanout-shortening-gap/PROOF.md

@@ -0,0 +1,120 @@
+# An integer shortening obstruction
+
+## Contract and theorem
+
+Let `a,b,p` be arbitrary elements of `Z^w`, where `w>=1`. The source p is
+preserved. Exactly two dirty working rows A and B start at a and b. Allowed
+gates have arbitrary integer coefficients and are only
+
+```text
+P0(t): A += t p       P1(t): B += t p       price mu each
+E0(t): A += t B       E1(t): B += t A       price c each.
+```
+
+Prices mu and c are positive, stationary and coefficient-independent. All
+gates, including inverses, are paid. There are no extra rows, free scales,
+free swaps, observers, branching or free basis changes. A word is finite
+and independent of its input values. Its endpoint must be
+
+```text
+A = a + 5p, B = b + 12p, with p unchanged.
+```
+
+**Theorem.** The exact minimum price over all such words is
+`min(2 mu, mu+6c)`. In particular it is 16 when mu=10 and c=1.
+
+This is a scoped algebraic tariff. The assumption of coefficient-independent
+prices is a declared interface, not a claim about actual fixed-tape costs.
+
+## Lower bound
+
+With no source insertion, both source coefficients stay zero, so the word
+cannot attain the endpoint. A word with at least two insertions costs at least
+2 mu. This bound does not limit their placement or their coefficients.
+
+Consider a word with exactly one insertion `Pi(beta)`. Let L be the 2-by-2
+integer matrix of all row additions before it and C the matrix of all row
+additions after it, in their chronological action order. Dirt restoration
+requires `CL=I`. The source column is `beta C e_i = (5,12)^T`.
+
+Every elementary row-addition matrix has determinant one. Each column of
+C is therefore primitive. Equivalently, its coordinates have gcd one,
+because the corresponding row of C inverse is an integral Bezout witness.
+The source equation gives `|beta|=gcd(5,12)=1`. Thus
+`C e_i` is either `(5,12)^T` or `(-5,-12)^T`.
+
+Neither signed column can be obtained from either coordinate vector with
+at most two integer row additions. Consecutive additions in one direction
+combine into one. Of the two alternating orders, one has an initially
+inactive first gate. The only remaining possibilities, including shorter
+words, are
+
+```text
+from e0: (1,t) or (1+s t,t),
+from e1: (t,1) or (t,1+s t),        s,t in Z.
+```
+
+For e0, the latter form would require t=12 or t=-12. Its first coordinate
+is 1 modulo 12, whereas 5 and -5 are not. The former form has first
+coordinate one. For e1 the latter form would require t=5 or t=-5. Its
+second coordinate is 1 modulo 5, whereas 12 and -12 are not. The former
+form has second coordinate one. All possibilities fail.
+
+Consequently every suffix C uses at least three row additions. Every
+prefix L uses at least three as well. Otherwise reversing its at-most-two
+gates and negating their coefficients would express `L^-1=C` with at most
+two gates, contradicting the same column obstruction. Exactly one insertion
+therefore costs at least `mu+6c`. Together with the insertion-count split
+this proves the lower envelope. Arbitrarily large integer coefficients and
+arbitrarily long interleavings have not been bounded or omitted.
+
+## Attainment
+
+Let C be the following three row additions in chronological order
+
+```text
+E1(2), E0(2), E1(2).
+```
+
+Their matrix is `[[5,2],[12,5]]`, with determinant one and first column
+(5,12). Perform C inverse, then `P0(1)`, then C. In literal order this is
+
+```text
+E1(-2), E0(-2), E1(-2), P0(1), E1(2), E0(2), E1(2).
+```
+
+Every dirt column returns and the source contribution is exactly (5,12).
+The price is `mu+6c`. Direct insertions `P0(5),P1(12)` cost 2 mu. These
+two words attain both branches of the envelope, including their tie at
+mu=6c. Since equality of the full integer coefficient matrices implies
+equality on each coordinate, both constructions work for every w>=1.
+
+## Why finiteness matters
+
+Ali Romman's PR5312 extends lee-phys's finite-commutative formula to finite
+associative rings. Its shortening step is expressly finite; this package
+does not dispute that theorem. Formally applying its five-term formula over
+Z to demand (5,12), with equal directional prices, would give
+`min(2mu,mu+4c)`: the demand ideal is principal and neither demand divides
+the other. At mu=10,c=1 this is 14, strictly below the proved optimum 16.
+
+Thus principality alone does not justify that finite-length tariff over
+integer coefficients. This example does admit one insertion; its extra
+restoration cost, rather than infeasibility, is the obstruction. The result
+does not exclude a different integer formula, extra dirty rows, rational or
+dyadic coefficients, coefficient-dependent pricing or a different caller.
+
+## Finite evidence
+
+The new verifier checks the complete 3-by-3 operators, literal dirty inputs,
+both attaining costs and semantic mutations. It also enumerates every
+column reachable in at most two shears over Z/60Z, with all sixty residue
+coefficients in each direction. Both signed target columns are absent from
+both origins. A separate direct normal-form set gives the identical result.
+Every integer two-shear word maps into this finite quotient, so this is
+also an independently rerunnable finite certificate of that local step.
+It does not replace the written insertion-count and restoration argument.
+
+Elementary matrices, primitivity and Bezout identities are classical. The
+new repository result is this exact integer tariff and its finite-ring
+extension discriminator; global literature priority is unclaimed.

research/integer-fanout-shortening-gap/README.md

@@ -0,0 +1,132 @@
+# An exact integer dirty-fanout tariff beyond finite-ring shortening
+
+This contribution was produced by Nick Petalas. Apache-2.0.
+Independent human and formal proof-kernel review are unclaimed.
+
+**Claim type: scoped proof with exact finite corroboration.** For two arbitrary
+dirty integer rows a,b and one preserved source p, require
+`A=a+5p, B=b+12p`. Permit only integer source insertions and integer scaled
+row additions, at uniform positive prices mu and c respectively. All dirt
+must return, with no extra row, free scale or free basis change. The exact
+minimum over arbitrary finite input-independent words is
+
+```text
+OPT = min(2 mu, mu + 6 c).
+```
+
+At mu=10,c=1 the optimum is 16. Formally extending the five-term finite-ring
+formula would give 14. This is a sharp obstruction to that extension; the
+predecessor's finite-ring theorem remains outside the claim being proved.
+
+[PROOF.md](PROOF.md) proves the unrestricted coefficient and word-length
+statement. With one insertion, the suffix must have primitive column
+plus or minus (5,12). Every two-shear integer column has a coordinate one
+or has one coordinate congruent to one modulo the other. Neither target
+sign passes. Dirt restoration requires the inverse prefix, giving at least
+six paid row additions. The following chronological word attains that bound
+
+```text
+B -= 2A; A -= 2B; B -= 2A; A += p; B += 2A; A += 2B; B += 2A.
+```
+
+Two direct insertions attain the other branch. The proof applies to every
+positive row width by exact equality of the full coefficient operators.
+
+## Evidence and reproduction
+
+From the repository root with CPython 3.12 and the standard library
+
+```sh
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/integer-fanout-shortening-gap/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -O -W error -B research/integer-fanout-shortening-gap/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/integer-fanout-shortening-gap
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/integer-fanout-shortening-gap --check-source-history
+```
+
+On another host substitute its CPython 3.12 executable. The direct verifier
+prints `PASS_INTEGER_FANOUT_SHORTENING_GAP` inside a generated JSON receipt
+bound to all six package files. It writes no files. The registered runner
+prints `PASS_REGISTERED_RESEARCH_PACKAGE`. No receipt is handwritten.
+
+The verifier checks both complete 3-by-3 dirty/source operators and the
+attaining inverse, literal integer input fixtures, rational price fixtures
+and semantic mutations. A complete modulo-60 column census includes every
+residue coefficient in both directions through two shears. A separate
+normal-form calculation produces the same reachable sets. Both signed
+columns are absent from both origins. Reduction maps every integer word
+into that quotient, making this a finite certificate of the local lower-bound
+step. The universal tariff still uses the written insertion-count proof.
+The generated receipt supplies the exact enumerated counts.
+
+The local replay enumerates 1,458 dirty-input executions, 729 rational
+price pairs, 1,617 reachable quotient columns per origin and 14,400
+quotient transitions across both searches. All sixteen semantic rejection
+controls pass. Normal and optimized receipts agree exactly.
+
+## Source, credit and overlap
+
+Credit Ali Romman's [PR5312](https://github.com/CrocSwap/integer-mult-bounds/pull/5312)
+for the finite-ring five-term tariff and its explicit infinite-ring boundary,
+lee-phys's PR5139 for the finite-commutative formula, Krzysztof Wojt's PR5045
+for the insertion/return classification, Ross Richardson's PR3121 for the
+dirty-fanout lineage, Nick Petalas's PR4916 for the older unit-demand ring
+contract, and Ali Romman's PR5310 for finite-module shortening. Their
+predecessor credits remain intact. No predecessor executable or scientific
+census is replayed as this contribution. Elementary matrices, Euclidean
+arithmetic and Bezout identities are classical; global literature priority
+is unclaimed.
+
+Base canonical main is `2485805a6d47f36ea83ddde6327d453ac82d44dc`, priority
+revision 8. [Advance claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19294861).
+[SOURCES.json](SOURCES.json) pins the finite-ring README as context, not as
+a mathematical dependency for the integer proof. The source PR head is
+`5cbdbc8e3858e67c8bfbd160f742ef1e9ced9d38`. TASK.json explicitly changes the
+connector-alphabet card to this scoped interface side result. Its first
+945-pairing control and the selected source-binding orientation passed.
+
+Live handoffs, active Discussions, current open PRs, recent account work,
+local reservations and distinctive main/merged searches were checked.
+No same-demand integer shortening result was found in that coverage.
+Recent three-row Boolean and directed-cycle tariff results have different
+row/topology contracts. Sparse local notes, arbitrary historical diffs and
+unpublished work remain coverage limits. No novelty guarantee follows.
+
+## Limits and implementation bounds
+
+This proves an abstract exact tariff under the stated arithmetic and price
+contract. It supplies no physical caller, rounded implementation, recursive
+invoice gain, new kappa or complete multiplication theorem. The selected
+frontier and five framework assumptions retain their status. No selected
+cold replay, native suite, Lean or Docker build was run.
+
+The checker has fixed domains: 3-by-3 matrices, words of at most eight gates,
+coefficients of magnitude at most twelve, 9^3 input triples, at most 40^2
+price fixtures, and two depth-two searches in a 60^2-state quotient. These
+are checker capacities, not bounds on the theorem. The proof covers arbitrary
+integer coefficients and word lengths. There is no recursion, subprocess,
+network access, dynamic code or writable output. Every function fits below
+sixty lines. Explicit guards remain enabled under optimized Python.
+
+Power of Ten rule 3 has a managed-runtime deviation: CPython allocates
+integers, fractions and bounded collections. At most 3600 quotient states
+and six one-MiB file reads constrain live data. No allocation-free runtime
+claim is made. A fixed-buffer port would be needed if that becomes a host
+requirement. Warning-strict normal/optimized runs and available static
+analysis provide the interpreted-code diagnostics.
+No separate Python linter is installed; source compilation and a static
+function-length inspection also pass, with a largest function of sixteen
+lines.
+
+## Open next questions
+
+- Can one-insertion restoration require arbitrarily many row additions for
+  primitive integer demands? This determines whether a finite shortening
+  allowance needs an unbounded replacement. Start with signed Euclidean
+  paths and include their inverse-prefix costs. A general shortest-column
+  classification is not supplied here.
+- Does a real helper caller enforce integer coefficients and supply complete
+  coefficient-independent prices? Pin its arithmetic, source access, frames,
+  precision and tape contract before using this tariff. No such caller or
+  favorable complete invoice is supplied here.
+
+These questions are recorded in TASK.json. Stop at this first exact result.

research/integer-fanout-shortening-gap/SOURCES.json

@@ -0,0 +1,24 @@
+{
+  "schema_version": 1,
+  "base_commit": "2485805a6d47f36ea83ddde6327d453ac82d44dc",
+  "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/noncommutative-two-row-tariff/README.md",
+      "usage": "input",
+      "git_blob": "e10c6ed3e334833381a5fdd6194f5997b748588a",
+      "sha256": "4493ad8069af23eec19c8bccc685a41444d712167a1e7b3e6cd5121a7d1ba130"
+    }
+  ]
+}

research/integer-fanout-shortening-gap/TASK.json

@@ -0,0 +1,75 @@
+{
+  "schema_version": 1,
+  "task_id": "connector-alphabet-change",
+  "priority_revision": 8,
+  "base_commit": "2485805a6d47f36ea83ddde6327d453ac82d44dc",
+  "original_card": {
+    "id": "connector-alphabet-change",
+    "question": "Does one explicit extension of the connector alphabet offer a favorable completed budget?",
+    "starting_points": [
+      "docs/research/research-family-status.md",
+      "research/universal-connector-boundary/README.md",
+      "certificates/selected-result.json"
+    ],
+    "methods": [
+      "Construct and charge a legal extra operation on a minimal instance.",
+      "Prove a target-specific bound after adding one specified operation family."
+    ],
+    "acceptance_gate": "State which fixed-alphabet premise changes and charge its implementation; do not declare it free. A scoped local result may be retained without a complete supplier. Expanding it into further construction rounds requires the family-level budget and obligation gate in research-family-status.md; an optimistic passing relaxation alone is not acceptance.",
+    "first_step": {
+      "command": [
+        "python3",
+        "-B",
+        "research/universal-connector-boundary/verify.py"
+      ],
+      "expected": "PASS_UNIVERSAL_CONNECTOR_BOUNDARY",
+      "inspect": "Reproduce the 945-pairing control, then read Exact interface to list the allowed calls.",
+      "scope": "Positive control / source-bound orientation only; this is not a new construction or full cold replay."
+    },
+    "first_experiment": "Add exactly one legally priced operation and test a tiny dirty-input instance before enumerating larger cases.",
+    "bottleneck_link": "A new legal connector operation could change recursive interface cost; a larger census in the same alphabet is a separate side result.",
+    "allowed_variations": [
+      "Choose one additional operation and a small source count for its first counterexample."
+    ],
+    "scope_change_triggers": [
+      "Keeping the alphabet and only increasing the source count; record this as a changed assignment.",
+      "Extending a source-count census without naming a supplier/interface decision it could change; audit #2973 pruning concerns before relying on the affected predecessor exclusions."
+    ],
+    "overlap_terms": [
+      "universal connector",
+      "source-toggle",
+      "connector alphabet"
+    ]
+  },
+  "scope_status": "changed",
+  "actual_scope": "Exact unrestricted integer-coefficient tariff for demand (5,12) on two dirty rows and one preserved source, at equal positive source and row-ADD prices.",
+  "scope_change_reason": "The connector card is changed to a scoped infinite-coefficient interface obstruction. The source finite-ring shortening theorem explicitly excludes infinite rings; this is a new tariff result, not a predecessor audit or a new operation supplied to the selected caller.",
+  "bottleneck_link": "Side result: prevents importing a finite-ring helper-delivery price into an integral dirty-restoration contract without an additional shortening proof. It does not improve the selected invoice.",
+  "budget_minutes": 60,
+  "stop_rule": "Ship the first exact tariff and its attaining word; no general Euclidean-length classification or physical implementation expansion.",
+  "outcome": "completed",
+  "evidence": "PROOF.md and standalone verify.py; full dirty/source operators, complete two-shear quotient obstruction, literal input executions, tariff fixtures and semantic rejection controls.",
+  "author": "Nick Petalas",
+  "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.",
+  "open_questions": [
+    {
+      "question": "Which primitive integer demands require arbitrarily many paid row additions with exactly one source insertion?",
+      "why_it_matters": "A uniform finite-ring shortening allowance might need an unbounded integer replacement.",
+      "first_step": "Relate the shortest attainable primitive-column path to a signed Euclidean algorithm, preserving the inverse-prefix cost.",
+      "blocked_by": "No general integer shortest-column classification is proved here."
+    },
+    {
+      "question": "Does an actual helper caller enforce integer coefficients and provide coefficient-independent complete prices?",
+      "why_it_matters": "The scoped tariff has no supplier consequence without a matching arithmetic and physical contract.",
+      "first_step": "Pin one caller, its allowed coefficient domain and its complete source/ADD tariff before applying the example.",
+      "blocked_by": "No selected caller or rounded/tape realization is supplied."
+    }
+  ],
+  "source_question": {
+    "source": "PR #5312",
+    "author": "aliromman",
+    "head": "5cbdbc8e3858e67c8bfbd160f742ef1e9ced9d38",
+    "question": "Originally posed exact integer tariff at the source theorem's explicit infinite-ring scope boundary; not a claimed question from its physical-realization handoff."
+  },
+  "claim_url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19294861"
+}

research/integer-fanout-shortening-gap/VERIFY.json

@@ -0,0 +1,36 @@
+{
+  "schema_version": 1,
+  "status": "ready",
+  "python": "3.12",
+  "requirements": [],
+  "inputs": [
+    "research/noncommutative-two-row-tariff/README.md"
+  ],
+  "commands": [
+    {
+      "argv": [
+        "{python}",
+        "-I",
+        "-W",
+        "error",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 60,
+      "checks": "Exact full dirty/source operators, complete modulo-60 short-column certificate, prices and semantic rejection controls."
+    },
+    {
+      "argv": [
+        "{python}",
+        "-I",
+        "-O",
+        "-W",
+        "error",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 60,
+      "checks": "Identical fixed-domain theorem corroboration with optimized Python; guards remain enabled."
+    }
+  ]
+}