# Independent audit of the finite cosine-sum result

## Verdict

The finite claim was independently reproduced:

\[
A_* = \{1,2,3,4,5,6,7,8,10,11,13,14,15,16,17,21\}
\]

is the **unique** minimizer of

\[
\frac{-\min_{x\in\mathbb R}\sum_{a\in A}\cos(ax)}{\sqrt{|A|}}
\]

among all **4,194,303 nonempty subsets of `{1,...,22}`**.

The certified bounds are strict:

\[
2.454832753<K(A_*)<2.4548327531,
\]

so

\[
0.61370818825<\frac{K(A_*)}{4}<0.613708188275.
\]

Every other nonempty subset of `{1,...,22}` has ratio at least
`0.613708188275`. Hence equality with the winner is excluded, even though
the comparison certificates for other sets only give non-strict bounds.

This says nothing about sets containing a frequency greater than `22`,
and gives no universal asymptotic constant. Mathematical novelty was not
established. The independent verification here is another program and
algebraic audit within this work, not outside expert review or a Lean proof.

## Independence and method

`redteam_finite_check.py` does not import `compute/exact_grid.py` or
`compute/certify.py`.

1. It constructs rigorous cosine upper bounds using **Machin's identity
   for pi plus exact rational alternating Taylor bounds**, rather than
   repeated half-angle square roots and interval rotations.
2. It enumerates subsets using two **direct 11-element subset-sum tables**,
   rather than Gray-code updates.
3. It independently derives the winner's Chebyshev coefficients from the
   **closed factorial formula**, rather than a recurrence.
4. It verifies every supplied Sturm-chain identity using exact polynomial
   division and checks that all scaling factors are positive. It verifies
   the endpoint signs and counts variations itself: `10` at both ends.
5. It verifies the rational witness for the strict lower bound.

The exhaustive pass on a 513-point certified grid left exactly one
unexcluded set, the winner. Rechecking that exception on the full
4097-point grid agreed with the original result. The runtime was about
2.31 seconds in this environment. The transcript is in
`redteam_finite_check.json`.

### Why the interval construction is rigorous

For an even number of terms, the alternating arctangent sum is a lower
bound and the next positive term supplies an upper bound. Machin's
identity gives bounds on pi using exact rational arithmetic. The identity
can be checked directly: if `alpha=atan(1/5)`, `beta=atan(1/239)`, then
`tan(2alpha)=5/12`, `tan(4alpha)=120/119`, and
`tan(4alpha-beta)=1`; this angle lies in `(0,pi/2)`, hence is `pi/4`.

Angles are reflected into `[0,pi/2]`. Cosine is decreasing there, so
evaluating its upper Taylor bound at a lower angle bound is safe. For
negative cosine values the lower Taylor bound is negated. The omitted
alternating tails have decreasing magnitudes. Final conversion to units
of `2^-40` uses an exact integer ceiling.

### Why the finite exclusions are rigorous

At every tested angle, the sum of the certified cosine upper bounds is
an upper bound on the true sum. Therefore its negative is a lower bound
on `K(A)`. If any such bound is at least

\[
0.613708188275\sqrt{|A|},
\]

that set cannot tie or beat the winner. The square root comparison is
performed by exact integer squares and ceilings; no floating-point square
root enters a logical decision. Using finitely many angles is sufficient
for this direction of inequality. For the winner's opposite inequality,
the Sturm argument covers the entire continuous interval.

## Source-code audit observations

No invalid inequality, overflow, missing subset, or sign error was found
in the original implementation for the stated inputs.

* `22 * 2^40 < 2^63`, so all signed 64-bit subset sums are safe.
* Gray-code membership and cardinality updates are consistent.
* The threshold is the exact integer ceiling of the required scaled
  square-root expression; its inequality direction is correct.
* Sturm normalization divides by positive factors only, preserving signs.
* The sine interval is clipped into `[0,1]`, valid for all states used in
  the cosine table. The original version also performed an unused rotation
  beyond pi; this update has been removed. No certified value changed.
* `exact_grid.py` divides the winning upper bound by `4`, relying on this
  particular winner having `16` terms. This was independently checked and
  is now explicitly asserted; this is a checker for the stated finite claim.
* At the time of inspection, `certify.py`'s main entry point regenerated
  certificates for the 6- and 11-term candidates but not the 16-term
  winner. The package-level `run_verification.py` now recomputes and checks
  all three supplied certificates, including the winner, and runs both
  finite enumerations. This reproduces the proof from the supplied inputs;
  the supplied winner certificate was also verified independently.