diff --git a/research/selected-k8-uniform-frame-audit/DUALS.json.gz b/research/selected-k8-uniform-frame-audit/DUALS.json.gz
new file mode 100644
index 0000000000..7d5186101b
Binary files /dev/null and b/research/selected-k8-uniform-frame-audit/DUALS.json.gz differ
diff --git a/research/selected-k8-uniform-frame-audit/NOTICE.md b/research/selected-k8-uniform-frame-audit/NOTICE.md
new file mode 100644
index 0000000000..284088ba95
--- /dev/null
+++ b/research/selected-k8-uniform-frame-audit/NOTICE.md
@@ -0,0 +1,30 @@
+# Attribution and license
+
+New uniform sign proof, equality-case argument, exact arithmetic and column
+audit: prepared for Ross Richardson with substantial OpenAI Codex assistance.
+No independent human or proof-assistant review is claimed. Apache-2.0.
+
+`DUALS.json.gz` is copied **byte for byte** from Gareth Davidson / bitplane's
+PR1671, head `ce130d291f5ab6dd801544886a16f62d42d86118`, path
+`research/selected-k8-frame-ceiling/DUALS.json.gz`. It is the only vendored
+predecessor file and is licensed under the repository's Apache-2.0 license.
+PR1671 disclosed substantial OpenAI Codex assistance. This audit does not
+claim authorship of the dual coefficients, LP construction or selected-word
+frame theorem at its two original exponents.
+
+The checker imports the pinned, unmodified
+`research/complex-x4-frame-bound/model.py`, by Aaron Wang / navinor with
+disclosed AI assistance. The event graph, cone extraction, domains and first
+LP assembly are inherited. The second column assembly shares that event
+model but reconstructs costs and dual inequalities directly from its edges.
+
+The selected word is read from the retained R480 source and bound through
+SLOT-PINS-k8. Its construction retains Jeremy Kothe, Rohan Arun, Hao Yan /
+FanPUYen, icekylinx, DreamingOfClouds, eumemic and the full selected lineage.
+The frame-method predecessors include chafreaky / PR557, ntedvs / PR776 and
+Rohan Guliani / PR815. The coverage-law and planning context credit Sagar
+Thakrar / PR1012 and Douglas Colkitt / PR1240. Arham Tahir / PR1605 and
+Aaron Wang's complementary climb-pair census retain their distinct work.
+
+Exact Git blobs, SHA256 hashes and predecessor paths are in SOURCES.json.
+No frozen source, selected record or predecessor file is changed.
diff --git a/research/selected-k8-uniform-frame-audit/PROOF.md b/research/selected-k8-uniform-frame-audit/PROOF.md
new file mode 100644
index 0000000000..7b7a9cd554
--- /dev/null
+++ b/research/selected-k8-uniform-frame-audit/PROOF.md
@@ -0,0 +1,206 @@
+# Uniform power-cost optimality and rigidity of the optimal paid profile
+
+This is a source-bound extension of Gareth Davidson / bitplane's
+[PR1671](https://github.com/CrocSwap/integer-mult-bounds/pull/1671), at
+`ce130d291f5ab6dd801544886a16f62d42d86118`. Its symbolic duals are retained
+unchanged. Its event/domain construction and the implication from an admissible
+physical frame assignment to an LP point remain inherited premises. The new
+result is a uniform sign proof and an equality-case consequence, not a new
+derivation of the physical interface.
+
+## Statement
+
+Fix the PR1671 R480 k8 word, scalar chronology and coefficients, register
+endpoints, A/B pins, centre cut, early-cleanup membership/order and low-end
+cone restrictions. Permit every frame in the complete monotone subspace
+intervals of its relaxed model. Each dimension-d climb pays one rank-d child;
+the eight rank-eight centre children are fixed. Let
+
+    P = {1:2412, 2:418, 3:432, 4:142, 5:82, 8:8}.
+
+For every real `0 <= a <= 1/32`, P minimizes
+
+    sum_r H_r r^(1-a)
+
+over this frame model, and attains the minimum of its local-polytope LP.
+For `0 < a <= 1/32`, **every optimizing assignment has exactly histogram P**.
+The same histogram statement holds for the expected child counts of every
+optimal fractional LP point. It does not say the frame assignment is unique.
+At a=0 every feasible point has the same rank mass, so histogram uniqueness
+is not asserted.
+
+Dividing the objective by any common positive width/normalization factor
+does not change the comparison. In particular this covers the physical
+power price `(r/73)^(1-a)` and the planning point `a=1/99`.
+
+## 1. Exact finite objects and the inherited relaxation
+
+The decompressed word is SHA256
+`c2b294300760e1fd6eeab8c22c4d13e4633dca40e52cac8da0d68163a76e3ca8`.
+It is bound to the selected word by SLOT-PINS-k8. The event graph has 5,413
+gate nodes, of which 1,741 have free frames, in 135 components. The domains
+have quotient dimensions 1, 2 or 3, with respectively 2, 5 or 16 subspaces.
+Distinctness, containment and the complete subspace counts are checked.
+The four graph/domain/cone hashes agree with PR1671.
+
+The inherited LP uses nonnegative gate distributions x and nested adjacent
+frame-pair distributions y. Gate distributions normalize to one and both
+edge marginals agree with x. Thus every literal feasible assignment is a
+zero/one LP point. Edges between fixed/forced nodes and the eight centre
+children are included separately.
+
+Every climb's dimension is the difference of its endpoint dimensions.
+Along each register these telescope, including in a fractional point because
+the edge marginals agree. The endpoint sum plus centres is always 5,586.
+This is checked independently from the stated histogram's rank mass.
+
+Put `C_d(a)=d^(1-a)-d`, for d=2,...,9, and C_0=C_1=0. Subtracting the
+fixed rank mass from the objective preserves all comparisons. These charges
+are PR1671's charges divided by the common positive factor `73^a`, so its
+symbolic rational dual coefficients apply unchanged.
+
+For each component, reconstruct `min c.z`, `Az=b`, `z>=0`. The retained dual
+q is a vector of rational linear forms in C_2,...,C_9. The checker establishes:
+
+1. All 17,507 rows and 23,004 columns are present.
+2. Every dual row is a row of this LP.
+3. `b^t q` equals the baseline's reduced histogram as an exact coefficient
+   identity, separately in every component.
+4. The reduced coefficient vector of every column is `v=c-A^t q`.
+5. Fixed plus variable baseline costs reconstruct every entry of P.
+
+A second column assembly starts directly from the event edges and domains.
+For gate columns it uses `unary - q_N + sum q_M`; for pair columns it uses
+`pair_cost - q_M0 - q_M1`. It independently accounts for edge multiplicity,
+nested pairs and ranks, then agrees with the first assembly on every column.
+Both assemblies share the pinned event/domain model. This is deliberately
+not called an independent physical-interface implementation.
+
+There are 239 distinct reduced vectors. Their multiplicities, exact rational
+coordinates, complete column-stream digest and sign proofs are in RESULT.json.
+
+## 2. Uniform reduced-cost signs
+
+For a reduced vector v define
+
+    R_v(a) = sum_(d=2)^9 v_d d (exp(-a log d)-1).
+
+The original reduced cost is the positive multiple `73^a R_v(a)`.
+
+There are three cases:
+
+| Columns | Distinct vectors | Proof |
+|---:|---:|---|
+| 16,564 | 1 | v=0, identically zero |
+| 10 | 1 | v=(-4,0,1,0,0,0,0,0), so R_v(a)=4(1-2^(-a))^2 |
+| 6,430 | 237 | Positive rational Bernstein bound for R_v(a)/a |
+
+The square is strictly positive for a>0. It needs its own argument: its
+derivative at zero vanishes, and interval cancellation at zero would not
+establish strict positivity on an interval beginning at zero.
+
+For the remaining vectors write l_d=log d and use the alternating series
+for exp(-a l_d). On the entire interval, `0 <= a l_d < 1`; this domain is
+checked with a rational upper bound on log 9. An odd truncation after k=9
+is a lower bound on the exponential, and the even truncation after k=8
+is an upper bound. For v_d>0 use the former, for v_d<0 the latter. After
+subtracting the constant term and dividing by a>0, this gives a polynomial
+lower bound of degree at most eight on R_v(a)/a.
+
+The logarithms have independently calculated rational enclosures. Write
+`d=2^k u`, `1<=u<2`, and use
+
+    log d = k log 2 + 2 atanh((u-1)/(u+1)),
+    log 2 = 2 atanh(1/3).
+
+After j terms, the remaining atanh series is bounded by
+
+    z^(2j+1) / ((2j+1)(1-z^2)).
+
+The code sums until that bound is less than 2^-144 and rounds the final
+log bounds outward to multiples of 2^-128. For each signed coefficient of
+the polynomial, use the lower or upper log-power endpoint according to
+its sign. Since a>=0, lowering every power-basis coefficient preserves the
+polynomial lower bound. No floating-point value is an acceptance input.
+
+Let the resulting polynomial be `p(a)=sum_(i=0)^8 c_i a^i` and A=1/32.
+Its Bernstein coefficients on [0,A] are exactly
+
+    b_j = sum_(i=0)^j c_i A^i binom(j,i)/binom(8,i).
+
+The Bernstein basis functions `binom(8,j)t^j(1-t)^(8-j)`, t=a/A, are
+nonnegative and sum to one. Therefore p(a)>=min_j b_j. All 237 vectors
+have strictly positive rational coefficients. The smallest checked bound,
+rounded down to a 2^-96 grid, is
+
+    1418585426042207139080866245 / 79228162514264337593543950336
+    > 0.0179.
+
+Consequently all 6,440 nonzero reduced-vector columns have strictly positive
+cost for `0<a<=1/32`. At a=0 every C_d vanishes. Weak duality plus the exact
+objective identities proves the stated uniform optimum.
+
+## 3. Why every optimal paid histogram is the same
+
+Fix any a in the positive interval. For a feasible LP point z, its objective
+gap from the baseline is the sum of z_j times the reduced cost of column j.
+Every summand is nonnegative, and every column whose **coefficient vector**
+is nonzero has strictly positive cost. Equality therefore forces z_j=0
+on every such column.
+
+On the remaining columns the residual coefficient vector is identically
+zero. Hence the vector equation, not merely its evaluation at this a, is
+
+    sum_j z_j c_j = b^t q.
+
+All expected rank-2 through rank-9 counts equal the baseline component
+counts. Restoring the fixed contributions gives P at those ranks. The
+invariant rank mass 5,586 then forces the rank-1 count to be 2,412.
+
+The conclusion does not require linear independence of the evaluated real
+numbers C_d(a), nor uniqueness of the dual or primal LP point. It follows
+from the strict signs and exact vector identities.
+
+As a positive boundary fixture, changing the frame of gate G616 from the
+zero subspace to span(148), leaving all other frames unchanged, satisfies
+the modeled nesting constraints and has exactly histogram P. The full
+graph price is recomputed. This is a second feasible **model assignment**;
+no separate native/physical admission of the alteration is claimed.
+
+## 4. Limits of the same certificate
+
+Two exact negative controls prevent overstatement:
+
+- For the nondecreasing concave price f(r)=min(r,2), the actual G4277 gate
+  column with vector `(-3,1,0,0,0,0,0,0)` has reduced cost -1. The published
+  dual therefore does not certify every concave price.
+- At a=1/20, an actual G1669/G1670 pair column with vector
+  `(0,8,1,-4,0,0,0,0)` has negative reduced cost. Rational 20th-root bounds
+  certify its interval in RESULT.json (approximately -0.004265).
+
+These refute extensions of this **particular dual certificate**, not the
+optimality of P outside [0,1/32]. No cheaper feasible assignment is supplied
+by a negative reduced cost alone. Neither control contradicts PR1671's
+two-exponent theorem. The uniform interval is certified, not claimed maximal.
+
+## 5. Relation to the full supplier
+
+The local invariant still leaves 1,646 ideal idle rank units per call under
+the inherited `72*(896/9)+64=7232` coverage law. PR1671/PR1240 already prove
+the fixed-word packing ceiling `a<0.001690054109089` and its conditional
+balanced kappa cap. This package does not improve that cap or repeat its
+complete moment arithmetic. Its added information is uniform local
+optimality and the impossibility of a different *equally optimal* rank shape
+in the positive interval.
+
+Scalar rewrites/reordering, changed endpoints, helper inventories, centre
+sharing, different coverage laws and changed physical billing remain outside
+scope. The source word, cone contract and finite-domain completeness proof
+are inherited; cold supplier replay, native execution, hosting, all-size
+compiler, common-label/mutable-source realization, precision/tape, analytic
+transfer, bit H1-H5, Lean and human review are not established here.
+
+New proof/checker: Ross Richardson with substantial OpenAI Codex assistance.
+Credit Gareth Davidson/bitplane for the unchanged duals and selected-word
+LP; Aaron Wang/navinor for the retained model and method; and the source
+lineage in NOTICE.md. Apache-2.0.
diff --git a/research/selected-k8-uniform-frame-audit/README.md b/research/selected-k8-uniform-frame-audit/README.md
new file mode 100644
index 0000000000..14e6aea164
--- /dev/null
+++ b/research/selected-k8-uniform-frame-audit/README.md
@@ -0,0 +1,126 @@
+# Selected k8 frames: uniform power-cost optimum and optimal-profile rigidity
+
+**Scoped audit and proof extension; no new kappa.** The selected k8 word's
+paid profile
+
+```text
+{1:2412, 2:418, 3:432, 4:142, 5:82, 8:8}
+```
+
+minimizes its frame-reassignment LP for **every `0 <= a <= 1/32`**, under
+the power price `r^(1-a)`. For **`0 < a <= 1/32`, every optimum has exactly
+this paid histogram**, even though its frames need not be unique. The range
+includes the `1/99` planning target.
+
+Gareth Davidson / bitplane's [PR1671](https://github.com/CrocSwap/integer-mult-bounds/pull/1671)
+already establishes the fixed-word packing ceiling by checking two exponents.
+This package audits its unchanged symbolic duals and proves their uniform
+validity and the equality-case result. It does not improve the existing ceiling.
+See [PROOF.md](PROOF.md) for the quantified argument.
+
+## Evidence
+
+The exact predecessor head is `ce130d291f5ab6dd801544886a16f62d42d86118`.
+The source-bound word, graph, cone caps and complete frame domains match it.
+Both column assemblies reconstruct **all 23,004 columns, 17,507 rows and
+135 component objectives**, including register-edge multiplicities and fixed
+centre children. The local rank mass remains 5,586.
+
+The 239 distinct rational reduced-cost vectors have these proofs:
+
+| Columns | Distinct vectors | Uniform sign proof |
+|---:|---:|---|
+| 16,564 | 1 | Identically zero |
+| 10 | 1 | Exact square `4(1-2^(-a))^2`, positive for a>0 |
+| 6,430 | 237 | Degree-eight Bernstein polynomials with rational positive coefficients |
+
+The polynomial proof uses independent logarithm bounds and alternating
+exponential series; no floating-point value, solver or sampled exponent
+establishes the interval claim. The smallest nonsquare slope bound exceeds
+0.0179. Strict positivity on all nonzero residual vectors forces every
+optimal LP point to use only identically-zero columns. The component objective
+identities then force the entire paid histogram, including rank one by mass
+conservation. At a=0 only optimality, not histogram uniqueness, is claimed.
+
+[RESULT.json](RESULT.json) contains every distinct vector and its multiplicity,
+its rational sign certificate, the complete column-stream digest and fixtures.
+Changing gate G616 from the zero frame to span(148) gives a distinct feasible
+model assignment with the same histogram. Separate native admission of that
+alteration is not claimed.
+
+Two exact boundaries prevent broader conclusions: a column of the same dual
+is negative for the concave price `min(r,2)`, and another is negative for the
+power exponent `a=1/20`. These invalidate extensions of **this dual**, not
+baseline optimality outside the certified range. Neither supplies a cheaper
+feasible assignment or contradicts PR1671.
+
+## Reproduce
+
+Python 3.12 and the standard library, from the repository root:
+
+```sh
+python3.12 -I -B scripts/research_package.py --package research/selected-k8-uniform-frame-audit
+```
+
+The registered replay checks source/provenance pins, runs the mathematical
+checker and eight test groups. The direct read-only mathematical replay is:
+
+```sh
+python3.12 -I -O -B research/selected-k8-uniform-frame-audit/verify.py
+```
+
+It prints `PASS_SELECTED_K8_UNIFORM_FRAME_AUDIT ... interval=0..1/32 optimal_profile_unique no_new_kappa`.
+Only an explicit `--write` regenerates RESULT.json. The tests include a separate
+integer-root arithmetic calibration at a=1/32, 1/64 and 1/128, exact Bernstein
+change-of-basis identities, rejected objective/column/domain mutations, source
+and receipt corruption, and optimized read-only relocation.
+
+## Scope, accounting and overlap
+
+The domain fixes the scalar word/order, coefficients, endpoints, centre cut,
+target pins and cleanup/cone contract. It uses PR1671's relaxed monotone
+frame-assignment model. Both column assemblies share Aaron Wang/navinor's
+pinned event/domain implementation; the second reconstructs column costs
+directly from the graph. This is an independent arithmetic audit, **not** an
+independent implementation or new proof of the physical interface.
+
+The original 1,646 idle rank units per call, 64-per-call centre charge,
+896/9 live families, width 73 and rank-51 idle cap remain. PR1671/PR1240's
+full packing bound is inherited rather than recomputed here. No physical
+decoder, new profile or kappa, selected cold replay, native execution, hosting,
+all-size compiler, common-label/mutable-source realization, precision/tape,
+analytic transfer, bit H1-H5, Lean or human review is established. Hosted CI
+status is separate from local validation.
+
+The revision-3 chooser selected `complex-rank-shape-decoder`, nonce
+`4071338634dbc7c5d72c8e5f2a5a4633`. [TASK.json](TASK.json) declares the **changed**
+scope from decoder synthesis to this audit/extension after fresh overlap found
+PR1671. PR1605 concerns abstract reblocking and overhead, and the retained X4
+package concerns an older word. The original physical-construction acceptance
+gate is not claimed satisfied. The claim is in
+[Discussion1659](https://github.com/CrocSwap/integer-mult-bounds/discussions/1659#discussioncomment-18916847).
+Exact source pins and overlap coverage are in TASK.json and SOURCES.json.
+
+## Open next questions
+
+- **A changed scalar dependency or gate order.** This could evade the fixed-word
+  obstruction. First name one explicit rewrite, prove its dirty-state and
+  endpoint contract, and screen its complete local plus idle profile. The old
+  event/domain certificate cannot certify the changed word.
+- **Optimality beyond a=1/32.** At one specified exponent, produce a new exact
+  dual or a feasible improving assignment. The present dual's negative column
+  is insufficient. This is lower priority for the current supplier, whose
+  full packing bill already fails at a much smaller exponent.
+
+The questions and blockers are also structured in TASK.json.
+
+## Credit
+
+Gareth Davidson / bitplane supplies PR1671's unchanged duals and selected-word
+frame theorem. Aaron Wang / navinor supplies the retained model and method.
+Credit the Jeremy Kothe, Rohan Arun, Hao Yan, icekylinx, DreamingOfClouds,
+eumemic and earlier frame/coverage lineage detailed in [NOTICE.md](NOTICE.md).
+
+Prepared for Ross Richardson with substantial OpenAI Codex assistance in the
+mathematics, implementation, testing and writing. No subagents or independent
+human review. Apache-2.0; predecessor files and selected evidence are unchanged.
diff --git a/research/selected-k8-uniform-frame-audit/RESULT.json b/research/selected-k8-uniform-frame-audit/RESULT.json
new file mode 100644
index 0000000000..7f1d84d195
--- /dev/null
+++ b/research/selected-k8-uniform-frame-audit/RESULT.json
@@ -0,0 +1,3692 @@
+{
+  "a_interval": [
+    "0",
+    "1/32"
+  ],
+  "baseline_profile": {
+    "1": 2412,
+    "2": 418,
+    "3": 432,
+    "4": 142,
+    "5": 82,
+    "8": 8
+  },
+  "boundaries": {
+    "a_one_twentieth": {
+      "a": "1/20",
+      "column": "[\"y\", [\"G\", 1669], [\"G\", 1670], [256, 128, 96, 16, 8, 6], [256, 128, 96, 16, 8, 6]]",
+      "component": 13,
+      "residual": [
+        "0",
+        "8",
+        "1",
+        "-4",
+        "0",
+        "0",
+        "0",
+        "0"
+      ],
+      "value_interval": [
+        "-84476677710376608913854145/19807040628566084398385987584",
+        "-337906710841506435655416567/79228162514264337593543950336"
+      ]
+    },
+    "all_concave": {
+      "column": "[\"x\", [\"G\", 4277], [298, 170, 97, 7]]",
+      "component": 0,
+      "price": [
+        0,
+        1,
+        2,
+        2,
+        2,
+        2,
+        2,
+        2,
+        2,
+        2
+      ],
+      "residual": [
+        "-3",
+        "1",
+        "0",
+        "0",
+        "0",
+        "0",
+        "0",
+        "0"
+      ],
+      "value": "-1"
+    },
+    "meaning": "The published dual fails outside the certified cone/range; neither fixture proves a better feasible frame assignment."
+  },
+  "column_stream_sha256": "20f7af2e0f14344e65db1ad225b70e08f3a48685a05da12461059f8f44c1bd4d",
+  "columns_by_proof": {
+    "4*(1-2^-a)^2": 10,
+    "degree-8-Bernstein": 6430,
+    "identically-zero": 16564
+  },
+  "distinct_frame_same_profile": {
+    "after": [
+      148
+    ],
+    "before": [],
+    "gate": [
+      "G",
+      616
+    ],
+    "profile": {
+      "1": 2412,
+      "2": 418,
+      "3": 432,
+      "4": 142,
+      "5": 82,
+      "8": 8
+    }
+  },
+  "distinct_residual_vectors": 239,
+  "duals_payload_sha256": "52eed9f637fb01f08ca8906535c8788c335e103478fb6cb9be1ec59e81a44ece",
+  "graph_sha256": {
+    "cones": "f844c0e7e667935050e02beb151b0cb9a5b45fc912ea436afc7158c425814661",
+    "domains": "a0592d32ef9cfbcc272ddc82a6fc4f6ac8b87e721ff9ac92a8c7ad15a65513be",
+    "edges": "a4ff296752a5697f574fb55fe99d3016be9d1d73873321ba9b2cd9bbfbe67edd",
+    "nodes": "a5dfe9d076d0a56f20c6eeb5141839a5d3fec0d0e2727d9012bb70d1259de219"
+  },
+  "local_mass": 5586,
+  "lp": {
+    "columns": 23004,
+    "components": 135,
+    "rows": 17507
+  },
+  "predecessor_head": "ce130d291f5ab6dd801544886a16f62d42d86118",
+  "residual_proofs": [
+    {
+      "columns": 15,
+      "proof": "degree-8-Bernstein",
+      "residual": [
+        "-13",
+        "8",
+        "-5",
+        "2",
+        "0",
+        "0",
+        "0",
+        "0"
+      ],
+      "slope_lower_bound": "65098609329215929840371803799/19807040628566084398385987584"
+    },
+    {
+      "columns": 3,
+      "proof": "degree-8-Bernstein",
+      "residual": [
+        "-11",
+        "7",
+        "-5",
+        "2",
+        "0",
+        "0",
+        "0",
+        "0"
+      ],
+      "slope_lower_bound": "301850426286328465259916981243/79228162514264337593543950336"
+    },
+    {
+      "columns": 3,
+      "proof": "degree-8-Bernstein",
+      "residual": [
+        "-10",
+        "4",
+        "-6",
+        "4",
+        "0",
+        "0",
+        "0",
+        "0"
+      ],
+      "slope_lower_bound": "34898075695996203971467021227/19807040628566084398385987584"
+    },
+    {
+      "columns": 15,
+      "proof": "degree-8-Bernstein",
+      "residual": [
+        "-9",
+        "-1",
+        "-3",
+        "4",
+        "0",
+        "0",
+        "0",
+        "0"
+      ],
+      "slope_lower_bound": "17371582825063705271168088375/79228162514264337593543950336"
+    },
+    {
+      "columns": 9,
+      "proof": "degree-8-Bernstein",
+      "residual": [
+        "-9",
+        "4",
+        "-6",
+        "4",
+        "0",
+        "0",
+        "0",
+        "0"
+      ],
+      "slope_lower_bound": "7439686962142467295896285663/19807040628566084398385987584"
+    },
+    {
+      "columns": 3,
+      "proof": "degree-8-Bernstein",
+      "residual": [
+        "-9",
+        "6",
+        "-5",
+        "2",
+        "0",
+        "0",
+        "0",
+        "0"
+      ],
+      "slope_lower_bound": "171653207627896605579173373645/39614081257132168796771975168"
+    },
+    {
+      "columns": 6,
+      "proof": "degree-8-Bernstein",
+      "residual": [
+        "-8",
+        "4",
+        "-4",
+        "2",
+        "0",
+        "0",
+        "0",
+        "0"
+      ],
+      "slope_lower_bound": "39548104782413469531615417141/9903520314283042199192993792"
+    },
+    {
+      "columns": 12,
+      "proof": "degree-8-Bernstein",
+      "residual": [
+        "-8",
+        "6",
+        "-5",
+        "2",
+        "0",
+        "0",
+        "0",
+        "0"
+      ],
+      "slope_lower_bound": "116736430160189132228031902517/39614081257132168796771975168"
+    },
+    {
+      "columns": 4,
+      "proof": "degree-8-Bernstein",
+      "residual": [
+        "-7",
+        "-4",
+        "4",
+        "0",
+        "0",
+        "0",
+        "0",
+        "0"
+      ],
+      "slope_lower_bound": "55990400942444036891436121931/79228162514264337593543950336"
+    },
+    {
+      "columns": 3,
+      "proof": "degree-8-Bernstein",
+      "residual": [
+        "-7",
+        "-2",
+        "-3",
+        "4",
+        "0",
+        "0",
+        "0",
+        "0"
+      ],
+      "slope_lower_bound": "29413785897264225584798927211/39614081257132168796771975168"
+    },
+    {
+      "columns": 6,
+      "proof": "degree-8-Bernstein",
+      "residual": [
+        "-7",
+        "-1",
+        "-4",
+        "4",
+        "0",
+        "0",
+        "0",
+        "0"
+      ],
+      "slope_lower_bound": "237038692695893598675733972887/79228162514264337593543950336"
+    },
+    {
+      "columns": 9,
+      "proof": "degree-8-Bernstein",
+      "residual": [
+        "-7",
+        "4",
+        "-4",
+        "2",
+        "0",
+        "0",
+        "0",
+        "0"
+      ],
+      "slope_lower_bound": "25818910415486601193830049359/9903520314283042199192993792"
+    },
+    {
+      "columns": 6,
+      "proof": "degree-8-Bernstein",
+      "residual": [
+        "-6",
+        "-3",
+        "-3",
+        "4",
+        "0",
+        "0",
+        "0",
+        "0"
+      ],
+      "slope_lower_bound": "210117115699408143770310562725/79228162514264337593543950336"
+    },
+    {
+      "columns": 12,
+      "proof": "degree-8-Bernstein",
+      "residual": [
+        "-6",
+        "0",
+        "-2",
+        "2",
+        "0",
+        "0",
+        "0",
+        "0"
+      ],
+      "slope_lower_bound": "65635421066584211610519129201/19807040628566084398385987584"
+    },
+    {
+      "columns": 9,
+      "proof": "degree-8-Bernstein",
+      "residual": [
+        "-5",
+        "-3",
+        "-3",
+        "4",
+        "0",
+        "0",
+        "0",
+        "0"
+      ],
+      "slope_lower_bound": "100283560763993197068027620469/79228162514264337593543950336"
+    },
+    {
+      "columns": 2,
+      "proof": "degree-8-Bernstein",
+      "residual": [
+        "-5",
+        "-3",
+        "3",
+        "0",
+        "0",
+        "0",
+        "0",
+        "0"
+      ],
+      "slope_lower_bound": "3633602993244822748251588971/19807040628566084398385987584"
+    },
+    {
+      "columns": 7,
+      "proof": "degree-8-Bernstein",
+      "residual": [
+        "-5",
+        "0",
+        "-2",
+        "2",
+        "0",
+        "0",
+        "0",
+        "0"
+      ],
+      "slope_lower_bound": "38177032332730474934948393637/19807040628566084398385987584"
+    },
+    {
+      "columns": 3,
+      "proof": "degree-8-Bernstein",
+      "residual": [
+        "-5",
+        "0",
+        "1",
+        "0",
+        "0",
+        "0",
+        "0",
+        "0"
+      ],
+      "slope_lower_bound": "6864597183463434168892683891/4951760157141521099596496896"
+    },
+    {
+      "columns": 12,
+      "proof": "degree-8-Bernstein",
+      "residual": [
+        "-5",
+        "7",
+        "-3",
+        "0",
+        "0",
+        "0",
+        "0",
+        "0"
+      ],
+      "slope_lower_bound": "36283243909369240748925605737/79228162514264337593543950336"
+    },
+    {
+      "columns": 6,
+      "proof": "degree-8-Bernstein",
+      "residual": [
+        "-4",
+        "-1",
+        "-2",
+        "2",
+        "0",
+        "0",
+        "0",
+        "0"
+      ],
+      "slope_lower_bound": "303997673235801592340506282851/79228162514264337593543950336"
+    },
+    {
+      "columns": 9,
+      "proof": "degree-8-Bernstein",
+      "residual": [
+        "-4",
+        "-1",
+        "0",
+        "1",
+        "0",
+        "0",
+        "0",
+        "0"
+      ],
+      "slope_lower_bound": "62893276167218222417185082193/79228162514264337593543950336"
+    },
+    {
+      "columns": 15,
+      "proof": "degree-8-Bernstein",
+      "residual": [
+        "-4",
+        "0",
+        "-2",
+        "2",
+        "0",
+        "0",
+        "0",
+        "0"
+      ],
+      "slope_lower_bound": "10718643598876738259377658073/19807040628566084398385987584"
+    },
+    {
+      "columns": 10,
+      "proof": "4*(1-2^-a)^2",
+      "residual": [
+        "-4",
+        "0",
+        "1",
+        "0",
+        "0",
+        "0",
+        "0",
+        "0"
+      ]
+    },
+    {
+      "columns": 9,
+      "proof": "degree-8-Bernstein",
+      "residual": [
+        "-4",
+        "1",
+        "0",
+        "0",
+        "0",
+        "0",
+        "0",
+        "0"
+      ],
+      "slope_lower_bound": "177918647513440393382617084423/79228162514264337593543950336"
+    },
+    {
+      "columns": 3,
+      "proof": "degree-8-Bernstein",
+      "residual": [
+        "-4",
+        "5",
+        "-2",
+        "0",
+        "0",
+        "0",
+        "0",
+        "0"
+      ],
+      "slope_lower_bound": "11060009494245872131476650079/79228162514264337593543950336"
+    },
+    {
+      "columns": 3,
+      "proof": "degree-8-Bernstein",
+      "residual": [
+        "-4",
+        "6",
+        "-3",
+        "0",
+        "0",
+        "0",
+        "0",
+        "0"
+      ],
+      "slope_lower_bound": "184322256670090735095366039803/79228162514264337593543950336"
+    },
+    {
+      "columns": 12,
+      "proof": "degree-8-Bernstein",
+      "residual": [
+        "-4",
+        "6",
+        "0",
+        "-2",
+        "0",
+        "0",
+        "0",
+        "0"
+      ],
+      "slope_lower_bound": "138053557259725638599043727173/79228162514264337593543950336"
+    },
+    {
+      "columns": 9,
+      "proof": "degree-8-Bernstein",
+      "residual": [
+        "-3",
+        "-1",
+        "-2",
+        "2",
+        "0",
+        "0",
+        "0",
+        "0"
+      ],
+      "slope_lower_bound": "194164118300386645638223340595/79228162514264337593543950336"
+    },
+    {
+      "columns": 3,
+      "proof": "degree-8-Bernstein",
+      "residual": [
+        "-3",
+        "0",
+        "-1",
+        "1",
+        "0",
+        "0",
+        "0",
+        "0"
+      ],
+      "slope_lower_bound": "65635421066584211610519129201/39614081257132168796771975168"
+    },
+    {
+      "columns": 3,
+      "proof": "degree-8-Bernstein",
+      "residual": [
+        "-3",
+        "1",
+        "-3",
+        "2",
+        "0",
+        "0",
+        "0",
+        "0"
+      ],
+      "slope_lower_bound": "111252140361457153841363808501/79228162514264337593543950336"
+    },
+    {
+      "columns": 6,
+      "proof": "degree-8-Bernstein",
+      "residual": [
+        "-3",
+        "1",
+        "-2",
+        "1",
+        "0",
+        "0",
+        "0",
+        "0"
+      ],
+      "slope_lower_bound": "307377350474545733727027139369/79228162514264337593543950336"
+    },
+    {
+      "columns": 83,
+      "proof": "degree-8-Bernstein",
+      "residual": [
+        "-3",
+        "1",
+        "0",
+        "0",
+        "0",
+        "0",
+        "0",
+        "0"
+      ],
+      "slope_lower_bound": "68377565965950200803853176209/79228162514264337593543950336"
+    },
+    {
+      "columns": 1,
+      "proof": "degree-8-Bernstein",
+      "residual": [
+        "-3",
+        "1",
+        "1",
+        "-1",
+        "0",
+        "0",
+        "0",
+        "0"
+      ],
+      "slope_lower_bound": "8159645345755646692122107243/2475880078570760549798248448"
+    },
+    {
+      "columns": 6,
+      "proof": "degree-8-Bernstein",
+      "residual": [
+        "-3",
+        "2",
+        "-1",
+        "0",
+        "0",
+        "0",
+        "0",
+        "0"
+      ],
+      "slope_lower_bound": "242528341264564627103487301317/79228162514264337593543950336"
+    },
+    {
+      "columns": 3,
+      "proof": "degree-8-Bernstein",
+      "residual": [
+        "-3",
+        "5",
+        "-3",
+        "0",
+        "0",
+        "0",
+        "0",
+        "0"
+      ],
+      "slope_lower_bound": "332361269430812229441806473869/79228162514264337593543950336"
+    },
+    {
+      "columns": 2,
+      "proof": "degree-8-Bernstein",
+      "residual": [
+        "-3",
+        "6",
+        "-3",
+        "0",
+        "0",
+        "0",
+        "0",
+        "0"
+      ],
+      "slope_lower_bound": "75669703245370105852346866973/79228162514264337593543950336"
+    },
+    {
+      "columns": 2,
+      "proof": "degree-8-Bernstein",
+      "residual": [
+        "-3",
+        "6",
+        "0",
+        "-2",
+        "0",
+        "0",
+        "0",
+        "0"
+      ],
+      "slope_lower_bound": "29401003835005009356024554343/79228162514264337593543950336"
+    },
+    {
+      "columns": 3,
+      "proof": "degree-8-Bernstein",
+      "residual": [
+        "-3",
+        "14",
+        "-5",
+        "-2",
+        "0",
+        "0",
+        "0",
+        "0"
+      ],
+      "slope_lower_bound": "31409385289475738351773170569/19807040628566084398385987584"
+    },
+    {
+      "columns": 9,
+      "proof": "degree-8-Bernstein",
+      "residual": [
+        "-3",
+        "14",
+        "-2",
+        "-4",
+        "0",
+        "0",
+        "0",
+        "0"
+      ],
+      "slope_lower_bound": "39684420873768928455385184823/39614081257132168796771975168"
+    },
+    {
+      "columns": 3,
+      "proof": "degree-8-Bernstein",
+      "residual": [
+        "-2",
+        "-9",
+        "1",
+        "3",
+        "0",
+        "0",
+        "0",
+        "0"
+      ],
+      "slope_lower_bound": "217748652447613249237567958349/79228162514264337593543950336"
+    },
+    {
+      "columns": 3,
+      "proof": "degree-8-Bernstein",
+      "residual": [
+        "-2",
+        "-6",
+        "1",
+        "2",
+        "0",
+        "0",
+        "0",
+        "0"
+      ],
+      "slope_lower_bound": "35971699170732767511761672031/39614081257132168796771975168"
+    },
+    {
+      "columns": 1,
+      "proof": "degree-8-Bernstein",
+      "residual": [
+        "-2",
+        "-6",
+        "4",
+        "0",
+        "0",
+        "0",
+        "0",
+        "0"
+      ],
+      "slope_lower_bound": "29068823945958581986012711769/79228162514264337593543950336"
+    },
+    {
+      "columns": 6,
+      "proof": "degree-8-Bernstein",
+      "residual": [
+        "-2",
+        "-1",
+        "-2",
+        "2",
+        "0",
+        "0",
+        "0",
+        "0"
+      ],
+      "slope_lower_bound": "84330563364971698935940398339/79228162514264337593543950336"
+    },
+    {
+      "columns": 48,
+      "proof": "degree-8-Bernstein",
+      "residual": [
+        "-2",
+        "-1",
+        "1",
+        "0",
+        "0",
+        "0",
+        "0",
+        "0"
+      ],
+      "slope_lower_bound": "20727994484732372949214883023/39614081257132168796771975168"
+    },
+    {
+      "columns": 20,
+      "proof": "degree-8-Bernstein",
+      "residual": [
+        "-2",
+        "0",
+        "-1",
+        "1",
+        "0",
+        "0",
+        "0",
+        "0"
+      ],
+      "slope_lower_bound": "10718643598876738259377658073/39614081257132168796771975168"
+    },
+    {
+      "columns": 220,
+      "proof": "degree-8-Bernstein",
+      "residual": [
+        "-2",
+        "0",
+        "0",
+        "0",
+        "0",
+        "0",
+        "0",
+        "0"
+      ],
+      "slope_lower_bound": "217305106849441258486038345659/79228162514264337593543950336"
+    },
+    {
+      "columns": 1,
+      "proof": "degree-8-Bernstein",
+      "residual": [
+        "-2",
+        "1",
+        "-3",
+        "2",
+        "0",
+        "0",
+        "0",
+        "0"
+      ],
+      "slope_lower_bound": "1418585426042207139080866245/79228162514264337593543950336"
+    },
+    {
+      "columns": 18,
+      "proof": "degree-8-Bernstein",
+      "residual": [
+        "-2",
+        "1",
+        "-2",
+        "1",
+        "0",
+        "0",
+        "0",
+        "0"
+      ],
+      "slope_lower_bound": "49681199262456276121001991635/19807040628566084398385987584"
+    },
+    {
+      "columns": 18,
+      "proof": "degree-8-Bernstein",
+      "residual": [
+        "-2",
+        "2",
+        "-1",
+        "0",
+        "0",
+        "0",
+        "0",
+        "0"
+      ],
+      "slope_lower_bound": "133875787839843997860468128487/79228162514264337593543950336"
+    },
+    {
+      "columns": 6,
+      "proof": "degree-8-Bernstein",
+      "residual": [
+        "-2",
+        "3",
+        "-2",
+        "0",
+        "0",
+        "0",
+        "0",
+        "0"
+      ],
+      "slope_lower_bound": "307138035015688860824357518211/79228162514264337593543950336"
+    },
+    {
+      "columns": 3,
+      "proof": "degree-8-Bernstein",
+      "residual": [
+        "-2",
+        "4",
+        "-2",
+        "0",
+        "0",
+        "0",
+        "0",
+        "0"
+      ],
+      "slope_lower_bound": "50446468830246737234897911315/79228162514264337593543950336"
+    },
+    {
+      "columns": 1,
+      "proof": "degree-8-Bernstein",
+      "residual": [
+        "-2",
+        "5",
+        "-3",
+        "0",
+        "0",
+        "0",
+        "0",
+        "0"
+      ],
+      "slope_lower_bound": "223708716006091600198787301039/79228162514264337593543950336"
+    },
+    {
+      "columns": 4,
+      "proof": "degree-8-Bernstein",
+      "residual": [
+        "-2",
+        "5",
+        "0",
+        "-2",
+        "0",
+        "0",
+        "0",
+        "0"
+      ],
+      "slope_lower_bound": "177440016595726503702464988409/79228162514264337593543950336"
+    },
+    {
+      "columns": 2,
+      "proof": "degree-8-Bernstein",
+      "residual": [
+        "-2",
+        "15",
+        "-3",
+        "-4",
+        "0",
+        "0",
+        "0",
+        "0"
+      ],
+      "slope_lower_bound": "35994633874665522657910146635/19807040628566084398385987584"
+    },
+    {
+      "columns": 2,
+      "proof": "degree-8-Bernstein",
+      "residual": [
+        "-1",
+        "-9",
+        "1",
+        "3",
+        "0",
+        "0",
+        "0",
+        "0"
+      ],
+      "slope_lower_bound": "107915097512198302535285016093/79228162514264337593543950336"
+    },
+    {
+      "columns": 3,
+      "proof": "degree-8-Bernstein",
+      "residual": [
+        "-1",
+        "-7",
+        "-2",
+        "4",
+        "0",
+        "0",
+        "0",
+        "0"
+      ],
+      "slope_lower_bound": "266107516641852180661746684657/79228162514264337593543950336"
+    },
+    {
+      "columns": 6,
+      "proof": "degree-8-Bernstein",
+      "residual": [
+        "-1",
+        "-7",
+        "1",
+        "2",
+        "0",
+        "0",
+        "0",
+        "0"
+      ],
+      "slope_lower_bound": "223232942246345227624236052365/79228162514264337593543950336"
+    },
+    {
+      "columns": 3,
+      "proof": "degree-8-Bernstein",
+      "residual": [
+        "-1",
+        "-5",
+        "-3",
+        "4",
+        "0",
+        "0",
+        "0",
+        "0"
+      ],
+      "slope_lower_bound": "183195538702922688864887152563/79228162514264337593543950336"
+    },
+    {
+      "columns": 4,
+      "proof": "degree-8-Bernstein",
+      "residual": [
+        "-1",
+        "-4",
+        "-2",
+        "2",
+        "0",
+        "0",
+        "0",
+        "0"
+      ],
+      "slope_lower_bound": "187933426053891771028459810275/19807040628566084398385987584"
+    },
+    {
+      "columns": 12,
+      "proof": "degree-8-Bernstein",
+      "residual": [
+        "-1",
+        "-1",
+        "-1",
+        "1",
+        "0",
+        "0",
+        "0",
+        "0"
+      ],
+      "slope_lower_bound": "172726831102633169119468024449/79228162514264337593543950336"
+    },
+    {
+      "columns": 6,
+      "proof": "degree-8-Bernstein",
+      "residual": [
+        "-1",
+        "-1",
+        "0",
+        "0",
+        "0",
+        "0",
+        "0",
+        "0"
+      ],
+      "slope_lower_bound": "182672059805081375721842037159/39614081257132168796771975168"
+    },
+    {
+      "columns": 2497,
+      "proof": "degree-8-Bernstein",
+      "residual": [
+        "-1",
+        "0",
+        "0",
+        "0",
+        "0",
+        "0",
+        "0",
+        "0"
+      ],
+      "slope_lower_bound": "108652553424720629243019172829/79228162514264337593543950336"
+    },
+    {
+      "columns": 3,
+      "proof": "degree-8-Bernstein",
+      "residual": [
+        "-1",
+        "0",
+        "1",
+        "-1",
+        "0",
+        "0",
+        "0",
+        "0"
+      ],
+      "slope_lower_bound": "75123777600045389812832173253/19807040628566084398385987584"
+    },
+    {
+      "columns": 6,
+      "proof": "degree-8-Bernstein",
+      "residual": [
+        "-1",
+        "0",
+        "2",
+        "-2",
+        "0",
+        "0",
+        "0",
+        "0"
+      ],
+      "slope_lower_bound": "492337667375642489259638213195/79228162514264337593543950336"
+    },
+    {
+      "columns": 8,
+      "proof": "degree-8-Bernstein",
+      "residual": [
+        "-1",
+        "1",
+        "-2",
+        "1",
+        "0",
+        "0",
+        "0",
+        "0"
+      ],
+      "slope_lower_bound": "89814853163703677322608492355/79228162514264337593543950336"
+    },
+    {
+      "columns": 36,
+      "proof": "degree-8-Bernstein",
+      "residual": [
+        "-1",
+        "1",
+        "-1",
+        "0",
+        "0",
+        "0",
+        "0",
+        "0"
+      ],
+      "slope_lower_bound": "281914800600565492206908562553/79228162514264337593543950336"
+    },
+    {
+      "columns": 3,
+      "proof": "degree-8-Bernstein",
+      "residual": [
+        "-1",
+        "1",
+        "0",
+        "-1",
+        "0",
+        "0",
+        "0",
+        "0"
+      ],
+      "slope_lower_bound": "473757357576026437235421904547/79228162514264337593543950336"
+    },
+    {
+      "columns": 13,
+      "proof": "degree-8-Bernstein",
+      "residual": [
+        "-1",
+        "1",
+        "1",
+        "-1",
+        "0",
+        "0",
+        "0",
+        "0"
+      ],
+      "slope_lower_bound": "10950886053684858915467271529/19807040628566084398385987584"
+    },
+    {
+      "columns": 3,
+      "proof": "degree-8-Bernstein",
+      "residual": [
+        "-1",
+        "1",
+        "2",
+        "-2",
+        "0",
+        "0",
+        "0",
+        "0"
+      ],
+      "slope_lower_bound": "235646101190200365670178606299/79228162514264337593543950336"
+    },
+    {
+      "columns": 2,
+      "proof": "degree-8-Bernstein",
+      "residual": [
+        "-1",
+        "2",
+        "-3",
+        "1",
+        "0",
+        "0",
+        "0",
+        "0"
+      ],
+      "slope_lower_bound": "131667245400474669102439091717/39614081257132168796771975168"
+    },
+    {
+      "columns": 9,
+      "proof": "degree-8-Bernstein",
+      "residual": [
+        "-1",
+        "2",
+        "-2",
+        "0",
+        "0",
+        "0",
+        "0",
+        "0"
+      ],
+      "slope_lower_bound": "113794261944102588792699488069/19807040628566084398385987584"
+    },
+    {
+      "columns": 83,
+      "proof": "degree-8-Bernstein",
+      "residual": [
+        "-1",
+        "2",
+        "-1",
+        "0",
+        "0",
+        "0",
+        "0",
+        "0"
+      ],
+      "slope_lower_bound": "25223234415123368617448955657/79228162514264337593543950336"
+    },
+    {
+      "columns": 5,
+      "proof": "degree-8-Bernstein",
+      "residual": [
+        "-1",
+        "3",
+        "-2",
+        "0",
+        "0",
+        "0",
+        "0",
+        "0"
+      ],
+      "slope_lower_bound": "198485481590968231581338345381/79228162514264337593543950336"
+    },
+    {
+      "columns": 9,
+      "proof": "degree-8-Bernstein",
+      "residual": [
+        "-1",
+        "4",
+        "0",
+        "-2",
+        "0",
+        "0",
+        "0",
+        "0"
+      ],
+      "slope_lower_bound": "325479029356447998048905422475/79228162514264337593543950336"
+    },
+    {
+      "columns": 1,
+      "proof": "degree-8-Bernstein",
+      "residual": [
+        "-1",
+        "7",
+        "-4",
+        "0",
+        "0",
+        "0",
+        "0",
+        "0"
+      ],
+      "slope_lower_bound": "15813421785886855165098955519/39614081257132168796771975168"
+    },
+    {
+      "columns": 1,
+      "proof": "degree-8-Bernstein",
+      "residual": [
+        "-1",
+        "13",
+        "-5",
+        "-2",
+        "0",
+        "0",
+        "0",
+        "0"
+      ],
+      "slope_lower_bound": "20628000061737977313814242939/9903520314283042199192993792"
+    },
+    {
+      "columns": 2,
+      "proof": "degree-8-Bernstein",
+      "residual": [
+        "-1",
+        "13",
+        "-2",
+        "-4",
+        "0",
+        "0",
+        "0",
+        "0"
+      ],
+      "slope_lower_bound": "59377650541769361007095815441/39614081257132168796771975168"
+    },
+    {
+      "columns": 8,
+      "proof": "degree-8-Bernstein",
+      "residual": [
+        "-1",
+        "15",
+        "-3",
+        "-4",
+        "0",
+        "0",
+        "0",
+        "0"
+      ],
+      "slope_lower_bound": "17662991036970730694310706855/39614081257132168796771975168"
+    },
+    {
+      "columns": 12,
+      "proof": "degree-8-Bernstein",
+      "residual": [
+        "0",
+        "-7",
+        "-1",
+        "3",
+        "0",
+        "0",
+        "0",
+        "0"
+      ],
+      "slope_lower_bound": "354503784379513650845274310767/79228162514264337593543950336"
+    },
+    {
+      "columns": 1,
+      "proof": "degree-8-Bernstein",
+      "residual": [
+        "0",
+        "-7",
+        "1",
+        "2",
+        "0",
+        "0",
+        "0",
+        "0"
+      ],
+      "slope_lower_bound": "113399387310930280921953110109/79228162514264337593543950336"
+    },
+    {
+      "columns": 6,
+      "proof": "degree-8-Bernstein",
+      "residual": [
+        "0",
+        "-6",
+        "3",
+        "0",
+        "0",
+        "0",
+        "0",
+        "0"
+      ],
+      "slope_lower_bound": "248735933816788475390578596281/79228162514264337593543950336"
+    },
+    {
+      "columns": 3,
+      "proof": "degree-8-Bernstein",
+      "residual": [
+        "0",
+        "-2",
+        "0",
+        "0",
+        "0",
+        "0",
+        "0",
+        "0"
+      ],
+      "slope_lower_bound": "513383132370884244401329802977/79228162514264337593543950336"
+    },
+    {
+      "columns": 24,
+      "proof": "degree-8-Bernstein",
+      "residual": [
+        "0",
+        "-2",
+        "1",
+        "0",
+        "0",
+        "0",
+        "0",
+        "0"
+      ],
+      "slope_lower_bound": "82911977938929491796859532093/79228162514264337593543950336"
+    },
+    {
+      "columns": 6,
+      "proof": "degree-8-Bernstein",
+      "residual": [
+        "0",
+        "-1",
+        "-1",
+        "1",
+        "0",
+        "0",
+        "0",
+        "0"
+      ],
+      "slope_lower_bound": "62893276167218222417185082193/79228162514264337593543950336"
+    },
+    {
+      "columns": 110,
+      "proof": "degree-8-Bernstein",
+      "residual": [
+        "0",
+        "-1",
+        "0",
+        "0",
+        "0",
+        "0",
+        "0",
+        "0"
+      ],
+      "slope_lower_bound": "16043222886590132637541556343/4951760157141521099596496896"
+    },
+    {
+      "columns": 16564,
+      "proof": "identically-zero",
+      "residual": [
+        "0",
+        "0",
+        "0",
+        "0",
+        "0",
+        "0",
+        "0",
+        "0"
+      ]
+    },
+    {
+      "columns": 46,
+      "proof": "degree-8-Bernstein",
+      "residual": [
+        "0",
+        "0",
+        "1",
+        "-1",
+        "0",
+        "0",
+        "0",
+        "0"
+      ],
+      "slope_lower_bound": "95921278487730465004154760091/39614081257132168796771975168"
+    },
+    {
+      "columns": 12,
+      "proof": "degree-8-Bernstein",
+      "residual": [
+        "0",
+        "0",
+        "2",
+        "-2",
+        "0",
+        "0",
+        "0",
+        "0"
+      ],
+      "slope_lower_bound": "383685113950921860016619040365/79228162514264337593543950336"
+    },
+    {
+      "columns": 121,
+      "proof": "degree-8-Bernstein",
+      "residual": [
+        "0",
+        "1",
+        "-1",
+        "0",
+        "0",
+        "0",
+        "0",
+        "0"
+      ],
+      "slope_lower_bound": "173262247175844862963889389723/79228162514264337593543950336"
+    },
+    {
+      "columns": 10,
+      "proof": "degree-8-Bernstein",
+      "residual": [
+        "0",
+        "1",
+        "0",
+        "-1",
+        "0",
+        "0",
+        "0",
+        "0"
+      ],
+      "slope_lower_bound": "182552402075652903996201365859/39614081257132168796771975168"
+    },
+    {
+      "columns": 10,
+      "proof": "degree-8-Bernstein",
+      "residual": [
+        "0",
+        "1",
+        "2",
+        "-2",
+        "0",
+        "0",
+        "0",
+        "0"
+      ],
+      "slope_lower_bound": "126993547765479736427159433469/79228162514264337593543950336"
+    },
+    {
+      "columns": 17,
+      "proof": "degree-8-Bernstein",
+      "residual": [
+        "0",
+        "2",
+        "-2",
+        "0",
+        "0",
+        "0",
+        "0",
+        "0"
+      ],
+      "slope_lower_bound": "346524494351689725927778779447/79228162514264337593543950336"
+    },
+    {
+      "columns": 6,
+      "proof": "degree-8-Bernstein",
+      "residual": [
+        "0",
+        "2",
+        "1",
+        "-2",
+        "0",
+        "0",
+        "0",
+        "0"
+      ],
+      "slope_lower_bound": "300255794941324614411252645005/79228162514264337593543950336"
+    },
+    {
+      "columns": 55,
+      "proof": "degree-8-Bernstein",
+      "residual": [
+        "0",
+        "3",
+        "-2",
+        "0",
+        "0",
+        "0",
+        "0",
+        "0"
+      ],
+      "slope_lower_bound": "89832928166247602338319172551/79228162514264337593543950336"
+    },
+    {
+      "columns": 3,
+      "proof": "degree-8-Bernstein",
+      "residual": [
+        "0",
+        "3",
+        "0",
+        "-2",
+        "0",
+        "0",
+        "0",
+        "0"
+      ],
+      "slope_lower_bound": "473518042117169492395345856541/79228162514264337593543950336"
+    },
+    {
+      "columns": 3,
+      "proof": "degree-8-Bernstein",
+      "residual": [
+        "0",
+        "4",
+        "0",
+        "-2",
+        "0",
+        "0",
+        "0",
+        "0"
+      ],
+      "slope_lower_bound": "216826475931727368805886249645/79228162514264337593543950336"
+    },
+    {
+      "columns": 1,
+      "proof": "degree-8-Bernstein",
+      "residual": [
+        "0",
+        "5",
+        "-3",
+        "0",
+        "0",
+        "0",
+        "0",
+        "0"
+      ],
+      "slope_lower_bound": "1600902289162585428187238845/19807040628566084398385987584"
+    },
+    {
+      "columns": 1,
+      "proof": "degree-8-Bernstein",
+      "residual": [
+        "0",
+        "8",
+        "1",
+        "-4",
+        "0",
+        "0",
+        "0",
+        "0"
+      ],
+      "slope_lower_bound": "924784625541934009554920215/19807040628566084398385987584"
+    },
+    {
+      "columns": 1,
+      "proof": "degree-8-Bernstein",
+      "residual": [
+        "0",
+        "11",
+        "-1",
+        "-4",
+        "0",
+        "0",
+        "0",
+        "0"
+      ],
+      "slope_lower_bound": "11691508333551919174592834403/9903520314283042199192993792"
+    },
+    {
+      "columns": 1,
+      "proof": "degree-8-Bernstein",
+      "residual": [
+        "0",
+        "13",
+        "-5",
+        "-2",
+        "0",
+        "0",
+        "0",
+        "0"
+      ],
+      "slope_lower_bound": "28185723534591594633747385341/39614081257132168796771975168"
+    },
+    {
+      "columns": 7,
+      "proof": "degree-8-Bernstein",
+      "residual": [
+        "0",
+        "13",
+        "-2",
+        "-4",
+        "0",
+        "0",
+        "0",
+        "0"
+      ],
+      "slope_lower_bound": "2525686914704523192793114513/19807040628566084398385987584"
+    },
+    {
+      "columns": 8,
+      "proof": "degree-8-Bernstein",
+      "residual": [
+        "0",
+        "14",
+        "-3",
+        "-4",
+        "0",
+        "0",
+        "0",
+        "0"
+      ],
+      "slope_lower_bound": "5730156088583217366720682743/2475880078570760549798248448"
+    },
+    {
+      "columns": 9,
+      "proof": "degree-8-Bernstein",
+      "residual": [
+        "1",
+        "-13",
+        "1",
+        "4",
+        "0",
+        "0",
+        "0",
+        "0"
+      ],
+      "slope_lower_bound": "295176340587810762647759396427/79228162514264337593543950336"
+    },
+    {
+      "columns": 5,
+      "proof": "degree-8-Bernstein",
+      "residual": [
+        "1",
+        "-12",
+        "1",
+        "4",
+        "0",
+        "0",
+        "0",
+        "0"
+      ],
+      "slope_lower_bound": "8513310436879030836190936467/19807040628566084398385987584"
+    },
+    {
+      "columns": 3,
+      "proof": "degree-8-Bernstein",
+      "residual": [
+        "1",
+        "-8",
+        "1",
+        "2",
+        "0",
+        "0",
+        "0",
+        "0"
+      ],
+      "slope_lower_bound": "66172232803952493380666454603/19807040628566084398385987584"
+    },
+    {
+      "columns": 4,
+      "proof": "degree-8-Bernstein",
+      "residual": [
+        "1",
+        "-7",
+        "-2",
+        "4",
+        "0",
+        "0",
+        "0",
+        "0"
+      ],
+      "slope_lower_bound": "46440406771022287257180800145/79228162514264337593543950336"
+    },
+    {
+      "columns": 5,
+      "proof": "degree-8-Bernstein",
+      "residual": [
+        "1",
+        "-7",
+        "-1",
+        "3",
+        "0",
+        "0",
+        "0",
+        "0"
+      ],
+      "slope_lower_bound": "244670229444098704142991368511/79228162514264337593543950336"
+    },
+    {
+      "columns": 6,
+      "proof": "degree-8-Bernstein",
+      "residual": [
+        "1",
+        "-5",
+        "2",
+        "0",
+        "0",
+        "0",
+        "0",
+        "0"
+      ],
+      "slope_lower_bound": "157448825389957989299265764979/39614081257132168796771975168"
+    },
+    {
+      "columns": 2,
+      "proof": "degree-8-Bernstein",
+      "residual": [
+        "1",
+        "-3",
+        "-2",
+        "2",
+        "0",
+        "0",
+        "0",
+        "0"
+      ],
+      "slope_lower_bound": "277076096239316137435082872689/79228162514264337593543950336"
+    },
+    {
+      "columns": 9,
+      "proof": "degree-8-Bernstein",
+      "residual": [
+        "1",
+        "-3",
+        "1",
+        "0",
+        "0",
+        "0",
+        "0",
+        "0"
+      ],
+      "slope_lower_bound": "231468331770318735770754545411/79228162514264337593543950336"
+    },
+    {
+      "columns": 21,
+      "proof": "degree-8-Bernstein",
+      "residual": [
+        "1",
+        "-2",
+        "0",
+        "0",
+        "0",
+        "0",
+        "0",
+        "0"
+      ],
+      "slope_lower_bound": "404730578946163615143642462353/79228162514264337593543950336"
+    },
+    {
+      "columns": 9,
+      "proof": "degree-8-Bernstein",
+      "residual": [
+        "1",
+        "-2",
+        "2",
+        "-1",
+        "0",
+        "0",
+        "0",
+        "0"
+      ],
+      "slope_lower_bound": "166619322560337543578399164105/79228162514264337593543950336"
+    },
+    {
+      "columns": 487,
+      "proof": "degree-8-Bernstein",
+      "residual": [
+        "1",
+        "-1",
+        "0",
+        "0",
+        "0",
+        "0",
+        "0",
+        "0"
+      ],
+      "slope_lower_bound": "4626219148772546654468048777/2475880078570760549798248448"
+    },
+    {
+      "columns": 2,
+      "proof": "degree-8-Bernstein",
+      "residual": [
+        "1",
+        "0",
+        "-1",
+        "0",
+        "0",
+        "0",
+        "0",
+        "0"
+      ],
+      "slope_lower_bound": "160650629968283178647830827997/39614081257132168796771975168"
+    },
+    {
+      "columns": 53,
+      "proof": "degree-8-Bernstein",
+      "residual": [
+        "1",
+        "0",
+        "1",
+        "-1",
+        "0",
+        "0",
+        "0",
+        "0"
+      ],
+      "slope_lower_bound": "41595001775370150375311089779/39614081257132168796771975168"
+    },
+    {
+      "columns": 24,
+      "proof": "degree-8-Bernstein",
+      "residual": [
+        "1",
+        "0",
+        "2",
+        "-2",
+        "0",
+        "0",
+        "0",
+        "0"
+      ],
+      "slope_lower_bound": "275032560526201230758931699741/79228162514264337593543950336"
+    },
+    {
+      "columns": 203,
+      "proof": "degree-8-Bernstein",
+      "residual": [
+        "1",
+        "1",
+        "-1",
+        "0",
+        "0",
+        "0",
+        "0",
+        "0"
+      ],
+      "slope_lower_bound": "64609693751124233706202049099/79228162514264337593543950336"
+    },
+    {
+      "columns": 42,
+      "proof": "degree-8-Bernstein",
+      "residual": [
+        "1",
+        "1",
+        "0",
+        "-1",
+        "0",
+        "0",
+        "0",
+        "0"
+      ],
+      "slope_lower_bound": "256452250726585178734715391093/79228162514264337593543950336"
+    },
+    {
+      "columns": 6,
+      "proof": "degree-8-Bernstein",
+      "residual": [
+        "1",
+        "1",
+        "2",
+        "-2",
+        "0",
+        "0",
+        "0",
+        "0"
+      ],
+      "slope_lower_bound": "18340994340759107169472092845/79228162514264337593543950336"
+    },
+    {
+      "columns": 36,
+      "proof": "degree-8-Bernstein",
+      "residual": [
+        "1",
+        "2",
+        "-2",
+        "0",
+        "0",
+        "0",
+        "0",
+        "0"
+      ],
+      "slope_lower_bound": "118935970463484548335045719411/39614081257132168796771975168"
+    },
+    {
+      "columns": 8,
+      "proof": "degree-8-Bernstein",
+      "residual": [
+        "1",
+        "2",
+        "-1",
+        "-1",
+        "0",
+        "0",
+        "0",
+        "0"
+      ],
+      "slope_lower_bound": "429714497902430041698604780817/79228162514264337593543950336"
+    },
+    {
+      "columns": 4,
+      "proof": "degree-8-Bernstein",
+      "residual": [
+        "1",
+        "2",
+        "1",
+        "-2",
+        "0",
+        "0",
+        "0",
+        "0"
+      ],
+      "slope_lower_bound": "191603241516603985153565304381/79228162514264337593543950336"
+    },
+    {
+      "columns": 21,
+      "proof": "degree-8-Bernstein",
+      "residual": [
+        "1",
+        "3",
+        "-3",
+        "0",
+        "0",
+        "0",
+        "0",
+        "0"
+      ],
+      "slope_lower_bound": "205567094051406979816990414273/39614081257132168796771975168"
+    },
+    {
+      "columns": 1,
+      "proof": "degree-8-Bernstein",
+      "residual": [
+        "1",
+        "3",
+        "0",
+        "-2",
+        "0",
+        "0",
+        "0",
+        "0"
+      ],
+      "slope_lower_bound": "91216372173112215784414628979/19807040628566084398385987584"
+    },
+    {
+      "columns": 1,
+      "proof": "degree-8-Bernstein",
+      "residual": [
+        "1",
+        "6",
+        "-4",
+        "0",
+        "0",
+        "0",
+        "0",
+        "0"
+      ],
+      "slope_lower_bound": "71013302907774575418951004479/79228162514264337593543950336"
+    },
+    {
+      "columns": 1,
+      "proof": "degree-8-Bernstein",
+      "residual": [
+        "1",
+        "13",
+        "-3",
+        "-4",
+        "0",
+        "0",
+        "0",
+        "0"
+      ],
+      "slope_lower_bound": "331404007595384450066834114047/79228162514264337593543950336"
+    },
+    {
+      "columns": 14,
+      "proof": "degree-8-Bernstein",
+      "residual": [
+        "2",
+        "-14",
+        "2",
+        "4",
+        "0",
+        "0",
+        "0",
+        "0"
+      ],
+      "slope_lower_bound": "7131664751030668439340335705/79228162514264337593543950336"
+    },
+    {
+      "columns": 8,
+      "proof": "degree-8-Bernstein",
+      "residual": [
+        "2",
+        "-14",
+        "3",
+        "3",
+        "0",
+        "0",
+        "0",
+        "0"
+      ],
+      "slope_lower_bound": "205361487424107085325150904071/79228162514264337593543950336"
+    },
+    {
+      "columns": 10,
+      "proof": "degree-8-Bernstein",
+      "residual": [
+        "2",
+        "-13",
+        "1",
+        "4",
+        "0",
+        "0",
+        "0",
+        "0"
+      ],
+      "slope_lower_bound": "185342785652395815945476454171/79228162514264337593543950336"
+    },
+    {
+      "columns": 9,
+      "proof": "degree-8-Bernstein",
+      "residual": [
+        "2",
+        "-13",
+        "4",
+        "2",
+        "0",
+        "0",
+        "0",
+        "0"
+      ],
+      "slope_lower_bound": "71234105628444431453982910939/39614081257132168796771975168"
+    },
+    {
+      "columns": 6,
+      "proof": "degree-8-Bernstein",
+      "residual": [
+        "2",
+        "-12",
+        "0",
+        "4",
+        "0",
+        "0",
+        "0",
+        "0"
+      ],
+      "slope_lower_bound": "90888476638440240862903143159/19807040628566084398385987584"
+    },
+    {
+      "columns": 3,
+      "proof": "degree-8-Bernstein",
+      "residual": [
+        "2",
+        "-12",
+        "1",
+        "3",
+        "0",
+        "0",
+        "0",
+        "0"
+      ],
+      "slope_lower_bound": "280891864613418690168711570501/39614081257132168796771975168"
+    },
+    {
+      "columns": 4,
+      "proof": "degree-8-Bernstein",
+      "residual": [
+        "2",
+        "-8",
+        "1",
+        "2",
+        "0",
+        "0",
+        "0",
+        "0"
+      ],
+      "slope_lower_bound": "38713844070098756705095719039/19807040628566084398385987584"
+    },
+    {
+      "columns": 1,
+      "proof": "degree-8-Bernstein",
+      "residual": [
+        "2",
+        "-8",
+        "4",
+        "0",
+        "0",
+        "0",
+        "0",
+        "0"
+      ],
+      "slope_lower_bound": "111980801884888073782872243863/79228162514264337593543950336"
+    },
+    {
+      "columns": 21,
+      "proof": "degree-8-Bernstein",
+      "residual": [
+        "2",
+        "-5",
+        "2",
+        "0",
+        "0",
+        "0",
+        "0",
+        "0"
+      ],
+      "slope_lower_bound": "103122548677597674670422094667/39614081257132168796771975168"
+    },
+    {
+      "columns": 1,
+      "proof": "degree-8-Bernstein",
+      "residual": [
+        "2",
+        "-4",
+        "-2",
+        "2",
+        "0",
+        "0",
+        "0",
+        "0"
+      ],
+      "slope_lower_bound": "425776043941405196355445387021/79228162514264337593543950336"
+    },
+    {
+      "columns": 3,
+      "proof": "degree-8-Bernstein",
+      "residual": [
+        "2",
+        "-3",
+        "0",
+        "0",
+        "0",
+        "0",
+        "0",
+        "0"
+      ],
+      "slope_lower_bound": "276384795853442554043310011609/39614081257132168796771975168"
+    },
+    {
+      "columns": 36,
+      "proof": "degree-8-Bernstein",
+      "residual": [
+        "2",
+        "-3",
+        "1",
+        "0",
+        "0",
+        "0",
+        "0",
+        "0"
+      ],
+      "slope_lower_bound": "122815778345598106513067204787/79228162514264337593543950336"
+    },
+    {
+      "columns": 81,
+      "proof": "degree-8-Bernstein",
+      "residual": [
+        "2",
+        "-2",
+        "0",
+        "0",
+        "0",
+        "0",
+        "0",
+        "0"
+      ],
+      "slope_lower_bound": "296078025521442985885955121729/79228162514264337593543950336"
+    },
+    {
+      "columns": 7,
+      "proof": "degree-8-Bernstein",
+      "residual": [
+        "2",
+        "-2",
+        "2",
+        "-1",
+        "0",
+        "0",
+        "0",
+        "0"
+      ],
+      "slope_lower_bound": "7245846141952114290088977935/9903520314283042199192993792"
+    },
+    {
+      "columns": 651,
+      "proof": "degree-8-Bernstein",
+      "residual": [
+        "2",
+        "-1",
+        "0",
+        "0",
+        "0",
+        "0",
+        "0",
+        "0"
+      ],
+      "slope_lower_bound": "2461653708500053980330638765/4951760157141521099596496896"
+    },
+    {
+      "columns": 20,
+      "proof": "degree-8-Bernstein",
+      "residual": [
+        "2",
+        "0",
+        "-1",
+        "0",
+        "0",
+        "0",
+        "0",
+        "0"
+      ],
+      "slope_lower_bound": "106324353255922864018987157685/39614081257132168796771975168"
+    },
+    {
+      "columns": 25,
+      "proof": "degree-8-Bernstein",
+      "residual": [
+        "2",
+        "0",
+        "2",
+        "-2",
+        "0",
+        "0",
+        "0",
+        "0"
+      ],
+      "slope_lower_bound": "41595001775370150375311089779/19807040628566084398385987584"
+    },
+    {
+      "columns": 27,
+      "proof": "degree-8-Bernstein",
+      "residual": [
+        "2",
+        "1",
+        "-2",
+        "0",
+        "0",
+        "0",
+        "0",
+        "0"
+      ],
+      "slope_lower_bound": "192955476843845295500931852547/39614081257132168796771975168"
+    },
+    {
+      "columns": 7,
+      "proof": "degree-8-Bernstein",
+      "residual": [
+        "2",
+        "1",
+        "0",
+        "-1",
+        "0",
+        "0",
+        "0",
+        "0"
+      ],
+      "slope_lower_bound": "147799697301864549477028050469/79228162514264337593543950336"
+    },
+    {
+      "columns": 1,
+      "proof": "degree-8-Bernstein",
+      "residual": [
+        "2",
+        "1",
+        "1",
+        "-2",
+        "0",
+        "0",
+        "0",
+        "0"
+      ],
+      "slope_lower_bound": "84910563569331369871334392663/19807040628566084398385987584"
+    },
+    {
+      "columns": 56,
+      "proof": "degree-8-Bernstein",
+      "residual": [
+        "2",
+        "2",
+        "-2",
+        "0",
+        "0",
+        "0",
+        "0",
+        "0"
+      ],
+      "slope_lower_bound": "64609693751124233706202049099/39614081257132168796771975168"
+    },
+    {
+      "columns": 6,
+      "proof": "degree-8-Bernstein",
+      "residual": [
+        "2",
+        "2",
+        "-1",
+        "-1",
+        "0",
+        "0",
+        "0",
+        "0"
+      ],
+      "slope_lower_bound": "321061944477709412440917440193/79228162514264337593543950336"
+    },
+    {
+      "columns": 3,
+      "proof": "degree-8-Bernstein",
+      "residual": [
+        "2",
+        "2",
+        "0",
+        "-2",
+        "0",
+        "0",
+        "0",
+        "0"
+      ],
+      "slope_lower_bound": "512904501453170357469430782187/79228162514264337593543950336"
+    },
+    {
+      "columns": 5,
+      "proof": "degree-8-Bernstein",
+      "residual": [
+        "2",
+        "3",
+        "-3",
+        "0",
+        "0",
+        "0",
+        "0",
+        "0"
+      ],
+      "slope_lower_bound": "151240817339046665188146743961/39614081257132168796771975168"
+    },
+    {
+      "columns": 4,
+      "proof": "degree-8-Bernstein",
+      "residual": [
+        "3",
+        "-14",
+        "3",
+        "3",
+        "0",
+        "0",
+        "0",
+        "0"
+      ],
+      "slope_lower_bound": "95527932488692138622867961815/79228162514264337593543950336"
+    },
+    {
+      "columns": 7,
+      "proof": "degree-8-Bernstein",
+      "residual": [
+        "3",
+        "-13",
+        "1",
+        "4",
+        "0",
+        "0",
+        "0",
+        "0"
+      ],
+      "slope_lower_bound": "75509230716980869243193511915/79228162514264337593543950336"
+    },
+    {
+      "columns": 15,
+      "proof": "degree-8-Bernstein",
+      "residual": [
+        "3",
+        "-13",
+        "4",
+        "2",
+        "0",
+        "0",
+        "0",
+        "0"
+      ],
+      "slope_lower_bound": "16317328160736958102841439811/39614081257132168796771975168"
+    },
+    {
+      "columns": 3,
+      "proof": "degree-8-Bernstein",
+      "residual": [
+        "3",
+        "-13",
+        "5",
+        "1",
+        "0",
+        "0",
+        "0",
+        "0"
+      ],
+      "slope_lower_bound": "57716119748637583272873361997/19807040628566084398385987584"
+    },
+    {
+      "columns": 4,
+      "proof": "degree-8-Bernstein",
+      "residual": [
+        "3",
+        "-12",
+        "0",
+        "4",
+        "0",
+        "0",
+        "0",
+        "0"
+      ],
+      "slope_lower_bound": "63430087904586504187332407595/19807040628566084398385987584"
+    },
+    {
+      "columns": 1,
+      "proof": "degree-8-Bernstein",
+      "residual": [
+        "3",
+        "-12",
+        "1",
+        "3",
+        "0",
+        "0",
+        "0",
+        "0"
+      ],
+      "slope_lower_bound": "225975087145711216817570099373/39614081257132168796771975168"
+    },
+    {
+      "columns": 9,
+      "proof": "degree-8-Bernstein",
+      "residual": [
+        "3",
+        "-11",
+        "0",
+        "3",
+        "0",
+        "0",
+        "0",
+        "0"
+      ],
+      "slope_lower_bound": "630161295192787581141276317211/79228162514264337593543950336"
+    },
+    {
+      "columns": 6,
+      "proof": "degree-8-Bernstein",
+      "residual": [
+        "3",
+        "-7",
+        "3",
+        "0",
+        "0",
+        "0",
+        "0",
+        "0"
+      ],
+      "slope_lower_bound": "22544795981354784323340677509/9903520314283042199192993792"
+    },
+    {
+      "columns": 7,
+      "proof": "degree-8-Bernstein",
+      "residual": [
+        "3",
+        "-5",
+        "-2",
+        "2",
+        "0",
+        "0",
+        "0",
+        "0"
+      ],
+      "slope_lower_bound": "286907528351063344649211473943/39614081257132168796771975168"
+    },
+    {
+      "columns": 16,
+      "proof": "degree-8-Bernstein",
+      "residual": [
+        "3",
+        "-5",
+        "2",
+        "0",
+        "0",
+        "0",
+        "0",
+        "0"
+      ],
+      "slope_lower_bound": "48723194955954391394932943989/39614081257132168796771975168"
+    },
+    {
+      "columns": 8,
+      "proof": "degree-8-Bernstein",
+      "residual": [
+        "3",
+        "-4",
+        "0",
+        "1",
+        "0",
+        "0",
+        "0",
+        "0"
+      ],
+      "slope_lower_bound": "38713844070098756705095719039/39614081257132168796771975168"
+    },
+    {
+      "columns": 4,
+      "proof": "degree-8-Bernstein",
+      "residual": [
+        "3",
+        "-3",
+        "0",
+        "0",
+        "0",
+        "0",
+        "0",
+        "0"
+      ],
+      "slope_lower_bound": "444117038282164478828932682593/79228162514264337593543950336"
+    },
+    {
+      "columns": 36,
+      "proof": "degree-8-Bernstein",
+      "residual": [
+        "3",
+        "-3",
+        "1",
+        "0",
+        "0",
+        "0",
+        "0",
+        "0"
+      ],
+      "slope_lower_bound": "7081612460438738627689932081/39614081257132168796771975168"
+    },
+    {
+      "columns": 36,
+      "proof": "degree-8-Bernstein",
+      "residual": [
+        "3",
+        "-2",
+        "0",
+        "0",
+        "0",
+        "0",
+        "0",
+        "0"
+      ],
+      "slope_lower_bound": "11714092006045147289266736319/4951760157141521099596496896"
+    },
+    {
+      "columns": 34,
+      "proof": "degree-8-Bernstein",
+      "residual": [
+        "3",
+        "0",
+        "-1",
+        "0",
+        "0",
+        "0",
+        "0",
+        "0"
+      ],
+      "slope_lower_bound": "103996153087125098780286974745/79228162514264337593543950336"
+    },
+    {
+      "columns": 19,
+      "proof": "degree-8-Bernstein",
+      "residual": [
+        "3",
+        "0",
+        "2",
+        "-2",
+        "0",
+        "0",
+        "0",
+        "0"
+      ],
+      "slope_lower_bound": "14431863419189993060889254623/19807040628566084398385987584"
+    },
+    {
+      "columns": 21,
+      "proof": "degree-8-Bernstein",
+      "residual": [
+        "3",
+        "1",
+        "-2",
+        "0",
+        "0",
+        "0",
+        "0",
+        "0"
+      ],
+      "slope_lower_bound": "277258400262969961744176364469/79228162514264337593543950336"
+    },
+    {
+      "columns": 7,
+      "proof": "degree-8-Bernstein",
+      "residual": [
+        "3",
+        "1",
+        "0",
+        "-1",
+        "0",
+        "0",
+        "0",
+        "0"
+      ],
+      "slope_lower_bound": "39147143877143920219340709845/79228162514264337593543950336"
+    },
+    {
+      "columns": 3,
+      "proof": "degree-8-Bernstein",
+      "residual": [
+        "3",
+        "2",
+        "-2",
+        "0",
+        "0",
+        "0",
+        "0",
+        "0"
+      ],
+      "slope_lower_bound": "10283417038763919077358378787/39614081257132168796771975168"
+    },
+    {
+      "columns": 2,
+      "proof": "degree-8-Bernstein",
+      "residual": [
+        "3",
+        "3",
+        "-3",
+        "0",
+        "0",
+        "0",
+        "0",
+        "0"
+      ],
+      "slope_lower_bound": "193829081253372701118606147297/79228162514264337593543950336"
+    },
+    {
+      "columns": 15,
+      "proof": "degree-8-Bernstein",
+      "residual": [
+        "3",
+        "3",
+        "-1",
+        "-2",
+        "0",
+        "0",
+        "0",
+        "0"
+      ],
+      "slope_lower_bound": "577514195204294591175632831287/79228162514264337593543950336"
+    },
+    {
+      "columns": 3,
+      "proof": "degree-8-Bernstein",
+      "residual": [
+        "3",
+        "5",
+        "-1",
+        "-2",
+        "0",
+        "0",
+        "0",
+        "0"
+      ],
+      "slope_lower_bound": "8016382854176292999589202187/9903520314283042199192993792"
+    },
+    {
+      "columns": 1,
+      "proof": "degree-8-Bernstein",
+      "residual": [
+        "4",
+        "-13",
+        "5",
+        "1",
+        "0",
+        "0",
+        "0",
+        "0"
+      ],
+      "slope_lower_bound": "30257731014783846597302626433/19807040628566084398385987584"
+    },
+    {
+      "columns": 4,
+      "proof": "degree-8-Bernstein",
+      "residual": [
+        "4",
+        "-12",
+        "1",
+        "3",
+        "0",
+        "0",
+        "0",
+        "0"
+      ],
+      "slope_lower_bound": "171058309678003743466428628245/39614081257132168796771975168"
+    },
+    {
+      "columns": 2,
+      "proof": "degree-8-Bernstein",
+      "residual": [
+        "4",
+        "-11",
+        "-1",
+        "4",
+        "0",
+        "0",
+        "0",
+        "0"
+      ],
+      "slope_lower_bound": "322097917584296217553182806589/79228162514264337593543950336"
+    },
+    {
+      "columns": 3,
+      "proof": "degree-8-Bernstein",
+      "residual": [
+        "4",
+        "-11",
+        "0",
+        "3",
+        "0",
+        "0",
+        "0",
+        "0"
+      ],
+      "slope_lower_bound": "520327740257372634438993374955/79228162514264337593543950336"
+    },
+    {
+      "columns": 3,
+      "proof": "degree-8-Bernstein",
+      "residual": [
+        "4",
+        "-11",
+        "1",
+        "2",
+        "0",
+        "0",
+        "0",
+        "0"
+      ],
+      "slope_lower_bound": "357725230153098909282237102263/39614081257132168796771975168"
+    },
+    {
+      "columns": 15,
+      "proof": "degree-8-Bernstein",
+      "residual": [
+        "4",
+        "-8",
+        "0",
+        "2",
+        "0",
+        "0",
+        "0",
+        "0"
+      ],
+      "slope_lower_bound": "93630621537806230056237190167/19807040628566084398385987584"
+    },
+    {
+      "columns": 13,
+      "proof": "degree-8-Bernstein",
+      "residual": [
+        "4",
+        "-7",
+        "3",
+        "0",
+        "0",
+        "0",
+        "0",
+        "0"
+      ],
+      "slope_lower_bound": "8815601614427915985555309727/9903520314283042199192993792"
+    },
+    {
+      "columns": 7,
+      "proof": "degree-8-Bernstein",
+      "residual": [
+        "4",
+        "-4",
+        "0",
+        "0",
+        "0",
+        "0",
+        "0",
+        "0"
+      ],
+      "slope_lower_bound": "296078025521442985885955121729/39614081257132168796771975168"
+    },
+    {
+      "columns": 7,
+      "proof": "degree-8-Bernstein",
+      "residual": [
+        "4",
+        "-3",
+        "0",
+        "0",
+        "0",
+        "0",
+        "0",
+        "0"
+      ],
+      "slope_lower_bound": "335464484857443849571245341969/79228162514264337593543950336"
+    },
+    {
+      "columns": 5,
+      "proof": "degree-8-Bernstein",
+      "residual": [
+        "4",
+        "-2",
+        "0",
+        "0",
+        "0",
+        "0",
+        "0",
+        "0"
+      ],
+      "slope_lower_bound": "2461653708500053980330638765/2475880078570760549798248448"
+    },
+    {
+      "columns": 1,
+      "proof": "degree-8-Bernstein",
+      "residual": [
+        "4",
+        "-1",
+        "2",
+        "-2",
+        "0",
+        "0",
+        "0",
+        "0"
+      ],
+      "slope_lower_bound": "51441616609370366296633644839/19807040628566084398385987584"
+    },
+    {
+      "columns": 7,
+      "proof": "degree-8-Bernstein",
+      "residual": [
+        "4",
+        "0",
+        "-2",
+        "0",
+        "0",
+        "0",
+        "0",
+        "0"
+      ],
+      "slope_lower_bound": "106324353255922864018987157685/19807040628566084398385987584"
+    },
+    {
+      "columns": 3,
+      "proof": "degree-8-Bernstein",
+      "residual": [
+        "4",
+        "2",
+        "0",
+        "-2",
+        "0",
+        "0",
+        "0",
+        "0"
+      ],
+      "slope_lower_bound": "295599394603729098954056100939/79228162514264337593543950336"
+    },
+    {
+      "columns": 3,
+      "proof": "degree-8-Bernstein",
+      "residual": [
+        "4",
+        "3",
+        "-3",
+        "0",
+        "0",
+        "0",
+        "0",
+        "0"
+      ],
+      "slope_lower_bound": "85176527828652071860918806673/79228162514264337593543950336"
+    },
+    {
+      "columns": 11,
+      "proof": "degree-8-Bernstein",
+      "residual": [
+        "4",
+        "3",
+        "-1",
+        "-2",
+        "0",
+        "0",
+        "0",
+        "0"
+      ],
+      "slope_lower_bound": "234430820889786980958972745331/39614081257132168796771975168"
+    },
+    {
+      "columns": 6,
+      "proof": "degree-8-Bernstein",
+      "residual": [
+        "5",
+        "-10",
+        "0",
+        "2",
+        "0",
+        "0",
+        "0",
+        "0"
+      ],
+      "slope_lower_bound": "195015038514330517169918695211/19807040628566084398385987584"
+    },
+    {
+      "columns": 3,
+      "proof": "degree-8-Bernstein",
+      "residual": [
+        "5",
+        "-10",
+        "2",
+        "1",
+        "0",
+        "0",
+        "0",
+        "0"
+      ],
+      "slope_lower_bound": "135487224417874017262959477361/19807040628566084398385987584"
+    },
+    {
+      "columns": 1,
+      "proof": "degree-8-Bernstein",
+      "residual": [
+        "5",
+        "-9",
+        "0",
+        "2",
+        "0",
+        "0",
+        "0",
+        "0"
+      ],
+      "slope_lower_bound": "523368587871879946479009879355/79228162514264337593543950336"
+    },
+    {
+      "columns": 6,
+      "proof": "degree-8-Bernstein",
+      "residual": [
+        "5",
+        "-9",
+        "3",
+        "0",
+        "0",
+        "0",
+        "0",
+        "0"
+      ],
+      "slope_lower_bound": "477099888461514948796888954985/79228162514264337593543950336"
+    },
+    {
+      "columns": 3,
+      "proof": "degree-8-Bernstein",
+      "residual": [
+        "5",
+        "-8",
+        "0",
+        "2",
+        "0",
+        "0",
+        "0",
+        "0"
+      ],
+      "slope_lower_bound": "66172232803952493380666454603/19807040628566084398385987584"
+    },
+    {
+      "columns": 6,
+      "proof": "degree-8-Bernstein",
+      "residual": [
+        "5",
+        "-4",
+        "0",
+        "0",
+        "0",
+        "0",
+        "0",
+        "0"
+      ],
+      "slope_lower_bound": "241751748809082671257111451417/39614081257132168796771975168"
+    },
+    {
+      "columns": 6,
+      "proof": "degree-8-Bernstein",
+      "residual": [
+        "5",
+        "-3",
+        "0",
+        "0",
+        "0",
+        "0",
+        "0",
+        "0"
+      ],
+      "slope_lower_bound": "226811931432723220313558001345/79228162514264337593543950336"
+    },
+    {
+      "columns": 6,
+      "proof": "degree-8-Bernstein",
+      "residual": [
+        "5",
+        "-2",
+        "1",
+        "-2",
+        "0",
+        "0",
+        "0",
+        "0"
+      ],
+      "slope_lower_bound": "195939823139872489925766239663/19807040628566084398385987584"
+    },
+    {
+      "columns": 3,
+      "proof": "degree-8-Bernstein",
+      "residual": [
+        "5",
+        "-1",
+        "2",
+        "-2",
+        "0",
+        "0",
+        "0",
+        "0"
+      ],
+      "slope_lower_bound": "24278478253190208982211809683/19807040628566084398385987584"
+    },
+    {
+      "columns": 1,
+      "proof": "degree-8-Bernstein",
+      "residual": [
+        "5",
+        "1",
+        "-1",
+        "-1",
+        "0",
+        "0",
+        "0",
+        "0"
+      ],
+      "slope_lower_bound": "251795850388989648257315025215/79228162514264337593543950336"
+    },
+    {
+      "columns": 1,
+      "proof": "degree-8-Bernstein",
+      "residual": [
+        "5",
+        "4",
+        "-4",
+        "0",
+        "0",
+        "0",
+        "0",
+        "0"
+      ],
+      "slope_lower_bound": "37446555394944076391780213943/19807040628566084398385987584"
+    },
+    {
+      "columns": 9,
+      "proof": "degree-8-Bernstein",
+      "residual": [
+        "6",
+        "-12",
+        "4",
+        "0",
+        "0",
+        "0",
+        "0",
+        "0"
+      ],
+      "slope_lower_bound": "708568220231833684567643500397/79228162514264337593543950336"
+    },
+    {
+      "columns": 6,
+      "proof": "degree-8-Bernstein",
+      "residual": [
+        "6",
+        "-10",
+        "0",
+        "2",
+        "0",
+        "0",
+        "0",
+        "0"
+      ],
+      "slope_lower_bound": "167851900158150359855496860055/19807040628566084398385987584"
+    },
+    {
+      "columns": 1,
+      "proof": "degree-8-Bernstein",
+      "residual": [
+        "6",
+        "-10",
+        "2",
+        "1",
+        "0",
+        "0",
+        "0",
+        "0"
+      ],
+      "slope_lower_bound": "433296344246775439794150568819/79228162514264337593543950336"
+    },
+    {
+      "columns": 12,
+      "proof": "degree-8-Bernstein",
+      "residual": [
+        "6",
+        "-10",
+        "3",
+        "0",
+        "0",
+        "0",
+        "0",
+        "0"
+      ],
+      "slope_lower_bound": "312569450611118220869933257925/39614081257132168796771975168"
+    },
+    {
+      "columns": 1,
+      "proof": "degree-8-Bernstein",
+      "residual": [
+        "6",
+        "-9",
+        "0",
+        "2",
+        "0",
+        "0",
+        "0",
+        "0"
+      ],
+      "slope_lower_bound": "414716034447159317221322538731/79228162514264337593543950336"
+    },
+    {
+      "columns": 3,
+      "proof": "degree-8-Bernstein",
+      "residual": [
+        "6",
+        "-8",
+        "0",
+        "2",
+        "0",
+        "0",
+        "0",
+        "0"
+      ],
+      "slope_lower_bound": "38713844070098756705095719039/19807040628566084398385987584"
+    },
+    {
+      "columns": 1,
+      "proof": "degree-8-Bernstein",
+      "residual": [
+        "6",
+        "-6",
+        "0",
+        "0",
+        "0",
+        "0",
+        "0",
+        "0"
+      ],
+      "slope_lower_bound": "888234076564328957657865365187/79228162514264337593543950336"
+    },
+    {
+      "columns": 3,
+      "proof": "degree-8-Bernstein",
+      "residual": [
+        "6",
+        "-2",
+        "0",
+        "-1",
+        "0",
+        "0",
+        "0",
+        "0"
+      ],
+      "slope_lower_bound": "483264182159308400437068097845/79228162514264337593543950336"
+    },
+    {
+      "columns": 16,
+      "proof": "degree-8-Bernstein",
+      "residual": [
+        "6",
+        "-2",
+        "1",
+        "-2",
+        "0",
+        "0",
+        "0",
+        "0"
+      ],
+      "slope_lower_bound": "168776684783692332611344404507/19807040628566084398385987584"
+    },
+    {
+      "columns": 6,
+      "proof": "degree-8-Bernstein",
+      "residual": [
+        "6",
+        "-2",
+        "2",
+        "-2",
+        "0",
+        "0",
+        "0",
+        "0"
+      ],
+      "slope_lower_bound": "245152925773482328871824799597/79228162514264337593543950336"
+    },
+    {
+      "columns": 6,
+      "proof": "degree-8-Bernstein",
+      "residual": [
+        "6",
+        "-1",
+        "3",
+        "-4",
+        "0",
+        "0",
+        "0",
+        "0"
+      ],
+      "slope_lower_bound": "100262535862531133532666469613/9903520314283042199192993792"
+    },
+    {
+      "columns": 15,
+      "proof": "degree-8-Bernstein",
+      "residual": [
+        "6",
+        "1",
+        "3",
+        "-4",
+        "0",
+        "0",
+        "0",
+        "0"
+      ],
+      "slope_lower_bound": "36089644316170602808900906065/9903520314283042199192993792"
+    },
+    {
+      "columns": 3,
+      "proof": "degree-8-Bernstein",
+      "residual": [
+        "6",
+        "2",
+        "3",
+        "-4",
+        "0",
+        "0",
+        "0",
+        "0"
+      ],
+      "slope_lower_bound": "4003198542990337360218455203/9903520314283042199192993792"
+    },
+    {
+      "columns": 4,
+      "proof": "degree-8-Bernstein",
+      "residual": [
+        "6",
+        "4",
+        "-4",
+        "0",
+        "0",
+        "0",
+        "0",
+        "0"
+      ],
+      "slope_lower_bound": "10283417038763919077358378787/19807040628566084398385987584"
+    },
+    {
+      "columns": 3,
+      "proof": "degree-8-Bernstein",
+      "residual": [
+        "7",
+        "-11",
+        "3",
+        "0",
+        "0",
+        "0",
+        "0",
+        "0"
+      ],
+      "slope_lower_bound": "773177913982957934682844076715/79228162514264337593543950336"
+    },
+    {
+      "columns": 3,
+      "proof": "degree-8-Bernstein",
+      "residual": [
+        "7",
+        "-10",
+        "0",
+        "2",
+        "0",
+        "0",
+        "0",
+        "0"
+      ],
+      "slope_lower_bound": "562755047207880810164300099595/79228162514264337593543950336"
+    },
+    {
+      "columns": 3,
+      "proof": "degree-8-Bernstein",
+      "residual": [
+        "7",
+        "-10",
+        "3",
+        "0",
+        "0",
+        "0",
+        "0",
+        "0"
+      ],
+      "slope_lower_bound": "258243173898757906241089587613/39614081257132168796771975168"
+    },
+    {
+      "columns": 3,
+      "proof": "degree-8-Bernstein",
+      "residual": [
+        "7",
+        "-9",
+        "3",
+        "0",
+        "0",
+        "0",
+        "0",
+        "0"
+      ],
+      "slope_lower_bound": "259794781612073690281514273737/79228162514264337593543950336"
+    },
+    {
+      "columns": 1,
+      "proof": "degree-8-Bernstein",
+      "residual": [
+        "7",
+        "-8",
+        "1",
+        "0",
+        "0",
+        "0",
+        "0",
+        "0"
+      ],
+      "slope_lower_bound": "431505421074602785613977504555/39614081257132168796771975168"
+    },
+    {
+      "columns": 3,
+      "proof": "degree-8-Bernstein",
+      "residual": [
+        "7",
+        "-4",
+        "3",
+        "-2",
+        "0",
+        "0",
+        "0",
+        "0"
+      ],
+      "slope_lower_bound": "219929691358358942441914443519/79228162514264337593543950336"
+    },
+    {
+      "columns": 9,
+      "proof": "degree-8-Bernstein",
+      "residual": [
+        "7",
+        "-3",
+        "2",
+        "-2",
+        "0",
+        "0",
+        "0",
+        "0"
+      ],
+      "slope_lower_bound": "393191938534203821814802360461/79228162514264337593543950336"
+    },
+    {
+      "columns": 1,
+      "proof": "degree-8-Bernstein",
+      "residual": [
+        "7",
+        "-2",
+        "0",
+        "-1",
+        "0",
+        "0",
+        "0",
+        "0"
+      ],
+      "slope_lower_bound": "374611628734587771179380757221/79228162514264337593543950336"
+    },
+    {
+      "columns": 1,
+      "proof": "degree-8-Bernstein",
+      "residual": [
+        "7",
+        "-2",
+        "1",
+        "-2",
+        "0",
+        "0",
+        "0",
+        "0"
+      ],
+      "slope_lower_bound": "566454185710048701187690277403/79228162514264337593543950336"
+    },
+    {
+      "columns": 2,
+      "proof": "degree-8-Bernstein",
+      "residual": [
+        "7",
+        "-2",
+        "2",
+        "-2",
+        "0",
+        "0",
+        "0",
+        "0"
+      ],
+      "slope_lower_bound": "34125093087190424903534364743/19807040628566084398385987584"
+    },
+    {
+      "columns": 1,
+      "proof": "degree-8-Bernstein",
+      "residual": [
+        "7",
+        "-1",
+        "3",
+        "-4",
+        "0",
+        "0",
+        "0",
+        "0"
+      ],
+      "slope_lower_bound": "86680966684441054875455552035/9903520314283042199192993792"
+    },
+    {
+      "columns": 3,
+      "proof": "degree-8-Bernstein",
+      "residual": [
+        "7",
+        "1",
+        "3",
+        "-4",
+        "0",
+        "0",
+        "0",
+        "0"
+      ],
+      "slope_lower_bound": "180064601104644193213519907895/79228162514264337593543950336"
+    },
+    {
+      "columns": 4,
+      "proof": "degree-8-Bernstein",
+      "residual": [
+        "8",
+        "-11",
+        "3",
+        "0",
+        "0",
+        "0",
+        "0",
+        "0"
+      ],
+      "slope_lower_bound": "332262680279118652712578368045/39614081257132168796771975168"
+    },
+    {
+      "columns": 1,
+      "proof": "degree-8-Bernstein",
+      "residual": [
+        "8",
+        "-4",
+        "3",
+        "-2",
+        "0",
+        "0",
+        "0",
+        "0"
+      ],
+      "slope_lower_bound": "111277137933638313184227102895/79228162514264337593543950336"
+    },
+    {
+      "columns": 7,
+      "proof": "degree-8-Bernstein",
+      "residual": [
+        "8",
+        "-3",
+        "2",
+        "-2",
+        "0",
+        "0",
+        "0",
+        "0"
+      ],
+      "slope_lower_bound": "284539385109483192557115019837/79228162514264337593543950336"
+    },
+    {
+      "columns": 9,
+      "proof": "degree-8-Bernstein",
+      "residual": [
+        "8",
+        "1",
+        "3",
+        "-4",
+        "0",
+        "0",
+        "0",
+        "0"
+      ],
+      "slope_lower_bound": "71412047679923563955832567271/79228162514264337593543950336"
+    },
+    {
+      "columns": 15,
+      "proof": "degree-8-Bernstein",
+      "residual": [
+        "9",
+        "-11",
+        "4",
+        "0",
+        "0",
+        "0",
+        "0",
+        "0"
+      ],
+      "slope_lower_bound": "125918993772229674593916577035/79228162514264337593543950336"
+    },
+    {
+      "columns": 9,
+      "proof": "degree-8-Bernstein",
+      "residual": [
+        "9",
+        "-9",
+        "2",
+        "0",
+        "0",
+        "0",
+        "0",
+        "0"
+      ],
+      "slope_lower_bound": "472443488123919433339692410919/79228162514264337593543950336"
+    },
+    {
+      "columns": 1,
+      "proof": "degree-8-Bernstein",
+      "residual": [
+        "9",
+        "-3",
+        "1",
+        "-2",
+        "0",
+        "0",
+        "0",
+        "0"
+      ],
+      "slope_lower_bound": "605840645046049564872980497643/79228162514264337593543950336"
+    },
+    {
+      "columns": 6,
+      "proof": "degree-8-Bernstein",
+      "residual": [
+        "9",
+        "-1",
+        "3",
+        "-4",
+        "0",
+        "0",
+        "0",
+        "0"
+      ],
+      "slope_lower_bound": "476142626626087180488269735031/79228162514264337593543950336"
+    },
+    {
+      "columns": 3,
+      "proof": "degree-8-Bernstein",
+      "residual": [
+        "10",
+        "-11",
+        "4",
+        "0",
+        "0",
+        "0",
+        "0",
+        "0"
+      ],
+      "slope_lower_bound": "4170414730613104518398914373/19807040628566084398385987584"
+    },
+    {
+      "columns": 6,
+      "proof": "degree-8-Bernstein",
+      "residual": [
+        "10",
+        "-9",
+        "2",
+        "0",
+        "0",
+        "0",
+        "0",
+        "0"
+      ],
+      "slope_lower_bound": "363790934699198804082005070295/79228162514264337593543950336"
+    },
+    {
+      "columns": 3,
+      "proof": "degree-8-Bernstein",
+      "residual": [
+        "11",
+        "-1",
+        "3",
+        "-4",
+        "0",
+        "0",
+        "0",
+        "0"
+      ],
+      "slope_lower_bound": "129418759888322960986447526891/39614081257132168796771975168"
+    },
+    {
+      "columns": 3,
+      "proof": "degree-8-Bernstein",
+      "residual": [
+        "12",
+        "-10",
+        "5",
+        "-2",
+        "0",
+        "0",
+        "0",
+        "0"
+      ],
+      "slope_lower_bound": "356908694624834526210361512469/79228162514264337593543950336"
+    },
+    {
+      "columns": 9,
+      "proof": "degree-8-Bernstein",
+      "residual": [
+        "13",
+        "-10",
+        "5",
+        "-2",
+        "0",
+        "0",
+        "0",
+        "0"
+      ],
+      "slope_lower_bound": "248256141200113896952674171845/79228162514264337593543950336"
+    },
+    {
+      "columns": 9,
+      "proof": "degree-8-Bernstein",
+      "residual": [
+        "14",
+        "-10",
+        "5",
+        "-2",
+        "0",
+        "0",
+        "0",
+        "0"
+      ],
+      "slope_lower_bound": "139603587775393267694986831221/79228162514264337593543950336"
+    },
+    {
+      "columns": 3,
+      "proof": "degree-8-Bernstein",
+      "residual": [
+        "15",
+        "-10",
+        "5",
+        "-2",
+        "0",
+        "0",
+        "0",
+        "0"
+      ],
+      "slope_lower_bound": "7737758587668159609324872649/19807040628566084398385987584"
+    }
+  ],
+  "schema": "selected-k8-uniform-frame-audit-v1",
+  "scope": "Uniform fixed-word frame LP optimum and uniqueness of the optimal paid histogram. Shared pinned event/domain model; no physical supplier, new kappa or full multiplication theorem.",
+  "status": "PASS_SELECTED_K8_UNIFORM_FRAME_AUDIT",
+  "strict_interval": "0 < a <= 1/32",
+  "word_sha256": "c2b294300760e1fd6eeab8c22c4d13e4633dca40e52cac8da0d68163a76e3ca8"
+}
diff --git a/research/selected-k8-uniform-frame-audit/SOURCES.json b/research/selected-k8-uniform-frame-audit/SOURCES.json
new file mode 100644
index 0000000000..cbd0ae9531
--- /dev/null
+++ b/research/selected-k8-uniform-frame-audit/SOURCES.json
@@ -0,0 +1,68 @@
+{
+  "schema_version": 1,
+  "base_commit": "418e40eb2572d930b58c1cf9b82b41c0fc7ee08d",
+  "files": [
+    {
+      "path": "certificates/selected-result.json",
+      "usage": "provenance",
+      "git_blob": "ae6a99f28aa468649eb66a361e764d769363bf11",
+      "sha256": "10b9e340fd8e354a37a0c4813c90e5de1dd42044b5f6aca4a3fc5a42b685fa32"
+    },
+    {
+      "path": "docs/research/agent-task-catalog.json",
+      "usage": "provenance",
+      "git_blob": "06c96f5579bb67ed1b86d334e78fbed7da6945f1",
+      "sha256": "6686ad58f1fbdbc87134a78901b60fd53a20d3984355e91defbbebc9e9fa8075"
+    },
+    {
+      "path": "research/complex-x4-frame-bound/model.py",
+      "usage": "input",
+      "git_blob": "33cfb4f404be0ed9fabd53a362084ef8dbc1911c",
+      "sha256": "0fa808a82e12a8928e43de3131958b9018476ee8c25b1ebc841316705e4f0eff"
+    },
+    {
+      "path": "research/gauge44-slots/construction/slots/SLOT-PINS-k8.json",
+      "usage": "input",
+      "git_blob": "2702c368f4de0b671577aee9a0e2df41c1b27658",
+      "sha256": "55dd229684febecb80638eff9c6b3986623e8539c6c956753b350209c3e0efe2"
+    },
+    {
+      "path": "research/r480-owner-optimum/inputs/local/FULL-WORD.json.gz",
+      "usage": "input",
+      "git_blob": "723decbca8995e916d6f4b783aa3e1ddd4eb47fe",
+      "sha256": "49596aa4ed4fd36cd4582fd0e8ddeb09fd80370a7d8aea1ede52a135b536d289"
+    }
+  ],
+  "predecessor": {
+    "pr": 1671,
+    "head": "ce130d291f5ab6dd801544886a16f62d42d86118",
+    "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/1671",
+    "author": "Gareth Davidson / bitplane",
+    "files": [
+      {
+        "path": "research/selected-k8-frame-ceiling/DUALS.json.gz",
+        "git_blob": "7d5186101b3c90e128d4ee3c336b459fee6802e1",
+        "sha256": "4047e520dcc04554a1233398070e2bec98ae6e2d44f209299b9febdbfb4dbb2a",
+        "usage": "retained dual payload"
+      },
+      {
+        "path": "research/selected-k8-frame-ceiling/PROOF.md",
+        "git_blob": "560d798e366a50d94de68e96f412a5df31838ab6",
+        "sha256": "d4ebb1c7355f717e548baea65768ff37d4599269ab356e8fd6741b00fca668c7",
+        "usage": "reviewed context, not runtime input"
+      },
+      {
+        "path": "research/selected-k8-frame-ceiling/EXPECTED.json",
+        "git_blob": "8ba1fee58cb17a00e3744ee46f39752c532ab596",
+        "sha256": "35b654ca2ba6718da47c38fbb04a381feb8eb4a984e786f58a0dbbacb836a26c",
+        "usage": "reviewed context, not runtime input"
+      },
+      {
+        "path": "research/selected-k8-frame-ceiling/independent.py",
+        "git_blob": "ab8be2176e53b37e4786afd1e11306b91fe7090c",
+        "sha256": "044f64316e94b458b1dc6723df846a4a2fc0104d64cddbdea30fb3ab2c735f60",
+        "usage": "reviewed context, not runtime input"
+      }
+    ]
+  }
+}
diff --git a/research/selected-k8-uniform-frame-audit/TASK.json b/research/selected-k8-uniform-frame-audit/TASK.json
new file mode 100644
index 0000000000..e672d11d11
--- /dev/null
+++ b/research/selected-k8-uniform-frame-audit/TASK.json
@@ -0,0 +1,185 @@
+{
+  "schema_version": 1,
+  "task_id": "complex-rank-shape-decoder",
+  "priority_revision": 3,
+  "base_commit": "418e40eb2572d930b58c1cf9b82b41c0fc7ee08d",
+  "original_card": {
+    "id": "complex-rank-shape-decoder",
+    "question": "Can a decoder deliver the local paid mass in fewer, larger-rank children (block frame climbs instead of rank-1 to rank-3 steps)?",
+    "starting_points": [
+      "research/complex-local-word-ceiling/README.md",
+      "research/complex-decoder-field-extension-seed44/README.md",
+      "research/complex-frame-pair-decoders/README.md"
+    ],
+    "methods": [
+      "Find one exact small decoding identity whose frame path climbs in blocks, and price its complete per-call profile.",
+      "Bound the best effective child rank achievable for one fixed support alphabet, including copies, frames and restoration."
+    ],
+    "acceptance_gate": "A per-call local profile, with all copied information, frames and restoration counted, whose ceiling exceeds the selected word's by at least 5%; masked or overcomplete supports must change an assumption of the eight-term all-pairs bound.",
+    "first_step": {
+      "command": [
+        "python3",
+        "-B",
+        "research/complex-local-word-ceiling/verify.py"
+      ],
+      "expected": "PASS_COMPLEX_LOCAL_WORD_CEILING",
+      "inspect": "Read the selected word's per-call local profile, its packing ceiling and the lever table; run levers.py for the ideal budget of the lever you target.",
+      "scope": "Positive control and planning budget only; this is not a new construction or full cold replay."
+    },
+    "first_experiment": "Before any synthesis, write the candidate per-call local profile (and centre charge / unpaid coordinates if changed) and screen it with ceiling.ceiling(); reject it if even the ideal ceiling does not beat the selected word's by your stated margin. Ideal budget: rank-16 delivery is 2.31x (levers.py).",
+    "bottleneck_link": "Rank-1 children are about half of recursive cost; the selected word's effective child rank is about 3.9. Larger-rank delivery lowers recursive cost per unit of paid mass.",
+    "allowed_variations": [
+      "One masked, overcomplete or block decoder family with exact labels and supports.",
+      "A scoped lower bound on effective rank for one alphabet.",
+      "If the coverage law, template or guard changes, derive an applicable fully charged replacement bound instead of applying the incumbent ceiling outside its scope."
+    ],
+    "scope_change_triggers": [
+      "Repacking idle remainders of an unchanged word (covered by the packing ceiling).",
+      "Repeating the eight-term all-pairs search inside its proved scope."
+    ],
+    "overlap_terms": [
+      "rank shape",
+      "block climb",
+      "masked decoder",
+      "overcomplete",
+      "effective rank"
+    ]
+  },
+  "scope_status": "changed",
+  "actual_scope": "Source-bound audit and uniform extension of PR1671: fixed selected k8 frame-LP optimality for 0<=a<=1/32, with uniqueness of the optimal paid histogram for a>0. Rebuild all 23004 columns and 135 objective identities, then certify their 239 distinct rational reduced vectors.",
+  "scope_change_reason": "The fresh overlap search found PR1671 already addressing fixed-word frame changes at two exponents. This session switched from decoder synthesis to its independent arithmetic audit and the previously unclaimed uniform/equality-case consequences. The initially proposed all-concave extension of the same dual fails; the one bounded refinement is the power family through 1/32. This does not satisfy the card's physical-construction acceptance gate.",
+  "bottleneck_link": "The complex side binds and rank-one children dominate much of its cost. Uniform optimal-profile rigidity identifies what fixed-word frame freedom cannot change even after retuning the exponent; an improvement must change a premise such as scalar dependencies or endpoints.",
+  "budget_minutes": 60,
+  "stop_rule": "One source-pinned dual and one event/domain model only. Stop after the uniform signs, exact boundaries and equality-case proof; no new word synthesis or claim of an optimal maximal exponent interval. Session approximately 06:19-07:19 UTC with verification/handoff reserved.",
+  "outcome": "completed",
+  "evidence": "RESULT.json and PROOF.md: all 23004 columns, 17507 rows, 135 components; 239 reduced vectors (237 Bernstein-positive, one exact square, one zero); same-profile alternative model assignment; exact all-concave and a=1/20 dual-failure controls.",
+  "author": "Ross Richardson",
+  "ai_assistance": "Substantial OpenAI Codex assistance in task selection, mathematics, implementation, tests, verification and writing. No subagents, independent human review or proof assistant.",
+  "open_questions": [
+    {
+      "question": "Which change of a scalar dependency or gate order permits a paid profile with a better complete moment?",
+      "why_it_matters": "The uniform certificate and equality-case rigidity exclude improved or differently shaped optima while its fixed-word premises remain.",
+      "first_step": "Choose one explicit changed dependency/order in the selected word, reconstruct its frame domain and source/dirty-state contract, and screen the entire local plus idle bill.",
+      "blocked_by": "This certificate applies only to the old chronology and endpoints; a rewrite needs new symbolic correctness and complete cost evidence."
+    },
+    {
+      "question": "How far does baseline frame optimality extend beyond a=1/32?",
+      "why_it_matters": "A negative column of the current dual at a=1/20 is not a cheaper feasible assignment and should not be mistaken for a primal transition.",
+      "first_step": "At one named exponent beyond 1/32, nominate a new dual or a feasible changed assignment, then check it exactly.",
+      "blocked_by": "No alternative dual or feasible improving assignment is established. This is lower priority for the current supplier because its full packing bill already fails much earlier."
+    }
+  ],
+  "chooser_nonce": "4071338634dbc7c5d72c8e5f2a5a4633",
+  "catalogue_scope_key": "cad3ba853d7f324f16fa",
+  "scope_key": "selected-k8/pr1671/uniform-power-dual-and-optimal-profile/0..1over32",
+  "claim_url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1659#discussioncomment-18916847",
+  "predecessor": {
+    "pr": 1671,
+    "head": "ce130d291f5ab6dd801544886a16f62d42d86118",
+    "author": "Gareth Davidson / bitplane"
+  },
+  "cost_boundary": {
+    "local_rank_mass": 5586,
+    "idle_rank_mass_per_call": 1646,
+    "centre_charge": 64,
+    "width": 73,
+    "families_per_call": "896/9",
+    "idle_cap": 51,
+    "new_kappa": false,
+    "physical_candidate": false
+  },
+  "overlap": {
+    "initial_snapshot": {
+      "open_prs": {
+        "fetched_at": "2026-10-14T06:21:02.029957+00:00",
+        "complete_pagination": true,
+        "records": 459
+      },
+      "discussions": {
+        "fetched_at": "2026-10-14T06:22:16.951518+00:00",
+        "complete_pagination": true,
+        "records": 323
+      }
+    },
+    "coverage_limit": "All open PR bodies including drafts and Discussion records plus local notes/ledger; not every code diff or closed PR. No matches is not proof of novelty.",
+    "nearest": [
+      {
+        "pr": 1671,
+        "head": "ce130d291f5ab6dd801544886a16f62d42d86118",
+        "delta": "Same selected word and dual; prior theorem checks two exponents and does not claim uniform optimality or optimal-profile rigidity."
+      },
+      {
+        "pr": 1605,
+        "head": "488f2ecf1835c6d813e96543656dddf0062fdc9a",
+        "delta": "Abstract integer reblocking/overhead screening, not the actual fixed-word frame LP."
+      },
+      {
+        "path": "research/complex-x4-frame-bound",
+        "delta": "Inherited model/method on an older word; unmodified source is explicitly pinned and credited."
+      },
+      {
+        "discussion": 1674,
+        "url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1674",
+        "delta": "Concurrent joint nested-endpoint/frame investigation changes the fixed-endpoint hypothesis; outside this audit and not obstructed by its theorem."
+      }
+    ],
+    "final_snapshot": {
+      "searched_at": "2026-10-14T06:45:47.158729+00:00",
+      "coverage": {
+        "open_prs": {
+          "fetched_at": "2026-10-14T06:44:12.165297+00:00",
+          "complete_pagination": true,
+          "records": 407
+        },
+        "discussions": {
+          "fetched_at": "2026-10-14T06:45:47.108825+00:00",
+          "complete_pagination": true,
+          "records": 332
+        }
+      },
+      "local_records": 710,
+      "warnings": [],
+      "limits": "Remote PR scope is open PRs including drafts. Closed work is searched through local READMEs, TASK metadata and ledger only. No code diffs or arbitrary package files are searched. Recheck relevant heads before submission.",
+      "terms": [
+        "uniform frame",
+        "optimal profile",
+        "concave",
+        "1671"
+      ]
+    }
+  },
+  "final_source_refresh": {
+    "main": "5e554ff58d01921747d27177045c0061f31e1ad1",
+    "predecessor_head": "ce130d291f5ab6dd801544886a16f62d42d86118",
+    "unchanged": [
+      "AGENTS.md",
+      "autoresearch.md",
+      "CONTRIBUTING.md",
+      "docs/research/agent-task-catalog.json",
+      "certificates/selected-result.json",
+      "research/complex-x4-frame-bound/model.py",
+      "research/gauge44-slots/construction/slots/SLOT-PINS-k8.json",
+      "research/r480-owner-optimum/inputs/local/FULL-WORD.json.gz"
+    ]
+  },
+  "validation": [
+    {
+      "command": "python3.12 -I -B scripts/research_package.py --package research/selected-k8-uniform-frame-audit",
+      "result": "PASS_REGISTERED_RESEARCH_PACKAGE outcome=completed; mathematical receipt plus all eight test groups; latest test-group wall time 21.433 seconds."
+    },
+    {
+      "command": "make selected-record-check",
+      "result": "PASS selected record, exact kappa, original source inventory and proof supplement."
+    },
+    {
+      "command": "python3.12 -I -O -B /path/to/pinned-pr1671/research/selected-k8-frame-ceiling/independent.py",
+      "result": "PASS_K8_FRAME_INDEPENDENT components=135 columns=23004 root_calibrations=72 graph_and_duality_match=True. Exact PR1671 package exported by git archive and replayed separately; not imported by the new checker."
+    }
+  ],
+  "receipt_sha256": "859fcb8c40601ce3a1d453b5703f20268c5bfab2228aac8484e1cbba47aea703",
+  "validation_environment": {
+    "python": "CPython 3.12.12",
+    "platform": "macOS 26.5.2 arm64",
+    "dependencies": "standard library only"
+  }
+}
diff --git a/research/selected-k8-uniform-frame-audit/VERIFY.json b/research/selected-k8-uniform-frame-audit/VERIFY.json
new file mode 100644
index 0000000000..9e7b16e9a8
--- /dev/null
+++ b/research/selected-k8-uniform-frame-audit/VERIFY.json
@@ -0,0 +1,33 @@
+{
+  "schema_version": 1,
+  "status": "ready",
+  "python": "3.12",
+  "requirements": [],
+  "inputs": [
+    "research/complex-x4-frame-bound/model.py",
+    "research/gauge44-slots/construction/slots/SLOT-PINS-k8.json",
+    "research/r480-owner-optimum/inputs/local/FULL-WORD.json.gz"
+  ],
+  "commands": [
+    {
+      "argv": [
+        "{python}",
+        "-I",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 120,
+      "checks": "Complete source-bound graph, two assemblies of every LP column, exact objective identities, uniform rational Bernstein/square signs, boundary counterexamples and deterministic receipt."
+    },
+    {
+      "argv": [
+        "{python}",
+        "-I",
+        "-B",
+        "{package}/test_package.py"
+      ],
+      "timeout_seconds": 300,
+      "checks": "Independent integer-root point calibration, Bernstein identity, dual/objective/coverage controls, source and receipt corruption, optimized read-only relocation and regeneration."
+    }
+  ]
+}
diff --git a/research/selected-k8-uniform-frame-audit/test_package.py b/research/selected-k8-uniform-frame-audit/test_package.py
new file mode 100644
index 0000000000..46dc5b83a8
--- /dev/null
+++ b/research/selected-k8-uniform-frame-audit/test_package.py
@@ -0,0 +1,216 @@
+#!/usr/bin/env python3
+# SPDX-License-Identifier: Apache-2.0
+"""Mathematical failure controls and source/receipt/relocation checks."""
+import copy
+from fractions import Fraction as Q
+import importlib.util
+import json
+from math import comb
+from pathlib import Path
+import shutil
+import subprocess
+import sys
+import tempfile
+import unittest
+from unittest.mock import patch
+
+HERE = Path(__file__).resolve().parent
+spec = importlib.util.spec_from_file_location('uniform_audit', HERE / 'verify.py')
+V = importlib.util.module_from_spec(spec)
+spec.loader.exec_module(V)
+
+
+class MathematicalChecks(unittest.TestCase):
+    @classmethod
+    def setUpClass(cls):
+        cls.module, cls.word, cls.dual = V.source_inputs()
+        cls.model = cls.module.Model(cls.word)
+        cls.histogram, _, _, _ = V.audit_lp(cls.module, cls.model, cls.dual)
+
+    def test_power_prices_by_independent_integer_roots(self):
+        # No logarithms, Taylor coefficients or Bernstein basis in this oracle.
+        scale = 1 << 96
+        for denominator in (32, 64, 128):
+            prices = {}
+            for d in V.RANKS:
+                radicand = d**(denominator-1) * scale**denominator
+                root = V.root_floor(radicand, denominator)
+                self.assertLessEqual(root**denominator, radicand)
+                self.assertGreater((root+1)**denominator, radicand)
+                prices[d] = (Q(root, scale)-d, Q(root+1, scale)-d)
+            for vector in self.histogram:
+                if vector == V.ZERO:
+                    continue
+                lower = sum(v*prices[d][0 if v > 0 else 1]
+                            for d, v in zip(V.RANKS, vector))
+                self.assertGreater(lower, 0, (denominator, vector))
+                V.uniform_certificate(vector)
+        # The exact square is positive, but reversing it must be rejected.
+        with self.assertRaisesRegex(ValueError, 'Bernstein positivity'):
+            V.uniform_certificate(tuple(-x for x in V.SQUARE))
+        # The first-order slope of this square is zero, not a strict margin.
+        self.assertEqual(V.uniform_certificate(V.SQUARE)['proof'], '4*(1-2^-a)^2')
+        with self.assertRaisesRegex(ValueError, 'alternating-series range'):
+            V.uniform_certificate(V.SQUARE, Q(1))
+
+    def test_bernstein_change_of_basis(self):
+        # Check exact polynomial identity for every nonspecial source vector.
+        for vector in self.histogram:
+            if vector in (V.ZERO, V.SQUARE):
+                continue
+            polynomial = V.slope_lower_polynomial(vector)
+            coefficients = V.bernstein(polynomial, V.A_MAX)
+            for t in (Q(0), Q(2, 7), Q(1)):
+                a = t*V.A_MAX
+                direct = sum(c*a**i for i, c in enumerate(polynomial))
+                bernstein = sum(c*comb(8, i)*t**i*(1-t)**(8-i)
+                                for i, c in enumerate(coefficients))
+                self.assertEqual(direct, bernstein)
+        # Deliberately omit the interval scaling: the identity must detect it.
+        polynomial = [Q(1), Q(-2), Q(3)]
+        wrong = V.bernstein(polynomial, Q(1))
+        t = Q(2, 7)
+        expected = sum(c*(t*V.A_MAX)**i for i, c in enumerate(polynomial))
+        self.assertNotEqual(expected, sum(c*comb(2, i)*t**i*(1-t)**(2-i)
+                                         for i, c in enumerate(wrong)))
+
+    def test_claim_boundaries(self):
+        vector = tuple(map(Q, (0, 8, 1, -4, 0, 0, 0, 0)))
+        self.assertIn(vector, self.histogram)
+        lo, hi = map(Q, V.power_boundary(vector))
+        self.assertLess(lo, hi)
+        self.assertLess(hi, 0)
+        with self.assertRaisesRegex(ValueError, 'Bernstein positivity'):
+            V.uniform_certificate(vector, Q(1, 20))
+        vector = tuple(map(Q, (-3, 1, 0, 0, 0, 0, 0, 0)))
+        f = [min(d, 2) for d in range(10)]
+        self.assertTrue(all(2*f[d] >= f[d-1]+f[d+1] for d in range(1, 9)))
+        self.assertEqual(sum(v*(f[d]-d*f[1]) for d, v in zip(V.RANKS, vector)), -1)
+        fixture = V.alternative_optimum(self.model)
+        self.assertNotEqual(fixture['before'], fixture['after'])
+        self.assertEqual(fixture['profile'], {str(r): n for r, n in V.PROFILE.items()})
+
+    def test_dual_objective_and_coverage_mutations(self):
+        corrupted = copy.deepcopy(self.dual)
+        normalization = json.dumps(('N', self.model.components()[0][0]))
+        values = corrupted['components'][0]['duals'].setdefault(normalization, {})
+        values['2'] = str(Q(values.get('2', '0')) + 1)
+        with self.assertRaisesRegex(ValueError, 'symbolic objective mismatch'):
+            V.audit_lp(self.module, self.model, corrupted)
+        missing = copy.deepcopy(self.dual)
+        missing['components'].pop()
+        with self.assertRaisesRegex(ValueError, 'component coverage'):
+            V.audit_lp(self.module, self.model, missing)
+        unknown = copy.deepcopy(self.dual)
+        unknown['components'][0]['duals']['unknown-row'] = {'2': '1'}
+        with self.assertRaisesRegex(ValueError, 'unknown dual row'):
+            V.audit_lp(self.module, self.model, unknown)
+
+    def test_second_column_assembly_and_graph_mutations(self):
+        original = self.module.lp
+        def missing_column(*args):
+            rows, rhs, columns = original(*args)
+            return rows, rhs, columns[:-1]
+        with patch.object(self.module, 'lp', missing_column):
+            with self.assertRaisesRegex(ValueError, 'two column assemblies disagree'):
+                V.audit_lp(self.module, self.model, self.dual)
+        model = copy.copy(self.model)
+        model.edges = dict(model.edges)
+        model.edges.pop(next(iter(model.edges)))
+        with self.assertRaisesRegex(ValueError, 'complete graph binding'):
+            V.graph_checks(model)
+        model = copy.copy(self.model)
+        model.domain = dict(model.domain)
+        node = next(iter(model.domain))
+        model.domain[node] = model.domain[node][:-1]
+        with self.assertRaisesRegex(ValueError, 'complete graph binding'):
+            V.graph_checks(model)
+        self.assertEqual(V.graph_checks(self.model), 5586)
+
+
+class PackageChecks(unittest.TestCase):
+    def setUp(self):
+        self.temp = tempfile.TemporaryDirectory(prefix='k8-uniform-audit-')
+        self.root = Path(self.temp.name)
+        self.package = self.root / 'research' / HERE.name
+        shutil.copytree(HERE, self.package, ignore=shutil.ignore_patterns('__pycache__'))
+        for path in V.INPUTS:
+            dest = self.root / path
+            dest.parent.mkdir(parents=True, exist_ok=True)
+            shutil.copyfile(V.ROOT / path, dest)
+
+    def tearDown(self):
+        for path in self.root.rglob('*'):
+            path.chmod(0o755 if path.is_dir() else 0o644)
+        self.root.chmod(0o755)
+        self.temp.cleanup()
+
+    def invoke(self, *args):
+        return subprocess.run([sys.executable, '-I', '-O', '-B', str(self.package / 'verify.py'), *args],
+                              cwd=self.root, text=True, capture_output=True, timeout=90)
+
+    def snapshot(self):
+        return {str(p.relative_to(self.root)): p.read_bytes()
+                for p in self.root.rglob('*') if p.is_file()}
+
+    def test_optimized_readonly_relocation_and_regeneration(self):
+        before = self.snapshot()
+        regenerated = self.invoke('--write')
+        self.assertEqual(regenerated.returncode, 0, regenerated.stderr)
+        self.assertEqual(before, self.snapshot())
+        for path in self.root.rglob('*'):
+            path.chmod(0o555 if path.is_dir() else 0o444)
+        self.root.chmod(0o555)
+        result = self.invoke()
+        self.assertEqual(result.returncode, 0, result.stderr)
+        self.assertIn('PASS_SELECTED_K8_UNIFORM_FRAME_AUDIT', result.stdout)
+        self.assertEqual(before, self.snapshot())
+
+    def test_receipt_mutations_and_missing_receipt(self):
+        path = self.package / 'RESULT.json'
+        original = path.read_bytes()
+        for change in ('missing_vector', 'false_interval', 'bool_for_int'):
+            result = V.parse(original)
+            if change == 'missing_vector':
+                result['residual_proofs'].pop()
+            elif change == 'false_interval':
+                result['a_interval'][1] = '1/20'
+            else:
+                result['residual_proofs'][0]['columns'] = True
+            path.write_text(json.dumps(result))
+            run = self.invoke()
+            self.assertNotEqual(run.returncode, 0, change)
+            self.assertIn('result receipt mismatch', run.stderr)
+        path.unlink()
+        self.assertNotEqual(self.invoke().returncode, 0)
+        with self.assertRaisesRegex(ValueError, 'duplicate JSON key'):
+            V.parse('{"x":1,"x":2}')
+        with self.assertRaisesRegex(ValueError, 'noninteger JSON number'):
+            V.parse('{"x":NaN}')
+
+    def test_source_pin_and_dual_corruption(self):
+        model = self.root / V.MODEL
+        original = model.read_bytes()
+        model.write_bytes(original + b'\n# drift\n')
+        run = self.invoke()
+        self.assertNotEqual(run.returncode, 0)
+        self.assertIn('live source SHA256', run.stderr)
+        model.write_bytes(original)
+        path = self.package / 'SOURCES.json'
+        original = path.read_bytes()
+        source = V.parse(original)
+        source['files'].pop()
+        path.write_text(json.dumps(source))
+        run = self.invoke()
+        self.assertNotEqual(run.returncode, 0)
+        self.assertIn('source inventory', run.stderr)
+        path.write_bytes(original)
+        dual = self.package / 'DUALS.json.gz'
+        dual.write_bytes(dual.read_bytes()[:-1])
+        run = self.invoke()
+        self.assertNotEqual(run.returncode, 0)
+        self.assertIn('dual source SHA256', run.stderr)
+
+
+if __name__ == '__main__':
+    unittest.main(verbosity=2)
diff --git a/research/selected-k8-uniform-frame-audit/verify.py b/research/selected-k8-uniform-frame-audit/verify.py
new file mode 100644
index 0000000000..3f88af33a9
--- /dev/null
+++ b/research/selected-k8-uniform-frame-audit/verify.py
@@ -0,0 +1,434 @@
+#!/usr/bin/env python3
+# SPDX-License-Identifier: Apache-2.0
+"""Uniform power-cost audit of Gareth Davidson's PR1671 symbolic duals.
+
+The source-bound event/domain model is Aaron Wang/navinor's retained X4
+implementation. Two column assemblies below share that model. The new
+arithmetic proof imports neither PR1671's numerical checker nor a solver.
+Ross Richardson, with substantial OpenAI Codex assistance.
+"""
+import argparse
+from collections import Counter, defaultdict
+from fractions import Fraction as Q
+from functools import lru_cache
+import gzip
+import hashlib
+import json
+from math import comb, factorial
+from pathlib import Path
+import types
+
+HERE = Path(__file__).resolve().parent
+ROOT = HERE.parents[1]
+BASE = '418e40eb2572d930b58c1cf9b82b41c0fc7ee08d'
+HEAD = 'ce130d291f5ab6dd801544886a16f62d42d86118'
+WORD_SHA = 'c2b294300760e1fd6eeab8c22c4d13e4633dca40e52cac8da0d68163a76e3ca8'
+MODEL = 'research/complex-x4-frame-bound/model.py'
+WORD = 'research/r480-owner-optimum/inputs/local/FULL-WORD.json.gz'
+PINS = 'research/gauge44-slots/construction/slots/SLOT-PINS-k8.json'
+INPUTS = {MODEL, WORD, PINS}
+PROFILE = {1: 2412, 2: 418, 3: 432, 4: 142, 5: 82, 8: 8}
+RANKS = tuple(range(2, 10))
+ZERO = (Q(0),) * 8
+SQUARE = (Q(-4), Q(0), Q(1), Q(0), Q(0), Q(0), Q(0), Q(0))
+A_MAX = Q(1, 32)
+GRAPH = {
+    'nodes': 'a5dfe9d076d0a56f20c6eeb5141839a5d3fec0d0e2727d9012bb70d1259de219',
+    'domains': 'a0592d32ef9cfbcc272ddc82a6fc4f6ac8b87e721ff9ac92a8c7ad15a65513be',
+    'edges': 'a4ff296752a5697f574fb55fe99d3016be9d1d73873321ba9b2cd9bbfbe67edd',
+    'cones': 'f844c0e7e667935050e02beb151b0cb9a5b45fc912ea436afc7158c425814661',
+}
+
+
+def need(ok, message):
+    if not ok:
+        raise ValueError(message)
+
+
+def parse(raw):
+    def pairs(items):
+        result = {}
+        for key, value in items:
+            need(key not in result, 'duplicate JSON key')
+            result[key] = value
+        return result
+    def bad(value):
+        raise ValueError('noninteger JSON number: ' + value)
+    return json.loads(raw, object_pairs_hook=pairs, parse_float=bad, parse_constant=bad)
+
+
+def canonical(obj):
+    return json.dumps(obj, sort_keys=True, separators=(',', ':'), allow_nan=False).encode()
+
+
+def digest(obj):
+    return hashlib.sha256(canonical(obj)).hexdigest()
+
+
+def source_inputs():
+    source = parse((HERE / 'SOURCES.json').read_bytes())
+    need(source['base_commit'] == BASE, 'source base')
+    entries = source['files']
+    provenance = {'certificates/selected-result.json', 'docs/research/agent-task-catalog.json'}
+    need(len(entries) == len(INPUTS | provenance) and
+         {r['path'] for r in entries} == INPUTS | provenance, 'source inventory')
+    for row in entries:
+        path = row['path']
+        need(row['usage'] == ('input' if path in INPUTS else 'provenance'), 'source usage')
+        if path in INPUTS:
+            raw = (ROOT / path).read_bytes()
+            need(hashlib.sha256(raw).hexdigest() == row['sha256'], 'live source SHA256')
+            blob = hashlib.sha1(b'blob ' + str(len(raw)).encode() + b'\0' + raw).hexdigest()
+            need(blob == row['git_blob'], 'live source Git blob')
+    predecessor = source['predecessor']
+    need(predecessor['pr'] == 1671 and predecessor['head'] == HEAD, 'predecessor head')
+    dual_pin = [r for r in predecessor['files'] if r['path'].endswith('/DUALS.json.gz')]
+    need(len(dual_pin) == 1, 'dual source inventory')
+    raw = (HERE / 'DUALS.json.gz').read_bytes()
+    need(hashlib.sha256(raw).hexdigest() == dual_pin[0]['sha256'], 'dual source SHA256')
+    blob = hashlib.sha1(b'blob ' + str(len(raw)).encode() + b'\0' + raw).hexdigest()
+    need(blob == dual_pin[0]['git_blob'], 'dual source Git blob')
+    dual = parse(gzip.decompress(raw))
+    need(dual['schema'] == 'selected-k8-frame-duals-v1' and
+         dual['word_sha256'] == WORD_SHA, 'dual word binding')
+    raw = gzip.decompress((ROOT / WORD).read_bytes())
+    pins = parse((ROOT / PINS).read_bytes())
+    need(hashlib.sha256(raw).hexdigest() == WORD_SHA == pins['word_sha256'], 'selected word binding')
+    word = parse(raw)
+    need(word['report']['R'] == 480 and word['report']['v'] == 112 and word['report']['h'] == 9,
+         'selected word dimensions')
+    need({int(r): n for r, n in word['report']['local_profile'].items()} == PROFILE,
+         'selected word profile')
+    model_module = types.ModuleType('retained_navinor_model')
+    model_module.__file__ = str(ROOT / MODEL)
+    # Frozen predecessor assertions stay enabled even under an optimized caller.
+    exec(compile((ROOT / MODEL).read_bytes(), str(ROOT / MODEL), 'exec', optimize=0),
+         model_module.__dict__)
+    return model_module, word, dual
+
+
+@lru_cache(None)
+def span(frame):
+    result = {0}
+    for vector in frame:
+        result |= {x ^ vector for x in result}
+    return sum(1 << x for x in result)
+
+
+def nested(left, right):
+    return span(left) & ~span(right) == 0
+
+
+def graph_checks(model):
+    payloads = {
+        'nodes': [[list(n), span(model.lo[n]), span(model.hi[n])] for n in sorted(model.lo)],
+        'domains': [[list(n), sorted(span(f) for f in model.domain[n])] for n in sorted(model.domain)],
+        'edges': [[list(a), list(b), k] for (a, b), k in sorted(model.edges.items())],
+        'cones': [[k, span(f)] for k, f in sorted(model.ceil.items())],
+    }
+    need({k: digest(v) for k, v in payloads.items()} == GRAPH, 'complete graph binding')
+    for node, domain in model.domain.items():
+        k = len(model.hi[node]) - len(model.lo[node])
+        need(k in (1, 2, 3), 'quotient dimension')
+        need(len(domain) == len(set(domain)) == {1: 2, 2: 5, 3: 16}[k], 'complete subspace interval')
+        need(all(nested(model.lo[node], f) and nested(f, model.hi[node]) for f in domain),
+             'frame interval containment')
+    need(len(model.gates) == 5413 and len(model.domain) == 1741, 'gate coverage')
+    need(model.profile(model.baseline()) == PROFILE, 'literal baseline profile')
+    # Every register's expected dimension increments telescope, also in the LP.
+    mass = sum(len(model.hi[ch[-1]]) - len(model.lo[ch[0]]) for ch in model.chains.values())
+    mass += sum(model.centre_children)
+    need(mass == sum(r*n for r, n in PROFILE.items()) == 5586, 'fixed local mass')
+    return mass
+
+
+def dual_vectors(record, rows):
+    allowed = {json.dumps(r) for r in rows}
+    need(set(record['duals']) <= allowed, 'unknown dual row')
+    result = {}
+    for row in rows:
+        values = record['duals'].get(json.dumps(row), {})
+        need(all(d in {str(r) for r in RANKS} and type(v) is str for d, v in values.items()),
+             'dual coefficient domain')
+        result[row] = tuple(Q(values.get(str(d), '0')) for d in RANKS)
+    return result
+
+
+def direct_columns(model, component, dual):
+    """Reassemble from graph edges, without component_problem(), lp() or their costs.
+
+    Shared event/domain model; this is an independent column assembly, not an
+    independent implementation of the source word or its cone conditions.
+    """
+    members = set(component)
+    links = defaultdict(list)
+    for (left, right), multiplicity in model.edges.items():
+        if left in members:
+            links[left].append((left, right, multiplicity, 0))
+        if right in members:
+            links[right].append((left, right, multiplicity, 1))
+    result = {}
+    for node in component:
+        for frame in model.domain[node]:
+            cost = [0] * 10
+            residual = [-v for v in dual[('N', node)]]
+            for left, right, multiplicity, side in links[node]:
+                other = right if side == 0 else left
+                if other in members:
+                    q = dual[('M', left, right, side, frame)]
+                    residual = [a+b for a, b in zip(residual, q)]
+                else:
+                    before, after = ((frame, model.lo[other]) if side == 0
+                                     else (model.lo[other], frame))
+                    need(nested(before, after), 'direct unary nesting')
+                    jump = len(after) - len(before)
+                    if jump:
+                        cost[jump] += multiplicity
+            residual = tuple(residual[d-2] + cost[d] for d in RANKS)
+            result[('x', node, frame)] = (tuple(cost), residual)
+    for (left, right), multiplicity in model.edges.items():
+        if left not in members or right not in members:
+            continue
+        for before in model.domain[left]:
+            for after in model.domain[right]:
+                if not nested(before, after):
+                    continue
+                cost = [0] * 10
+                jump = len(after) - len(before)
+                if jump:
+                    cost[jump] = multiplicity
+                q0 = dual[('M', left, right, 0, before)]
+                q1 = dual[('M', left, right, 1, after)]
+                residual = tuple(cost[d] - q0[d-2] - q1[d-2] for d in RANKS)
+                result[('y', left, right, before, after)] = (tuple(cost), residual)
+    return result
+
+
+def audit_lp(module, model, data):
+    components = model.components()
+    need(len(data['components']) == len(components) == 135, 'complete component coverage')
+    histogram, stats, witnesses = Counter(), Counter(), {}
+    total = Counter(model.fixed_profile())
+    stream = hashlib.sha256()
+    for ci, (component, record) in enumerate(zip(components, data['components'])):
+        need(record['first'] == json.dumps(component[0]) and record['nodes'] == len(component),
+             'component identity')
+        labels, unary, pairs = model.component_problem(component)
+        rows, rhs, columns = module.lp(labels, unary, pairs)
+        dual = dual_vectors(record, rows)
+        table = {}
+        for key, cost, entries in columns:
+            residual = [Q(cost[d]) for d in RANKS]
+            for index, coefficient in entries:
+                residual = [a-coefficient*b for a, b in zip(residual, dual[rows[index]])]
+            need(key not in table, 'duplicate LP column')
+            vector = tuple(residual)
+            table[key] = (tuple(cost), vector)
+            histogram[vector] += 1
+            witnesses.setdefault(vector, {'component': ci, 'column': json.dumps(key)})
+            stream.update(canonical([ci, key, cost, list(map(str, vector))]) + b'\n')
+        need(table == direct_columns(model, component, dual), 'two column assemblies disagree')
+        objective = tuple(sum((b*dual[row][d-2] for row, b in zip(rows, rhs)), Q(0)) for d in RANKS)
+        baseline = module.assignment_cost(labels, unary, pairs,
+                                          {n: model.baseline()[n] for n in component})
+        need(objective == tuple(baseline[d] for d in RANKS), 'symbolic objective mismatch')
+        total.update({d: baseline[d] for d in range(1, 10) if baseline[d]})
+        stats.update(components=1, rows=len(rows), columns=len(columns))
+    need(dict(total) == PROFILE, 'full fixed and variable profile coverage')
+    need(dict(stats) == {'components': 135, 'rows': 17507, 'columns': 23004}, 'LP coverage')
+    need(len(histogram) == 239 and histogram[ZERO] == 16564, 'residual coverage')
+    return histogram, witnesses, dict(stats), stream.hexdigest()
+
+
+def dyadic_down(value, bits):
+    scale = 1 << bits
+    return Q((value.numerator * scale) // value.denominator, scale)
+
+
+@lru_cache(None)
+def log_bounds(n):
+    """Independent ln(n) enclosure by binary range reduction and atanh.
+
+    Remaining atanh tail after j terms is bounded by
+    z^(2j+1)/((2j+1)(1-z^2)); all computation is rational.
+    """
+    need(type(n) is int and 1 <= n <= 9, 'log domain')
+    def series(z):
+        need(0 <= z <= Q(1, 3), 'atanh domain')
+        if not z:
+            return Q(0), Q(0)
+        total, power, j = Q(0), z, 0
+        while True:
+            total += power / (2*j+1)
+            power *= z*z
+            j += 1
+            tail = power / ((2*j+1)*(1-z*z))
+            if tail < Q(1, 1 << 144):
+                return total, total+tail
+    k = n.bit_length()-1
+    base = 1 << k
+    l2, u2 = series(Q(1, 3))
+    lo, hi = series(Q(n-base, n+base))
+    return dyadic_down(2*k*l2+2*lo, 128), -dyadic_down(-2*k*u2-2*hi, 128)
+
+
+def slope_lower_polynomial(vector):
+    """Lower bound for sum v_d*d*(exp(-a ln d)-1)/a, a>0.
+
+    Nine exponential terms give a lower bound, eight give an upper bound.
+    Choose by the coefficient sign, then round each log power in the
+    direction appropriate for its signed polynomial coefficient.
+    """
+    result = [Q(0)] * 9
+    for d, weight in zip(RANKS, vector):
+        if not weight:
+            continue
+        terms = 9 if weight > 0 else 8
+        lo, hi = log_bounds(d)
+        for k in range(1, terms+1):
+            multiplier = Q((-1)**k) * weight*d / factorial(k)
+            result[k-1] += multiplier * (lo if multiplier > 0 else hi)**k
+    return result
+
+
+def bernstein(power_coefficients, endpoint):
+    n = len(power_coefficients)-1
+    return tuple(sum((power_coefficients[i] * endpoint**i * Q(comb(j, i), comb(n, i))
+                      for i in range(j+1)), Q(0)) for j in range(n+1))
+
+
+def uniform_certificate(vector, endpoint=A_MAX):
+    need(Q(0) < endpoint and endpoint*log_bounds(9)[1] < 1, 'alternating-series range')
+    need(len(vector) == 8, 'residual dimension')
+    if vector == ZERO:
+        return {'proof': 'identically-zero'}
+    if vector == SQUARE:
+        # 4*(4^-a-1) - 8*(2^-a-1) = 4*(1-2^-a)^2.
+        return {'proof': '4*(1-2^-a)^2'}
+    coefficients = bernstein(slope_lower_polynomial(vector), endpoint)
+    margin = dyadic_down(min(coefficients), 96)
+    need(margin > 0, 'uniform Bernstein positivity failed')
+    return {'proof': 'degree-8-Bernstein', 'slope_lower_bound': str(margin)}
+
+
+def root_floor(value, exponent):
+    """Integer-only root enclosure, used for the out-of-range control."""
+    need(type(value) is int and value >= 0 and type(exponent) is int and exponent > 0,
+         'root domain')
+    lo, hi = 0, 1 << ((value.bit_length()+exponent-1)//exponent)
+    while hi-lo > 1:
+        mid = (lo+hi)//2
+        if mid**exponent <= value:
+            lo = mid
+        else:
+            hi = mid
+    need(lo**exponent <= value < (lo+1)**exponent, 'integer root enclosure')
+    return lo
+
+
+def power_boundary(vector):
+    """Exact residual interval at a=1/20, after removing the positive 73^a."""
+    scale = 1 << 96
+    lower = upper = Q(0)
+    for d, weight in zip(RANKS, vector):
+        if not weight:
+            continue
+        radicand = d**19 * scale**20
+        integer = root_floor(radicand, 20)
+        lo, hi = Q(integer, scale)-d, Q(integer+1, scale)-d
+        lower += weight * (lo if weight > 0 else hi)
+        upper += weight * (hi if weight > 0 else lo)
+    need(upper < 0, 'power-boundary counterexample must be negative')
+    return [str(lower), str(upper)]
+
+
+def alternative_optimum(model):
+    """One distinct legal frame assignment, with exactly the same paid profile."""
+    baseline = model.baseline()
+    touching = defaultdict(list)
+    for (left, right), mult in model.edges.items():
+        touching[left].append((left, right, mult))
+        touching[right].append((left, right, mult))
+    def current(node):
+        return baseline.get(node, model.lo[node])
+    for node in sorted(model.domain):
+        for candidate in model.domain[node]:
+            if candidate == baseline[node]:
+                continue
+            change = Counter()
+            for left, right, mult in touching[node]:
+                before, after = current(left), current(right)
+                x = candidate if left == node else before
+                y = candidate if right == node else after
+                if not nested(x, y):
+                    break
+                old, new = len(after)-len(before), len(y)-len(x)
+                if old:
+                    change[old] -= mult
+                if new:
+                    change[new] += mult
+            else:
+                if not any(change.values()):
+                    altered = dict(baseline)
+                    altered[node] = candidate
+                    need(model.profile(altered) == PROFILE, 'alternative optimum full replay')
+                    return {'gate': list(node), 'before': list(baseline[node]),
+                            'after': list(candidate), 'profile': {str(r): n for r, n in PROFILE.items()}}
+    raise ValueError('no distinct optimum fixture found')
+
+
+def run():
+    module, word, duals = source_inputs()
+    model = module.Model(word)
+    mass = graph_checks(model)
+    histogram, witnesses, stats, columns_digest = audit_lp(module, model, duals)
+    proofs = []
+    by_kind = Counter()
+    for vector, count in sorted(histogram.items()):
+        proof = uniform_certificate(vector)
+        by_kind[proof['proof']] += count
+        proofs.append({'residual': list(map(str, vector)), 'columns': count, **proof})
+    concave_vector = (Q(-3), Q(1), Q(0), Q(0), Q(0), Q(0), Q(0), Q(0))
+    hinge = [min(r, 2) for r in range(10)]
+    concave_value = sum(v*(hinge[d]-d*hinge[1]) for d, v in zip(RANKS, concave_vector))
+    need(concave_vector in histogram and concave_value == -1, 'concave boundary fixture')
+    power_vector = (Q(0), Q(8), Q(1), Q(-4), Q(0), Q(0), Q(0), Q(0))
+    need(power_vector in histogram, 'power boundary source column')
+    boundaries = {
+        'all_concave': {'price': hinge, 'residual': list(map(str, concave_vector)),
+                        'value': str(concave_value), **witnesses[concave_vector]},
+        'a_one_twentieth': {'a': '1/20', 'residual': list(map(str, power_vector)),
+                           'value_interval': power_boundary(power_vector), **witnesses[power_vector]},
+        'meaning': 'The published dual fails outside the certified cone/range; neither fixture proves a better feasible frame assignment.',
+    }
+    return {
+        'schema': 'selected-k8-uniform-frame-audit-v1',
+        'status': 'PASS_SELECTED_K8_UNIFORM_FRAME_AUDIT',
+        'predecessor_head': HEAD, 'word_sha256': WORD_SHA, 'duals_payload_sha256': digest(duals),
+        'graph_sha256': GRAPH, 'column_stream_sha256': columns_digest,
+        'a_interval': ['0', str(A_MAX)], 'strict_interval': '0 < a <= 1/32',
+        'local_mass': mass, 'baseline_profile': {str(r): n for r, n in PROFILE.items()},
+        'lp': stats, 'distinct_residual_vectors': len(proofs),
+        'columns_by_proof': dict(sorted(by_kind.items())), 'residual_proofs': proofs,
+        'distinct_frame_same_profile': alternative_optimum(model),
+        'boundaries': boundaries,
+        'scope': 'Uniform fixed-word frame LP optimum and uniqueness of the optimal paid histogram. Shared pinned event/domain model; no physical supplier, new kappa or full multiplication theorem.',
+    }
+
+
+def main():
+    parser = argparse.ArgumentParser(description=__doc__)
+    parser.add_argument('--write', action='store_true', help='explicitly regenerate RESULT.json')
+    args = parser.parse_args()
+    result = run()
+    path = HERE / 'RESULT.json'
+    if args.write:
+        path.write_text(json.dumps(result, indent=2, sort_keys=True)+'\n')
+    else:
+        need(canonical(parse(path.read_bytes())) == canonical(result), 'result receipt mismatch')
+    print(result['status'], 'columns=23004 vectors=239 interval=0..1/32 optimal_profile_unique',
+          'no_new_kappa receipt='+digest(result))
+
+
+if __name__ == '__main__':
+    main()