Arithmetic-progression discrepancy: whole-proof examination

Subject and independence

Examination date: 2026-10-15 UTC. Role: independent whole-proof reviewer, in a fresh isolated context, with disclosed model profile gpt-6-astra. The reviewer neither authored nor collaborated on the subject, had not previously built on it, and received no prior verdict or author advocacy. This is a mathematical examination of static source text and finite computations. It makes no Lean elaboration, kernel, tier, acceptance or problem-status claim.

Frozen subject: the extraction frozen on 2026-10-15 at 13:17:10 UTC, preserved byte-for-byte under subject/manifest.json. All paths below are relative to this report's repository directory. The preserved subject consists of the exact statement, candidate proof, exponential deductions, Basic source slice, Sqrt source slice, small-case definitions, source one-term argument, case 2, case 3, case 4, finite checker, its finite fixture, the 17 individually listed runtime files in the manifest, and source provenance and scope. The snapshot is the supplied extraction, including its uniform cut markers; it is not a reconstruction from canonical pages. Its mathematical bytes remained unchanged throughout this examination.

Reading depth: every statement, deduction, supplied analytic source slice, small-case source file, checker and complete finite fixture above was read in full. The two analytic slices contain 1702 and 964 lines, respectively. Their essential mathematical deductions are examined below. All 17 supplied runtime files were read in full, including their import and initialization surfaces. Their uncalled repository utilities are not mathematical premises and were not verified as repository tools. Only the unchanged finite-checker route used this package.

The operating instructions were separately frozen and checked against their manifest before use. The required portions of anatomy, the complete neutral and campaign verification contracts, README, campaign guidance, the permitted research-reading section, evidence, mathematical authoring and weaving were read. These instructions did not expand the mathematical read set. No canonical mathematical page, live ledger, full source archive, source README, author inspection account, previous examination, external paper or website was read. No inbox, feed, sibling context or substantive steering was consumed. The subscription tables checked at the examination boundaries were empty; the accepted settings recorded blind, sealed, no-sync operation. These are supporting isolation facts, not a claim that those settings impose a filesystem sandbox. No excluded exposure occurred.

Independent evidence: the mathematical derivations in this report and the independent finite program, its exact inputs, counts and certificates, false-minimum controls, and control witnesses. The rerun driver freshly executes the unchanged author checker, the independent program and the negative controls. Concrete commands appear under “Reproduction.” This is one examination with a disjoint computational route, not a claim to two independent review cycles.

Credits and source limits: Kenta Kitamura / KitaKen1 owns the original source mechanism. The supplied provenance preserves preparation-assistance credits to Codex 5.5 and ChatGPT 5.5 Pro. The analytic extraction, finite Python probe and exponential deductions are original Plasma AI work. The independent derivations and reproduction retained in this report are also Plasma AI work. The source locators are KitaKen1/erdos176-nk2-polynomial-bound-lean at external revision 88be9174c1b85548fa48d2498ba907a9e80f04c7 and KitaKen1/erdos176-nksqrtk-polynomial-bound-lean at external revision 19b2ad31c81207613f7cfdaa68467d3dca98b3b7. The supplied provenance records Apache 2.0 for both archives. Archive identity and license texts were not separately inspected. The proof examined is the supplied common Basic mathematics together with the supplied Sqrt extension; the claimed equality with the second archive's unlisted Basic file was not independently compared. No conclusion below relies on that unperformed comparison or on a reported source build.

Restatement with all quantifiers

For integers $k\geq1$, real $\ell>0$ and integers $N\geq1$, let $P(k,\ell,N)$ mean the following:

For every map $f:\{0,\ldots,N-1\}\to\{-1,1\}$, there exist integers $a\geq0$ and $d\geq1$ such that $a+(k-1)d<N$ and

The terms form an ordinary progression with positive difference. The final discrepancy comparison includes equality. If the set of positive integers satisfying $P(k,\ell,N)$ is nonempty, $N(k,\ell)$ denotes its least element. It is undefined otherwise.

The separately examined conclusions are:

All divisions defining $T_2,T_s$ are real divisions before applying the ordinary integer floor. No natural-number division is substituted. Translating every index by one gives exactly the same minima for $\{1,\ldots,N\}$. Cyclic progressions used below do not themselves establish any final assertion.

