Prove sharp mixed-rank invoice envelopes with touching roots (no κ)

research/mixed-rank-touching-envelope/EXAMPLE.json

@@ -0,0 +1,24 @@
+{
+  "schema": "synchronized-invoice-envelope/v1",
+  "old": {
+    "schema": "integer-mult-recursive-invoice/v1",
+    "contract": {
+      "model": "synthetic signed power invoice",
+      "boundary": "arithmetic example; no physical supplier",
+      "rank_semantics": "H_r costs r^t"
+    },
+    "paid": {"4": 3, "9": 2, "7": 11},
+    "targets": {"5": 13}
+  },
+  "new": {
+    "schema": "integer-mult-recursive-invoice/v1",
+    "contract": {
+      "model": "synthetic signed power invoice",
+      "boundary": "arithmetic example; no physical supplier",
+      "rank_semantics": "H_r costs r^t"
+    },
+    "paid": {"1": 6, "36": 1, "7": 11},
+    "targets": {"5": 13}
+  },
+  "certificate": {"bases": [2, 3], "p": 1, "q": 2, "scale": 1, "offset": 0}
+}

research/mixed-rank-touching-envelope/PROOF.md

@@ -0,0 +1,121 @@
+# Sharp synchronized mixed-rank invoice envelopes
+
+Let m be a positive even integer, let a_1,...,a_m be integers greater than
+one, let p,q be integers with 0<p<q, and let lambda>0 and epsilon>=0 be real.
+Define
+
+```text
+D(t) = epsilon + lambda product_(i=1)^m (a_i^(q t) - a_i^p).
+```
+
+Then D has global minimum epsilon on the whole real line. Its unique minimizer
+is t=p/q, which lies inside (0,1). If epsilon=0, its only real zero has exactly
+m-fold multiplicity. If epsilon>0, D is strictly positive everywhere.
+
+## Proof
+
+Each factor is strictly increasing. It vanishes exactly at p/q, is negative
+below p/q, and is positive above p/q. All m factors therefore have the same
+nonzero sign away from p/q. Their product is positive because m is even.
+At p/q the product vanishes. Positivity of lambda proves both the minimum
+and its unique location.
+
+The derivative of the i-th factor at p/q is
+q log(a_i) a_i^p>0. Its zero is simple. The product of m analytic functions
+with simple zeros at the same point has a zero of exact multiplicity m.
+Adding a positive epsilon removes all zeros, while leaving the minimizer
+and the sharp lower envelope unchanged. This proves every claim.
+
+## Exact signed invoices
+
+Suppose lambda and epsilon are nonnegative integers, with lambda positive.
+Expansion gives
+
+```text
+D(t) = epsilon + lambda sum_(S subset {1,...,m})
+          (-1)^(m-|S|) (product_(i not in S) a_i^p)
+                         (product_(i in S) a_i^q)^t.
+```
+
+All ranks and signed coefficients are integers. Equal subset products must be
+combined before comparison. No independence or distinctness of the bases is
+assumed. Put positive coefficients into the new paid histogram and negated
+negative coefficients into the old paid histogram. This realizes the signed
+difference as two nonnegative integer invoices. More generally, the checker
+accepts any placement in paid and target histograms whose full net difference
+is this polynomial. Identical arbitrary paid and target charges on both sides
+cancel. This is arithmetic realization, not a physical construction.
+
+For rational positive lambda and nonnegative epsilon, clearing their common
+denominator gives the same integer-certificate form with the correspondingly
+scaled envelope. The executable accepts the integer form only.
+
+## First mixed-rank example
+
+For m=2, a_1=2, a_2=3, p=1 and q=2,
+
+```text
+6 - 3*4^t - 2*9^t + 36^t = (4^t-2)(9^t-3) >= 0.
+```
+
+Equality holds only at t=1/2 and has exact multiplicity two. Thus the seven-job
+invoice 6 H1 + H36 costs at least the five-job invoice 3 H4 + 2 H9 for every
+power tariff, with equality at sqrt-rank pricing. Adding one H1 to the former
+gives sharp minimum gap one for every real t. Swapping the invoices reverses
+the ordering, but is not claimed to implement a cheaper physical circuit.
+
+The ranks 4 and 9 are not powers of a common integer greater than one, since
+that integer would have a prime divisor dividing both ranks. This supplies a
+genuinely mixed-rank example. There are two coefficient sign changes, and
+neither endpoint is zero. A closure rule using simple interior witnesses alone
+cannot spend a two-root budget on this double zero. The factor certificate
+supplies its multiplicity directly. This is an implication from the documented
+certificate rules in #5788, not a replay or audit of its implementation.
+
+With two distinct prime bases a,b, arbitrary 0<p<q, and offset epsilon, the
+four coefficients are epsilon+a^p b^p, -b^p, -a^p, and 1 at ranks
+1,a^q,b^q,(ab)^q. This gives an infinite family with the same sharp envelope.
+
+## Checker soundness and scope
+
+`envelope.py` parses both complete invoice histograms and identical declared
+contracts. It forms new-paid minus new-targets minus old-paid plus old-targets.
+It separately expands the supplied factors by repeated sparse multiplication,
+combines collisions, and requires exact coefficient equality. The theorem then
+justifies its reported envelope, minimizer and zero multiplicity. A matching
+contract string does not establish that either invoice describes a circuit.
+
+The verifier has no numeric root search, logarithm approximation or predecessor
+executable dependency. `verify.py` corroborates expansion independently by a
+literal subset formula, executes exact rational-power checks at exponents whose
+denominators divide q, tests target debits, and rejects mutated certificates.
+It does not use finite samples as the proof of a continuum claim.
+
+The executable bounds factors to an even count from two through eight, bases
+to 2..64, q to 2..16, expanded ranks to 10^9, histogram counts to 10^60,
+each histogram to 4096 keys, and each input to one MiB. Sparse multiplication
+has at most 256 terms per step; all loops have finite bounds from these
+capacities. The mathematical theorem has no such finite capacities. Managed
+Python allocation is a Power of Ten deviation, bounded here by input and
+support capacities; standard-library parser allocation is not statically
+preallocated. The isolated registered normal and optimized runs use the same
+explicit checks, which remain active without assertions. No shared modules
+or source pins are changed.
+
+## Predecessors and remaining obligations
+
+Ali Romman's [#5788](https://github.com/CrocSwap/integer-mult-bounds/pull/5788)
+poses the explicit touching-root continuation and supplies the general-rank
+root-budget context. Its proof and limitations are cited, not reverified.
+The signed-invoice interface is due to zxv, the moment-order context to
+mightyOil and predecessors, and the specialized T16 crossing work to woklerx.
+The factor expansion and elementary sign argument are standard algebra and
+calculus. The contribution is their exact synchronized-envelope application,
+integer invoice family and portable certificate checker; no literature
+priority for these elementary methods is claimed.
+
+There is no source-bound physical bill, native implementation, ownership or
+restoration proof, compiler admission, new kappa or complete multiplication
+theorem. Independent human and formal proof-kernel review are unclaimed.
+
+New work produced by Nick Petalas. Apache-2.0.

