Record identity and current filing

This is the filed page of the completed whole-claim report (working storage). It retains the report's mathematical assessment and limitations. It does not claim byte identity with that working report or constitute another review. The original working report remains preserved separately from this filing.

Documentary source-locator wording is normalized. The review and its distinct grading concern the exact assessed subjects identified below; they do not certify these locator labels or report fresh checks of the current pages.

Commissioning attribution: independent review by separate fresh-context reviewers, commissioned and read by the commissioning role. The distinct roles were blind reviewer, first-cycle grader, report writer, and second-cycle grader of the completed record. The commissioning role selected the subjects, wrote the instructions and read the outputs. This supplied attribution identifies the review roles; it is not a new mathematical verdict. The preparation of this page and the shared-harness adaptation is by the filing author, who was exposed to all those records, not an independent reviewer.

Within the retained assessment below, verify_quartic.py means the exact reviewer's checker. The current checker is a separately identified shared-harness adaptation. Its current review and execution standing is recorded in the verification index; the earlier mathematical verdict does not certify that adaptation. References to RUN_RECORD.txt mean the complete reported record retained in the "Reported execution record" section below.

The two documentary qualifications are explicit. First, the result page is the filed page for the exact reviewed proposal; the proposal was not filed unchanged. Second, seeds, C1, relation pairings, identifying box and cyclic order have input fields compared with reviewer-side constants. The row profile is tested directly against code constants, with no corresponding profile field in the input. Neither qualification changes the accepted nine-point mathematical subject.

The exact reviewed context remains available as the result, the source digest, the evidence account, the source transcription, and the proposed problem account. Except for the source transcription's disclosed provenance-only redaction and the identity edits of 2026-10-02 to the transcription and the evidence index (hash values replaced by paths, dates and removal markers), those snapshots keep original bytes and original link context. The verification index identifies both transcription versions; use the live owner pages for navigation. The author ../main.py and ../assets/witness.json as committed on the date named below are the files named in the subject list; the witness is unchanged since, and the live checker's later edit is stated on the owning evidence page. The earlier canonical E0097 context is wiki/problems/distance_problems/E0097/_index.md as it stood at 2026-09-09T21:17:39Z.

The review's post7604 reading depth stays unread. The subsequently filed mysticflounder transcription supports the current problem-page wording; it does not retrospectively extend this review. No numerical tier or catalog status is created by retaining these records.

Subject and independence