Common derivations: finite Fourier and Fejér identities

Fix a positive integer $N$ and a sign coloring $f$, extended periodically to the integers. Write

Finite Fourier normalization

Take $\omega=\exp(2\pi i/N)$. For $t,u\in\{0,\ldots,N-1\}$, put $q=\omega^{t-u}$. If $t=u$, the sum of $q^a$ is $N$. Otherwise $N$ cannot divide the nonzero integer $t-u$ in this range, so $q\neq1$, while $q^N=1$. Multiplying the finite geometric sum by $1-q$ gives $1-q^N=0$. Thus

For $N=1$ only the first case occurs.

Define

Interchanging two finite sums and applying the same geometric identity with the roles of index and frequency exchanged gives $f(x)=\sum_t\widehat f(t)\omega^{tx}$. For arbitrary complex coefficients $c_t$, direct multiplication gives

In particular $\sum_t|\widehat f(t)|^2=1$.

With $G_d(z)=\sum_{j=0}^{k-1}z^{jd}$, the periodic expansion of $f$ yields

This independently supplies the normalization and finite basis/Parseval content used in the source. It holds for every positive $N$ and every natural $d$, with no primality, coprimality or distinct-residue assumption.

Fejér expansion and the factor two

For a unit complex number $z$, integers $k,D\geq0$, and $1\leq d\leq D$, let $w_d=1-d/(D+1)$. Consider

Every summand is nonnegative. When $p=q$, its value after division by $D+1$ is $D+1$, since $z^p\overline{z^p}=1$. Therefore $Q\geq k(D+1)$, even when different powers $z^p$ coincide.

Expand the square and interchange the four finite sums. For fixed $r,s$, the sum over $p,q$ is

Negative exponents are well-defined because $z\neq0$. Their sums are the conjugates of the positive-exponent sums, and have the same squared modulus. There are $D+1$ pairs with $r=s$. For a positive difference $d$, the pairs $(r,s)=(s+d,s)$ number exactly $D+1-d$, and there are equally many pairs of difference $-d$. It follows that

Consequently

Since $0\leq w_d\leq1$, the same lower bound holds for $\sum_{d=1}^{D}|G_d(z)|^2$.

This includes the empty $D=0$ case: the identity gives $Q=k^2$, while the lower bound becomes $0\geq(k-k^2)/2$ for natural $k$. No limiting argument is involved.

As an exact normalization attack, take $k=2,D=4,z=-1$. Then $G_1=G_3=0$ and $G_2=G_4=2$, so the weighted energy is $16/5$. Directly, the two diagonal pair terms total $10$, and each off-diagonal term is $1/5$, giving $Q=52/5=4+2(16/5)$. This tests the normalization, diagonal contribution and factor two away from the all-ones case. The general proof above, rather than this example, establishes (4)–(5).

Multiplying (5) by the nonnegative masses $|\widehat f(t)|^2$ and summing over $t$ gives

The masses sum to exactly one, not $N$ or $1/N$.

The source's conditional helpers with a scalar Cassels hypothesis are discharged by its own scalar proof. In the supplied Basic slice, the nonnegative pair terms, expansion and bounds lead to casselsGeomLowerClaim_true, then to the unconditional moment bound. The Sqrt slice retains the exact weighted identity. No Cassels or Turán literature result is imported into this examination.

Common derivations: ordinary progressions, wrapping and minima

Wrap loss and target conventions

Let $m=(k-1)d$. Among $a=0,\ldots,N-1$, exactly $\min(N,m)$ satisfy $a+m\geq N$: if $m<N$, they are $N-m,\ldots,N-1$; if $m\geq N$, all starts qualify. In particular their number is at most $m$. Equality at the endpoint $a+m=N$ belongs to the wrapping set.

For every cyclic start, the triangle inequality gives $|S_d(a)|\leq k$, even if residues repeat. If every non-wrapping start has $S_d(a)^2\leq b$, then, for $k^2-b\geq0$,

The second estimate remains valid when its right side exceeds $k^2$. No implicit assumption $(k-1)d<N$ was used to count wrapping starts.