research/mixed-rank-touching-envelope/README.md

@@ -0,0 +1,118 @@
+# Sharp mixed-rank invoice envelopes with an interior touching point
+
+For every positive even m, integers a_i>1 and 0<p<q, lambda>0 and epsilon>=0,
+
+```text
+epsilon + lambda product_i (a_i^(q t) - a_i^p)
+```
+
+has sharp global minimum epsilon, attained uniquely at t=p/q. At epsilon=0,
+the unique zero has exact multiplicity m. The written [proof](PROOF.md) covers
+all real t and arbitrary finite even m. This is a **scoped algebraic proof**,
+with finite executable corroboration. It is an arithmetic side result, with
+no physical construction or new kappa claim.
+
+The first example is
+
+```text
+6 H1 + H36 - 3 H4 - 2 H9
+  = (4^t-2)(9^t-3) >= 0,
+```
+
+where H_r costs r^t. Equality holds only at t=1/2 and is a double zero. Adding
+one H1 makes the sharp minimum gap one. Ranks 4 and 9 have no common integer
+base. This resolves the touching-point obligation for this explicit infinite
+family without numeric root isolation or exhaustion of a global root budget.
+
+## Scope and predecessors
+
+The question is the touching-root continuation in Ali Romman's
+[#5788](https://github.com/CrocSwap/integer-mult-bounds/pull/5788), pinned at
+`56565b9aec29203bddb14f5d0e76a657d7090699`. Its
+[proof and limitation](https://github.com/aliromman/integer-mult-bounds/blob/56565b9aec29203bddb14f5d0e76a657d7090699/docs/research/recursive-power-variation.md)
+are cited, not audited or replayed. Credit zxv for signed-invoice accounting,
+mightyOil for the moment-order context, and woklerx for the specialized
+crossing predecessor. Elementary factorization and calculus retain their
+classical status; no literature priority is claimed for those methods.
+
+This changes the `independent-moment` card from checking an existing supplier
+to constructing a new exact invoice family and certificate. The card's first
+selected-baseline binding command passed; no scientific predecessor replay
+was run. [TASK.json](TASK.json) records the changed scope and source URL.
+[SOURCES.json](SOURCES.json) binds the revision-8 catalogue and selected record
+as historical provenance, with no live mathematical predecessor dependency.
+
+The complete signed difference is new paid minus new targets minus old paid
+plus old targets. `envelope.py` requires equal declared contracts and exact
+agreement with an independently supplied sparse factor certificate. Equal
+subset-product ranks are combined, including repeated bases. The executable
+reports the sharp envelope only after this identity check. Matching contract
+text does not prove a source-to-circuit interpretation.
+
+## Reproduce
+
+From the repository root, with CPython 3.12 and the standard library:
+
+```sh
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -W error -B research/mixed-rank-touching-envelope/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -O -W error -B research/mixed-rank-touching-envelope/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/mixed-rank-touching-envelope
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/mixed-rank-touching-envelope --check-source-history
+```
+
+The first two commands print a generated JSON receipt with package/input hashes,
+then `PASS_MIXED_RANK_TOUCHING_ENVELOPE`. They enumerate 696 factor contexts,
+4,176 certificates, 49,944 expanded support entries and 23,472 exact
+rational-power evaluations, with 26 rejection or mathematical failure controls.
+Two-factor contexts use every ordered pair of bases in 2..7, q in 2..5 and
+1<=p<q. Higher-factor contexts use every tuple over {2,3} of lengths 4,6,8,
+with p=1,q=2. Each context uses scales 1,3 and offsets 0,1,7. Paid and target
+placement alternates across certificates. These are finite corroboration of
+the written proof, not a finite substitute for its continuum argument.
+
+Inspect the portable authored example directly:
+
+```sh
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B research/mixed-rank-touching-envelope/envelope.py research/mixed-rank-touching-envelope/EXAMPLE.json
+```
+
+Expected minimum is 0, unique minimizer is 1/2, and root multiplicity is 2.
+The checker and verifier write no files. Redirect receipts outside the checkout
+if needed. Local checks use CPython 3.12.15 on Darwin arm64; no native packages
+are required. Hosted CI status belongs to the PR, not to this proof.
+
+## Limits
+
+The checker accepts 2,4,6,8 synchronized factors, integer bases 2..64,
+2<=q<=16, 1<=p<q, integer scale in 1..10^60 and offset in 0..10^60.
+Expanded ranks must be at most 10^9 and coefficients at most 10^60.
+Each histogram has at most 4096 keys; input files have at most one MiB.
+The mathematical theorem is not restricted to these executable capacities.
+Certificate discovery, unsynchronized touching points and arbitrary
+exponential-polynomial classification remain outside the checker.
+
+The example is synthetic. Source extraction, native implementation, ownership,
+restoration, physical target independence, supplier/compiler admission, the
+selected cold replay, Lean and a complete multiplication theorem are unclaimed.
+Independent human and formal proof-kernel review are unclaimed. The selected
+frontier and its five framework assumptions retain their existing status.
+
+## Open next questions
+
+Can an actual changed construction's complete signed invoice admit this factor
+certificate after a justified common bill cancels? Start with one published
+source-bound old/new pair and test exact sparse divisibility. This would turn
+the arithmetic envelope into a useful source comparison. The blocker is a
+complete physical bill, not finer sampling of the synthetic example.
+
+Can exact factor certificates treat several distinct touching points without
+assuming a decidable equality test for arbitrary logarithmic root ratios?
+Start with factors whose roots are supplied rational exponents and group them
+by exact rational equality. This would broaden the certified class. Root
+recognition beyond that stated rational domain remains unresolved here.
+
+## Credit
+
+New proof application, integer invoice family and portable certificate checker
+produced by Nick Petalas. Predecessor credit is retained above and in the proof.
+New work is Apache-2.0.

research/mixed-rank-touching-envelope/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"
+    }
+  ]
+}