Spend the power-variation root budget on outside-domain roots: 391 → 2987 certified (no new κ)

research/power-variation-outside-roots/README.md

@@ -0,0 +1,157 @@
+# Outside-domain root witnesses for the power-variation certificate
+
+**Scoped proof and exact checker; no new κ.** The general-rank invoice
+certificate from Ali Romman's PR5788
+([`recursive-power-variation.md`](../../docs/research/recursive-power-variation.md))
+bounds all real roots of `F(t) = Σ c_r r^t` by the number `V` of sign changes
+in the rank-ordered coefficients. It spends that budget only on `t = 0`, `t = 1`
+and brackets inside `(0,1)`. Roots at `t < 0` or `t > 1` leave the budget
+unspent, so the report is `inconclusive`. That document's Open next question
+asks for a proof that a root lies outside the domain.
+
+This package proves such roots from exact data and subtracts them before the
+interior count. On a factored oracle census of 4,455 invoices, the predecessor
+certifies 391. With this change, 2,987 are certified (2,596 newly settled).
+There are no false certificates and no changed predecessor verdicts.
+
+For example, `4 - 8·2^t - 3^t + 2·6^t = 2(2^t - 1/2)(3^t - 4)` has `V = 2` and
+equal endpoint values `-3`. The predecessor reports `inconclusive`. Here an
+exact zero at `t = -1` and a sign change on `(1,2)` use both roots, so the
+difference is **uniformly lower on all of `0 < t < 1`**. The fixture
+`15 - 20·2^t - 3·3^t + 4·6^t` has an irrational root in `(-1,0)` and is settled
+in the same way.
+
+## Statement
+
+Let `F(t) = Σ_i c_i r_i^t` with distinct positive integer ranks
+`r_0 < … < r_n` and nonzero integer coefficients. Let `V` be the number of
+sign changes in `c_0, …, c_n`, and let `e_0, e_1` be the exact endpoint
+multiplicity lower bounds from PR5788. On the left, list
+`-∞, -K, …, -1`, followed by `0` when `F(0) ≠ 0`. On the right, list `1`
+when `F(1) ≠ 0`, followed by `2, …, K, +∞`. Give `-∞` the sign of `c_0`
+and `+∞` the sign of `c_n`. Each finite point gets the sign of the exact
+rational `F(k)`. Let `W` count the exact zeros at listed integers plus the
+strict sign changes between adjacent strictly signed points, with an exact zero
+breaking adjacency. Then `F` has at least `W` distinct real roots in
+`(-∞,0) ∪ (1,∞)`, and
+
+`(roots in (0,1), with multiplicity) ≤ V - e_0 - e_1 - W`.
+
+If the interior brackets and exact interior zeros number exactly this
+remainder, every interior root is simple and witnessed. With remainder zero
+and one strict interior sample, the sign is uniform on `(0,1)`. These are
+the same closure rules as PR5788, applied to a smaller budget.
+
+## Proof
+
+*Asymptotic signs.* `F(t) = r_0^t (c_0 + Σ_{i>0} c_i (r_i/r_0)^t)`. Every
+ratio exceeds one, so the bracket tends to `c_0` as `t → -∞`. Hence `F` has
+the sign of `c_0` on some ray `(-∞, T)`. Symmetrically, `F(t) = r_n^t (c_n + …)`
+has the sign of `c_n` on some ray `(T', ∞)`.
+
+*Witnesses.* A strict sign change between adjacent finite listed points gives
+a root in that open interval by continuity. Between `-∞` and the first finite
+point `-K`, choose `T < -K` inside the asymptotic ray; the opposite signs at
+`T` and `-K` give a root in `(T,-K)`. The `+∞` case is symmetric. An exact zero
+at a listed integer is a root. The open intervals are pairwise disjoint. They
+avoid every listed integer and neither contains `0` or `1`: the point `0` or
+`1` is listed when `F` is nonzero there. When `F(0) = 0`, the last left point is
+`-1` and no interval reaches `0`. So the `W` roots are distinct, lie outside
+`[0,1]`, and are disjoint from the endpoint roots counted by `e_0, e_1`.
+
+*Budget.* PR5788 proves (generalized Descartes rule, Rolle induction) that `F`
+has at most `V` real roots counted with multiplicity. Each outside witness has
+multiplicity at least one. Subtracting `W` and the endpoint lower bounds leaves
+the stated interior bound. The closure step is unchanged. Interior witnesses
+lie in disjoint subintervals, so if they exhaust the remainder, each has
+multiplicity exactly one and no other interior root exists. ∎
+
+Outside witnesses only reduce an upper bound, so they cannot turn a valid
+predecessor certificate into a different verdict. The census also checks this
+on every fixture.
+
+## Evidence
+
+[`outside_roots.py`](outside_roots.py) imports the unchanged
+`scripts/compare_power_variation.py` helpers (endpoint multiplicities,
+directed interior enclosures). It adds `outside_witnesses` and the reduced
+budget. Values at integer exponents are exact `Fraction`s. Reach `K` defaults
+to 8 (at most 64). It accepts the same invoice pair as the shared tool:
+
+```sh
+python3 -B research/power-variation-outside-roots/outside_roots.py OLD.json NEW.json
+```
+
+[`verify.py`](verify.py) checks the following (about 13 s on CPython 3.12):
+
+- The two fixtures above are `inconclusive` under PR5788 and become
+  `uniformly_lower` with the stated witnesses.
+- **Factored oracle census.** Every product of one, two or three factors
+  `q·a^t − p` is checked. Bases are `a ∈ {2,3,5}`, three-factor products use
+  three distinct bases, and `p/q` ranges over 15 thresholds from `1/3` to `25`.
+  This gives 4,455 expanded invoices. Roots are `log(p/q)/log a` in closed form.
+  Interior membership (`1 < p/q < a`), integer roots and the sign at `t = 1/2`
+  are exact integer tests. Floats only order distinct non-integer roots, and a
+  near-coincidence would be excluded and counted (0 occurred). Every predecessor
+  and extended certificate is compared with the oracle: uniform sign, number of
+  interior roots, simplicity and bracket location. Result: predecessor 391
+  certified, extension 2,987, newly settled 2,596. False certificates,
+  budget overruns and changed predecessor verdicts are all 0. 3,544 reports use
+  an outside witness. Both tools use a 32-cell interior grid in the census.
+- **Failure controls.** Two deliberately wrong witness rules are rejected by the
+  same oracle. Swapping the two asymptotic signs gives 887 false certificates,
+  2,026 budget overruns and 94 changed verdicts. Listing `0`/`1` as a witness
+  point even when `F` vanishes there double-counts endpoint roots: 463 false,
+  491 overruns and 104 changed.
+
+Reproduce from the repository root (local run: CPython 3.12.14 at
+`~/git/integer-mult-bounds/.venv/bin/python3.12`):
+
+```sh
+python3.12 -B research/power-variation-outside-roots/verify.py
+python3.12 -B scripts/research_package.py --package research/power-variation-outside-roots
+python3.12 -B scripts/check_research_commit.py --package research/power-variation-outside-roots --check-source-history
+```
+
+Expected final line: `PASS_POWER_VARIATION_OUTSIDE_ROOTS`. The verifier
+fails closed without `assert`, so an isolated optimized run
+(`python3.12 -I -O -B research/power-variation-outside-roots/verify.py`)
+checks the same conditions.
+
+## Scope and limits
+
+This is invoice arithmetic only. It is not a construction, source extraction,
+native operator, compiler endpoint, supplier admission or new κ. The selected
+result is unchanged. The census is a finite exact check of the implementation,
+not a proof of completeness. Two roots in the same unit interval outside
+`[0,1]` with equal signs at its ends are not witnessed; the report then stays
+`inconclusive`, which remains sound. Touching interior roots (even
+multiplicity) are still unresolved, as in PR5788. The shared
+`scripts/compare_power_variation.py` is not modified. Merging this check into it
+is a separate maintainer decision.
+
+## Open next questions
+
+Structured versions are in [TASK.json](TASK.json).
+
+- **Finer outside brackets.** Can rational points beyond the unit grid
+  (directed enclosures at `t < 0` and `t > 1`) separate two outside roots in one
+  unit interval? Start with `(2^t − 5/2)(3^t − 4)`, whose two roots
+  (about 1.32 and 1.26) both lie in `(1,2)`. The existing power engine accepts
+  only `0 < t < 1`, so this needs an exact `r^(k+s)` reduction.
+- **Pinned source invoices.** Does any committed paid-minus-target invoice
+  that PR5788 leaves `inconclusive` become certified here? Run `outside_roots.py`
+  on the pinned P104 ledger exported by the selected-invoice tool (#5735) and
+  its declared edits.
+- **Touching interior roots.** Even-multiplicity interior roots still block
+  closure. A Sturm-type argument for exponential sums with commensurable
+  exponents, or an exact derivative-sign witness, is needed.
+
+## Credit
+
+The root budget, endpoint multiplicities, interior brackets, invoice schema and
+directed power engine are Ali Romman's PR5788/PR5746 work and their credited
+predecessors (zxv's signed-invoice interface, woklerx's T16 unique-crossing
+proof, mightyOil's moment-order audit). The generalized Descartes rule is
+classical. New here: the outside-domain witness rule, its proof, the factored
+oracle census and controls, produced by Nick Petalas. Apache-2.0.

research/power-variation-outside-roots/SOURCES.json

@@ -0,0 +1,36 @@
+{
+  "schema_version": 1,
+  "base_commit": "19fdb086ea96af9a9f87936a2b888e10af4ed810",
+  "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"
+    },
+    {
+      "path": "scripts/compare_power_variation.py",
+      "usage": "input",
+      "git_blob": "6a06c55174fb0f37d792ed7b84eaeae08da9c88a",
+      "sha256": "6650eebabaf65360b4efedb6074776b9a8966cb1bdf07650806e4361326ad590"
+    },
+    {
+      "path": "scripts/compare_recursive_invoices.py",
+      "usage": "input",
+      "git_blob": "fda2a852e9937e42fe40df0707694465ca7c1b48",
+      "sha256": "3930c22c11da7bc6042cfeb6e459ecb06e4478430037bee3469d034353855fc6"
+    },
+    {
+      "path": "scripts/evaluate_recursive_power.py",
+      "usage": "input",
+      "git_blob": "ca50f8021fc3238a58fd420383f4619a8d008ace",
+      "sha256": "52b20f41fd0bb55fa88dccd6015af2ce358917817b9506720f3e60ce681cc3ad"
+    }
+  ]
+}