For discrepancy 2, failure of the non-strict target means integer $|S_d(a)|<2$, hence $S_d(a)^2\leq1$. For the other target, both $\sqrt{k}$ and $|S_d(a)|$ are nonnegative, and squaring preserves their order. Thus

Failure gives the integer inequality $S_d(a)^2\leq k-1$. The caps in (7) are therefore $b=1$ and $b=k-1$, respectively. Equality in (8) remains admissible, including square $k$. For example a four-term sum $1+1+1-1=2$ reaches $\sqrt4$; replacing the final comparison by a strict one would change the subject.

If $a+(k-1)d<N$ and $j<k$, then $a+jd\leq a+(k-1)d<N$. Every cyclic index equals its ordinary index. For $d\geq1$ the indices are distinct. The canonical representatives of $\mathbb Z/N\mathbb Z$ are in bijection with $\{0,\ldots,N-1\}$, so transport through Fin and ZMod changes neither the sum nor its normalization. An integer embedded in $\mathbb C$ has squared norm equal to its integer square embedded in $\mathbb R$. These observations supply every model bridge used in (3), (6) and (7).

Polynomial bound for discrepancy 2

Assume $k\geq5$ and that every ordinary $k$-term AP misses target 2. Put $D=2k$. Summing (7) with $b=1$ and dividing by $D$ gives

The unweighted half of (6) gives

Writing $A_2=(k^2-1)(k-1)(2k+1)$, subtraction gives the exact gap

Both $N$ and $k-3$ are positive. Therefore $N>T_2(k)$ makes the gap strictly positive, a contradiction. The conclusion is an ordinary AP with $1\leq d\leq2k$ and non-strict discrepancy at least 2.

A floor boundary attack is decisive about the needed strictness: $T_2(5)=1056$. At $N=1056$, (9) is zero and this contradiction is unavailable. The stated choice is $N=1057$, where the gap is exactly $1/2114>0$. Thus the added one is doing necessary work in the argument; it was not lost when passing between real and integer bounds.

Polynomial bound for discrepancy $\sqrt{k}$

Assume $k\geq2$ and every ordinary AP fails (8). The exact finite sums, obtained from $\sum d=D(D+1)/2$ and $\sum d^2=D(D+1)(2D+1)/6$, are

Nonnegativity of every weight permits summing (7). Set $A=(k^2-k+1)(k-1)$ and $K=k(k-1)>0$, and take $D=2K$. The weighted bounds become

Before inserting the error term, the difference is $L_s-(k-1)D/2=(D-K)/2=K/2$. Hence

For $N>T_s(k)$ this is strictly positive, again a contradiction. It produces a positive difference at most $2k(k-1)$ and a non-wrapping ordinary AP satisfying (8).

At the smallest allowed $k=2$, the threshold is the integer $12$. At $N=12$ the gap is zero, while at the stated integer choice $13$ it is $1/13$. The proof uses the exact weighted estimate and the integer cap $k-1$; replacing either by a heuristic average would not prove (11).

Existence, floors and least values

On their stated domains, both thresholds are positive real numbers. For either threshold $T$, let $B=\lfloor T\rfloor+1$. Then $B\geq1$ and $T<B$, including integral $T$. The preceding contradiction proves the universal property at $B$ before selecting a minimum. The nonempty set of positive successful lengths therefore has a least element, and that element is at most $B$.

The source properties explicitly require positive length. Consequently their Nat.find selections over natural numbers are these same positive minima. On the positive threshold domains, Nat.floor agrees with the ordinary floor. No default value supplies existence. N176 is guarded by $k\geq5$, and N176Sqrt by $k\geq2$; their default zero values outside those guards are different definitions from the mathematical minima.

For completeness, if the property holds at $M$ and $N\geq M$, restricting a coloring of length $N$ to its first $M$ entries supplies an AP still contained in the larger interval. Translation by one is also bijective: set $g(x)=f(x-1)$, send $(a,d)$ to $(a+1,d)$, and reverse by subtraction. Both successful-length sets, and hence their minima, are unchanged.

Finite bases: exact independent reproduction

Boolean codes and sign colorings

For any $N\geq0$, encode a sign coloring by