Reviewed with this repository as it stood at the filing of these paths on 2026-09-10; evidence/main.py and evidence/assets/witness.json carried their reviewed bytes then. The reviewed checker bytes are not retained (the evidence index states how today's file differs); the witness is unchanged since.

Frozen subject. Three files, named by path as they stood on 2026-09-10 and matched by the reviewer and again by the grader before any of this text was written. Paths are the canonical destinations under library/distance_problems/sallerk_2026_convex_nonagon_relations/; the reviewed bytes were a frozen proposal copy of those pages. The exact result is now retained as evidence/assets/reviewed_result.md; the current result page has documentary profile and standing corrections. The witness retains its exact reviewed bytes; the reviewed checker is evidence/main.py as committed on 2026-09-10 (the live file was edited after the review and the reviewed bytes are not retained; see the evidence index).

• library/distance_problems/sallerk_2026_convex_nonagon_relations/evidence/assets/reviewed_result.md
• library/distance_problems/sallerk_2026_convex_nonagon_relations/evidence/main.py
• library/distance_problems/sallerk_2026_convex_nonagon_relations/evidence/assets/witness.json

Context read alongside the subject, not part of the claim under review:

• _index.md, retained as reviewed_source_index.md
• sallerk_2026_convex_nonagon_relations.md; the original is not retained, its provenance-redacted derivative is reviewed_source.md
• evidence/_index.md, retained as reviewed_evidence_index.md
• wiki/problems/distance_problems/E0097/_index.md (proposal), retained as reviewed_problem.md

Also read: the current corpus page wiki/problems/distance_problems/E0097/_index.md (as it stood at 2026-09-09T21:17:39Z) and the canonical source PDF library/discrete_geometry/erdos_1987_combinatorial_metric_problems_geometry/erdos_1987_combinatorial_metric_problems_geometry.pdf, printed pp. 175-176, rendered at 150 dpi and read visually.

At the reviewed state, two internal pins in the subject were self-consistent: _INPUT_SHA256 at evidence/main.py:38 equals the actual witness.json hash, and the "executed checker SHA-256" recorded in evidence/_index.md equals the actual main.py hash.

Independence. The reviewer is distinct from the author and from every collaborator who constructed the subject, and worked in a fresh context that had not built on it. The reviewer did not read the author's handoff, replay record, staged check directory, or any earlier snapshot of the subject, opened no URLs, and did not execute the author's evidence/main.py (it was read, for the code review below). A grader distinct from both author and reviewer recorded the findings in the "Grader findings" section, having independently recomputed the seven SHA-256 values the report originally listed and found them matching, including both internal pins.

Standing-text exposure. The frozen subject library/distance_problems/sallerk_2026_convex_nonagon_relations/evidence/assets/reviewed_result.md as it stood on 2026-09-10 carried the author's standing section "Current verification record" (lines 177-188), and the commissioned context carried the author's execution record in evidence/assets/reviewed_evidence_index.md (lines 67-83) and one author-standing sentence each in evidence/assets/reviewed_problem.md (line 42) and evidence/assets/reviewed_source_index.md (line 22); a materiality grader (Claude Fable 5.1), distinct from the reviewer and both earlier graders, ruled this exposure immaterial under the content test on 2026-09-18: every passage says the standing is undetermined and awaiting review, none states or implies the verdict, and the review's reasoning rests on the reviewer's and grader's structurally independent reproductions rather than on the author's recorded run.

Independent code and rerun commands. The exact reviewer source is evidence/assets/reviewed_quartic.py. At this same directory depth its original default still resolves to evidence/assets/witness.json. The commands below name that exact input explicitly. From an ordinary clone:

uv run --no-sync python library/distance_problems/sallerk_2026_convex_nonagon_relations/evidence/assets/reviewed_quartic.py --input library/distance_problems/sallerk_2026_convex_nonagon_relations/evidence/assets/witness.json
uv run --no-sync python -O library/distance_problems/sallerk_2026_convex_nonagon_relations/evidence/assets/reviewed_quartic.py --input library/distance_problems/sallerk_2026_convex_nonagon_relations/evidence/assets/witness.json

These commands reproduce the original program, not the current evidence entry point. The complete historical record below reports exit zero in both modes and one summary line. Those are reviewer-reported executions; no fresh native run is asserted here. The exact snapshot needs the standard library only, performs no network access and writes no files. The current shared-harness entry point and its pending checks are documented in the evidence account.

Restatement

In the reviewer's own words, with every quantifier, hypothesis and scope qualification.

Definitions used. A finite set P of points in the plane is in strict convex position when every point of P is an extreme point of its convex hull and no point of P lies in the relative interior of a hull edge; equivalently, no redundant collinear boundary points. For v in P,

mu_P(v) = max over d > 0 of #{ w in P \ {v} : ||w - v||^2 = d },

the largest number of other points of P at one common distance from v. Property E_k means mu_P(v) >= k at every vertex, with the repeated distance allowed to depend on the vertex.

The objects. Let s = sqrt(3) > 0 and u = sqrt(5s - 8) > 0; both radicands are positive, since 3 > 64/25 gives 5s - 8 > 0. Let R be the counterclockwise rotation by 120 degrees,

R = [ -1/2  -s/2 ]
    [  s/2  -1/2 ]

and set, for i = 1, 2, 3,

A_i = R^(i-1) (1, 0),
B_i = R^(i-1) (s - 1/2, s/2),
C_i = R^(i-1) (x, y),   where
x = (8s - 11 + (s + 6) u) / 10,
y = (12 - s + (3 - 2s) u) / 10.

The nine points are P = {A_1, A_2, A_3, B_1, B_2, B_3, C_1, C_2, C_3}. The two coordinate denominators are the nonzero rationals 2 and 10. The branch taken is the one with +u, identified by the rational box 91/100 < x < 92/100, 98/100 < y < 1.

The assertion. For this one fixed P:

1. the nine points are pairwise distinct and lie in strict convex position, and the printed cycle A1, B1, C1, A2, B2, C2, A3, B3, C3 is their hull boundary traversed counterclockwise;

2. mu_P(v) = 3 at every one of the nine vertices — not merely at least three: exactly one distance value is attained three times from each vertex and no value is attained four or more times; and

3. P realizes the three distance relations printed in Er87b p. 175, in that printed order and with those printed pairings:

   textCopy

   A1A2 = A1A3 = A1B3,
   B1B2 = B1C2 = B1B3,
   C1C2 = C1A3 = C1C3.

Consequently P is a strictly convex E_3 witness of nine points, and, having multiplicity exactly three everywhere, it is emphatically not a counterexample to Problem 97, which asks for a vertex with no four other vertices equidistant from it.

Explicitly outside the claim. None of the following is asserted, and none is reviewed here:

• uniqueness of the completion (x, y) in the normalized labeled family;
• nonconvexity, or any other property, of the alternate -u branch;
• the degree-four assertion for the third orbit, or any minimal polynomial;
• the forum's mirror-symmetry exclusion theorem for D_m symmetry;
• the lower bound n_3 >= 7 and the resulting set {7, 8, 9};
• identification of these coordinates as Danzer's original choice, or a reconstruction of the printed Reuleaux-triangle existence construction;
• any resolution of Problem 97 or change to its imported status.

One wording note, not overreach. The page defines E_k with >= k, while its actual conclusion is the sharper mu_P(v) = 3. The certificate and both independent reproductions establish the sharper statement.

Checklist

An explicit verdict for every item of the audit checklist. Silence is not a verdict, so items that do not apply say why.

1. Quantifiers and scope — passes. The claim is a single existential statement about one fixed nine-point set, with no "almost all", no eventual or all-order distinction, no limit inferior or superior, and no exceptional set. The one quantifier that matters is "for every vertex", and it is discharged by enumerating all nine rows rather than by symmetry. The page's E_k definition uses >= k while the conclusion proves = 3; the stronger reading is the one certified. Nothing in the claim is stated for a family or a limit.

2. Circularity — passes. Nothing assumes the conclusion. The two completion equations are derived from the distance requirements on formal unknowns and are then checked on the resulting explicit coordinates; the convexity and multiplicity conclusions come from exhaustive exact comparison, not from the symmetry that motivated the construction. In particular the row maxima are established by comparing all eight distances at each vertex, not inferred from the advertised triples. There is no induction.

3. Model and convention changes — passes. The objects are the actual planar points; nothing is relaxed, averaged or abstracted. The one representation change is arithmetic: exact algebraic numbers are carried as coefficient tuples. The owner's checker verifies s^2 = 3 and u^2 = 5s - 8 inside its own model (main.py:236-239) and never assumes {1, s, u, su} is a linearly independent basis, using a zero tuple only in the sound direction (zero tuple implies zero value) and certifying every inequality by interval sign. The reviewer's model is a different one — a single-generator quartic field — and agrees term for term. The 120-degree rotation is the stated matrix, and the convention that indices run modulo three is used consistently.

4. Finite and statistical overreach — passes. The claim is finite and is proved finitely; no finite computation is extended to a universal statement. Nothing is sampled, averaged or estimated, so there is no question of correlated samples. The page states in its own words that the witness bears on Problem 97 only as an E_3 example, and both index pages and the problem proposal repeat that it establishes no lower bound, no counterexample and no status change.

5. Uniformity — inapplicable, because the claim contains no asymptotics, no error terms, no interchange of limits or sums, and no parameter family. Every quantity is a single algebraic number in a fixed field; there is no constant whose dependence could be misstated. For completeness, the only numerical parameters in either checker are refinement budgets (precision levels in the owner's main.py:37, a bisection cap in the reviewer's check), and both fail closed when exhausted rather than widening a claim.

6. Extremal conclusions — passes, in the narrow sense in which the claim makes one. The only extremal quantity is mu_P(v), the maximum multiplicity at a vertex, and it is taken in the proposition's own units (squared Euclidean distance) over a finite attained set, so existence and boundedness are automatic. The maximum is certified as exactly three at every vertex by comparing all 28 pairs in each row. No infimum, supremum or sharpness claim over a family is made — in particular the page does not claim nine is the least possible size, and holds n_3 >= 7 out as an unaccepted report.

7. Consequences and composition — passes, with one provenance qualification. Each "hence" was checked separately. The rotation identity ||v - Rv||^2 = ||v - R^2 v||^2 = 3||v||^2 makes the A-A, B-B and C-C legs automatic, so relation 1 reduces to the seed obligation A1B3^2 = 3, relation 2 to B1C2^2 = 3||B1||^2, and relation 3 to C1A3^2 = 3||C1||^2; the page is right that the first printed relation is an independent obligation on the six seeds and not a consequence of the two completion equations, and it is discharged exactly (A1 - B3 = (s/2, 3/2), squared norm 3/4 + 9/4 = 3). The elimination step is an equivalence, not just an implication, and uses division only by the nonzero rational 2. The bridge from 63 strictly positive supporting determinants to "nine distinct extreme vertices with no redundant collinear boundary points" is valid and is spelled out under Weakest steps. The qualification: the page's sentences "The unique triple in each row is as follows" and "Every other neighbor belongs to a singleton distance class" are true, but the owner's checker names only the row maximum as a check; see finding N1.

8. Computation — passes. Inputs are exact and pinned: witness.json is byte-pinned by SHA-256 in the checker (main.py:38, verified at main.py:210-214) and coordinates are parsed only as rational coefficient strings through fractions.Fraction (main.py:43), never evaluated as code. Arithmetic is exact; equality is a zero reduction and every strict sign is a certified rational interval, with no floating-point tolerance anywhere. Coverage is complete for the stated domain: 36 unordered distances, 63 supporting-edge signs, 252 within-row comparisons, nine rows, three named source relations. Failure cases are meaningful and exits are nonzero: the sign routine raises after its last precision level (main.py:111-121), the divider rejects a zero denominator (main.py:124-128), the radicand enclosure rejects a non-positive or misordered interval (main.py:79-80), and main.py:342-354 converts any of these into a recorded failed check and a nonzero exit, including under python -O, since no bare assert carries a theorem check. Exhausted numerical limits are never presented as certified enclosures. The reviewer's own check behaves the same way and was shown to do so by mutation (see RUN_RECORD.txt).

9. Reproduction — passes. The stated rerun commands in evidence/_index.md were checked for resolvability from an ordinary clone (input resolved relative to the script at main.py:210; dependencies are the standard library and the installed root tools package). The required computations were rerun rather than inferred from cached success — but by the reviewer's own structurally different check, not by replaying the author's script, which the reviewer deliberately did not execute. The retained reproduction is evidence/assets/reviewed_quartic.py with RUN_RECORD.txt; the reviewer's and grader's exploratory scripts in temporary storage are not the warrant and are not retained.

10. Source and verdict fidelity — passes. Er87b pp. 175-176 were read visually and print exactly the three relations with exactly those mixed terms A1B3, B1C2, C1A3, in that order, for the nonagon written in the cyclic order A1B1C1A2B2C2A3B3C3, and print no coordinates. The page's account of the printed existence construction, of the three-neighbor conjecture Danzer disproved, and of the separate four-neighbor question on p. 176 is faithful. The six A/B coordinates are attributed to the forum post and the third orbit to this compilation; Danzer's authorship of these particular coordinates is explicitly declined; the post's AI-assistance disclosure is preserved with the source. No source finding is strengthened anywhere in the three subject files, and the four separate forum claims are held out with their actual limits on the result page, the source index and the problem proposal.

Weakest steps

Three steps carry the argument. Each was rederived independently, in the reviewer's own field model, without substituting the page's answer and checking it. How they compose: step 1 turns the two distance requirements into a line; step 2 intersects that line with the circle and picks the branch, producing the coordinates; step 3 turns the resulting explicit algebraic numbers into the geometric conclusions. A failure in step 1 or 2 would mean the page's (x, y) does not satisfy the relations; a failure in step 3 would mean the point set, even if it satisfies the relations, is not a strictly convex nine-gon with multiplicity three. Steps 1 and 2 are also not load-bearing on their own: they motivate the coordinates, and the actual warrant is the direct exact verification of the defining equations and the relations on the fixed coordinates, which is what both checkers do.

Step 1 — elimination to the line. Writing q = x^2 + y^2, the C/A condition ||C1 - A3||^2 = ||C1 - C2||^2 expands to q + x + sy + 1 = 3q, i.e. 2q = x + sy + 1, which is the circle with centre h = (1/4, s/4) and squared radius 3/4 (completing the square: 1/2 + 1/16 + 3/16 = 3/4). The B/C condition ||B1 - C2||^2 = 12 - 3s expands to q + 4 - s + (s-2)x + 3y = 12 - 3s, using (2s-1)s = 6 - s, i.e. q + (s-2)x + 3y + 2s - 8 = 0. The reviewer set C1 = (X, Y) as formal symbols over the field, built C2 = R C1 symbolically, and formed both relations from scratch; both came out with monomial support {1, X, Y, X^2, Y^2} and matched the page's expansions. Eliminating the quadratic part gives a purely linear relation which is exactly one half of the page's line

(2s - 3)x + (s + 6)y + 4s - 15 = 0,

with coefficients x: s - 3/2, y: (s+6)/2, constant (4s-15)/2. (The reviewer's first write-up said one tenth; that was a prose slip in the reported scalar, corrected here — see grader correction (b). The line itself, and every downstream conclusion, is unaffected, since the two differ by a nonzero rational factor.) The converse direction holds too: the circle equation is an equivalence with the C/A condition, and the line is exactly twice the B/C expression after substituting q = (x + sy + 1)/2, so the pair is equivalent to the two distance conditions. Only division by the nonzero rational 2 is used; there is no hidden division by a possibly-zero quantity.

Step 2 — the quadratic and the branch choice. The page's route is the perpendicular foot H = h + ((15-6s)/60)(a, b) with a = 2s-3, b = s+6; the reviewer confirmed a^2 + b^2 = (21-12s) + (39+12s) = 60, `(a,b) . h = (2s-3)/4

• s(s+6)/4 = 2s, H_x = (48s-66)/60 = (8s-11)/10, H_y = (72-6s)/60 = (12-s)/10, and the substitution 60t^2 = 3/4 - (15-6s)^2/60with(15-6s)^2 = 333 - 180s, giving 3600t^2 = 180s - 288, i.e. 100t^2 = 5s - 8. Independently, the reviewer inverted the line's x-coefficient in the field by 4x4 rational linear algebra, solved for xin terms ofy, substituted into the circle, and obtained a quadratic in ywhose coefficients lie inQ(sqrt 3)`, namely, up to an overall sign,

  A = -280 - 160 s, B = 576 + 328 s, C = -306 - 162 s,

with discriminant D = B^2 - 4AC = 768 + 576 s, certified strictly positive. (The reviewer's first write-up rendered this quadratic with garbled rational coefficients; corrected here — see grader correction (c). The quadratic itself and its roots were right.) The page's y is an exact root of it, the line then recovers the page's x exactly, and the second root is the other branch. So the third orbit's coordinates are exactly the printed ones. The branch choice t = u/10 > 0 is a choice, not a uniqueness claim, and the page says so; the rational identifying box does separate the branches, since the chosen branch has x = 0.913916..., y = 0.989083... (truncated, not rounded) while the other has x' ~ -0.3426, y' ~ 1.0645, far outside the box. Since the page asserts only the existence of one witness and defers uniqueness and the other branch to separate unaccepted reports, the branch choice creates no gap.

Step 3 — the sign certification of convexity and distinctness. The bridge is: for each directed edge P_i P_{i+1} of the printed cycle, the determinant with each of the other seven vertices is strictly positive; hence the line through P_i and P_{i+1} is a supporting line meeting the set exactly in {P_i, P_{i+1}}, so that edge is exposed; the nine exposed edges close up into a strictly convex nine-gon; and strictness excludes any third point on an edge line, so there are no redundant collinear boundary points. Combined with all 36 squared distances strictly positive, the nine points are distinct and all nine are extreme. This inference is valid, and the reviewer confirmed the same conclusion by a structurally different route: an exact convex hull computed by Andrew's monotone chain, with lexicographic comparisons done in the field (needed, since A2 and A3 share x = -1/2) and collinear points dropped by popping on non-positive cross products. The hull came back with exactly nine vertices which, rotated to start at A1, are A1, B1, C1, A2, B2, C2, A3, B3, C3 — the page's order, not its reverse. Margins are comfortable: the smallest of the 63 determinants is about 0.213 and the smallest squared distance about 0.116, so nothing is near-degenerate and no sign is decided at the edge of the certification budget.

Strongest attack

The strongest available refutation was an attack on the third orbit itself: if the page's (x, y) were a mis-simplified or wrong-branch root — the most likely way a two-radical hand derivation goes wrong — then either a relation would fail, or the point would fall outside convex position, or a fourth equidistant neighbor would appear somewhere, and the author's checker could still pass if it shared the derivation's error. The attack was mounted in three ways.

First, derive the third orbit from scratch and compare, rather than substituting the page's formula. Setting C1 = (X, Y) formally and carrying the elimination, the quadratic in Y and the branch selection through independently, the reviewer obtained the page's (x, y) character for character, and obtained the other root explicitly. The attack failed: there is no third possibility, and the printed branch is the one inside the printed box.

Second, look for a fourth equidistant neighbor. If the construction were an E_4 counterexample in disguise, or if some row had two triples, the page's "unique triple" sentence and the "not a counterexample to Problem 97" sentence would both be wrong. All 36 squared distances were computed exactly and every row of eight was partitioned into exact equality classes with every cross-class inequality certified. Every row has profile [1,1,1,1,1,3]: one triple, five singletons, no quadruple anywhere. The attack failed, and in the direction that strengthens the page rather than weakening it.

Third, attack the arithmetic rather than the mathematics: if the author's reduction table for s^2 = 3 and u^2 = 5s - 8, or his square-root interval endpoints, were wrong, every conclusion would be suspect. The reviewer verified the reduction table term by term against the expansion of `(a + bs + cu + dsu)(e

• fs + gu + hsu)` and both directions of the integer square-root bounds (see the code review), and then, more decisively, redid every computation in an arithmetic model with a different reduction rule and a different sign oracle, obtaining the same answers. The attack failed.

Two smaller probes also failed to find anything. Checking whether the page overstates its own source: it does not — the reviewer independently computed the minimal polynomial of y and found the page's caution about the reported degree-four polynomial to be conservative rather than mistaken. And checking whether the identifying box could admit the wrong branch: it cannot, as the second root's coordinates lie well outside it.

No refutation succeeded, and no material defect was found.

Independent reproduction

The retained reproduction is evidence/assets/reviewed_quartic.py, 199 lines of standard-library Python. Its runs are recorded in RUN_RECORD.txt.

The structurally different primitive. The author models every quantity as a 4-tuple of rationals over the two radicals (1, s, u, s*u), reduces products by the two rules s^2 = 3 and u^2 = 5s - 8, and certifies strict signs by outward interval arithmetic built from nested integer-square-root enclosures of s and then of 5s - 8. The reviewer instead observed that u^2 = 5s - 8 gives (u^2 + 8)^2 = 75, so u is a root of m(t) = t^4 + 16t^2 - 11 and s = (u^2 + 8)/5; the whole configuration therefore lives in the single-generator quartic field K = Q[t]/(m). Elements are degree-at-most-three rational polynomials in t with the single reduction rule t^4 = 11 - 16t^2 (hence t^5 = 11t - 16t^3, t^6 = 267t^2 - 176), and s is recovered as (t^2 + 8)/5. Every strict sign is certified by exact bisection of an isolating interval for the real root of m: m(0) = -11 < 0, m(1) = 6 > 0, and m'(t) = 4t^3 + 32t > 0 for t > 0, so the positive root is unique and lies in (0, 1); candidate expressions are bounded by monomial interval evaluation on the current interval and the interval is halved until the bound is strictly one-sided, under a hard cap that raises rather than accepting.

Why it is structurally different, and why a shared bug is implausible. The two models differ in their generators (two radicals versus one), in their reduction rules (two rules versus one), in the shape of their canonical forms, and — most importantly — in their sign oracles: square-root enclosures of two correlated radicals versus bisection of a single polynomial's root interval. A transposed coefficient in the author's mul table, or an endpoint-rounding error in his root_bounds, has no counterpart in a model that never extracts a square root and never multiplies two independently enclosed radicals. Conversely a reduction error in t^4 = 11 - 16t^2 would produce different numbers, not the same ones. Soundness of the reviewer's model needs no irreducibility assumption: each element is a rational polynomial evaluated at a real number, so a zero coefficient tuple proves the real value is zero, and a nonzero value is accepted only against a strictly one-sided rational enclosure. (For the record m is irreducible over Q: no rational root among the divisors of 11, and a factorization (t^2 + at + b)(t^2 - at + c) forces either a = 0 with b + c = 16, bc = -11 and discriminant 300, not a square, or c = b with b^2 = -11.)

What the reproduction established. Working in K:

• s^2 = 3 and u^2 = 5s - 8 hold exactly in the model, with both radicals certified positive.
• The six A/B seeds reproduce, character for character, the six coordinates the forum post prints, and R^3 = I holds on each orbit; A2 = (-1/2, s/2), A3 = (-1/2, -s/2), B2 = (-s/2 - 1/2, 3/2 - s/2), B3 = (1 - s/2, -3/2).
• The third orbit was derived, not substituted, as described under Weakest steps, and equals the page's (x, y); the page's coordinates are exact roots of both the circle and the line, and lie in the identifying box 91/100 < x < 92/100, 98/100 < y < 1, certified with strict signs.
• The first Er87b relation is a pure seed identity, A1A2^2 = A1A3^2 = A1B3^2 = 3; ||B1||^2 = 4 - s, so the B-orbit sides are 12 - 3s; and, with the derived C1, C1C2^2 = C1A3^2 = C1C3^2 = 3q and B1B2^2 = B1C2^2 = B1B3^2 = 12 - 3s. All three printed relations reduce to exact zeros in the printed order and with the printed pairings.
• All 36 unordered squared distances are strictly positive, so the nine points are distinct; all 63 supporting-edge determinants of the printed cycle are strictly positive, so the cycle is a strictly convex nonagon with no redundant collinear boundary point; and an exact monotone-chain hull returns exactly nine vertices in exactly the printed counterclockwise order.
• Every row of eight distances has profile [1,1,1,1,1,3]. The triples are A_i : {A_{i+1}, A_{i+2}, B_{i+2}} at squared distance 3; B_i : {B_{i+1}, B_{i+2}, C_{i+1}} at 12 - 3s; and C_i : {C_{i+1}, C_{i+2}, A_{i+2}} at 3q = -3/5 + 3s + 3su/5, confirmed as an exact identity. This matches the page's table under its stated modulo-three convention, including the C-row value.
• Margins: smallest supporting determinant about 0.213, smallest squared distance about 0.116. The retained check needs only 8 bisection refinements in total against a cap of 400, so no sign is decided near the budget.

Adversarial cross-check, recorded but not part of the claim. The reviewer computed the minimal polynomial of y over Q by exact linear algebra on 1, y, ..., y^4: 200y^4 - 960y^3 + 3108y^2 - 4212y + 1863 = 0, with no relation of degree 1, 2 or 3. The forum's reported `1600y^4 - 7680y^3 + 24864y^2 - 33696y

• 14904is exactly eight times that and does annihilatey. So the page's transcription of the reported polynomial is accurate and the degree-four assertion is in fact true; the page's refusal to accept it without a discriminant and field-degree argument is conservative, not wrong. For completeness, xsatisfies200x^4 + 880x^3 + 1212x^2 - 1364x - 577 = 0`. None of this is part of the accepted claim.

Coverage and failure behavior of the retained check. verify_quartic.py records 21 named obligations covering the seeds and C1 against the expected rational 4-tuples, the radical identities, the rotation orbits with R^3 = I, the circle and line equations, the identifying box, the three source relations, the 36 distances, the 63 supporting determinants and the nine row profiles. Two deliberate design choices answer findings below. First, every value that fixes what is being asserted is a reviewer-side constant written into the check itself, not a value read from the input: the six seeds and C1, the printed cyclic order, the three Er87b pairings, the identifying box 91/100 < x < 92/100, 98/100 < y < 1, and the required row profile [1,1,1,1,1,3]. The input's seeds, C1, cyclic order, relation pairings and identifying box are read and must equal the corresponding constants. The full row profile is asserted directly against code constants; there is no corresponding profile field in the input. The geometry is checked against those fixed obligations, so the checked property is the printed finite theorem. (An earlier revision of this check read the pairings and the box from the input; the grader showed that two mutations then passed — repeating one pair inside each relation triple, and widening the box to [-100, 100]^2 — and both now exit 1.) Second, the row obligation asserts the full profile, not merely the maximum.

Negative controls recorded in RUN_RECORD.txt confirm real failure modes. Perturbing the u-part of C1's y, corrupting a seed coefficient, reversing the cyclic-order field, repointing a relation pair, shifting the identifying box, repeating a pair inside each relation triple, and widening the box to [-100, 100]^2 each fail with exit code 1, in plain and optimized Python alike. Transposing two labels in the reviewer-side cycle makes the supporting-edge obligation fail, so the convexity check has a real failure mode. Lowering the bisection cap to zero raises "bisection cap exhausted; no sign accepted" and exits 1, so exhausted refinement never masquerades as a certified enclosure.

Code and input review

Overall. evidence/main.py checks exactly the stated obligations with exact arithmetic, fails closed on unresolved signs and zero denominators, uses no numeric tolerance and no search, resolves its input relative to itself, and uses the shared harness correctly. No defect was found that could let a false claim pass.

1. Exact arithmetic, no tolerance. Values are 4-tuples of fractions.Fraction over (1, s, u, su); the only non-rational primitive is math.isqrt. The reduction table in mul (main.py:56-67) was verified term by term against the expansion of (a + bs + cu + dsu)(e + fs + gu + hsu) with s^2 = 3, u^2 = 5s - 8: constant `ae + 3bf - 8cg + 15ch + 15dg

   • 24dh, s-coefficient af + be + 5cg - 8ch - 8dg + 15dh, u-coefficient ag + 3bh + ce + 3df, su-coefficient ah + bg + cf + de. All match. Equality is certified only by a zero tuple, and a nonzero tuple is never treated as an inequality certificate; the comment at main.py:33and the contract atmain.py:112` are honest about this.

2. Enclosures are outward and sound. root_bounds (main.py:76-86) is correct in both directions: the lower endpoint is isqrt(floor(r * 2^(2b))) / 2^b <= sqrt(r), and the upper is (isqrt(floor(R * 2^(2b))) + 1) / 2^b >= sqrt(R) because (h+1)^2 > M implies (h+1)^2 >= M + 1 >= R * 2^(2b). It raises on a non-positive or misordered radicand (main.py:79-80). basis_bounds (main.py:89-97) propagates the s enclosure into 5s - 8 before taking the second root, and interval_mul takes min and max over all four endpoint products, so negative coefficients are handled. enclosure (main.py:100-108) ignores the s/u correlation, which only widens intervals.

3. Fail closed on unresolved signs. sign (main.py:111-121) accepts only a strictly one-sided interval and raises ArithmeticError after the 256-bit level; there is no "assume zero" or "assume positive" fallback. main (main.py:342-354) catches ArithmeticError, KeyError, OSError, TypeError and ValueError and records a FAILED named check, so an exhausted refinement produces a nonzero exit rather than silent success; any other exception propagates and also exits nonzero. The measured margins show 16 bits already suffice here, so the cap is nowhere near binding.

4. Fail closed on denominators and malformed input. divide_rational (main.py:124-128) rejects a zero denominator. The input is byte-pinned by SHA-256 (main.py:38, main.py:210-214) and the run returns early with a recorded failure on mismatch. Missing or misnamed JSON keys reach the KeyError handler. Coordinates are parsed only as rational coefficient strings through Fraction (main.py:43), never evaluated as code.

5. No tolerance-based acceptance and no search. Confirmed: no float comparison, no epsilon, no root finding, no candidate enumeration. evidence_parser(..., quick=False) (main.py:344-346) exposes no reduced mode, matching the "default to the full check" requirement.

6. Input resolution and determinism. pathlib.Path(__file__).parent / 'assets' / 'witness.json' (main.py:210) resolves relative to the script, so the documented repository-root command and any other working directory both work. functools.cache on basis_bounds is keyed only on the bit count, so runs are deterministic. Nothing is written to disk.

7. Harness contract. tools.Checker plus sys.exit(main()) with main returning checker.finish() (main.py:348, main.py:354, main.py:357-358) is the prescribed pattern. No bare assert carries a theorem check anywhere in the file, so python -O behaves identically.

8. Coverage matches the page. A static count gives 7 controls + 1 input hash

   • 1 label set + 1 radicand positivity + 1 radical squares + 2 denominators + 9 rotations + 1 chosen coordinates + 2 box bounds + 2 defining equations + 36 positive distances + 1 count + 3 source relations + 63 supporting signs + 1 count + 9 row maxima + 1 count = 141 named checks, matching the page and the evidence index. The three source_relations in witness.json are, in order, [A1A2, A1A3, A1B3], [B1B2, B1C2, B1B3], [C1C2, C1A3, C1C3] — exactly the printed Er87b relations in the printed order — and main.py:295-302 labels them 'A/B first', 'B/C second', 'C/A third' consistently.

9. Row grouping is computed correctly, but only its maximum is asserted. main.py:320-339 compares all 28 pairs per row; because exact distance equality is a genuine equivalence relation and every pair is compared, groups[name] ends up as the full equivalence class, so the set of sorted tuples at main.py:332 is the exact class partition and main.py:333 takes the true multiplicity. comparison_count == 252 (main.py:339) confirms the coverage, and a genuine equality that failed to reduce to a zero tuple would raise in sign rather than be silently misclassified. What is checked, however, is only maximum == data['required_row_maximum'] (main.py:334-337); the partition itself is only printed (main.py:338). See finding N1.

10. The controls exercise real failure paths. The 8-bit exhaustion control (main.py:196-204) builds s minus the 16-bit lower endpoint of s, a positive quantity whose 8-bit interval straddles zero, so the control genuinely reaches the raise. The zero-denominator and negative-radicand controls likewise reach their raises.

Input. evidence/assets/witness.json is a single small JSON file, byte-pinned by SHA-256 in both main.py:38 and evidence/_index.md; the hash was recomputed and both pins are correct. Its six seeds entries are exactly the six coordinates printed in the forum post, expressed as rational 4-tuples over (1, s, u, su); C1 = [(-11/10, 4/5, 3/5, 1/10), (6/5, -1/10, 3/10, -1/5)] expands to exactly (8s - 11 + (s+6)u)/10 and (12 - s + (3-2s)u)/10, matching both the page's displayed radical and the checker's hard-coded reconstruction. source_relations lists the three relations in the printed page order with the printed pairs; counterclockwise_order is the printed cycle; identifying_box is the box certified above, which also excludes the other branch; required_row_maximum is 3. The input is a fixed finite witness with its role and provenance stated in evidence/_index.md and the source _index.md — the six A/B coordinates from the pinned forum capture, the third orbit supplied by the compilation — not a discovery log. There is no produce.py, no cached success file, no reviewer JSON, no external checkout dependency and no network input. Everything the checker needs resolves from an ordinary clone once the proposal is filed at its intended path. Repository hygiene: witness.json sits under evidence/assets/, which the corpus settings exclude from page naming and navigation and which the whitespace and end-of-file fixers skip, so the pinned bytes cannot drift under automatic formatting.

Layout. The folder follows author_year_slug one level under a taxonomy category matching the problem's folder. No PDF exists, and the rule for that case is met by sallerk_2026_convex_nonagon_relations.md, which is named after the folder and records the URL, account, date and pinned capture. _index.md carries the catalog desc in frontmatter and the digest below the separator, ending with the "Bears on" line the incoming-library generator reads. nonagon_from_relations.md is a descriptive result-page name, correct since the source gives its coordinate claim no label, and carries statement, derivation, certificate description, source scope, verification record and "Bears on" list. evidence/ follows the prescribed layout with main.py and assets/ only, and evidence/_index.md states domain, full command, dependencies, arithmetic model, fail-closed behavior, controls, author-execution record and outstanding-review limits. All wikilink targets resolve, and the relative PDF link with #page=9 resolves from the result page's directory.

Nonmaterial findings

No material finding was recorded: nothing found affects the truth of the claim. The following are non-material. N1 is the one that touches warrant provenance.

• N1 — the page's unique-triple sentence outruns its named checks. nonagon_from_relations.md states "The unique triple in each row is as follows" and "Every other neighbor belongs to a singleton distance class", but main.py:332-337 asserts only that the row maximum equals data['required_row_maximum']; the class partition is printed at main.py:338 and is never a named check. A configuration with two triples in one row would pass all 141 checks. The stronger statement is nonetheless true: every one of the nine rows has profile [1,1,1,1,1,3], confirmed independently by both the reviewer and the grader, and asserted as a named obligation by the retained evidence/assets/reviewed_quartic.py. The page needs either a sentence saying this is read off the printed transcript, or a named check in a separately identified checker successor.
• main.py:240-244 — the two "coordinate denominator N nonzero" checks test only that the literals 2 and 10 are nonzero rationals. They have no failure mode tied to the witness and duplicate the guard already inside divide_rational; two of the 141 named checks are content-free.
• main.py:220-221 with main.py:247-253 — points['C2'] and points['C3'] are defined as rotate(C1) and rotate(C2), so the loop's "rotation C1 to C2" and "rotation C2 to C3" checks are tautologies that can never fail. Only "rotation C3 to C1", i.e. R^3 C1 = C1, has content there. Two more of the 141 checks have no failure mode. The six A/B rotation checks are genuine, since A2, A3, B2, B3 come from JSON literals.
• main.py:254-264 and main.py:277-280 versus evidence/assets/witness.json — the chosen-branch formula and both defining equations are hard-coded in the script, while witness.json separately carries chosen_formula and defining_equations (and basis, positive_radicals, subject) that main.py never reads. Nothing cross-checks the two, so those input fields are documentation that could silently diverge from the checked mathematics. They are accurate as currently written; each string was checked against the code and the page. The SHA pin freezes the bytes but does not tie them to the mathematics.
• main.py:336 — the row maximum is compared against data['required_row_maximum'] rather than the literal 3 of the stated theorem, so the checked property is parameterised by the input file. Harmless given the hash pin and the printed transcript, but it slightly weakens "the check tests the stated property".
• main.py:134 — the local name half = fractions.Fraction(2) is misleading; the value is the denominator two, not one half.
• main.py:332 — {tuple(sorted(group)) for _, group in groups.items()} discards the key; groups.values() is the idiomatic form. Cosmetic.
• main.py:293 and main.py:338 — forty-five extra print lines are emitted alongside the 141 transcript lines. Declared in evidence/_index.md and harmless, but verbose.
• nonagon_from_relations.md, "Derivation of the chosen completion" — the derivation is presented as motivation for the coordinates, and the actual warrant is the direct exact verification of the two relations on the fixed coordinates. That is sound, but the page could say so once, so a reader does not treat the perpendicular-foot construction as load-bearing.
• nonagon_from_relations.md, degree-four bullet — the reported polynomial 1600y^4 - 7680y^3 + 24864y^2 - 33696y + 14904 is exactly eight times the true minimal polynomial of y, and y really does have degree four over Q. The page's refusal to accept it without a discriminant argument is conservative rather than wrong; nothing needs correcting, but the caution could be relaxed if a short argument is ever supplied.
• evidence/_index.md — records author wall-clock timings ("0.06 and 0.07 seconds", "under a hard 30-second timeout"), which belong in working storage rather than corpus material. Harmless.
• Pre-integration mechanics — the three proposal pages lack the tool-owned frontmatter name: and H1, the E0097 proposal has no generated problem-library links block, and library/distance_problems/_index.md is not included in the proposal. scripts/build_library_subjects.py, wiki update and wiki lint must run on both roots at integration. The reviewer could not run wiki lint against a proposal outside the corpus.
• Er87b's own digest still lists section_8_danzer_nonagon under "Results to transcribe", so the canonical Er87b result page for the nonagon does not exist and the proposal cites the digest _index and the PDF page directly. Legitimate today, but the one-canonical-page rule points toward transcribing that section and linking it from here.
• wiki/problems/distance_problems/E0097/_index.md (proposal) — asserts that an older forum announcement (post 7604) was withdrawn with the author marking the gist out of date, but no transcription or capture of post 7604 is filed with this proposal; the claim rests on the same local forum capture that is identified only in the post-8669 transcription's provenance block. That page is outside the frozen subject, but the supporting record should be filed with it.
• The result page and both index pages omit the post's opening context line (AlphaEvolve reached k = 3 but not k = 4, Problem 6.53 of arXiv:2511.02864). The transcription retains it verbatim so nothing is lost, but it is arguably the most decision-relevant external lead in the post for E0097's progress account.

Premises

Consumed local claims: none. This is a library result page, not a native L-claim, and it consumes no native L-claim as an established premise. There is therefore no premise standing to check, no staleness question, and no batch acceptance order. The page states explicitly that no external code, hidden six-point result, minimal-polynomial claim or independent tier is a premise of the finite reconstruction, and the review confirms that.

External source interfaces. Three, each with its reading depth.

1. Er87b — P. Erdős, "Some combinatorial and metric problems in geometry", Intuitive geometry (Siófok, 1985), 1987, pp. 167-177, cited at printed pp. 175-176 (physical PDF pp. 9-10), Fig. 5, via the canonical copy in library/discrete_geometry/erdos_1987_combinatorial_metric_problems_geometry/ named above. Exact statement used: the figure is "a convex nonagon A1B1C1A2B2C2A3B3C3 of threefold rotational symmetry, satisfying A1A2 = A1A3 = A1B3, B1B2 = B1C2 = B1B3, C1C2 = C1A3 = C1C3", with the accompanying Reuleaux-triangle and intermediate-value existence construction, and, separately on p. 176, the four-neighbor question that is Problem 97. Interface: the three relations and the cyclic order are the target the local witness is built to realize; nothing else from the paper is used, and Er87b's existence proof is not a premise of the local claim, which exhibits its own explicit set. Reading depth: claims checked (visually, at 150 dpi), coordinates not printed in the source. The pages contain no numerical coordinates, so the local coordinates cannot be, and are not, attributed to that source. The printed existence construction was read and its description on the page checked for fidelity; it was not independently reconstructed, and no such reconstruction is claimed.

2. The forum post 8669 by account sallerk, Erdős Problem 97 thread, 31 August 2026, 19:37 (no timezone in the preserved record), as pinned in the local forum capture identified in the transcription page by the public post anchor and the date it was read. Exact statement used: the six A/B coordinates (1,0), (-1/2, sqrt3/2), (-1/2, -sqrt3/2), (-1/2 + sqrt3, sqrt3/2), `(-sqrt3/2

   • 1/2, 3/2 - sqrt3/2), (1 - sqrt3/2, -3/2)`. Interface: these are the seeds of the two rotation orbits; the third orbit and its derivation are supplied by the compilation, not by the post. Reading depth: claims checked against the pinned transcription; the post's external repository and arXiv lead were not acquired or inspected, and the post's own degree-four, mirror-exclusion and minimality assertions are not consumed — they are held out as separate unaccepted reports. The post's AI-assistance disclosure belongs to the source and is preserved with it.

3. The forum post 7604 in the same thread, cited only by the E0097 problem proposal for the fact that an older proof announcement was withdrawn. Interface: none to the finite claim; it supports a progress sentence on a page outside the frozen subject. Reading depth: unread by this review — no transcription or capture of that post is filed with the proposal, so the sentence rests on an unfiled record. Recorded as a gap on that page, not on the claim.

Explicit assumptions. None beyond the definitions restated above. The claim is unconditional: there is no antecedent left open, and no quoted terminology carries an unproved assertion — strict convex position and mu_P(v) are defined outright on the page and were checked to be meaningful without appeal to any unproved statement.

Grader findings

A grader distinct from both author and reviewer assessed the report contract and independence. Grader verdict: accept with corrections. Reviewer independence confirmed; the seven SHA-256 values the report originally listed were recomputed by the grader and match, including both internal pins. The grader's findings are recorded here and, where they correct the reviewer, the corrected statement — not the slip — is what stands in the body above.

Reviewer prose errors, corrected above; none reached the verdict.

• (a) The reviewer's decimal enclosures for the chosen branch were wrong. The certified rational box 91/100 < x < 92/100, 98/100 < y < 1 is correct, and the other branch x' ~ -0.3426, y' ~ 1.0645 is correct. The chosen branch is x = 0.9139163..., y = 0.9890838..., both truncated rather than rounded. (Record note: the grader quoted these as 0.9139164... and 0.9890835...; an independent 40-digit evaluation while preparing this record gives x = 0.913916301713... and y = 0.989083870286..., agreeing with the grader to six and five decimal places. The discrepancy is confined to quoted decimal digits. Nothing in the claim rests on a decimal expansion: the certified statement is the rational box, and the exact statement is the radical.)
• (b) The reviewer's eliminated linear relation is one half of the page's line (2), not one tenth: its coefficients are x: s - 3/2, y: (s+6)/2, constant (4s-15)/2.
• (c) The reviewer's sentence about "the rational quadratic 335y^2 - 688y + 353.25" was garbled. The quadratic's coefficients lie in Q(sqrt 3), namely, up to sign, A = -280 - 160 s, B = 576 + 328 s, C = -306 - 162 s, with discriminant D = 768 + 576 s. The quadratic itself is correct.

A gap the reviewer missed — non-material, warrant provenance. Recorded as finding N1 above and reflected in the checklist item on consequences and composition and in Weakest steps: the page's "unique triple" and "singleton distance class" sentences are backed only by a row-maximum check in the owner's script, with the class partition merely printed. The grader verified that the stronger statement is true — every one of the nine rows has distance-class profile [1,1,1,1,1,3] — and required that the retained review-side check assert the full profile rather than the maximum. It does.

The grader's own third reproduction, independent of author and reviewer. Canonical arithmetic in K = Q[t]/(t^4 + 16t^2 - 11) with a bisection sign oracle (200 bisections), after proving m irreducible over Q — no rational root among the divisors of 11; no factorization (t^2 + at + b)(t^2 - at + c), since a = 0 forces b + c = 16, bc = -11 with discriminant 300, not a square, and c = b forces b^2 = -11. A from-scratch elimination over Q(sqrt 3) with formal C1 = (X, Y) gave eqA = -2X^2 - 2Y^2 + X + sY + 1 = 0 and eqB = X^2 + Y^2 + (s-2)X + 3Y + 2s - 8 = 0, then the quadratic above, then an exact square-in-the-field test sqrt(768 + 576 s) = (24 + 16 s) u with alpha = 24, beta = 16, giving Y = (6/5 - s/10) +/- (3/10 - s/5) u and `X = (-11/10

• 4s/5) +/- (3/5 + s/10) u, the plus branch being the page's coordinates character for character. An exact gift-wrapping (Jarvis march) hull with hard failure on any collinear triple returned hull size 9 in exactly the page's counterclockwise order A1 B1 C1 A2 B2 C2 A3 B3 C3, with no collinear triple anywhere — stronger than the page's "no redundant collinear boundary points". All 63 supporting determinants were strictly positive (minimum about 0.21314) and all 36 squared distances strictly positive (minimum about 0.11635). A finite-field homomorphism cross-check modulo 1000000007, with r^2 = 3andw^2 = 5r - 8, reproduced the orbits, distances, relations and row profiles by integer arithmetic. Exact values: A rows 3, B rows 12 - 3s, C rows 3qwith3q = -3/5 + 3s + 3su/5, and ||B1||^2 = 4 - s. The page's derivation was re-verified line by line, including (15-6s)(2s-3) = 48s - 81and(15-6s)(s+6) = 72 - 21s. Minimal polynomials: yhas degree 4 with200y^4 - 960y^3 + 3108y^2 - 4212y + 1863(the forum's polynomial is exactly eight times it), andxsatisfies200x^4 + 880x^3 + 1212x^2 - 1364x - 577. Er87b pp. 175-176 were read visually at 150 dpi, confirming the relations, the mixed terms, the cyclic order, the absence of coordinates, that the disproved conjecture is the three-neighbor one, and that the four-neighbor question is asked separately. The harness contract was confirmed: Checker.finish` returns nonzero on any failure and on zero checks.

Second-cycle grading. A distinct grader re-graded the completed record in a second cycle, using a third arithmetic model — neither the author's two-radical tuples over (1, s, u, s*u) nor the reviewer's single-generator quartic field, but a two-level tower Q(s)[u]/(u^2 - (5s - 8)) with an exact repeated-squaring sign oracle. Fifty facts of the record were confirmed. Seventeen mutations were run against the retained check; fifteen failed closed as they should, and two passed, both because the check was still reading a value from the input that fixes what is asserted: repeating one pair inside each Er87b relation triple, and widening the identifying box to [-100, 100]^2. Both are now closed — the pairings and the box are reviewer-side constants that the input must match, and both mutations exit 1 in plain and optimized Python. The second-cycle verdict is pass, subject to three non-blocking corrections, all applied here: the input-parameterization just described; two over-wide transcript lines in RUN_RECORD.txt, now inside a fenced block; and two decimal figures quoted round-to-nearest, now stated as truncations.

Corrections that gate the standing.

1. Durability. The reviewer's and grader's exploratory scripts in temporary storage are not a warrant. The retained script evidence/assets/reviewed_quartic.py and this report resolve from an ordinary clone. The exact original program is retained separately from its current shared-harness adaptation, and the reported runs are retained below.
2. The owning page's record. The page's verification record must become an independently reviewed record naming both lanes, the exact mathematics checked, the verdict and the limits. The unique-triple and singleton sentence must be either marked as read off the printed transcript or backed by a named check in a separately identified checker successor.

Non-blocking cleanups. The two literal-denominator checks and the two tautological C-orbit rotation checks; the unread witness.json fields (read and cross-check them, or delete them); the literal 3 instead of data['required_row_maximum']; renaming half at main.py:134; moving wall-clock timings out of evidence/_index.md; running scripts/build_library_subjects.py, wiki update and wiki lint on both roots at integration; and filing a transcription for forum post 7604 before the E0097 page's withdrawal sentence stands.

Verdict and grading

Mathematical verdict: refutation-failed. The proof survives the commissioned attacks under the full contract. No counterexample, no real error and no unsupported essential step was found, and every finite fact was reproduced by two further structurally independent exact computations.

Standing, at exactly the frozen finite scope. Established: the nine points are distinct and in strict convex position, with hull cycle A1 B1 C1 A2 B2 C2 A3 B3 C3 and no three collinear; the maximum distance multiplicity is exactly three at every vertex; and the three Er87b p. 175 relations hold in the printed order and pairing. Hence the set is a strictly convex E_3 witness and is not an E_4 counterexample.

Not covered. No resolution of Problem 97 and no change to its imported status; no uniqueness of the completion; no nonconvexity of the alternate branch; no degree-four or minimal-polynomial claim (true, but unaccepted here); no mirror exclusion; no n_3 >= 7 or {7, 8, 9} conclusion; no identification of the coordinates as Danzer's; and no reconstruction of the printed Er87b construction.

Tier and obligations. No numerical tier is created: this is a library result page, not a native L-claim, and the tier contracts do not apply to it. The outstanding obligation to transcribe Er87b section 8 as the canonical result page for the nonagon is untouched by this review.

Grading. The grader, distinct from both author and reviewer, recorded accept with corrections for the report contract and independence, with the corrections folded in above. Attribution on the claim names the reviewer for the mathematical verdict and the grader for the contract and independence assessment.

Reported execution record

The following is the complete supplied run record. Its original checker name refers to the exact snapshot identified above. The 21-obligation runs concern that program, not the shared-harness successor. The mutation copies and precise recipes were not retained. In particular, the nine listed successor controls below and the completed-record grader's 17-control account are different records, not a single reproduced control set.

Run record: independent review check of the exact E3 nonagon realizing the
Er87b distance relations.

Checker      evidence/verify/verify_quartic.py, run as the bytes retained at
             evidence/assets/reviewed_quartic.py
Input        evidence/assets/witness.json
             --input pointed at the frozen copy of that exact file, which
             is what the default ../assets/witness.json resolves to once
             the check is filed at its canonical path. Resolution from a
             different working directory was confirmed separately.
Interpreter  CPython 3.13.12 on Darwin arm64
Environment  standard library only; no network, no files written

Transcripts (fenced; the summary lines run past 80 columns):

```
$ python3 verify_quartic.py --input <frozen evidence/assets/witness.json>
verify_quartic: PASS, 21 obligations re-checked in K = Q[t]/(t^4+16t^2-11), 8 bisections, cap 400
```
exit code 0; elapsed 0.064 s

```
$ python3 -O verify_quartic.py --input <frozen evidence/assets/witness.json>
verify_quartic: PASS, 21 obligations re-checked in K = Q[t]/(t^4+16t^2-11), 8 bisections, cap 400
```
exit code 0; elapsed 0.068 s

Both runs exit 0 and print the same summary line. The optimized run is
identical to the plain run, as required: no obligation is carried by a bare
assert.

Negative controls, run against mutated copies of the input and of the
checker held in the reviewer's working storage and not filed. Every one
exits 1 in plain and in optimized Python:

  perturb the u-part of C1.y              12 of 21 obligations fail
  corrupt one B2 seed coefficient          2 of 21 fail
  reverse the cyclic-order field           the input-pin obligation fails
  repoint one Er87b relation pair          the input-pin obligation fails
  shift the identifying box                the input-pin obligation fails
  repeat one pair inside each Er87b        the input-pin obligation fails
  relation triple                          (this mutation passed an earlier
                                           revision that read the pairings
                                           from the input; it no longer does)
  widen the identifying box to             the input-pin obligation fails
  [-100, 100]^2                            (likewise a former pass, now
                                           closed by pinning the box)
  transpose B1 and C1 in the checker       the supporting-edge obligation
  cyclic-order constant                    fails, so the convexity check has
                                           a real failure mode
  set the bisection cap to zero            "bisection cap exhausted; no sign
                                           accepted": exhausted refinement
                                           fails closed instead of accepting
                                           an uncertified sign

Completed-record grading

The following preserves the supplied distinct completed-record grading, with heading levels adapted for this page. It assessed the program before the final relation/box pinning corrections; its two unexpected passing mutations therefore refer to that earlier program. The completed successor report and its supplied index record those corrections and reported new runs. This confirmation does not independently assess the new shared-harness code.

Verdict on the completed record: pass-with-corrections; a pass for the report contract and independence, with three non-blocking corrections and two page-side integration actions. The mathematical verdict refutation-failed stands at the frozen finite scope.

Subject identity

nonagon_from_relations.md (retained as ../assets/reviewed_result.md), evidence/main.py and evidence/assets/witness.json as committed on 2026-09-10, and the cited Er87b PDF, recomputed and matched; main.py's internal input pin equals the witness hash; INDEX.md self-hashes match the record files.

Required corrections: all present

Durability (Subject and independence, "Independent code and rerun commands"; checklist item 9 states the temporary scripts are not the warrant); page verification-record and unique-triple corrections recorded as gating (Corrections that gate the standing, item 2; finding N1, checklist item 7, code review item 9); the retained check asserts the full row profile as a named obligation; ten checklist items with bolded verdicts, Uniformity inapplicable with a correct justification; Weakest steps, Strongest attack, Premises present; the three reviewer slips corrected in the body (decimals; the eliminated relation is exactly one half of the page's line (2); the quadratic's coefficients -280 - 160 s, 576 + 328 s, -306 - 162 s up to sign, discriminant 768 + 576 s, square root (24 + 16 s) u).

Independent mathematics

Third arithmetic model: a two-level tower Q(s)[u]/(u^2 - (5s - 8)) with an exact repeated-squaring sign oracle (no enclosures, no bisection). Confirmed: rotation identity; C/A condition equals -1 times the circle (1), B/C condition equals q + (s - 2) x + 3 y + 2 s - 8, monomial support {1, X, Y, X^2, Y^2}, elimination an equivalence; quadratic, discriminant and square-in-the-field test; page y is the plus branch and the line recovers page x; the other root lies outside the box; 36 squared distances strictly positive (minimum about 0.11635); 63 supporting determinants strictly positive (minimum about 0.21314); no three points collinear; nine consecutive left turns; the bridge from 63 positive determinants to strict convex position valid; every row profile [1,1,1,1,1,3] with the page's triples under its mod-3 convention; all page derivation identities; minimal polynomials 200y^4 - 960y^3 + 3108y^2 - 4212y + 1863 (forum polynomial exactly 8 times it) and 200x^4 + 880x^3 + 1212x^2 - 1364x - 577; irreducibility of t^4 + 16t^2 - 11; the structural difference between the single-generator quartic model and the author's two-radical 4-tuples with isqrt enclosures (author's mul table verified term by term); every main.py line citation accurate; the 141-check tally exact; finding N1 confirmed (main.py:334-337 checks only the row maximum; the partition is printed); the five unread witness.json fields confirmed. Decimals: x = 0.913916301713657..., y = 0.989083870286031..., x' = -0.342635009603454..., y' = 1.064505968200193...

Independent runs and controls

Plain and -O runs of verify_quartic.py against the frozen input: exit 0, 0.04 s, output identical to RUN_RECORD.txt. Seventeen mutations exercised; fifteen exit nonzero in both modes (perturbed C1; swapped cyclic order; repointed relation; shifted box; perturbed seed; missing box field; missing input; truncated JSON; extra relation; consistent minus-u branch; bisection cap zero; transposed reviewer-side cycle; C1 nudged by 1/1000 with six row-profile failures; corrupted t^4 reduction; alternate pairing B1C3). Two mutations passed when they should not: source_relations rewritten with a repeated pair, and identifying_box widened to [-100, 100]^2, because both are read from the input rather than fixed in the check.

Remaining corrections

C1 (non-blocking, retained check lines 155-168 and report lines 471-474): promote source_relations and identifying_box to module-level constants, or narrow the sentence claiming the checked property is the stated theorem rather than the input's request. The nine points, the boundary cycle and the row profile are fixed independently of the input, so the verified statement is intact. C2 (trivial): RUN_RECORD.txt lines 16 and 20 are 97-column transcript lines outside a fence. C3 (trivial): the quoted decimals 0.989084 and 0.9890839 are round-to-nearest rather than truncations; the exact 12-digit values are correct. Integration actions (page side, correctly handed off): rewrite the page's verification record as independently reviewed with the limits; fix the unique-triple sentence; file the three record files under the owner's evidence/verify/.

Grading note (quotable)

A grader distinct from both the author and the reviewer assessed the completed independent review record against the whole-claim report contract and recorded pass, with three non-blocking corrections. The frozen subject's three file identities and the cited source-PDF hash were recomputed and match, as did the checker's internal input pin. Every required part of the contract is present, each audit-checklist item carries an explicit verdict, and the one inapplicable item is correctly justified. The grader re-derived the mathematics in a third arithmetic model, a two-level radical tower with an exact repeated-squaring sign oracle using neither square-root enclosures nor bisection, and reproduced every asserted fact: the rotation identity, the equivalence of the two completion conditions with the circle and the line, the eliminated relation as exactly one half of the printed line, the quadratic and its discriminant, both branches and the separating rational box, thirty-six strictly positive squared distances, sixty-three strictly positive supporting determinants with no collinear triple, and the distance-class profile of one triple and five singletons in all nine rows. Both minimal polynomials and the quartic's irreducibility were confirmed independently. The retained review-side check was rerun in plain and optimized Python with results identical to the recorded run, and seventeen grader-devised mutations were exercised; all failures exit nonzero in both modes, an exhausted refinement budget raises rather than accepting a sign, and no obligation is carried by a bare assertion. Two residual mutations showed that the relation pairings and the identifying box were read from the input rather than fixed in the check, which narrowed one coverage sentence but left the verified statement intact, since the nine points, the boundary cycle and the required row profile are all fixed independently of the input. The mathematical verdict of refutation-failed stands at exactly the frozen finite scope, and the record creates no tier, no uniqueness, no degree claim, and no change to the catalog problem's status.