# Sources and mathematical certification for T656

Instruction authority: `agents/runs/20261101T171341Z-build-skills/manifest.json`.
The archived local and live skills are byte-identical, both SHA-256
`a2b28d9953264d7b0ca62663785c2952190c5be6d6d3597fd695d9a54d606278`.
Both copies were read; `skill-manifest.json` is attached unchanged in content.

## Sources actually checked

- Robert Kleinberg, Will Sawin and David E. Speyer, *The growth rate of
  tri-colored sum-free sets*, introduction and Section 3, Lemma 5 and Remark 6.
  https://arxiv.org/html/1607.00047v3
  Defines the positive-real minimizer rho, proves the entropy relation, and
  discusses the maximizing probability law at mean (q-1)/3. Their q is our n;
  their theta is the companion C_n. The displayed law is proportional to rho^j.
- Matthias Christandl, Péter Vrana and Jeroen Zuiddam, *Universal points in the
  asymptotic spectrum of tensors*, Section 4.2.1, equations (30)–(31).
  https://arxiv.org/html/1709.07851v3#S4.SS2.SSS1
  Defines the reduced polynomial multiplication support and the reciprocal
  gamma equation. The algebra may have any positive integer dimension; it
  does not impose a prime-power restriction on this optimization.
- Live API documents T655, T339, T35 and T5 were inspected. T655 is still
  private, so public search does not return it. Its canonical slug was read
  from the API's no-op writability response. The other slugs and the n=3
  T35 entry keys came from live search and lookup results.

## Deductions used for certification

For S_n(t)=sum_{j=0}^{n-1}t^j and F_n(t)=S_n(t)t^(-(n-1)/3),
write t=exp(s). Differentiating log F gives E_s[j]-(n-1)/3, for positive
probabilities proportional to exp(js). Differentiating again gives Var_s(j),
which is strictly positive for n>=2 because at least j=0 and j=1 have positive
probability. The first derivative tends to -(n-1)/3 as s tends to minus
infinity and equals (n-1)/6 at s=0. It has one zero, with rho in (0,1).
F tends to infinity at both ends of t>0, so this stationary point is its unique
global minimum. This is a mathematical argument, not an inference from digits.

The derivative has the sign of
P_n(t)=3t S'_n(t)-(n-1)S_n(t)=sum_j(3j-n+1)t^j.
Hence exact rational opposite signs isolate the intended root. Replacing
t by 1/gamma in the stationary condition gives
1/(gamma-1)-n/(gamma^n-1)=(n-1)/3.
Clearing denominators introduces a double root at gamma=1; the independent
checker works strictly above 1, so never admits that extraneous root.

The n=2 equations give rho=1/2 and gamma=2 exactly. At n=3 they give
rho=(sqrt(33)-1)/8 and gamma=(sqrt(33)+1)/4. The rational root theorem is
checked exhaustively for n=2 through 32; no other positive rational optimizer
occurs. These decisions are based on the equations, not on trailing zeros.

## Planned and executed checks

`checks.py` solves the reciprocal equation without calling the generator's
root finder. It checks controls first, then exact polynomial identities and
opposite signs at the endpoints of every printed irrational interval.
Independent enclosures must lie wholly within the displayed intervals; an
overlap alone is insufficient. Ball comparisons also require finite values
and diameter below 10^-130.

All dimensions are checked against T655 through the objective, reciprocal
objective and entropy. The n=2 probability law is Bernoulli(1/3), so T339
provides a fact outside this family; the exact n=3 radicals and T35 provide
another. The same checks are run again on values read from T656 after filling.
`numerical-evidence.json` and the separate stored-check evidence record the
actual outcomes, versions, bounds and precision measurements.