diff --git a/research/invoice-class-polarization/PROOF.md b/research/invoice-class-polarization/PROOF.md new file mode 100644 index 0000000000..f1861ba7b8 --- /dev/null +++ b/research/invoice-class-polarization/PROOF.md @@ -0,0 +1,213 @@ +# The polarized invoice ceiling for the signed concave screen + +## 1. The screen + +Fix an integer ambient rank `m >= 2` and an invoice: a paid multiset + + P = (r_1, ..., r_Kp), 1 <= r_i <= m, + +and a target multiset + + T = (s_1, ..., s_Kt), 1 <= s_j <= m, + +with entry counts `Kp = |P|`, `Kt = |T|`, rank masses `Mp = sum r_i`, +`Mt = sum s_j`. For an exponent `x` the signed net is + + N_{P,T}(x) = sum_i r_i^x - sum_j s_j^x. + +This is exactly the quantity of the documented comparator +`scripts/compare_recursive_invoices.py`, whose tariff is `r^(1-C)` with +saving `C`; write `x = 1 - C`, so the admitted range is `0 < x < 1`. The +comparator decides the order of two *given* invoices for every increasing +concave tariff, in particular for every power `r^x`, `0 < x < 1`. + +The question here is different: over the whole class of invoices with the +same four summary numbers `(Kp, Mp, Kt, Mt)`, which one is the most +favourable for the screen, and is that extreme independent of `x`? + +Throughout, `f(r) = r^x` with `0 < x < 1`. Then `f` is strictly concave and +strictly increasing on `[0, inf)`, so its increments `f(j+1) - f(j)` are +strictly decreasing in `j >= 0`. + +## 2. The paid extreme: maximum spread + +**Definition (greedy spread vector).** For integers `1 <= K <= M <= K m` put + + j = min(K - 1, (M - K) // (m - 1)), + r0 = M - K + 1 - j (m - 1), + +and let `G(K, M, m)` be the multiset with `j` copies of `m`, one copy of +`r0`, and `K - j - 1` copies of `1`. + +The constraints `1 <= r0 <= m` hold: `r0 >= 1` because +`j (m-1) <= M - K`; and `r0 <= m` because either `j = K - 1`, when +`r0 = M - (K-1)m <= m`, or `j < K - 1`, when maximality of `j` gives +`(j+1)(m-1) > M - K`, i.e. `r0 < m`. + +**Lemma 1 (paid spread).** Let `1 <= a <= b` with `a >= 2` and `b <= m - 1`. +Then + + f(a - 1) + f(b + 1) < f(a) + f(b). + +*Proof.* The increments of a strictly concave function are strictly +decreasing, and `a - 1 <= b`, so +`f(b+1) - f(b) < f(a) - f(a-1)`. Rearranging gives the claim. QED + +Call a multiset `V` *spread-terminal* if no such pair of entries exists, i.e. +after sorting, every entry that is `>= 2` is followed only by entries equal to +`m`. A spread-terminal multiset therefore has the shape `1^a v m^b` with +`a, b >= 0`, at most one entry `v`, and `1 <= v <= m` (the cases `v = 1` and +`v = m` are the pure `1^a m^b` shapes). + +**Lemma 2.** For `1 <= K <= M <= K m` the multiset `G(K, M, m)` is +spread-terminal, and it is the only spread-terminal multiset with `K` entries +and mass `M`. + +*Proof.* Write `G = 1^a v m^b` with `v = r0`. If `v = m` then `j = K - 1` and +`G` is all `m`. Otherwise every entry strictly between `1` and `m` is the +single `v`, so `G` is spread-terminal. + +For uniqueness, let `1^a v m^b` and `1^A w m^B` be two spread-terminal +multisets with the same count and mass, using the convention that `v` or `w` +may be absent. Equal counts give `a + b = A + B` when both are pure, and +`a + b + 1 = A + B + 1` when both have an interior entry. Equal masses then +force `a = A`, `b = B`, `v = w` by the two computations below. + +*Both have an interior entry.* Equal counts give `b - B = A - a =: d`, and +equal masses give `(a - A) + (v - w) + d m = 0`, i.e. +`v - w = d (m - 1)`. Since `1 < v, w < m`, `|v - w| <= m - 3 < m - 1`, hence +`d = 0` and `v = w`. + +*One has an interior entry.* Say `1^a v m^b` and `1^A m^B` have equal count +and mass. Equal counts give `a + b + 1 = A + B`, i.e. `A - a = b - B + 1`. +Equal masses give `(a - A) + v + (b - B) m = 0`. Substitute +`a - A = B - b - 1`: + + v = (b - B + 1) - (b - B) m = 1 + (b - B)(1 - m). + +If `b - B >= 0` then `v >= 1` forces `b - B = 0`, so `v = 1`, contradicting +`1 < v`. If `b - B <= -1` then `v = 1 + (B - b)(m - 1) >= m`, contradicting +`v < m`. So this case cannot occur. QED + +**Proposition 1 (paid minimum).** For every multiset `P` with `K` entries, +entries in `[1, m]` and mass `M`, + + sum_{r in P} f(r) >= sum_{r in G(K,M,m)} f(r), + +with equality if and only if `P = G(K, M, m)`. + +*Proof.* Sort `P`. If `P` is not spread-terminal there is a pair `a <= b` with +`a >= 2`, `b <= m - 1`; replacing `a` by `a - 1` and `b` by `b + 1` keeps the +count, the mass and the bound `[1, m]`, and by Lemma 1 strictly decreases the +sum. Iterating terminates because each step strictly decreases the sum and +the feasible set is finite. The terminal endpoint has the same count and mass, +so by Lemma 2 it is `G`. Hence every `P != G` admits a strictly decreasing +path to `G`, and since a global minimum cannot be non-terminal, `G` is the +unique minimiser. QED + +## 3. The target extreme: balance + +**Definition (balanced vector).** For `1 <= K <= N <= K m` write +`q = N // K`, `t = N - q K`, and let `B(K, N, m)` be the multiset with `t` +copies of `q + 1` and `K - t` copies of `q`. + +**Lemma 3.** Let `1 <= b <= m - 2` and `b + 2 <= a <= m`. Then + + f(a - 1) + f(b + 1) > f(a) + f(b). + +*Proof.* Here `b + 1 <= a - 1`, so strict monotonicity of the decreasing +increments gives `f(b+1) - f(b) > f(a) - f(a-1)`; rearrange. QED + +**Proposition 2 (target maximum).** For every multiset `T` with `K` entries, +entries in `[1, m]` and mass `N`, + + sum_{s in T} f(s) <= sum_{s in B(K,N,m)} f(s), + +with equality if and only if `T = B(K, N, m)`. + +*Proof.* If two entries differ by at least two, Lemma 3 applied to the larger +`a` and the smaller `b` strictly increases the sum while preserving count, +mass and bounds. The only terminal multisets have all entries in `{q, q+1}` +for their common quotient, hence are balanced, and the balanced multiset is +unique for `(K, N)`. The same iteration argument gives the claim. QED + +## 4. The class ceiling + +**Theorem.** Let `P, T` be any invoice with entry counts `Kp, Kt`, rank masses +`Mp, Mt` and ranks in `[1, m]` (`m >= 2`). Then for every `x` with +`0 < x < 1`, + + N_{P,T}(x) >= N_{G(Kp,Mp,m), B(Kt,Mt,m)}(x), + +and equality holds if and only if `P = G(Kp, Mp, m)` and +`T = B(Kt, Mt, m)`. + +*Proof.* Apply Proposition 1 to the paid side and Proposition 2 to the target +side; the two sides are independent and the inequality subtracts the target +sum. Equality in the difference forces equality on both sides because each +side's deviation is nonnegative (paid) or nonpositive (target) with a sign +fixed by Propositions 1 and 2. QED + +**Corollary 1 (sharpness).** Both `G` and `B` are valid rank multisets in +`[1, m]`, so the bound is attained inside the class: the canonical invoice +`(G, B)` is a schema-valid input to the comparator. The canonical invoice +depends on `(Kp, Mp, Kt, Mt, m)` only, not on `x`. + +**Corollary 2 (uniformity).** The theorem holds simultaneously for every +exponent in `(0, 1)`: one canonical invoice is the pointwise-in-`x` extreme of +the whole class. The class ceiling is therefore a single function + + Lambda(x) = sum_{r in G} r^x - sum_{s in B} s^x, + +a signed sum of at most four pure powers. + +## 5. Consequences for the screen + +**(a) O(1) necessary condition.** Let `I` be an incumbent invoice with net +`Psi(x)`. A candidate with summary numbers `(Kp, Mp, Kt, Mt)` can beat `I` at +some exponent `x` only if `Lambda(x) < Psi(x)`. In particular, using the +cruder mass-only bounds `sum r^x >= Mp m^{x-1}` and `sum s^x <= Mt`, + + Mt > Mp m^{x-1} - Psi(x) + +is necessary. Neither test replays a construction. + +**(b) O(1) sufficient certificate for `uniformly_worse`.** Let `Lambda_NEW` be +the canonical ceiling of the candidate class and let `U_OLD` be the +*antipodal* invoice of the incumbent class: paid balanced at +`B(Kp, Mp, m)` and targets spread at `G(Kt, Mt, m)`. Then +`N_NEW(x) >= Lambda_NEW(x)` and `N_OLD(x) <= U_OLD(x)` for all `0 < x < 1`, so + + Lambda_NEW(x) > U_OLD(x) for all x ==> N_NEW(x) > N_OLD(x) for all x. + +Both sides are 2-rank invoices, so the existing hinge comparator verifies the +hypothesis exactly, in constant time, without enumerating either class. This +turns a per-invoice comparison into a per-class comparison. + +**(c) Sharpness of the exponent range.** At `x = 1` the paid sum and the +target sum both equal the rank mass, so the theorem's inequality is an +equality for *every* pair of invoices with the same masses, canonical or not. +At `x = 0` both sides count entries. Hence `0 < x < 1` is exactly the range in +which the extreme is the polarized invoice; outside it the class has no unique +extreme. This is the sense in which the theorem is sharp and not an artefact +of the chosen extremal vectors. + +**(d) Relation to the existing tool.** The comparator answers "is this given +invoice uniformly better than that given invoice" by a hinge criterion. The +theorem answers "what is the best possible invoice with these four numbers", +which the comparator does not compute, and it composes with the comparator in +both directions (a) and (b). + +## 6. What is not claimed + +1. No physical, native, compiler, precision, hosting, ownership or supplier + admission. Ranks here are declared histogram entries, as in the comparator; + the comparator's own assurance block makes the same restriction. +2. No claim about paid *call* counts, scalar instruction counts or additional + charges outside the raw signed moment. +3. No `kappa` change. The result is a scoped arithmetic theorem about the + documented screen, and it inherits the comparator's status as an arithmetic + screen, not a construction. +4. Nothing here asserts that a canonical invoice is *realizable* by a word. It + is a bound over declarations; Corollary 1 says only that the bound cannot be + improved inside the declared class. diff --git a/research/invoice-class-polarization/README.md b/research/invoice-class-polarization/README.md new file mode 100644 index 0000000000..c8af9ab214 --- /dev/null +++ b/research/invoice-class-polarization/README.md @@ -0,0 +1,172 @@ +# The polarized invoice ceiling for the signed concave screen + +produced by Nick Petalas + +## Scope + +The documented comparator `scripts/compare_recursive_invoices.py` decides the +order of two declared invoices for every increasing concave tariff, in +particular for the power tariff `r^(1-C)` with saving `C`. Each invoice is a +paid multiset and a target multiset of ranks in `[1, m]`, and its signed net at +exponent `x = 1 - C` is + + N(x) = sum_paid r^x - sum_target s^x. + +The comparator answers a comparison question about two *given* invoices. This +package answers a different question about the same arithmetic screen: over the +whole class of invoices that share the four summary numbers + + paid entry count Kp, paid rank mass Mp, target entry count Kt, target rank mass Mt, + +which invoice is the most favourable for the screen, and is that extreme +independent of `x`? + +## Result + +Claim type: **scoped written proof with exact finite corroboration.** + +For `m >= 2` and every exponent `0 < x < 1`, the most favourable invoice in a +class `(Kp, Mp, Kt, Mt)` is the *polarized* invoice + +* paid ranks: `Kp - 1` entries as spread as the mass allows, namely `j` copies + of `m`, one remainder `r0`, and the rest `1`, where + `j = min(Kp - 1, (Mp - Kp) // (m - 1))` and `r0 = Mp - Kp + 1 - j(m - 1)` + (the greedy spread vector `G`); +* target ranks: the balanced vector `B`, with entries `q = Mt // Kt` and + `q + 1`. + +Every invoice in the class satisfies `N(x) >= N_canonical(x)` for all +`0 < x < 1` simultaneously, with equality exactly at the canonical invoice. +The canonical invoice depends only on `(Kp, Mp, Kt, Mt, m)`, so one 2-rank +invoice is the pointwise extreme of the whole class. + +Two consequences that cost no construction replay: + +1. **Necessary condition.** A candidate in class `(Kp, Mp, Kt, Mt)` can beat an + incumbent with net `Psi(x)` only if `Lambda(x) < Psi(x)`, where `Lambda` is + the canonical net. The cruder mass-only form is + `Mt > Mp m^(x-1) - Psi(x)`. +2. **Sufficient class certificate.** Let `U` be the *antipodal* invoice of the + incumbent class (paid balanced, targets spread). If + `Lambda_candidate(x) > U_incumbent(x)` for all `0 < x < 1`, then every + invoice in the candidate class is uniformly worse than every invoice in the + incumbent class. Both sides are 2-rank invoices, so the existing hinge + comparator verifies the hypothesis exactly in constant time. + +The proof is an exchange argument: the increments of a strictly concave power +are strictly decreasing, so spreading paid mass and equalizing target mass +never hurt, and the terminal configurations are unique. `PROOF.md` states the +lemmas, the uniqueness argument and the sharpness controls. + +## What is not claimed + +* No physical, native, compiler, precision, hosting, ownership or supplier + admission. Ranks are declared histogram entries, exactly as in the + comparator, whose own assurance block records the same restriction. +* No paid *call* count, scalar instruction count, or charge outside the raw + signed moment. +* No `kappa` change, and no claim that a canonical invoice is realizable by a + word. The bound is over declarations and cannot be improved inside the + declared class. +* The result is about the documented arithmetic screen, not a new supplier. + +## Evidence + +`PROOF.md` contains the written argument: two exchange lemmas, the uniqueness +of the spread-terminal and balanced vectors, the class theorem, the sharpness +of the exponent range, and the two consequences. + +`verify.py` checks the argument with integer interval arithmetic only (rank +powers are bracketed by integer k-th roots; there is no floating point): + +* both exchange lemmas for every admissible pair with `m <= 6` and five + exponents `1/2, 1/3, 2/3, 1/5, 3/7`; +* Proposition 1 (unique paid minimum) and Proposition 2 (unique target maximum) + exhaustively on every integer multiset in four boxes: `(m, max entries)` = + `(5, 3)`, `(4, 4)`, `(6, 2)`, `(3, 5)`; +* the class theorem on every ordered pair of invoices in those boxes: 40,705 + strict comparisons and 16,995 equality cases; +* the `x = 1` and `x = 0` boundary controls that make the exponent range sharp + (at `x = 1` the inequality is an equality for every invoice with the same + masses, so the strict statement genuinely needs `x < 1`); +* composition with `scripts/compare_recursive_invoices.py` on schema-valid + invoices: the comparator classifies a non-canonical invoice against its + canonical replacement as `uniformly_worse` with a strictly positive power + sign, the reverse as `uniformly_better`, identical canonical invoices as + `equal`, a rank above the declared ambient rank as invalid, and it confirms + the antipodal class certificate; +* mutation controls (balanced paid, spread targets, a half-spread paid vector) + and hypothesis controls (infeasible counts and masses, ambient rank one). + +The comparator integration is an independent implementation: its hinge +criterion is not the exchange argument used here, so agreement is a genuine +cross-check rather than a restatement. + +## Reproduction + +From the repository root, with CPython 3.12: + +```sh +python3.12 -B research/invoice-class-polarization/verify.py +python3.12 -W error -B research/invoice-class-polarization/verify.py +python3.12 -O -W error -B research/invoice-class-polarization/verify.py +python3.12 -B scripts/research_package.py --package research/invoice-class-polarization +python3.12 -B scripts/check_research_commit.py --package research/invoice-class-polarization --check-source-history +``` + +The verifier prints a census and `PASS_INVOICE_CLASS_POLARIZATION`, and rewrites +`RESULT.json` with the source hashes of the package files. + +## Open next questions + +1. **Signed target counts with multiplicity caps.** The theorem treats target + entries as freely repeatable. If a construction can host at most `c` targets + of a given rank, the target extremum becomes a bounded-composition problem. + *Why it matters:* multiplicity caps are the realistic constraint on + independent helper refinements, and they can only lower the ceiling. + *First step:* derive the exact maximum of `sum s_j^x` under per-rank caps. + *Blocked by:* no declared cap inventory for a concrete word. +2. **Which summary quadruples are physically achievable?** The ceiling is exact + over declarations; the useful screening version needs the achievable set of + `(Kp, Mp, Kt, Mt)` for a fixed controller. + *Why it matters:* an unachievable canonical invoice is still a valid bound + but a weaker one. *First step:* count the four numbers for one audited + invoice and compare against the ceiling. *Blocked by:* no source inventory + is bound in this package. +3. **Tightening with the number of distinct ranks.** The canonical invoices use + at most two distinct ranks per side. A bound that also fixes the number of + distinct ranks could separate proposals that the four summary numbers + cannot. *Why it matters:* it would sharpen the class certificate at fixed + cost. *First step:* solve the two-constraint extremal problem with a + distinct-rank budget. *Blocked by:* the extremal vector is no longer unique, + so the equality characterisation needs a tie-breaking rule. + +## Related open work + +* PR #5973 (josecarlosgonzalezroque-design) keeps the selected-invoice stdout + bytes consistent with its receipt. It studies the invoice tooling's output + contract, not the signed moment or its class extremum, so it neither + overlaps nor supplies the quantity bounded here. +* PR #7175 (petalas) certifies fixed-profile helper-split first-crossing + ceilings for the selected frontier. It bounds a different model (a fixed + helper-split profile at one crossing), so its numbers are not comparable with + the class ceiling here; the two would compose only after that profile is + expressed as a declared paid/target invoice. +* The comparator itself and its documented screen are the subject here; the + live tool files are pinned in `SOURCES.json`. +* `docs/research/recursive-invoice-preflight.md` records the signed-invoice + comparison procedure and its "not a new theorem" disclaimer for the + concave-order interface; this package supplies the class-extremal theorem + that the interface left open, and changes nothing in that document. + +## Credit + +The comparator and its hinge criterion are by zxv, on the classical +concave-order and majorization lineage recorded in its docstring, including +mightyOil's `research/t16-moment-order-audit` and its credited predecessors. +The signed-invoice preflight procedure is recorded in +`docs/research/recursive-invoice-preflight.md`. This package reuses that +arithmetic interface unchanged and adds the class-extremal theorem, its +uniqueness proof and the sharpness controls. + +Apache-2.0. diff --git a/research/invoice-class-polarization/RESULT.json b/research/invoice-class-polarization/RESULT.json new file mode 100644 index 0000000000..1e593c75cd --- /dev/null +++ b/research/invoice-class-polarization/RESULT.json @@ -0,0 +1,37 @@ +{ + "census": { + "antipodal_hypothesis": 5, + "boundary_controls": 2, + "boxes": 4, + "class_equality": 16995, + "class_strict": 40705, + "comparator_cases": 6, + "comparator_rejections": 1, + "hypothesis_rejections": 5, + "lemma1": 100, + "lemma3": 100, + "mutations": 3, + "paid_groups": 113, + "paid_strict": 465, + "target_groups": 113, + "target_strict": 465 + }, + "claim_type": "scoped written proof with exact finite corroboration", + "exponents": [ + "1/2", + "1/3", + "2/3", + "1/5", + "3/7" + ], + "interval_digits": 24, + "method": "integer k-th root brackets; no floating point", + "source_sha256": { + "PROOF.md": "245215a846ab1e97262f11991c2d430c4cc1cb593338aaf73da4f9a652f8ae04", + "README.md": "db1f77d26bd8dca35c40199f8513ea491b01ff549f9ce1ff1b304ad0ef11b341", + "SOURCES.json": "12f413e4082885f156d619dc636a029a72c1670aaa7aabfe5d3b1adc5cdf00fc", + "TASK.json": "2a75aab8b6e37ffa43d76f20b4391bcbf7aba81c25d70b083f43a45ce7552d7e", + "VERIFY.json": "0dad840716b73d382b00a3eb92f6c8b091cf862300e7c266d5339026f2dc50db", + "verify.py": "8b0f0b82bc7de600ab37fcfaebc91e73e359209ea09fdbb3b73cce3b621a3312" + } +} diff --git a/research/invoice-class-polarization/SOURCES.json b/research/invoice-class-polarization/SOURCES.json new file mode 100644 index 0000000000..99e48cecbe --- /dev/null +++ b/research/invoice-class-polarization/SOURCES.json @@ -0,0 +1,30 @@ +{ + "schema_version": 1, + "base_commit": "e54523517d0f03e58352e647c403a5af3e525a57", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "75d77b328ea02ded535e7f23aee5b1e55d0bb1a8", + "sha256": "154c3d30455d778fd3343b6b4851f0fa4665f0f7625b0adb3675e2bafbbf6bf1" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec", + "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81" + }, + { + "path": "scripts/compare_recursive_invoices.py", + "usage": "input", + "git_blob": "fda2a852e9937e42fe40df0707694465ca7c1b48", + "sha256": "3930c22c11da7bc6042cfeb6e459ecb06e4478430037bee3469d034353855fc6" + }, + { + "path": "docs/research/recursive-invoice-preflight.md", + "usage": "provenance", + "git_blob": "3ea54e719c3e01031ad5e75945e524b6f6929806", + "sha256": "6e21a610efff4aaf07e2c6f7ee60b832ddc4386a648fcb8b3a5ce969661dfba8" + } + ] +} diff --git a/research/invoice-class-polarization/TASK.json b/research/invoice-class-polarization/TASK.json new file mode 100644 index 0000000000..ce8b3a40a4 --- /dev/null +++ b/research/invoice-class-polarization/TASK.json @@ -0,0 +1,86 @@ +{ + "schema_version": 1, + "task_id": "coverage-law-change", + "priority_revision": 8, + "base_commit": "e54523517d0f03e58352e647c403a5af3e525a57", + "original_card": { + "id": "coverage-law-change", + "question": "Can a completed call earn more independent productive target credit without an offsetting paid bill?", + "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" + ], + "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": "A source-bound arbitrary-input identity and legal producer/consumer boundary with the complete paid and productive target invoice, including restoration, ownership, native alignment and extra charges. Price under the actual current model; historical ceiling.py assumptions must be established before use. A favorable optimistic relaxation keeps a route open but is not a completed supplier. A scoped local result remains useful; expansion requires the family-level budget gate.", + "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": "Use #5599 as a completed positive control, then choose one uncovered cut/module beyond an applicable frozen exclusion. Derive independence, saturation and chronological availability rather than counting rational rank alone. Price target credits and all new jobs together, then check compiler and actual caller compatibility. Stop on a nonphysical credit or an unfavorable complete relaxation.", + "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": [ + "target credit", + "helper split", + "coverage law" + ], + "existing_checks": [ + { + "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 pointwise-in-exponent extreme of a declared paid/target invoice class on the documented signed concave screen, with uniqueness, sharpness and comparator composition.", + "scope_change_reason": "The card asks for a changed target-credit contract with a complete physical invoice and caller. This package instead settles the arithmetic screening question for every declaration that shares the four summary numbers (paid entry count, paid rank mass, target entry count, target rank mass). No physical credit, owner, restoration or supplier is claimed; the card's requirement to judge the complete signed target/paid bill is the link that is advanced.", + "bottleneck_link": "The selected interface compares declared invoices by the signed target/paid moment. The package supplies the exact best-case invoice of a declared class and an O(1) class certificate, so a proposal whose declared moment would need more than its class ceiling is rejected before another construction round without replaying the word.", + "budget_minutes": 60, + "stop_rule": "Ship the first verified class-extremal theorem and its comparator composition; do not extend to multiplicity caps, distinct-rank budgets or physical inventories.", + "outcome": "completed", + "evidence": "PROOF.md; exhaustive exchange and class census over four boxes; comparator composition on schema-valid invoices; generated source-hash-bound RESULT.json.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "Does a per-rank multiplicity cap on hostable targets lower the class ceiling, and by how much?", + "why_it_matters": "Independent helper refinements are bounded by how many targets of one rank a controller can host; a cap can only reduce the credit.", + "first_step": "Compute the exact maximum of sum s_j^x under per-rank caps for one audited invoice.", + "blocked_by": "No declared per-rank target cap inventory is bound for a concrete word." + }, + { + "question": "Which summary quadruples (Kp, Mp, Kt, Mt) are physically achievable for a fixed controller?", + "why_it_matters": "An unachievable canonical invoice is still a valid bound but a weaker one; an achievable set turns the ceiling into a sharper screen.", + "first_step": "Count the four numbers for one audited invoice and compare its net against its own class ceiling.", + "blocked_by": "No source inventory is bound in this package." + }, + { + "question": "Can a bound that also fixes the number of distinct ranks separate proposals the four summary numbers cannot?", + "why_it_matters": "The canonical invoices use at most two distinct ranks per side, so the summary quadruple loses distinct-rank information.", + "first_step": "Solve the same extremal problem with a distinct-rank budget and a tie-breaking rule.", + "blocked_by": "The extremal vector is no longer unique, so the equality characterisation needs a tie-breaking rule." + } + ], + "coordination": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19551797" +} diff --git a/research/invoice-class-polarization/VERIFY.json b/research/invoice-class-polarization/VERIFY.json new file mode 100644 index 0000000000..bc8f14187e --- /dev/null +++ b/research/invoice-class-polarization/VERIFY.json @@ -0,0 +1,34 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "scripts/compare_recursive_invoices.py" + ], + "commands": [ + { + "argv": [ + "{python}", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 300, + "checks": "Exchange lemmas, exhaustive paid/target/class census, exponent boundary controls, comparator composition and mutation controls." + }, + { + "argv": [ + "{python}", + "-O", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 300, + "checks": "Identical exact evidence and failure controls under optimized Python." + } + ] +} diff --git a/research/invoice-class-polarization/verify.py b/research/invoice-class-polarization/verify.py new file mode 100644 index 0000000000..73989af16d --- /dev/null +++ b/research/invoice-class-polarization/verify.py @@ -0,0 +1,422 @@ +#!/usr/bin/env python3 +# SPDX-License-Identifier: Apache-2.0 +"""Exact corroboration for the polarized invoice ceiling. + +Checks, with integer interval arithmetic only: + +* the two exchange lemmas for every admissible pair and every tested exponent; +* Proposition 1: the greedy spread vector is the unique paid minimum over + every multiset with the same entry count and rank mass; +* Proposition 2: the balanced vector is the unique target maximum; +* the class theorem: every invoice is at least its canonical invoice, with + equality exactly at the canonical invoice; +* the x = 1 and x = 0 boundary controls that make the exponent range sharp; +* the composition with the documented comparator on schema-valid invoices; +* mutation controls that must fail. + +Every power is bracketed by integer k-th roots, so each comparison is a +certified rational bound, not a floating-point approximation. +""" + +from __future__ import annotations + +import hashlib +import itertools +import json +import subprocess +import sys +import tempfile +from fractions import Fraction +from pathlib import Path + +DIGITS = 24 +SCALE = 10 ** DIGITS +X_SET = ((1, 2), (1, 3), (2, 3), (1, 5), (3, 7)) +PACKAGE = Path(__file__).resolve().parent +REPO = PACKAGE.parent.parent +COMPARATOR = REPO / "scripts" / "compare_recursive_invoices.py" + + +def iroot(n: int, k: int) -> int: + """Floor of the k-th root of a nonnegative integer.""" + if n < 2: + return n + lo = 0 + hi = 1 << ((n.bit_length() + k - 1) // k + 1) + while lo + 1 < hi: + mid = (lo + hi) // 2 + if mid ** k <= n: + lo = mid + else: + hi = mid + return lo + + +_BRACKET: dict[tuple[int, int, int], tuple[int, int]] = {} + + +def bracket(rank: int, p: int, q: int) -> tuple[int, int]: + """Certified integers lo <= rank**(p/q) * SCALE < lo + 1 <= hi.""" + key = (rank, p, q) + cached = _BRACKET.get(key) + if cached is None: + root = iroot(rank ** p * SCALE ** q, q) + cached = (root, root + 1) + _BRACKET[key] = cached + return cached + + +def multiset_sum(ranks, x): + """Certified interval [lo, hi] for sum rank**x, scaled by SCALE.""" + p, q = x + lo = hi = 0 + for rank in ranks: + a, b = bracket(rank, p, q) + lo += a + hi += b + return lo, hi + + +def linear_sum(ranks): + """Exact value of sum rank**1 (scaled by SCALE).""" + return SCALE * sum(ranks) + + +def greedy(K: int, M: int, m: int) -> tuple[int, ...]: + """Unique paid minimiser: j copies of m, one remainder, rest ones.""" + require(1 <= K <= M <= K * m, "infeasible (K, M, m)") + require(m >= 2, "ambient rank must be at least two") + j = min(K - 1, (M - K) // (m - 1)) + r0 = M - K + 1 - j * (m - 1) + require(1 <= r0 <= m, "greedy remainder out of range") + return (1,) * (K - j - 1) + (r0,) + (m,) * j + + +def balanced(K: int, N: int, m: int) -> tuple[int, ...]: + """Unique target maximiser: entries q or q + 1.""" + require(1 <= K <= N <= K * m, "infeasible (K, N, m)") + q, t = divmod(N, K) + require(1 <= q <= m, "balanced quotient out of range") + vector = (q,) * (K - t) + (q + 1,) * t + require(max(vector) <= m, "balanced entry exceeds ambient rank") + return vector + + +def require(condition, message): + if not condition: + raise AssertionError(message) + + +def multisets(m: int, K: int): + """Every nondecreasing tuple of K entries in 1..m.""" + return tuple(itertools.combinations_with_replacement(range(1, m + 1), K)) + + +def check_exchange_lemmas(m: int, counts: dict) -> None: + """Lemmas 1 and 3, certified for each tested exponent.""" + for x in X_SET: + for a in range(2, m + 1): + for b in range(a, m): # b + 1 <= m + left = multiset_sum((a - 1, b + 1), x) + right = multiset_sum((a, b), x) + require(left[1] < right[0], + f"lemma 1 fails at m={m} a={a} b={b} x={x}") + counts["lemma1"] += 1 + for b in range(1, m - 1): + for a in range(b + 2, m + 1): # b + 2 <= a + left = multiset_sum((a - 1, b + 1), x) + right = multiset_sum((a, b), x) + require(left[0] > right[1], + f"lemma 3 fails at m={m} a={a} b={b} x={x}") + counts["lemma3"] += 1 + + +def check_box(m: int, max_entries: int, counts: dict) -> None: + """Exhaustive propositions 1 and 2 and the class theorem on one box.""" + require(m >= 2, "ambient rank must be at least two") + by_count = {K: multisets(m, K) for K in range(1, max_entries + 1)} + + for K in range(1, max_entries + 1): + groups: dict[int, list[tuple[int, ...]]] = {} + for vector in by_count[K]: + groups.setdefault(sum(vector), []).append(vector) + counts["paid_groups"] += len(groups) + for mass, members in groups.items(): + canonical = greedy(K, mass, m) + require(canonical in members, "greedy vector missing from its class") + require(len(set(members)) == len(members), "duplicate multiset") + for x in X_SET: + base = multiset_sum(canonical, x) + for vector in members: + if vector == canonical: + continue + value = multiset_sum(vector, x) + require(value[0] > base[1], + f"paid minimum fails m={m} K={K} M={mass} " + f"x={x}: {vector} vs {canonical}") + counts["paid_strict"] += 1 + # Boundary control at x = 1: every vector attains the same value. + require(linear_sum(canonical) == linear_sum(members[0]), + "linear tariff control fails") + + for K in range(1, max_entries + 1): + groups = {} + for vector in by_count[K]: + groups.setdefault(sum(vector), []).append(vector) + counts["target_groups"] += len(groups) + for mass, members in groups.items(): + canonical = balanced(K, mass, m) + require(canonical in members, "balanced vector missing from its class") + for x in X_SET: + base = multiset_sum(canonical, x) + for vector in members: + if vector == canonical: + continue + value = multiset_sum(vector, x) + require(value[1] < base[0], + f"target maximum fails m={m} K={K} N={mass} " + f"x={x}: {vector} vs {canonical}") + counts["target_strict"] += 1 + + for Kp in range(1, max_entries + 1): + for Kt in range(1, max_entries + 1): + for paid in by_count[Kp]: + for target in by_count[Kt]: + gp = greedy(Kp, sum(paid), m) + bt = balanced(Kt, sum(target), m) + canonical = paid == gp and target == bt + for x in X_SET: + p_lo, _ = multiset_sum(paid, x) + _, p_hi_canonical = multiset_sum(gp, x) + t_hi, _ = multiset_sum(target, x) + t_lo_canonical, _ = multiset_sum(bt, x) + margin = (p_lo - p_hi_canonical) - (t_hi - t_lo_canonical) + if canonical: + require(paid == gp and target == bt, + "canonical identification error") + require(multiset_sum(paid, x) == multiset_sum(gp, x), + "canonical paid equality fails") + require(multiset_sum(target, x) == multiset_sum(bt, x), + "canonical target equality fails") + counts["class_equality"] += 1 + else: + require(margin > 0, + f"class ceiling fails m={m} " + f"paid={paid} target={target} x={x}") + counts["class_strict"] += 1 + counts["boxes"] += 1 + + +def write_invoice(path: Path, m: int, paid, targets) -> None: + invoice = { + "schema": "integer-mult-recursive-invoice/v1", + "contract": { + "model": "mixed-target-unnormalized-power-v1", + "rank_semantics": "H_r costs r^(1-C); debit surrendered productive fields", + "ambient_rank": m, + "boundary": "complete unit before the same mixed-target compiler", + }, + "paid": {str(r): paid.count(r) for r in sorted(set(paid), reverse=True) + if paid.count(r)}, + "targets": {str(r): targets.count(r) for r in sorted(set(targets), reverse=True) + if targets.count(r)}, + } + path.write_text(json.dumps(invoice), encoding="utf-8") + + +def run_comparator(old_path: Path, new_path: Path) -> dict: + result = subprocess.run( + [sys.executable, "-B", str(COMPARATOR), str(old_path), str(new_path)], + capture_output=True, text=True, timeout=120, check=False) + if result.returncode != 0: + return {"status": "REJECTED", "stderr": result.stderr.strip()} + report = json.loads(result.stdout) + return {"status": "OK", + "classification": report["classification"], + "power_sign": report["power_moment"]["new_minus_old_sign"]} + + +def check_comparator(counts: dict) -> None: + """Compose the theorem with the existing hinge comparator.""" + m = 6 + cases = [ + # old canonical, new non-canonical: theorem predicts uniformly worse. + ("uniformly_worse", "strictly_positive", + greedy(3, 9, m), balanced(2, 5, m), (2, 3, 4), (2, 3)), + # old non-canonical, new canonical: theorem predicts uniformly better. + ("uniformly_better", "strictly_negative", + (2, 3, 4), (2, 3), greedy(3, 9, m), balanced(2, 5, m)), + # paid canonical, target non-canonical: still uniformly worse. + ("uniformly_worse", "strictly_positive", + greedy(3, 9, m), balanced(2, 5, m), greedy(3, 9, m), (1, 4)), + # identical canonical invoices are equal. + ("equal", "identically_zero", + greedy(3, 9, m), balanced(2, 5, m), greedy(3, 9, m), balanced(2, 5, m)), + ] + with tempfile.TemporaryDirectory() as name: + root = Path(name) + for index, (classification, sign, op, ot, np_, nt) in enumerate(cases): + old_path = root / f"old{index}.json" + new_path = root / f"new{index}.json" + write_invoice(old_path, m, op, ot) + write_invoice(new_path, m, np_, nt) + verdict = run_comparator(old_path, new_path) + require(verdict.get("classification") == classification, + f"comparator classification {verdict} != {classification}") + require(verdict.get("power_sign") == sign, + f"comparator power sign {verdict} != {sign}") + counts["comparator_cases"] += 1 + + # Sufficient class certificate: the most favourable candidate still + # exceeds the least favourable incumbent, so every candidate loses. + old_path = root / "old_antipodal.json" + new_path = root / "new_canonical.json" + write_invoice(old_path, 8, (3, 6), (2, 7)) + write_invoice(new_path, 8, (8, 8), (1, 1)) + verdict = run_comparator(old_path, new_path) + require(verdict.get("classification") == "uniformly_worse", + f"antipodal certificate failed: {verdict}") + counts["comparator_cases"] += 1 + # The certificate hypothesis, checked with certified brackets. + for x in X_SET: + candidate = multiset_sum((8, 8), x) + candidate_credit = multiset_sum((1, 1), x) + incumbent_paid = multiset_sum((4, 5), x) + incumbent_credit = multiset_sum((1, 8), x) + margin = (candidate[0] - candidate_credit[1]) - ( + incumbent_paid[1] - incumbent_credit[0]) + require(margin > 0, f"antipodal hypothesis fails at x={x}") + counts["antipodal_hypothesis"] += 1 + + # Negative control: the reversed classes are not dominated. + old_path = root / "old_reverse.json" + new_path = root / "new_reverse.json" + write_invoice(old_path, 8, (4, 5), (1, 8)) + write_invoice(new_path, 8, (1, 8), (4, 5)) + verdict = run_comparator(old_path, new_path) + require(verdict.get("classification") == "uniformly_better", + f"reverse control failed: {verdict}") + counts["comparator_cases"] += 1 + + # Schema control: a rank above the declared ambient rank is rejected. + bad_path = root / "bad.json" + write_invoice(bad_path, 4, (1, 4), (2,)) + payload = json.loads(bad_path.read_text(encoding="utf-8")) + payload["paid"]["9"] = 1 + bad_path.write_text(json.dumps(payload), encoding="utf-8") + verdict = run_comparator(bad_path, new_path) + require(verdict.get("status") == "REJECTED", + "comparator accepted a rank above the ambient rank") + require("ambient_rank" in verdict.get("stderr", ""), + "rejection did not name the ambient rank") + counts["comparator_rejections"] += 1 + + +def check_mutations(counts: dict) -> None: + """Mutations of the canonical constructors must be detected.""" + m = 4 + # A balanced paid vector is strictly worse than the greedy spread. + require(balanced(3, 6, m) == (2, 2, 2), "unexpected balanced fixture") + require(greedy(3, 6, m) == (1, 1, 4), "unexpected greedy fixture") + x = (1, 2) + require(multiset_sum((2, 2, 2), x)[0] > multiset_sum((1, 1, 4), x)[1], + "paid mutation control did not fail") + counts["mutations"] += 1 + + # A spread target vector is strictly worse than the balanced vector. + require(greedy(3, 6, m) == (1, 1, 4), "unexpected spread fixture") + require(balanced(3, 6, m) == (2, 2, 2), "unexpected balance fixture") + require(multiset_sum((1, 1, 4), x)[1] < multiset_sum((2, 2, 2), x)[0], + "target mutation control did not fail") + counts["mutations"] += 1 + + # A half-spread paid mutant is not spread-terminal and not minimal. + mutant = (2, 2, 3) # K=3, M=7 for m=4 + require(sum(mutant) == 7 and len(mutant) == 3, "bad mutant fixture") + require(greedy(3, 7, m) == (1, 2, 4), "unexpected greedy fixture") + require(multiset_sum(mutant, x)[0] > multiset_sum(greedy(3, 7, m), x)[1], + "spread mutant control did not fail") + counts["mutations"] += 1 + + # Hypothesis controls: infeasible and degenerate parameter ranges. + for bad in ((3, 2, 4), (3, 13, 4)): + try: + greedy(*bad) + except AssertionError: + counts["hypothesis_rejections"] += 1 + else: + raise AssertionError(f"greedy accepted infeasible {bad}") + for bad in ((3, 1, 4), (3, 13, 4)): + try: + balanced(*bad) + except AssertionError: + counts["hypothesis_rejections"] += 1 + else: + raise AssertionError(f"balanced accepted infeasible {bad}") + try: + greedy(2, 4, 1) + except AssertionError: + counts["hypothesis_rejections"] += 1 + else: + raise AssertionError("greedy accepted ambient rank one") + + # Exponent boundary: at x = 1 strictness fails for a non-canonical vector. + require(linear_sum((2, 2, 2)) == linear_sum((1, 1, 4)), + "x = 1 boundary control did not tie") + counts["boundary_controls"] += 1 + # At x = 0 every entry contributes one, so the extreme is not polarized. + require(multiset_sum((2, 2, 2), (0, 1))[0] == 3 * SCALE, + "x = 0 boundary control value is wrong") + counts["boundary_controls"] += 1 + + +def source_hashes() -> dict[str, str]: + names = ("README.md", "PROOF.md", "SOURCES.json", "TASK.json", "VERIFY.json", + "verify.py") + return {name: hashlib.sha256((PACKAGE / name).read_bytes()).hexdigest() + for name in names} + + +def main() -> int: + counts = { + "boxes": 0, + "lemma1": 0, + "lemma3": 0, + "paid_groups": 0, + "paid_strict": 0, + "target_groups": 0, + "target_strict": 0, + "class_strict": 0, + "class_equality": 0, + "comparator_cases": 0, + "comparator_rejections": 0, + "antipodal_hypothesis": 0, + "mutations": 0, + "hypothesis_rejections": 0, + "boundary_controls": 0, + } + + for m, max_entries in ((5, 3), (4, 4), (6, 2), (3, 5)): + check_exchange_lemmas(m, counts) + check_box(m, max_entries, counts) + + check_mutations(counts) + check_comparator(counts) + + report = { + "claim_type": "scoped written proof with exact finite corroboration", + "census": counts, + "exponents": [f"{p}/{q}" for p, q in X_SET], + "interval_digits": DIGITS, + "method": "integer k-th root brackets; no floating point", + "source_sha256": source_hashes(), + } + (PACKAGE / "RESULT.json").write_text( + json.dumps(report, indent=2, sort_keys=True) + "\n", encoding="utf-8") + print(json.dumps(report, sort_keys=True)) + print("PASS_INVOICE_CLASS_POLARIZATION") + return 0 + + +if __name__ == "__main__": + raise SystemExit(main())