Then $0\leq c<2^N$ since $\sum_{x=0}^{N-1}2^x=2^N-1$. For a fixed $x$, split the sum as $c=c_{<x}+\epsilon_x2^x+2^{x+1}t$, where $0\leq c_{<x}<2^x$ and $\epsilon_x$ is one or zero according as $f(x)=1$ or $-1$. Then $(c\mathbin{\mathrm{div}}2^x)\bmod2=\epsilon_x$. Conversely repeated Euclidean division by two gives each $0\leq c<2^N$ exactly $N$ binary digits, padded with zeros; their reconstruction gives $c$. Thus these codes and sign colorings are bijective. This includes the empty coloring and the sole code zero at $N=0$.

For $k\geq2$, an admissible positive difference satisfies $d\leq(k-1)d\leq a+(k-1)d<N$. Also $a<N$. Thus the source loops over $a,d<N$, with the positive-difference guard, exhaust all ordinary APs. Its endpoint guard implies every $j<k$ is in range, so the fold skips no term on an accepted candidate. The Boolean predicate goodCode is exactly the universal coloring property on these finite domains. allBeforeFalse rejects every smaller length. At $N=0$, one empty coloring exists but there is no start, so the property fails. The mathematical bridge is proved here; no claim is made that the source has formalized this bridge.

The author checker enumerates sign tuples and equal-gap subsets, then compares with its start/difference inventory. Its integer arithmetic, positive endpoint conditions, empty cases, target comparison and failure exit were inspected. The unchanged script was freshly run through the supplied runtime, producing 12 passing checks and exactly the retained 28 data rows. Actual script-file import tracing identified all 17 runtime files at the supplied paths. Neither a stored success message nor native_decide was used as a premise.

Independent inclusion-exclusion for $k=2,3$

For $k=2$, a sum reaches absolute value 2 exactly when the two signs agree. For $k=3$, its absolute value is 1 or 3, so reaching 2 is equivalent to all three signs agreeing. Avoidance is therefore absence of monochromatic AP edges in both cases.

Generate an AP by its endpoints $x<y$: it exists precisely when $k-1$ divides $y-x$, with points $x+j(y-x)/(k-1)$. This is separate from both author generators. For any selected subset $J$ of AP edges, requiring every edge of $J$ to be monochromatic identifies its vertices into $c(J)$ equivalence classes. There are exactly $2^{c(J)}$ sign assignments satisfying those equalities. Inclusion-exclusion gives the number of avoiding colorings:

The independent implementation starts with the discrete partition and coefficient one. For each edge it keeps each current term, and subtracts the same coefficient on the partition obtained by merging that edge's classes. Induction on the number of processed edges proves that the resulting coefficient of each partition is exactly the sum of the inclusion-exclusion signs producing it. Equal partitions can therefore be combined without enumerating sign tuples. This is a terminating expansion over a finite edge list, not an assumption that all colorings have been visited.

For prescribed prefix signs, a partition contributes zero if a class receives both signs. Otherwise each unfixed class has two choices. Using these conditional counts, the program selects sign $-1$ whenever that branch has a completion, and sign $+1$ otherwise. The two branch counts sum to the parent count. This constructs the lexicographically first avoiding coloring and records its exact branch counts. No author witness is supplied to this construction.

At $(k,N)=(2,3)$ the resulting coefficient polynomial is $q^3-3q^2+2q$, whose value at $q=2$ is zero. At $(3,9)$ it is

Its value at 2 is $512-2048+1344+1344-1616+464+20-20=0$. The retained data supplies the endpoint edges and coefficient polynomial for every checked length; rerunning reconstructs the partition expansion.

There is also a direct independent proof at $k=2$: among three signs two agree, and any pair of distinct indices is a positive-difference two-term AP. The opposite signs at length two show the lower bound.

Independent recurrence for $k=4$

A four-term signed sum misses absolute value 2 exactly when it is zero. In particular every consecutive block of four must sum to zero. Subtracting neighboring block equations gives $f(i+4)=f(i)$ whenever both indices occur.

For $4\leq N\leq6$, the first four entries must be a balanced seed with two signs of each kind, of which there are six. The recurrence determines any remaining entries, and only difference one is possible, so all six work.

For $7\leq N\leq12$, the AP $0,2,4,6$ has sum $2(f(0)+f(2))$. It must vanish, so $f(2)=-f(0)$. The balanced seed then forces $f(3)=-f(1)$. Every avoiding coloring is therefore the restriction of