research/power-variation-outside-roots/TASK.json

@@ -0,0 +1,111 @@
+{
+  "schema_version": 1,
+  "task_id": "independent-moment",
+  "priority_revision": 8,
+  "base_commit": "19fdb086ea96af9a9f87936a2b888e10af4ed810",
+  "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": "Invoice-order certificate tooling: spend the generalized Descartes root budget of PR5788's general-rank power-variation comparator on exactly witnessed roots at t<0 and t>1, then close the interior count on the reduced budget.",
+  "scope_change_reason": "The card asks for an independent recount of a changed construction's invoice. This package instead answers the Open next question of docs/research/recursive-power-variation.md (PR5788): proving outside-domain roots so an unspent budget can be closed. It strengthens the certificate that such invoice comparisons use; it recounts no construction.",
+  "bottleneck_link": "Revision 8 asks contributors to compare complete paid and target power sums over the whole exponent interval; PR5788's certificate is the general-rank tool for that and returns inconclusive when roots lie outside 0<t<1. This removes that cause of inconclusive reports. Side result for the accounting tools; it does not change any supplier bill or kappa.",
+  "budget_minutes": 60,
+  "stop_rule": "Stop at the first sound outside-witness rule verified against an independent factored oracle with failure controls; leave finer outside brackets, source invoices and touching roots as open questions.",
+  "outcome": "completed",
+  "evidence": "verify.py: 2 motivating fixtures move from inconclusive to uniformly_lower; factored oracle census of 4455 invoices: predecessor 391 certified, extension 2987, newly settled 2596, 0 false certificates, 0 budget overruns, 0 changed predecessor verdicts; two mutation controls rejected.",
+  "author": "Nick Petalas",
+  "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.",
+  "open_questions": [
+    {
+      "question": "Can rational points outside [0,1] separate two outside roots in one unit interval?",
+      "why_it_matters": "Same-interval outside roots leave the budget unspent and the report inconclusive.",
+      "first_step": "Extend directed power enclosures to r^(k+s) for integer k and 0<s<1, then test (2^t-5/2)(3^t-4), whose roots both lie in (1,2).",
+      "blocked_by": "scripts/evaluate_recursive_power.py accepts only 0<t<1."
+    },
+    {
+      "question": "Does any committed paid-minus-target invoice left inconclusive by PR5788 become certified with outside witnesses?",
+      "why_it_matters": "A source-bound case would show the rule matters for an actual comparison, not only for fixtures.",
+      "first_step": "Export the pinned P104 ledger with the #5735 selected-invoice tool and run outside_roots.py on it and its declared edits.",
+      "blocked_by": "No source invoice was run in this package."
+    },
+    {
+      "question": "Can touching (even-multiplicity) interior roots be certified for general ranks?",
+      "why_it_matters": "They are the remaining cause of inconclusive reports when the budget is otherwise exhausted.",
+      "first_step": "Try an exact derivative-sign witness or a Sturm sequence on commensurable-exponent subfamilies.",
+      "blocked_by": "No general exact root-isolation method for exponential sums is implemented here."
+    }
+  ]
+}

research/power-variation-outside-roots/VERIFY.json

@@ -0,0 +1,24 @@
+{
+  "schema_version": 1,
+  "status": "ready",
+  "python": "3.12",
+  "requirements": [],
+  "inputs": [
+    "research/power-variation-outside-roots/outside_roots.py",
+    "research/power-variation-outside-roots/verify.py",
+    "scripts/compare_power_variation.py",
+    "scripts/compare_recursive_invoices.py",
+    "scripts/evaluate_recursive_power.py"
+  ],
+  "commands": [
+    {
+      "argv": [
+        "{python}",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 300,
+      "checks": "Two predecessor-inconclusive fixtures become uniformly_lower; factored oracle census of 4455 invoices with 0 false certificates and 0 changed predecessor verdicts; two mutation controls (swapped asymptotic signs, double-counted zero endpoints) rejected."
+    }
+  ]
+}