From dc5f8e94c8764d2048af85c0cc07a290d5ee153b Mon Sep 17 00:00:00 2001 From: commdata2338 <199849969+commdata2338@users.noreply.github.com> Date: Sun, 25 Oct 2026 00:49:13 -0500 Subject: [PATCH] Research: independently audit PR #4091's pooled duals with rational binomial bounds Independently verifies Ross Richardson's PR #4091 pooled ceiling for the fixed PR #4088 THREE/FOUR words. A separate standard-library checker enumerates all 841 whole-helper bin patterns (5/21/158/657 at capacities 8/16/32/48, cross-checked by a generating-function count), re-solves the three duals from exact equality systems, and proves every nonzero reduced cost positive for all 0.00173 <= a <= 0.00174 with a positive binomial series, outward integer rounding and an explicit geometric tail. The faces have 11/8/9 identically tight patterns; the central balance determinant is -10 and forces the unique optimum x = 1080; affine witnesses cover every real mixture 0..3240. At x = 1090 the right-face witness uses five capacity-48 bins (6,6,9,9,9,9) with idle {3:22783, 5:1625, 48:138492}, answering PR #5280's pooled-feasibility question, while the central idle multiset has ten too few residual rank units for 1090. No discrepancy and no new kappa. The local paid profiles and stock coefficient are inherited; chronology, native, physical and all-size admission are not checked. Adds research/staged-fourth-dual-binomial-audit/ only. Submitted by @commdata2338 with substantial AI assistance (OpenAI Codex research and implementation; packaged with Claude Code). Co-Authored-By: Claude Opus 5.5 (1M context) Claude-Session: https://claude.ai/code/session_01Jur4aiU6BBSmBiaRjkbECf --- .../PROOF.md | 228 ++++++ .../README.md | 143 ++++ .../RESULT.json | 702 ++++++++++++++++++ .../SOURCES.json | 66 ++ .../TASK.json | 146 ++++ .../VERIFY.json | 72 ++ .../test_verify.py | 174 +++++ .../verify.py | 445 +++++++++++ 8 files changed, 1976 insertions(+) create mode 100644 research/staged-fourth-dual-binomial-audit/PROOF.md create mode 100644 research/staged-fourth-dual-binomial-audit/README.md create mode 100644 research/staged-fourth-dual-binomial-audit/RESULT.json create mode 100644 research/staged-fourth-dual-binomial-audit/SOURCES.json create mode 100644 research/staged-fourth-dual-binomial-audit/TASK.json create mode 100644 research/staged-fourth-dual-binomial-audit/VERIFY.json create mode 100644 research/staged-fourth-dual-binomial-audit/test_verify.py create mode 100644 research/staged-fourth-dual-binomial-audit/verify.py diff --git a/research/staged-fourth-dual-binomial-audit/PROOF.md b/research/staged-fourth-dual-binomial-audit/PROOF.md new file mode 100644 index 0000000000..dd8cb54eda --- /dev/null +++ b/research/staged-fourth-dual-binomial-audit/PROOF.md @@ -0,0 +1,228 @@ +# Independent certificate for the fixed PR4091 pooled dual + +This is a scoped verification of Ross Richardson's PR4091 theorem, not a new +packing theorem or construction. Its source is +`a29bdd8f56cd18b805917775cdec09ff935eddc4`; the package is unchanged at the +scientific base `32890bc5de034ab8fc93ac88ead7279a6a416d04`. Its frozen PR4088 +inputs come from Cinna Davis's `76088d49e3ed4142a958659aa996b0ca4da5e88e`. +The eight input files and their exact bytes are listed in `SOURCES.json`. + +## 1. Declared model and source boundary + +Write `H_r(a)=r^(1-a)`, with `H_0=0`. There are 3,240 calls and a real variable +`0 <= x <= 3240` for FOUR calls. The reported local invoices are + +``` +L3 = 2487 H1 + 713 H2 + 224 H3 + 102 H4 + 20 H5 + 8 H8, +d = L4-L3 = 2 H1 + 3 H3 - 3 H4. +``` + +This audit **inherits those local reports**. It does not recompute the scalar +word's paid transitions or operator correctness. It separately enumerates +the complete binary spans of the entry and exit frames of all 408 helpers in +both orientations. Entry is contained in exit, and only helper 601 changes, +from residual width 8 to 7. This gives the item inventory + +``` +(N5,N6,N7,N8,N9) = (90720,58320,181440+x,301320-x,690120). +``` + +The template has 112 ports, each with six capacity-8 and four each of +capacity-16/32/48 children. The current order is exactly nine stages times +360 replicas, so the available bins are + +``` +(B8,B16,B32,B48) = (241920,161280,161280,161280). +``` + +The historical template's `replicas:37` fields are not multipliers. The stock +coefficient `(896*360)H73` is a declared comparison premise of PR4091's proof, +not inferred from the historical template's physical-field count. + +A pattern consists of a capacity `c`, five nonnegative integral helper counts +`n_w`, and a residual `r=c-sum(w*n_w)>=0`. Each bin pays exactly `H_r`. +The relaxed objective is + +``` +3240 L3 + x d + sum_pattern y_pattern H_residual, +``` + +where `y>=0` obeys all four bin balances and all five item balances. This +retains every empty bin and allows real multiplicities. Chronology, identities, +physical-family exclusions and offsets are omitted. A legal source fill maps +to this relaxation only under the declared whole-helper/residual accounting +contract. This audit supplies no new physical justification of that contract. + +## 2. Complete patterns by two finite methods + +The checker enumerates the Cartesian product +`0 <= n_w <= floor(c/w)` and keeps precisely the capacity-feasible tuples. +Independently, let `A(s)` be the coefficient of `z^s` in + +``` +product_(w=5..9) 1/(1-z^w). +``` + +The ordinary unbounded-coin recurrence computes these coefficients through +degree 48. For each capacity and every residual, the first enumeration must +have exactly `A(c-r)` distinct patterns. It also verifies nonnegative integral +counts and the exact capacity equation for every tuple. Thus there are +5, 21, 158 and 657 patterns respectively, 841 in total. Missing empty or +nonempty patterns, duplicates at unchanged total count, and wrong residuals +are rejected. The complete ordered census is hashed in `RESULT.json`. + +## 3. A different exact power enclosure + +The numerical part imports no predecessor Python and uses no logarithms, +exponentials, Decimal powers, floating-point decisions or optimizer. For an +integer `r>=1`, put `z=1-1/r`. If `0=1) t_k(a), +t_1(a)=z, +t_(k+1)(a)=t_k(a) * (k-a) * z/(k+1). +``` + +Equivalently, +`t_k(a)=z^k/k * product_(j=1..k-1)(1-a/j)`. Every term is nonnegative and +nonincreasing in `a`. The convergent sum therefore shows that the normalized +power `g_r(a)=(H_r(a)-r)/a` is nondecreasing in `a` (including `r=1`, where +it is zero). This is enough for an interval result, not merely a grid test. + +After `N` included terms, consecutive omitted terms have ratio at most `z`. +Their sum is at most `t_(N+1)/(1-z)=r*t_(N+1)`. At scale `S=10^40`, the +implementation starts with floor/ceiling bounds for `S*z`, rounds each positive +rational recurrence outward using integer division, and sums those bounds. +If `L_k <= S*t_k <= U_k`, positivity of the multiplier preserves this relation. +Consequently its final bounds are + +``` +-r * (sum_(k=1..N) U_k + r*U_(N+1))/S + <= g_r(a) <= +-r * sum_(k=1..N) L_k/S. +``` + +It uses `N=2048`. The tail is included even if it is much larger than rounding +error. Independent exact rational-power fixtures and short Fraction sums check +the arithmetic, direction of rounding and first-omitted-term index. A one-term +enclosure is deliberately too wide for the dual and must fail closed. + +Every nonzero dual slack below has zero rank mass: `sum c_r*r=0`. Hence + +``` +(sum c_r H_r(a))/a = sum c_r g_r(a). +``` + +For each positive coefficient, use the lower `g_r` bound at `a0=173/100000` +and the upper bound at `a1=174/100000`; reverse them for negative coefficients. +This encloses the expression **for all real a in [a0,a1]**. The checker refuses +to cancel the linear part when the rank mass is nonzero. + +## 4. Recovering the duals and their faces + +There are nine dual variables: four capacity prices `u_c` and five item prices +`v_w`. The desired inequalities are + +``` +u_c + sum n_w v_w <= H_(c-sum w*n_w). +``` + +The source certificate's eight central primal patterns are declarative data, +not executable evidence. We solve their eight tightness equations symbolically +over rational coefficients of `H_r`. The ninth equation is one of: + +- middle: `v8-v7=d` (free-mixture stationarity); +- left: tightness of capacity-32 pattern `7+8+8+9`; +- right: tightness of capacity-48 pattern `6+6+9+9+9+9`. + +Each exact linear system is nonsingular, and its solution must equal the +published potential expressions. Every recovered dual is then evaluated on +all 841 patterns. Zero expressions are recognized algebraically; all others +have strictly positive interval lower bounds. The following displayed bounds +are conservative rational truncations of `RESULT.json`: + +| Dual | Identically tight | Strict | Lower bound on every nonzero slack/a | +|---|---:|---:|---:| +| Left | 11 | 830 | > 4.38806 | +| Middle | 8 | 833 | > 0.69698 | +| Right | 9 | 832 | > 2.37161 | + +The left face has eleven tight patterns, even though the chosen affine witness +uses nine. No uniqueness claim about every left-face allocation is needed. +The middle face has exactly the eight source patterns. + +## 5. Primal balance, uniqueness and the whole interval of mixtures + +For the middle support, solve all nine balance equations with its eight +multiplicities and `x` as unknowns. The determinant is exactly `-10` and the +unique solution is + +``` +x=1080, +y=(241920,161280,1620,10620,58320,90720,138492,22788) +``` + +in the source table's order. Each multiplicity is positive. Its idle invoice +is `22788 H3+1620 H5+138492 H48`. All other patterns have strict dual slack, +so any global optimum must use this support. The exact balance system then +forces the displayed multiplicities and mixture. This proves uniqueness in +the relaxed pattern program for every exponent in the certified interval. + +For each side, add its ninth tight pattern and solve the nine balances with +right-hand side affine in `x`. The result gives every multiplicity as +`b_j+d_j*x`; no sampled interpolation is used to infer this form. Exact +nonnegativity at each segment's endpoints proves it throughout that segment. +All patterns in the affine witnesses are symbolically complementary to the +corresponding dual. Thus both witnesses attain the dual bound for every real +`x` in `[0,1080]` or `[1080,3240]` respectively. + +The complete objective slopes are independently recovered as + +``` +s_left = d-H3/20-H5/4+H48/20, +s_right = d+(H5-H3)/2. +``` + +The binomial certificate encloses `s_left/a` in +`[-0.348858,-0.348494]` and `s_right/a` in `[4.365719,4.365912]`. +The complete bill therefore strictly decreases to 1080 and strictly increases +after 1080. These facts concern the complete invoice, not scalar ADD counts. + +At `x=1090`, the derived right-face witness has idle +`22783 H3+1625 H5+138492 H48` and exactly five capacity-48 bins containing +`6+6+9+9+9+9`. This verifies the pooled feasibility question raised by PR5280. +The eight central patterns alone cannot serve `x=1090`: the central balance +system forces `x=1080`. The original central idle multiset itself also has ten +too few residual rank units at `x=1090`. Thus PR4170's request for that same +idle multiset at 1090 must change the mixture or the invoice; it is not an +unresolved chronological rearrangement. All these formulas already follow +from PR4091. Their derivation and audit, not their discovery, are claimed here. + +## 6. Root implication and limits + +The derived complete profile is + +``` +8060040 H1 + 2310120 H2 + 751788 H3 + 327240 H4 + + 66420 H5 + 25920 H8 + 138492 H48. +``` + +The checker evaluates only the coarse endpoints `a0,a1`, obtaining negative +and positive signed moments respectively against `(896*360)H73`. +Every paid rank is positive and below 73. After division by `H73`, every term +is strictly increasing in `a`, so this profile has exactly one root in the +certified interval. At that root the middle dual bounds every feasible +complete profile below by the same stock bill. Each such normalized profile +is also strictly increasing, so none has a larger root, including outside +the interval where these dual formulas were certified. + +This independently checks the pooled optimality implication. The published +24-place root bracket is not recomputed, refined or used as an acceptance +input. No κ improvement, chronological construction, native/operator replay, +stock implementation, compiler, precision/tape, BIT/outer admission or +all-size multiplication theorem is claimed. The current selected result is +a changed mechanism and is not subject to this historical fixed-model cap. + +Prepared for commdata2338 (@commdata2338), with substantial OpenAI Codex assistance. +Ross Richardson, Cinna Davis and the predecessor lineage credited in README.md +retain their construction and theorem credit. Apache-2.0. diff --git a/research/staged-fourth-dual-binomial-audit/README.md b/research/staged-fourth-dual-binomial-audit/README.md new file mode 100644 index 0000000000..5104034e34 --- /dev/null +++ b/research/staged-fourth-dual-binomial-audit/README.md @@ -0,0 +1,143 @@ +# Independent binomial-series audit of the PR4091 pooled dual + +**No discrepancy found in the scoped pooled proof. No new κ.** A separate +standard-library implementation verifies all three duals of +[Ross Richardson's PR4091](https://github.com/CrocSwap/integer-mult-bounds/pull/4091) +on every whole-helper bin pattern, uniformly for +`0.00173 <= a <= 0.00174`. It reconstructs the affine primal witnesses for +every real mixture `0 <= x <= 3240` and the unique global optimum `x=1080`. + +This closes a specific independent-verification obligation on the revision-7 +`independent-moment` card. It does not recompute more digits of a root or +search for another packing. The mathematical optimum and its witnesses remain +PR4091's contribution. + +| Checked object | Result | +|---|---| +| Complete pattern census, independently counted by a generating-function recurrence | 5 / 21 / 158 / 657 at capacities 8 / 16 / 32 / 48; 841 total | +| Left / middle / right dual faces | 11 / 8 / 9 identically tight patterns; all others strictly positive throughout the interval | +| Nonzero slack divided by `a`, conservative lower bounds | > 4.38806 / 0.69698 / 2.37161 | +| Central balance matrix | determinant −10; unique `x=1080` and all eight multiplicities recovered | +| Complete objective slope divided by `a` | left in [−0.348858,−0.348494]; right in [4.365719,4.365912] | +| `x=1090` consequence | right-face optimum has five `48:(6,6,9,9,9,9)` bins and idle `{3:22783,5:1625,48:138492}` | + +The last row answers the pooled-feasibility question in +[PR5280](https://github.com/CrocSwap/integer-mult-bounds/pull/5280). +The central eight-pattern support alone forces 1080 calls. The central idle +multiset also has ten too few residual rank units for 1090. Thus +[PR4170](https://github.com/CrocSwap/integer-mult-bounds/pull/4170)'s open +question about reaching that same multiset **at 1090** requires changing the +mixture or invoice. These are independently checked consequences of PR4091's +existing formulas, not newly discovered constructions. + +## Independence and evidence + +The checker imports no predecessor Python. It recovers dual prices from exact +linear equations instead of executing the published formulas. It enumerates +patterns by a Cartesian product and checks every residual count against a +separate coin-generating-function recurrence. Its power enclosures use the +positive binomial series for `(r^(1-a)-r)/a`, integer outward rounding and an +explicit geometric tail. They use no logarithm/exponential engine, floating +acceptance, optimizer or external numerical library. + +[PROOF.md](PROOF.md) proves the interval enclosure, weak-duality implication, +unique central optimum and global root-ceiling implication. [RESULT.json](RESULT.json) +records exact rational evidence, the census hash, affine solutions and input +hashes. Only the coarse endpoints `.00173` and `.00174` are evaluated to put +the root inside the dual-certified interval. The published 24-place root +bracket is not freshly verified or refined. + +Twenty-one arithmetic/control tests include exact rational-root fixtures, a +Fraction partial-sum oracle, omitted-tail discrimination, missing/duplicate +patterns, a zero-mass perturbation that violates dual feasibility, inadequate +precision, wrong mixture/width/replica factor, an unpaid local charge and +corrupt source bytes. Explicit checks remain active under Python `-O`. + +This is an independently implemented audit, author-checked in this package. +There was no separate human, external-agent or formal-kernel review. + +## Source and accounting boundaries + +Base: `32890bc5de034ab8fc93ac88ead7279a6a416d04`. Audited PR4091: +`a29bdd8f56cd18b805917775cdec09ff935eddc4`; its package is unchanged at the base. +Frozen PR4088: `76088d49e3ed4142a958659aa996b0ca4da5e88e`. + +The eight exact input files are pinned in [SOURCES.json](SOURCES.json) and +declared in [VERIFY.json](VERIFY.json). The audit reconstructs helper widths +by explicit binary spans in all four word exports and derives bin counts +from the template and current order. It **inherits the local paid-profile +reports and comparison stock coefficient**. It does not rescan every paid +frame transition or establish native/operator correctness. + +The complete bill includes `3240 L3 + x(L4-L3)` and every residual child, +including empty bins, against `(896*360)H73`. Words, whole-helper widths, +capacities, stock and this accounting boundary are fixed. Changing them +requires a new model. The selected PR5413 mechanism is outside this historical +ceiling's scope. + +Not checked: chronological/family/offset feasibility, native and dirty-state +identities, source local-profile correctness, actual stock provision, compiler, +all-size, precision/tape, BIT or outer admission. No supplier promotion or +complete multiplication theorem follows from this audit. PR4181's reported +chronological attainment is credited but not replayed here. + +## Reproduce + +From the repository root, Python 3.12 and its standard library: + +```sh +python3 -B scripts/research_package.py --package research/staged-fourth-dual-binomial-audit --check-only +python3 -B scripts/research_package.py --package research/staged-fourth-dual-binomial-audit +``` + +The registered commands run the checker and all 21 tests in normal and +optimized modes. A direct checker run takes about one second on the measured +Linux/Python 3.12 environment; timing is host-dependent. Expected checker line: + +```text +PASS_STAGED_FOURTH_DUAL_BINOMIAL_AUDIT patterns=841 duals=3 tight=11/8/9 unique_x=1080 +``` + +The direct scripts also work from an official export containing the declared +inputs, without Git or network access: + +```sh +python3 -I -W error -B research/staged-fourth-dual-binomial-audit/verify.py +python3 -I -W error -B research/staged-fourth-dual-binomial-audit/test_verify.py +``` + +Add `-O` to check optimized execution. Normal replay compares the complete +canonical JSON result and never rewrites it. Regeneration is explicit: +`verify.py --output PATH`. + +## Open next questions + +No further fixed-inventory packing search is justified by this audit: +[PR4181](https://github.com/CrocSwap/integer-mult-bounds/pull/4181) already reports +attaining PR4091's cap. A consequential follow-up must name a changed word, +inventory or consumer boundary and derive its complete signed invoice before +reusing a ceiling. The first step is to identify which of the model's item, +capacity, residual or stock equations changes; absent such a source-bound +change, this audit supplies no reason to expand the search. Physical admission +and independent source-transition coverage remain separate obligations, not +closed by these LP checks. + +## Credit + +Prepared for commdata2338 (@commdata2338), with substantial OpenAI Codex assistance. + +Ross Richardson and the credited PR4091 specialists supplied the pooled +theorem, all three duals and the affine witnesses. Cinna Davis/PR4088 supplied +the fixed words and fill. Nick Petalas/PR4170 and unpaidmoon/PR5280 supplied +the source-transfer checks and follow-up questions; their checks explicitly +exclude the pooled dual proof. Rohan Arun/PR4181 supplied the chronological +attainment. Retain Rohan Arun/PR4076; David Ganz (Dugongue)/PR3945 and +zxv/PR4085 with their lineage; dataisfire/PR3734; Erwan Secousses +(ChaloupeMusic)/PR3949/3815; and the original geometry, native, owner, compiler and transfer +contributors credited in PR4091's notices. This account's PR3237 concerned a +different PR2979 final-fill model and is not repeated here. + +The new work is the binomial enclosure implementation, independently solved +dual/primal certificate, finite audit and controls. Substantial OpenAI Codex +(GPT-6 Astra) assistance was used for derivation, implementation, checking and +writing. No independent human review is claimed. Apache-2.0. diff --git a/research/staged-fourth-dual-binomial-audit/RESULT.json b/research/staged-fourth-dual-binomial-audit/RESULT.json new file mode 100644 index 0000000000..58e9643cd2 --- /dev/null +++ b/research/staged-fourth-dual-binomial-audit/RESULT.json @@ -0,0 +1,702 @@ +{ + "affine_primal": { + "left": { + "determinant": "-20", + "domain": [ + 0, + 1080 + ], + "multiplicity_constant_and_x": [ + [ + "241920", + "0" + ], + [ + "161280", + "0" + ], + [ + "1890", + "-1/4" + ], + [ + "9810", + "3/4" + ], + [ + "58320", + "0" + ], + [ + "90720", + "0" + ], + [ + "138438", + "1/20" + ], + [ + "22842", + "-1/20" + ], + [ + "540", + "-1/2" + ] + ], + "patterns": [ + [ + 8, + 0, + 0, + 0, + 1, + 0, + 0 + ], + [ + 16, + 0, + 0, + 1, + 0, + 1, + 0 + ], + [ + 32, + 0, + 0, + 0, + 0, + 3, + 5 + ], + [ + 32, + 0, + 0, + 2, + 0, + 2, + 0 + ], + [ + 32, + 0, + 1, + 0, + 1, + 2, + 0 + ], + [ + 32, + 1, + 0, + 0, + 0, + 3, + 0 + ], + [ + 48, + 0, + 0, + 0, + 0, + 0, + 48 + ], + [ + 48, + 0, + 0, + 0, + 0, + 5, + 3 + ], + [ + 32, + 0, + 0, + 1, + 2, + 1, + 0 + ] + ] + }, + "right": { + "determinant": "20", + "domain": [ + 1080, + 3240 + ], + "multiplicity_constant_and_x": [ + [ + "241920", + "0" + ], + [ + "161280", + "0" + ], + [ + "1080", + "1/2" + ], + [ + "10080", + "1/2" + ], + [ + "59400", + "-1" + ], + [ + "90720", + "0" + ], + [ + "138492", + "0" + ], + [ + "23328", + "-1/2" + ], + [ + "-540", + "1/2" + ] + ], + "patterns": [ + [ + 8, + 0, + 0, + 0, + 1, + 0, + 0 + ], + [ + 16, + 0, + 0, + 1, + 0, + 1, + 0 + ], + [ + 32, + 0, + 0, + 0, + 0, + 3, + 5 + ], + [ + 32, + 0, + 0, + 2, + 0, + 2, + 0 + ], + [ + 32, + 0, + 1, + 0, + 1, + 2, + 0 + ], + [ + 32, + 1, + 0, + 0, + 0, + 3, + 0 + ], + [ + 48, + 0, + 0, + 0, + 0, + 0, + 48 + ], + [ + 48, + 0, + 0, + 0, + 0, + 5, + 3 + ], + [ + 48, + 0, + 2, + 0, + 0, + 4, + 0 + ] + ] + } + }, + "central_multiplicities": [ + "241920", + "161280", + "1620", + "10620", + "58320", + "90720", + "138492", + "22788" + ], + "central_primal_determinant": "-10", + "coarse_root_endpoint_moments": [ + [ + "-16241015791501797116692177719626473852647925323/250000000000000000000000000000000000000000000", + "-2030126973913945743290013383041304863372925493/31250000000000000000000000000000000000000000" + ], + [ + "597746902052439528171854380263200542988490579/1000000000000000000000000000000000000000000", + "4669897672290662409923564408045473057741744641/7812500000000000000000000000000000000000000" + ] + ], + "complete_paid_profile": { + "1": "8060040", + "2": "2310120", + "3": "751788", + "4": "327240", + "48": "138492", + "5": "66420", + "8": "25920" + }, + "dual": { + "left": { + "basis_determinant": "-20", + "minimizing_enclosure_pattern": [ + 32, + 0, + 0, + 0, + 1, + 2, + 6 + ], + "minimum_slack_over_a_lower_bound": "877612649190601461796731127324849256083173/200000000000000000000000000000000000000000", + "slope_expression": { + "1": "2", + "3": "59/20", + "4": "-3", + "48": "1/20", + "5": "-1/4" + }, + "slope_over_a_interval": [ + "-69771542229381529416471873498085228012297/200000000000000000000000000000000000000000", + "-34849405712051065308162278764024479025607/100000000000000000000000000000000000000000" + ], + "strict_patterns": 830, + "tight_patterns": [ + [ + 8, + 0, + 0, + 0, + 1, + 0, + 0 + ], + [ + 16, + 0, + 0, + 0, + 2, + 0, + 0 + ], + [ + 16, + 0, + 0, + 1, + 0, + 1, + 0 + ], + [ + 32, + 0, + 0, + 0, + 0, + 3, + 5 + ], + [ + 32, + 0, + 0, + 0, + 4, + 0, + 0 + ], + [ + 32, + 0, + 0, + 1, + 2, + 1, + 0 + ], + [ + 32, + 0, + 0, + 2, + 0, + 2, + 0 + ], + [ + 32, + 0, + 1, + 0, + 1, + 2, + 0 + ], + [ + 32, + 1, + 0, + 0, + 0, + 3, + 0 + ], + [ + 48, + 0, + 0, + 0, + 0, + 0, + 48 + ], + [ + 48, + 0, + 0, + 0, + 0, + 5, + 3 + ] + ] + }, + "middle": { + "basis_determinant": "-10", + "minimizing_enclosure_pattern": [ + 16, + 0, + 0, + 0, + 2, + 0, + 0 + ], + "minimum_slack_over_a_lower_bound": "34849405712051065308162278764024479025607/50000000000000000000000000000000000000000", + "slope_expression": {}, + "slope_over_a_interval": [ + "0", + "0" + ], + "strict_patterns": 833, + "tight_patterns": [ + [ + 8, + 0, + 0, + 0, + 1, + 0, + 0 + ], + [ + 16, + 0, + 0, + 1, + 0, + 1, + 0 + ], + [ + 32, + 0, + 0, + 0, + 0, + 3, + 5 + ], + [ + 32, + 0, + 0, + 2, + 0, + 2, + 0 + ], + [ + 32, + 0, + 1, + 0, + 1, + 2, + 0 + ], + [ + 32, + 1, + 0, + 0, + 0, + 3, + 0 + ], + [ + 48, + 0, + 0, + 0, + 0, + 0, + 48 + ], + [ + 48, + 0, + 0, + 0, + 0, + 5, + 3 + ] + ] + }, + "right": { + "basis_determinant": "20", + "minimizing_enclosure_pattern": [ + 8, + 0, + 0, + 1, + 0, + 0, + 1 + ], + "minimum_slack_over_a_lower_bound": "9486450986012095651884369696156928829747/4000000000000000000000000000000000000000", + "slope_expression": { + "1": "2", + "3": "5/2", + "4": "-3", + "5": "1/2" + }, + "slope_over_a_interval": [ + "87314384458316548461893549780584673777801/20000000000000000000000000000000000000000", + "43659118684412402591158647074026511203123/10000000000000000000000000000000000000000" + ], + "strict_patterns": 832, + "tight_patterns": [ + [ + 8, + 0, + 0, + 0, + 1, + 0, + 0 + ], + [ + 16, + 0, + 0, + 1, + 0, + 1, + 0 + ], + [ + 32, + 0, + 0, + 0, + 0, + 3, + 5 + ], + [ + 32, + 0, + 0, + 2, + 0, + 2, + 0 + ], + [ + 32, + 0, + 1, + 0, + 1, + 2, + 0 + ], + [ + 32, + 1, + 0, + 0, + 0, + 3, + 0 + ], + [ + 48, + 0, + 0, + 0, + 0, + 0, + 48 + ], + [ + 48, + 0, + 0, + 0, + 0, + 5, + 3 + ], + [ + 48, + 0, + 2, + 0, + 0, + 4, + 0 + ] + ] + } + }, + "enclosure": { + "exponent_interval": [ + "173/100000", + "87/50000" + ], + "method": "positive binomial series; integer outward rounding; geometric tail", + "scale": "10000000000000000000000000000000000000000", + "terms": 2048 + }, + "idle": { + "3": "22788", + "48": "138492", + "5": "1620" + }, + "inherited_local_profiles": { + "FOUR": { + "1": 2489, + "2": 713, + "3": 227, + "4": 99, + "5": 20, + "8": 8 + }, + "THREE": { + "1": 2487, + "2": 713, + "3": 224, + "4": 102, + "5": 20, + "8": 8 + } + }, + "pattern_counts": { + "8": 5, + "16": 21, + "32": 158, + "48": 657 + }, + "pattern_sha256": "3bbb7e039600e9ac39d7da145384354c1541eac7987a482ed556dcd4e5729e14", + "patterns": 841, + "scope": "Fixed PR4091 pooled LP; source local-profile reports inherited; no owner/native/admission replay or new kappa.", + "source_bins": { + "8": 241920, + "16": 161280, + "32": 161280, + "48": 161280 + }, + "source_sha256": { + "research/staged-fourth-mixture-ceiling/PROOF.md": "fc9a073b2c334e8e413062157569653e8bb52db81d72d68621287f6810090f40", + "research/staged-fourth-mixture-ceiling/RESULT.json": "53849028b12f7d9b726ac7576eeb64dc9a1a51bb2890edbb15aa83d1e39fae5f", + "research/staged-fourth-mixture-ceiling/source4088/inputs/FOUR-base.json.gz": "aecaddba48fdff6353a6511c3623346b05aa607e30103fb016604a2b1025ce95", + "research/staged-fourth-mixture-ceiling/source4088/inputs/FOUR-extra.json.gz": "615093190aa5479034bb8acdd8925d7a910e082b84dec7df84b459b62421235a", + "research/staged-fourth-mixture-ceiling/source4088/inputs/THREE-base.json.gz": "df31495cff95a1e512da398f52841c6b5ade29067869b3d68b89d756a5641112", + "research/staged-fourth-mixture-ceiling/source4088/inputs/THREE-extra.json.gz": "9a28f7ef91938c0866e408eb06e03eb5f8e727a00b44eb936ddd5ed48704bd4c", + "research/staged-fourth-mixture-ceiling/source4088/owner/ORDER.json": "743e74b538432e2b2045e754b0de9c18f36fc5039fdb8eb542177a898ec78e44", + "research/staged-fourth-mixture-ceiling/source4088/owner/TEMPLATE.json.gz": "21297b20f1f2dc76eb9dd8124416068c3cb096bab9df17fa4da19bc68dfe082e" + }, + "source_widths": { + "FOUR": { + "5": 28, + "6": 18, + "7": 57, + "8": 92, + "9": 213 + }, + "THREE": { + "5": 28, + "6": 18, + "7": 56, + "8": 93, + "9": 213 + } + }, + "status": "PASS_STAGED_FOURTH_DUAL_BINOMIAL_AUDIT", + "unique_mixture": "1080", + "x1090": { + "idle": { + "3": "22783", + "48": "138492", + "5": "1625" + }, + "new_cap48_pattern_count": "5", + "status": "right-face pooled optimum; central eight-pattern support alone is infeasible" + } +} diff --git a/research/staged-fourth-dual-binomial-audit/SOURCES.json b/research/staged-fourth-dual-binomial-audit/SOURCES.json new file mode 100644 index 0000000000..9281cce687 --- /dev/null +++ b/research/staged-fourth-dual-binomial-audit/SOURCES.json @@ -0,0 +1,66 @@ +{ + "schema_version": 1, + "base_commit": "32890bc5de034ab8fc93ac88ead7279a6a416d04", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "fc3d4ba105e1f097d0d7d051a308281e86ab1446", + "sha256": "66974efdced4083c00025f97d95d83909a226cdf801edb9301c195c6641f6903" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "f126dd2e2dad2b669e75d1d0d0bd05c600725602", + "sha256": "f7a48bfa2659b88378282a8eee7d9fe52cdf505594124c4d1686b58510fffd72" + }, + { + "path": "research/staged-fourth-mixture-ceiling/PROOF.md", + "usage": "input", + "git_blob": "c67a80c8727ee45e2ba61de28bbaca8bb6d45e2a", + "sha256": "fc9a073b2c334e8e413062157569653e8bb52db81d72d68621287f6810090f40" + }, + { + "path": "research/staged-fourth-mixture-ceiling/RESULT.json", + "usage": "input", + "git_blob": "2803d5c42b5d49ea72bd9bb006ffb4a9eec6a316", + "sha256": "53849028b12f7d9b726ac7576eeb64dc9a1a51bb2890edbb15aa83d1e39fae5f" + }, + { + "path": "research/staged-fourth-mixture-ceiling/source4088/inputs/FOUR-base.json.gz", + "usage": "input", + "git_blob": "65957e5ca322049d985f23fdc0bd8da07ffa4c2a", + "sha256": "aecaddba48fdff6353a6511c3623346b05aa607e30103fb016604a2b1025ce95" + }, + { + "path": "research/staged-fourth-mixture-ceiling/source4088/inputs/FOUR-extra.json.gz", + "usage": "input", + "git_blob": "1f3239c30e9343cf4e34b4371fcbeebb94a19011", + "sha256": "615093190aa5479034bb8acdd8925d7a910e082b84dec7df84b459b62421235a" + }, + { + "path": "research/staged-fourth-mixture-ceiling/source4088/inputs/THREE-base.json.gz", + "usage": "input", + "git_blob": "137793e275870db2161048405017b83dcc1824ee", + "sha256": "df31495cff95a1e512da398f52841c6b5ade29067869b3d68b89d756a5641112" + }, + { + "path": "research/staged-fourth-mixture-ceiling/source4088/inputs/THREE-extra.json.gz", + "usage": "input", + "git_blob": "7cce921b20dc0504cea954ab3297c5b55a9468dc", + "sha256": "9a28f7ef91938c0866e408eb06e03eb5f8e727a00b44eb936ddd5ed48704bd4c" + }, + { + "path": "research/staged-fourth-mixture-ceiling/source4088/owner/ORDER.json", + "usage": "input", + "git_blob": "58d4b4c34170788a825d4c4e595fe45e28ef3fd2", + "sha256": "743e74b538432e2b2045e754b0de9c18f36fc5039fdb8eb542177a898ec78e44" + }, + { + "path": "research/staged-fourth-mixture-ceiling/source4088/owner/TEMPLATE.json.gz", + "usage": "input", + "git_blob": "114808c32b1799da53524bdc25cea67efb60009e", + "sha256": "21297b20f1f2dc76eb9dd8124416068c3cb096bab9df17fa4da19bc68dfe082e" + } + ] +} diff --git a/research/staged-fourth-dual-binomial-audit/TASK.json b/research/staged-fourth-dual-binomial-audit/TASK.json new file mode 100644 index 0000000000..4f97b6f698 --- /dev/null +++ b/research/staged-fourth-dual-binomial-audit/TASK.json @@ -0,0 +1,146 @@ +{ + "schema_version": 1, + "task_id": "independent-moment", + "priority_revision": 7, + "base_commit": "32890bc5de034ab8fc93ac88ead7279a6a416d04", + "original_card": { + "id": "independent-moment", + "question": "Does a new paid-profile or mixture-ceiling claim have independent source-bound coverage of its actual changed ledger?", + "starting_points": [ + "docs/research/research-family-status.md", + "certificates/selected-result.json", + "research/staged544-mixed-fourth-entry/README.md", + "research/staged-fourth-mixture-ceiling/README.md", + "research/r437-two-window-carrier/README.md" + ], + "methods": [ + "Independently reconstruct one changed paid ledger or pooled dual with exact source and model binding.", + "Check a genuinely uncovered moment implication with a different enclosure method and semantic controls." + ], + "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_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Choose one uncovered implication in #4088 literal mixed fill, #4091 pooled dual/model binding or #4067 changed frame/host bill. #4091 pins an earlier #4088 head: validate word, capacity and stock equivalence before applying that ceiling to the later fill.", + "scope": "Source-binding orientation only; no scientific replay, theorem acceptance or supplier admission. Budget any heavy replay separately." + }, + "first_experiment": "Independently reconstruct one changed ledger or pooled certificate with a positive case and a semantic failure control. Compare exact sources and name what existing checks miss. Keep this separate from supplier-boundary-audit (ordinary/outer dispatch) and uniform-transfer-audit (all-size proof). Stop after the chosen implication; more digits of an unchanged root are not additional mechanism coverage.", + "bottleneck_link": "Independent pricing prevents unsupported frontier claims and can reveal genuine accounting slack.", + "allowed_variations": [ + "Reconstruct either a source ledger or a numeric enclosure with a different method." + ], + "scope_change_triggers": [ + "Importing the primary function and calling its output independent verification.", + "Calling an aggregate histogram or source archive an independently accepted physical supplier." + ], + "overlap_terms": [ + "independent moment", + "rank histogram", + "exact enclosure", + "2979", + "rank7 joint endframes", + "paired extraction", + "joint lowering", + "4088", + "4091", + "4067", + "staged544-mixed-fourth-entry", + "staged-fourth-mixture-ceiling", + "r437-two-window-carrier" + ], + "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_status": "refined", + "actual_scope": "Independent exact binomial-series audit of PR4091 three pooled duals, all 841 whole-helper patterns, affine primal witnesses for real x in [0,3240], and unique x=1080 optimum for every a in [0.00173,0.00174].", + "scope_change_reason": "The revision-7 card explicitly requests pooled-dual coverage. PR4170 and PR5280 cover source transfer but exclude the dual proof; this audit uses a different enclosure method and independently solves its equality systems. No root refinement or packing search.", + "bottleneck_link": "Supply independent source-bound evidence for a named complete-invoice ceiling, separating fixed-model pooled optimality from chronological construction and supplier admission.", + "budget_minutes": 60, + "stop_rule": "Stop at an exact discrepancy or completion of the three-dual, complete-pattern, affine-primal audit. No dependent search, ordinary/outer replay or selected-frontier change.", + "outcome": "completed", + "evidence": "RESULT.json and PROOF.md; verify.py plus 21 positive/arithmetic/rejection tests in test_verify.py, normal and optimized Python. Eight immutable live inputs are authenticated. Source local-profile reports and stock coefficient remain inherited.", + "author": "commdata2338", + "ai_assistance": "Substantial OpenAI Codex (GPT-6 Astra) assistance in derivation, implementation, checking and writing; author-checked independent implementation, no independent human or external-agent review.", + "open_questions": [], + "scope_key": "9f27273fb945e4fc4274", + "scope_detail_key": "pr4091-binomial-dual-audit", + "no_open_questions_reason": "None is justified within this fixed invoice: PR4181 already reports chronological attainment of the cap. A new source word, inventory or consumer boundary needs its own complete signed invoice and model before a fresh expansion; source-transition correctness and physical admission remain separate obligations.", + "track": "independent-verification", + "selection": { + "method": "handoff-first; specific revision-7 card retrieval after checking source-transfer and pooled-fill coverage", + "command": "python3 -B scripts/choose_current_research_task.py --task independent-moment", + "seed": "c96fb7aca3d981b76569c66ee826ff3a", + "canonical_thread": "https://github.com/CrocSwap/integer-mult-bounds/discussions/3606#discussioncomment-19046131" + }, + "dependencies": { + "PR4091": "a29bdd8f56cd18b805917775cdec09ff935eddc4", + "PR4088_frozen": "76088d49e3ed4142a958659aa996b0ca4da5e88e", + "PR4088_later_context_only": "72d7efc181edb21806a878f174847c96dd410ab0", + "PR4170_context_only": "6fc2f387b13157778aff09b1611425b5cdd2f406", + "PR5280_context_only": "a0dab1be029af75ef635a10eb9c905014dc54a31" + }, + "nearest_overlap": [ + { + "pr": 4091, + "difference": "Its original theorem and same-session primary/secondary checks are credited; this supplies separately implemented binomial arithmetic and exact-system reconstruction." + }, + { + "pr": 4170, + "difference": "Source-equivalence and root comparison explicitly exclude the all-pattern dual proof." + }, + { + "pr": 5280, + "difference": "Source-equivalence follow-up excludes LP feasibility; the x1090 pooled consequence is checked here." + }, + { + "pr": 4181, + "difference": "Chronological fill and root; the scoped independent finding excludes the ceiling proof." + }, + { + "pr": 3237, + "difference": "This account earlier audited a different PR2979 2551-pattern terminal-control model." + } + ], + "family_expansion_decision": "Narrow and complete the bounded audit; no new construction or fixed-invoice optimization.", + "remaining_obligations": [ + "Local paid-profile reports are inherited, not independently reconstructed from every source transition.", + "One residual per bin, fixed stock and legal-fill-to-LP mapping retain their declared source contract.", + "Chronology, family exclusion, offsets, native phases and dirty-state identities are not replayed.", + "Uniform compiler, actual stock, precision/tape, BIT, outer admission and all-size multiplication assumptions remain separate.", + "The 24-place root bracket is not freshly checked; only the broad certified interval is bracketed." + ], + "upstream_checkpoint": { + "commit": "32890bc5de034ab8fc93ac88ead7279a6a416d04", + "checked_at_utc": "2026-10-25T05:29:49.117685+00:00", + "priority_revision": 7, + "changes_since_base": "none; source pins and selected record preserved" + } +} diff --git a/research/staged-fourth-dual-binomial-audit/VERIFY.json b/research/staged-fourth-dual-binomial-audit/VERIFY.json new file mode 100644 index 0000000000..a57b419dc8 --- /dev/null +++ b/research/staged-fourth-dual-binomial-audit/VERIFY.json @@ -0,0 +1,72 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/staged-fourth-mixture-ceiling/PROOF.md", + "research/staged-fourth-mixture-ceiling/RESULT.json", + "research/staged-fourth-mixture-ceiling/source4088/inputs/FOUR-base.json.gz", + "research/staged-fourth-mixture-ceiling/source4088/inputs/FOUR-extra.json.gz", + "research/staged-fourth-mixture-ceiling/source4088/inputs/THREE-base.json.gz", + "research/staged-fourth-mixture-ceiling/source4088/inputs/THREE-extra.json.gz", + "research/staged-fourth-mixture-ceiling/source4088/owner/ORDER.json", + "research/staged-fourth-mixture-ceiling/source4088/owner/TEMPLATE.json.gz" + ], + "commands": [ + { + "name": "normal-verify", + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 30, + "checks": "Exact binomial interval certificate, all 841 patterns and three duals; complete saved JSON equality" + }, + { + "name": "normal-test_verify", + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-B", + "{package}/test_verify.py" + ], + "timeout_seconds": 30, + "checks": "21 positive arithmetic fixtures and semantic rejection tests; assertions remain active via unittest" + }, + { + "name": "optimized-verify", + "argv": [ + "{python}", + "-I", + "-O", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 30, + "checks": "Exact binomial interval certificate, all 841 patterns and three duals; complete saved JSON equality" + }, + { + "name": "optimized-test_verify", + "argv": [ + "{python}", + "-I", + "-O", + "-W", + "error", + "-B", + "{package}/test_verify.py" + ], + "timeout_seconds": 30, + "checks": "21 positive arithmetic fixtures and semantic rejection tests; assertions remain active via unittest" + } + ] +} diff --git a/research/staged-fourth-dual-binomial-audit/test_verify.py b/research/staged-fourth-dual-binomial-audit/test_verify.py new file mode 100644 index 0000000000..ea51edd10d --- /dev/null +++ b/research/staged-fourth-dual-binomial-audit/test_verify.py @@ -0,0 +1,174 @@ +"""Positive arithmetic fixtures and adversarial controls for the scoped audit. + +Prepared for commdata2338 with substantial OpenAI Codex assistance. Apache-2.0. +""" + +import copy +from fractions import Fraction as F +import hashlib +import importlib.util +from pathlib import Path +import unittest +from unittest.mock import patch + +SPEC = importlib.util.spec_from_file_location("dual_audit", Path(__file__).with_name("verify.py")) +v = importlib.util.module_from_spec(SPEC) +SPEC.loader.exec_module(v) + + +class AuditControls(unittest.TestCase): + @classmethod + def setUpClass(cls): + cls.rows = v.patterns() + cls.bins, cls.profiles, cls.widths, cls.delta = v.source_model() + cls.published = v.read_source("RESULT.json") + cls.support = v.support_from_certificate(cls.published) + cls.dual, _ = v.reconstruct_dual(cls.support, "middle", cls.delta) + central, _ = v.primal_system(cls.support, cls.bins, cls.widths, True) + cls.values = [row[0] for row in central[:-1]] + + def test_known_rational_powers(self): + # Exact roots, not a second floating-point evaluation of the same formula. + for base, degree in ((2, 2), (3, 2), (5, 2), (7, 2), (2, 3), (3, 3), (2, 6)): + rank = base**degree + a = 1 - F(1, degree) + exact = (base - rank) / a + lower, upper = v.normalized_power(rank, a) + with self.subTest(rank=rank, a=a): + self.assertLessEqual(lower, exact) + self.assertGreaterEqual(upper, exact) + + def test_integer_rounding_against_exact_partial_sum(self): + # A slow Fraction oracle checks rounding and the first-omitted-term index. + for rank, a, terms in ((2, v.LOW, 1), (3, v.HIGH, 8), (48, F(1, 2), 17)): + z = F(rank - 1, rank) + term, total = z, F(0) + for k in range(1, terms + 1): + total += term + term *= (k - a) * z / (k + 1) + exact_lower, exact_upper = -rank * (total + rank * term), -rank * total + lower, upper = v.normalized_power(rank, a, terms, 1000) + self.assertLessEqual(lower, exact_lower) + self.assertGreaterEqual(upper, exact_upper) + + def test_every_used_rank_against_square_identity(self): + # At a=1/2, positivity and squaring give an exact oracle for every + # consumed rank, including the stock rank73, without a root routine. + for rank in range(1, 74): + lower, upper = v.normalized_power(rank, F(1, 2)) + lower, upper = rank + lower / 2, rank + upper / 2 + with self.subTest(rank=rank): + self.assertGreater(lower, 0) + self.assertLessEqual(lower * lower, rank) + self.assertGreaterEqual(upper * upper, rank) + + def test_tail_is_necessary_and_included(self): + # At r=4,a=1/2 the normalized power is exactly -4. A one-term + # tail-free sum says -3 and excludes the true value. + lower, upper = v.normalized_power(4, F(1, 2), 1) + self.assertLessEqual(lower, -4) + self.assertGreaterEqual(upper, -4) + self.assertGreater(-4 * F(3, 4), -4) + + def test_outside_series_domain_rejected(self): + for rank, a in ((0, v.LOW), (1, F(0)), (8, F(1))): + with self.subTest(rank=rank, a=a), self.assertRaisesRegex(ValueError, "binomial domain"): + v.normalized_power(rank, a) + + def test_missing_empty_pattern_rejected(self): + rows = [row for row in self.rows if row != (48, 0, 0, 0, 0, 0, 48)] + with self.assertRaisesRegex(ValueError, "residual spectrum"): + v.validate_patterns(rows) + + def test_missing_nonempty_pattern_rejected(self): + rows = [row for row in self.rows if row != (32, 0, 1, 0, 1, 2, 0)] + with self.assertRaisesRegex(ValueError, "residual spectrum"): + v.validate_patterns(rows) + + def test_duplicate_preserving_pattern_count_rejected(self): + rows = list(self.rows) + rows[-1] = rows[-2] + self.assertEqual(len(rows), 841) + with self.assertRaisesRegex(ValueError, "duplicate pattern"): + v.validate_patterns(rows) + + def test_wrong_residual_rejected(self): + rows = list(self.rows) + rows[0] = (*rows[0][:-1], rows[0][-1] + 1) + with self.assertRaisesRegex(ValueError, "pattern capacity"): + v.validate_patterns(rows) + + def test_zero_mass_dual_perturbation_rejected_by_sign(self): + dual = copy.deepcopy(self.dual) + # H1-H2/2 is positive for 0= 0 and 0 < r < 73 + for r, n in profile.items()), "reported local profile") + if kind in profiles: + require(profiles[kind] == profile and widths[kind] == histogram, + "orientation agreement") + profiles[kind], widths[kind] = profile, dict(histogram) + by_kind[kind] = by_role + require(by_kind["THREE"].keys() == by_kind["FOUR"].keys(), + "same helper identities") + difference = {h: (by_kind["THREE"][h], by_kind["FOUR"][h]) + for h in by_kind["THREE"] + if by_kind["THREE"][h] != by_kind["FOUR"][h]} + require(difference == {601: (8, 7)}, "changed helper601 width") + require(widths["THREE"] == {5: 28, 6: 18, 7: 56, 8: 93, 9: 213}, + "THREE width model") + delta = combine((1, profiles["FOUR"]), (-1, profiles["THREE"])) + require(delta == {1: 2, 3: 3, 4: -3}, "reported local delta") + return bins, profiles, widths, delta + + +def patterns(): + rows = [] + for capacity in CAPACITIES: + for counts in product(*(range(capacity // w + 1) for w in WIDTHS)): + residual = capacity - sum(w * n for w, n in zip(WIDTHS, counts)) + if residual >= 0: + rows.append((capacity, *counts, residual)) + validate_patterns(rows) + return rows + + +def validate_patterns(rows): + """Check every residual coefficient by an independent coin-series DP.""" + ways = [1] + [0] * max(CAPACITIES) + for width in WIDTHS: + for used in range(width, len(ways)): + ways[used] += ways[used - width] + expected = {(c, residual): ways[c - residual] + for c in CAPACITIES for residual in range(c + 1)} + actual = Counter((row[0], row[-1]) for row in rows) + require(len(rows) == len(set(rows)), "duplicate pattern") + for row in rows: + require(len(row) == 7 and row[0] in CAPACITIES, "pattern schema") + require(all(type(n) is int and n >= 0 for n in row[1:]), "whole helpers") + require(sum(w * n for w, n in zip(WIDTHS, row[1:6])) + row[-1] == row[0], + "pattern capacity") + require(all(actual[key] == count for key, count in expected.items()) + and set(actual) <= set(expected), "pattern residual spectrum") + require(len(rows) == 841, "841 patterns") + + +def constraint_row(pattern): + return [int(pattern[0] == cap) for cap in CAPACITIES] + list(pattern[1:6]) + + +def solve(matrix, rhs): + """Exact Gauss-Jordan solve, with several RHS columns and explicit pivots.""" + n = len(matrix) + require(all(len(row) == n for row in matrix) and len(rhs) == n, + "square exact system") + columns = len(rhs[0]) + require(all(len(row) == columns for row in rhs), "RHS shape") + augmented = [[F(v) for v in a + b] for a, b in zip(matrix, rhs)] + determinant = F(1) + for col in range(n): + pivot = next((i for i in range(col, n) if augmented[i][col]), None) + require(pivot is not None, "singular exact system") + if pivot != col: + augmented[col], augmented[pivot] = augmented[pivot], augmented[col] + determinant = -determinant + factor = augmented[col][col] + determinant *= factor + augmented[col] = [v / factor for v in augmented[col]] + for row in range(n): + if row != col: + factor = augmented[row][col] + augmented[row] = [x - factor * y + for x, y in zip(augmented[row], augmented[col])] + solution = [row[n:] for row in augmented] + require(all(sum(F(matrix[i][j]) * solution[j][k] for j in range(n)) + == rhs[i][k] for i in range(n) for k in range(columns)), + "solution residual") + return solution, determinant + + +def dense(expression): + return [expression.get(r, F(0)) for r in range(DIM)] + + +def sparse(vector): + return {r: coefficient for r, coefficient in enumerate(vector) if coefficient} + + +def support_from_certificate(certificate): + support = [] + for row in certificate["primal"]: + support.append((row["capacity"], *(row["helper_counts"][str(w)] for w in WIDTHS), + row["residual"])) + require(len(support) == 8 and len(set(support)) == 8, "central support") + require(set(support) <= set(patterns()), "central whole-helper patterns") + return support + + +def reconstruct_dual(support, side, delta): + equations = [constraint_row(row) for row in support] + rhs = [dense(symbol(row[-1])) for row in support] + if side == "middle": + # d + v7 - v8 = 0 is free-mixture stationarity. + equations.append([0, 0, 0, 0, 0, 0, -1, 1, 0]) + rhs.append(dense(delta)) + else: + entering = ((32, 0, 0, 1, 2, 1, 0) if side == "left" + else (48, 0, 2, 0, 0, 4, 0)) + equations.append(constraint_row(entering)) + rhs.append(dense(symbol(entering[-1]))) + answer, determinant = solve(equations, rhs) + return [sparse(row) for row in answer], determinant + + +def ceil_div(numerator, denominator): + return -(-numerator // denominator) + + +@lru_cache(None) +def normalized_power(rank, exponent, terms=TERMS, scale=SCALE): + """Enclose (rank**(1-a)-rank)/a by a positive binomial series. + + t1=z, t(k+1)=t(k)*(k-a)*z/(k+1), z=1-1/rank. + The omitted tail is <= rank*t(N+1). All operations round outwards. + """ + require(type(rank) is int and rank >= 1 and 0 < exponent < 1, + "binomial domain") + require(type(terms) is int and terms >= 1 and scale >= 1, "series precision") + if rank == 1: + return F(0), F(0) + a_num, a_den = exponent.numerator, exponent.denominator + low = scale * (rank - 1) // rank + high = ceil_div(scale * (rank - 1), rank) + sum_low = sum_high = 0 + for k in range(1, terms + 1): + sum_low += low + sum_high += high + numerator = (k * a_den - a_num) * (rank - 1) + denominator = (k + 1) * a_den * rank + low = low * numerator // denominator + high = ceil_div(high * numerator, denominator) + # high now bounds the first OMITTED term, scaled by `scale`. + return F(-rank * (sum_high + rank * high), scale), F(-rank * sum_low, scale) + + +def interval_expression(expression, lower=LOW, upper=HIGH, terms=TERMS): + require(0 < lower <= upper < 1, "exponent interval") + require(sum(r * c for r, c in expression.items()) == 0, "zero rank mass") + low = high = F(0) + for rank, coefficient in expression.items(): + # Each normalized power is increasing: positive-series coefficients decrease. + a = normalized_power(rank, lower, terms)[0] + b = normalized_power(rank, upper, terms)[1] + low += coefficient * (a if coefficient > 0 else b) + high += coefficient * (b if coefficient > 0 else a) + return low, high + + +def slack(pattern, dual): + return combine((1, symbol(pattern[-1])), + *((-n, expression) for n, expression in + zip(constraint_row(pattern), dual))) + + +def check_dual(rows, dual): + tight, bounds = [], [] + for row in rows: + expression = slack(row, dual) + if not expression: + tight.append(row) + else: + low, high = interval_expression(expression) + require(low > 0, f"nonpositive dual slack: {row}") + bounds.append((low, high, row)) + require(bounds, "nontrivial strict constraints") + return tight, min(bounds) + + +def primal_system(support, bins, widths, free_mixture=False): + columns = [constraint_row(row) for row in support] + if free_mixture: + # B*y = N*widths + x*(e7-e8), put x on the left. + columns.append([0, 0, 0, 0, 0, 0, -1, 1, 0]) + matrix = list(map(list, zip(*columns))) + base = [bins[c] for c in CAPACITIES] + [3240 * widths["THREE"][w] for w in WIDTHS] + direction = [0, 0, 0, 0, 0, 0, 1, -1, 0] + rhs = [[value] if free_mixture else [value, dx] + for value, dx in zip(base, direction)] + return solve(matrix, rhs) + + +def check_primal(rows, multiplicities, x, bins, widths): + require(len(rows) == len(multiplicities), "primal length") + require(0 <= x <= 3240 and all(value >= 0 for value in multiplicities), + "nonnegative primal") + totals = [sum(F(n) * value for n, value in zip(column, multiplicities)) + for column in zip(*(constraint_row(row) for row in rows))] + expected = [bins[c] for c in CAPACITIES] + [ + 3240 * widths["THREE"][w] + x * ((w == 7) - (w == 8)) for w in WIDTHS] + require(totals == expected, "primal bin/helper balance") + return combine(*((value, symbol(row[-1])) for row, value in zip(rows, multiplicities))) + + +def fixed_power_expression(expression, exponent): + low = high = F(0) + for rank, coefficient in expression.items(): + a, b = normalized_power(rank, exponent) + a, b = rank + exponent * a, rank + exponent * b + low += coefficient * (a if coefficient > 0 else b) + high += coefficient * (b if coefficient > 0 else a) + return low, high + + +def json_expression(expression): + return {str(r): str(c) for r, c in sorted(expression.items())} + + +def interval_json(pair): + return list(map(str, pair)) + + +def compute(): + pins = authenticate() + bins, profiles, widths, delta = source_model() + published = read_source("RESULT.json") + rows = patterns() + support = support_from_certificate(published) + require(bins == {int(k): v for k, v in published["bin_counts"].items()}, "source bins") + central, determinant = primal_system(support, bins, widths, True) + mixture = central[-1][0] + values = [row[0] for row in central[:-1]] + require(mixture == published["optimum_fourth_calls"] == 1080, "unique mixture") + require(values == [F(row["multiplicity"]) for row in published["primal"]], + "published central primal") + idle = check_primal(support, values, mixture, bins, widths) + profile = combine((3240, profiles["THREE"]), (mixture, delta), (1, idle)) + require(profile == {int(r): n for r, n in published["complete_profile"].items()}, + "complete paid profile") + require(sum(r * n for r, n in profile.items()) == 23431680, "complete paid mass") + dual_reports, affine_reports = {}, {} + for side in ("left", "middle", "right"): + dual, dual_det = reconstruct_dual(support, side, delta) + recorded = published["dual"][side] + expected = [{int(r): F(c) for r, c in recorded[kind][str(key)].items()} + for kind, keys in (("capacity_dual", CAPACITIES), ("item_dual", WIDTHS)) + for key in keys] + require(dual == expected, f"{side} independently solved potentials") + tight, smallest = check_dual(rows, dual) + recorded_tight = {(c, *counts, residual) + for c, counts, residual in recorded["identically_tight"]} + require(set(tight) == recorded_tight, f"{side} exact tight face") + slope = combine((1, delta), (1, dual[6]), (-1, dual[7])) + require(slope == {int(r): F(c) for r, c in recorded["slope_expression"].items()}, + f"{side} mixture slope") + slope_bounds = interval_expression(slope) + if side == "middle": + require(not slope and set(tight) == set(support), "central uniqueness support") + else: + require(slope_bounds[1] < 0 if side == "left" else slope_bounds[0] > 0, + f"{side} strict slope sign") + entering = ((32, 0, 0, 1, 2, 1, 0) if side == "left" + else (48, 0, 2, 0, 0, 4, 0)) + segment_support = support + [entering] + affine, primal_det = primal_system(segment_support, bins, widths) + endpoints = (0, 1080) if side == "left" else (1080, 3240) + for x in endpoints: + check_primal(segment_support, [b + x * d for b, d in affine], x, bins, widths) + require(all(not slack(row, dual) for row in segment_support), + f"{side} affine complementary slackness") + affine_reports[side] = { + "domain": list(endpoints), "determinant": str(primal_det), + "patterns": [list(row) for row in segment_support], + "multiplicity_constant_and_x": [list(map(str, pair)) for pair in affine], + } + if side == "right": + at1090 = [b + 1090 * d for b, d in affine] + idle1090 = check_primal(segment_support, at1090, 1090, bins, widths) + require(idle1090 == {3: 22783, 5: 1625, 48: 138492}, "1090 idle consequence") + require(at1090[-1] == 5, "five entering cap48 patterns") + dual_reports[side] = { + "basis_determinant": str(dual_det), "tight_patterns": [list(row) for row in tight], + "strict_patterns": len(rows) - len(tight), + "minimum_slack_over_a_lower_bound": str(smallest[0]), + "minimizing_enclosure_pattern": list(smallest[2]), + "slope_expression": json_expression(slope), + "slope_over_a_interval": interval_json(slope_bounds), + } + # Coarse existence check only: do not refine or replay the published root digits. + bill = combine((1, profile), (-896 * 360, symbol(73))) + low_bill, high_bill = fixed_power_expression(bill, LOW), fixed_power_expression(bill, HIGH) + require(low_bill[1] < 0 < high_bill[0], "root inside dual-certified interval") + return { + "status": "PASS_STAGED_FOURTH_DUAL_BINOMIAL_AUDIT", + "source_sha256": pins, + "scope": "Fixed PR4091 pooled LP; source local-profile reports inherited; no owner/native/admission replay or new kappa.", + "enclosure": {"method": "positive binomial series; integer outward rounding; geometric tail", + "terms": TERMS, "scale": str(SCALE), "exponent_interval": [str(LOW), str(HIGH)]}, + "patterns": len(rows), "pattern_counts": dict(Counter(row[0] for row in rows)), + "pattern_sha256": hashlib.sha256(canonical(rows)).hexdigest(), + "source_widths": widths, "source_bins": bins, + "inherited_local_profiles": profiles, + "central_primal_determinant": str(determinant), "unique_mixture": str(mixture), + "central_multiplicities": list(map(str, values)), "idle": json_expression(idle), + "complete_paid_profile": json_expression(profile), + "dual": dual_reports, "affine_primal": affine_reports, + "x1090": {"idle": json_expression(idle1090), "new_cap48_pattern_count": "5", + "status": "right-face pooled optimum; central eight-pattern support alone is infeasible"}, + "coarse_root_endpoint_moments": [interval_json(low_bill), interval_json(high_bill)], + } + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--output", type=Path, help="Explicitly write a new evidence JSON") + args = parser.parse_args() + result = compute() + if args.output: + args.output.write_text(json.dumps(result, indent=2, sort_keys=True) + "\n") + else: + require(canonical(result) == canonical(json.loads((HERE / "RESULT.json").read_text())), + "saved evidence differs") + print(result["status"], "patterns=841 duals=3 tight=11/8/9 unique_x=1080") + + +if __name__ == "__main__": + main()