Conversely all four choices work through length 12. Every admissible difference is at most 3. An odd difference visits each residue class modulo four once; difference two alternates opposite signs. Both sums are zero.

At length 13, the positive-difference AP $0,4,8,12$ lies in the interval and has sum $4u$, eliminating all four possibilities. At length 12 its last point is outside the interval, so it cannot be used early. For $N<4$, there are no four-term APs and all $2^N$ colorings avoid.

This proves the count formula used by the independent program. The zero at 13 follows from the exhibited obstruction to all recurrence seeds; it is not inferred from a hard-coded assertion of the desired minimum. The program retains the allowable seeds and checks its first witnesses against the endpoint-generated APs.

Complete count and witness coverage

Every AP count, coloring-domain size, avoiding count and first avoiding coloring agrees between the fresh author route and the independent route, in all 28 rows. The independent route represents 17,421 assignments; it does not enumerate 17,421 sign tuples. The separate AP count formula is $mN-(k-1)m(m+1)/2$, with $m=\max(0,\lfloor(N-1)/(k-1)\rfloor)$. Indeed, each $1\leq d\leq m$ permits exactly $N-(k-1)d$ starts, and no larger difference permits a start. Summing these counts gives the formula; each AP has a unique start and positive difference.

The first avoiding witnesses at one below each minimum are, respectively, $(-1,1)$, $(-1,-1,1,1,-1,-1,1,1)$, and $(-1,-1,1,1,-1,-1,1,1,-1,-1,1,1)$. All earlier lengths have positive counts, and the claimed upper lengths have count zero. This establishes each exact positive minimum.

The negative input asks for minima 2, 8 and 12 at $k=2,3,4$. It was executed under Python -O and exited 1, with respective avoiding counts 2, 6 and 4 and concrete witnesses. Thus each computational case has an observed failing input at the relevant boundary. For the author's separate predicates, an omitted AP such as $(0,1)$ at $k=2,N=2$ would fail inventory agreement; reporting $(-1,-1)$ there as an avoider would fail witness validation; the false upper lengths above fail universality; a proposed minimum of 4 at $k=2$ fails its smaller-length test because length 3 already has zero avoiders. These describe failure conditions, not modifications made to the frozen author program.

The independent route changes both the counted objects and the arithmetic primitive. A sign-loop stopping or bit-coverage error cannot silently remove the same assignments from the partition inclusion-exclusion calculation. The four-term recurrence avoids a full assignment census altogether. Their endpoint inventory and the closed AP-count formula also differ from the author's subset and bounded-start inventories. Agreement alone is not the warrant: equations (12), the partition induction, the conditional-count argument and the proof of (14) provide the mathematical reductions.

One-term cases and exponential consequences

For $k=1$, every admissible sum is a single sign, of absolute value one. Thus for every positive $N$ no coloring has a one-term AP of discrepancy 2, and the universal property for target 2 fails. There is no $N(1,2)$.

For target $\sqrt1=1$, at length one take $a=0,d=1$. Its endpoint is zero and its absolute sum is one, including equality. Since every positive length is at least one, the minimum is $N(1,1)=1$. The source default N176Sqrt 1 = 0 has no role in this argument.

For integers $k\geq5$, the positive factors satisfy $k-3\geq k/3$, $k^2-1\leq k^2$, $k-1\leq k$ and $2k+1\leq3k$. Therefore

For every integer $k\geq1$, $k\leq2^k$: start at one and use $k+1\leq2k\leq2^{k+1}$ in the induction step. For $k\geq5$, also $19\leq2^k$, since $19\leq32$ and powers of two increase. Hence

At $k=2,3,4$, the independently established minima are $3\leq256$, $9\leq4096$, and $13\leq65536$. These cover exactly the remaining domain of the exponential bound for 2. No assertion for $k=1$ is imported.

For $k\geq2$, the three factors in $T_s$ satisfy $k^2-k+1\leq k^2$, $k-1\leq k$, and $k(k-1)+1\leq k^2$. Thus

Now $3\leq2^k$ and $k\leq2^k$, so $3k^5\leq2^k(2^k)^5=64^k$. The remaining $k=1$ case is the actual minimum $1\leq64$ just proved. These are uniform inequalities for every parameter in the stated ranges, not extrapolations from finite tests.

Weakest steps and strongest attempted refutations

The following table identifies at most three weakest links for each conclusion. The derivations above supply the links; the last column states their composition and the attempted break, rather than relying on agreement with source output.

The most consequential attempted refutation was the cyclic-to-ordinary passage. For $k=5,N=6$, the alternating coloring $f(a)=(-1)^a$ has only difference-one ordinary five-term APs, each of absolute sum one. On the cycle, every even difference gives absolute sum five. Thus a large cyclic moment alone cannot entail the ordinary conclusion. This is an exact counterexample to that shortcut, not to the commissioned bound. Extending the alternating coloring to any interval of length at least 9 already supplies the ordinary AP $0,2,4,6,8$ of absolute sum five. More generally, (7) accounts for every possible wrapping start, and (9) leaves a strictly positive gap at every stated polynomial length, including $1/2114$ at $k=5,N=1057$.

The same failure mechanism is visible for $k=4$ and the coloring with period $(-1,-1,1,1)$: at length four the ordinary sum is zero, while cyclic difference four has absolute sum four. The exact recurrence analysis shows that it avoids target 2, which equals $\sqrt4$, through length 12 and fails at length 13. It therefore checks the model and endpoint obstruction without purporting to refute the much larger square-root polynomial bound. These examples test a mechanism the proof must control; merely finding large cyclic sums would have missed it.

Additional attacks covered composite $N$, non-coprime and repeated cyclic steps, $N=1$, empty $D=0$, saturated wrap sets, the nonnegative coefficient $k^2-b$, natural subtraction before real coercion, and integral thresholds. The Fourier proof requires only $N>0$. Natural subtractions used in the public ranges agree with their integer differences: $k-1\geq0$, $k-3>0$, and $k^2-(k-1)=k^2-k+1>0$. No discarded exceptional coloring or unstated arithmetic restriction survived these checks.

Premises, interfaces and actual reading depth

The premise list was derived from the frozen statement, proof, source slices and every consequence sentence. There is no consumed native L-claim and no accepted external Cassels, Turán, van der Waerden or other source theorem being taken as a black box. The elementary finite identities, integer inequalities and well-ordering used here are stated and derived at their points of use. The exact external source versions are identified in the subject block. The following table distinguishes the source interfaces from any claim of formal execution.

Dependency reading at verdict filing, 2026-10-15 UTC: the consumed-native-claim set is empty. A live ledger read is therefore inapplicable and was excluded by the commission; no stale or pending native premise is silently being relied on. No pending source grade is assumed. All substantive mathematical interfaces in the table are within this examination.

The acyclic order for the batch is: common finite identities and model bridges; the two polynomial conclusions separately; the three finite minima and both one-term conclusions independently; then the exponential bound for 2 using its polynomial conclusion and the three finite minima, and the square-root exponential bound using its polynomial conclusion and the one-term minimum. The square-root polynomial proof uses common Basic identities, not the discrepancy-2 polynomial conclusion. The finite proofs use neither polynomial bound. Any grading of the consequences must preserve these dependencies and cannot substitute agreement on the last arithmetic line for acceptance of a consumed premise.

Checklist

Each row below applies to all nine restated conclusions. Where a failure mode has no corresponding mathematical operation, the inapplicability is stated explicitly. The claim-specific derivations and attacks in the preceding table supply the evidence for the shared verdicts.

Canonical failure modes

Named patterns

Correlated-sample inference is inapplicable: no random sample, statistical confidence statement or repeated-run independence estimate appears. The evidence-coverage discipline is applied throughout: static mathematical proof coverage is separated from Lean execution, the exact finite rows from infinite families, and the independent route from both author algorithms. This is a first examination; the distinct-attack requirement for a second independent review cycle is inapplicable. Structural disjointness for the computational batch is supplied and justified.

Erdős whole-claim checklist

Reproduction

The retained package is self-contained for the checks, with the repository's already prepared Python environment. It requires no installation, synchronization, Lean, network, corpus scan, gate or ledger command. The independent program uses only the Python standard library. The unchanged author program additionally uses the supplied 17-file runtime closure.

From the directory containing this report, set REVIEW_SCRATCH to an absolute writable scratch directory and run the following. The output directory is explicitly selected; no result is written into the subject snapshot.

test -n "$REVIEW_SCRATCH" &&
nice -n 10 env \
  -u VIRTUAL_ENV -u UV_PROJECT -u UV_PROJECT_ENVIRONMENT \
  -u UV_WORKING_DIR -u UV_NO_PROJECT -u PYTHONPATH \
  PYTHONDONTWRITEBYTECODE=1 \
  OMP_NUM_THREADS=1 OPENBLAS_NUM_THREADS=1 MKL_NUM_THREADS=1 \
  NUMEXPR_NUM_THREADS=1 VECLIB_MAXIMUM_THREADS=1 BLIS_NUM_THREADS=1 \
  uv run --no-sync python -B rerun.py --output "$REVIEW_SCRATCH"

The driver runs sequentially, using the interpreter selected by this command. For the author invocation it sets PYTHONPATH to the absolute subject/tools_runtime directory and invokes subject/finite/small_cases.py.txt as an actual script file, with --output under the selected scratch directory. It verifies the loaded tools source paths from that invocation's import trace. The original historical docstring command is left unchanged in the snapshot and is not the current path. The driver then runs finite/independent.py on finite/claims.json and on finite/negative_claims.json, the latter under Python -O.

Expected successful driver result: exit zero; all 28 count/witness rows equal; 17 supplied tools origins confirmed; the positive independent run exits zero and the three-case negative run exits one. The driver writes fresh author_results.json, independent_results.json, negative_results.json and verification.json plus disposable subprocess diagnostics into scratch. Ordinary runtime is under one minute on one thread; the bounded inputs here completed within that scope. A failure in a constituent run, comparison or import-origin obligation makes the driver exit nonzero. No cached success is an input to its decision.

For a direct independent run from the same directory:

test -n "$REVIEW_SCRATCH" &&
nice -n 10 env \
  -u VIRTUAL_ENV -u UV_PROJECT -u UV_PROJECT_ENVIRONMENT \
  -u UV_WORKING_DIR -u UV_NO_PROJECT -u PYTHONPATH \
  PYTHONDONTWRITEBYTECODE=1 \
  OMP_NUM_THREADS=1 OPENBLAS_NUM_THREADS=1 MKL_NUM_THREADS=1 \
  NUMEXPR_NUM_THREADS=1 VECLIB_MAXIMUM_THREADS=1 BLIS_NUM_THREADS=1 \
  uv run --no-sync python -B finite/independent.py \
  --input finite/claims.json --output "$REVIEW_SCRATCH/direct.json"

The scratch directory must already exist for this direct invocation. Replacing the input by finite/negative_claims.json, adding Python's -O flag and choosing another output filename must return exit one, not zero. The full driver performs that control automatically. These instructions use package-relative inputs so moving the complete report directory does not alter a mathematical check.

Retained artifacts are the unchanged subject snapshot, the independent source, the two exact input files, the complete fresh author data, the independent counts/certificates and the failed-control counts/witnesses. In particular finite/author_results.json is the concrete fresh count/witness data, not a terminal success summary. The independent outputs retain endpoint AP inventories, partition polynomials and conditional witness counts, or the allowable recurrence seeds. The prose derivation is essential to interpreting the four-term recurrence computation.

Verdict and limitations

The frozen argument survived the stated attacks. No missing essential mathematical premise, counterexample or unfinished mathematical coverage obligation was found within the commissioned read set. This includes the complete finite Fourier/Fejér and wrapping chain, all model and minimum bridges, exact finite rerun and disjoint reproduction, and every base and exponential consequence.

The scope is mathematical proof inspection plus the specified exact finite computations. No Lean elaboration, native_decide execution, compiler trust audit or kernel replay was performed. The report does not establish fidelity of an unlisted source file, the complete archives, their license texts, any reported source build, or later changed bytes. The finite data says nothing about other parameter values without the displayed mathematical reductions. No optimality of the general bounds is asserted.

A distinct fresh grader must assess this unchanged report, its independence and its keeper evidence, preserving the premise order for the two consequences. This report awards no tier, problem status or acceptance.