Certify a stronger four-support entropy advantage

[SamPetkov]

Summary

This is the next clean follow-up in the Erdős 625 review sequence. It isolates a stronger exact certificate for the same four-size support {2,3,4,5} used by the canonical candidate manuscript.

The certificate proves

D_4(delta) < log(639/500),
log(2) - D_4(delta) > log(1000/639)

uniformly over the full limiting phase interval.

No profile, second-moment estimate, canonical manuscript, PDF, or Lean source is changed.

Main certificate

The retained tilt is enclosed by

(49/20) log(2) < lambda_4 < (83/20) log(2).

Splitting at (29/10) log(2), exact rational interval arithmetic gives

L(49q/20) < 263/1000,
H(29q/10) < 3/200,
L(29q/10) < 33/250,
H(83q/20) < 29/200.

Monotonicity therefore yields the uniform omitted-weight bound

L(lambda_4) + H(lambda_4) < 139/500.

Evaluating the full-support dual function at the four-support optimizer gives

D_4(delta) <= log(1+L+H) < log(639/500).

Files

• 625/proofs/FOUR_SUPPORT_ENTROPY_CERTIFICATE.md
• 625/audits/FOUR_SUPPORT_ENTROPY_CERTIFICATE_AUDIT.md
• 625/experiments/four_support_entropy_certificate.py
• .github/workflows/erdos625-four-support-entropy-certificate.yml

Exact verification

The checker uses Fraction arithmetic for every proof gate. It certifies:

• a rational enclosure for log(2) from 2*atanh(1/3) and an explicit tail;
• a rational enclosure for 2^(1/20) by twentieth powers;
• both tilt-mean brackets;
• all four omitted-ratio inequalities;
• the two monotonicity-case sums.

It uses explicit exceptions rather than assert, so the gates remain active under python -O.

Local output:

ERDOS 625 FOUR-SUPPORT ENTROPY CERTIFICATE: PASS
  tilt bracket: (49/20)q < lambda_4 < (83/20)q
  L(49q/20) < 263/1000
  H(29q/10) < 3/200
  L(29q/10) < 33/250
  H(83q/20) < 29/200
  uniform omitted ratio < 139/500
  D_4(delta) < log(639/500)
  log(2)-D_4(delta) > log(1000/639)

The separate phase scan is diagnostic only. It reports an approximate minimum advantage 0.520701335491228, larger than the certified log(1000/639).

Constant implications

Using the canonical manuscript's current /32 final propagation, this certificate would give

(log 2)^2 log(1000/639) / 32 = 0.006724102452095...

If PR #31's independently reviewed /8 propagation is accepted, the combined coefficient becomes

(log 2)^2 log(1000/639) / 8 = 0.026896409808379...

Those theorem-constant changes require their respective propagation reviews. This PR itself proves only the limiting entropy certificate conditional on the variational dual comparison already used by Lemma 5.1.

Scope boundary

This PR does not independently verify:

• finite-to-limiting optimizer convergence;
• equation (5.11);
• the normalized second moment;
• amplification;
• Erdos625Statement.

It is an exact elementary replacement certificate for the limiting four-support entropy loss.

[SamPetkov]

Focused verification status: PASS for the stated limiting certificate. The exact-certificate workflow passed bytecode compilation, normal execution, and python -O; the canonical source-tag scan ran in the repository. The artifact-synchronization workflow also passed. The remaining review boundary is the finite-to-limiting transport already used by canonical Lemma 5.1, not the rational weight inequalities themselves.

[SamPetkov]

Review-sequence coordination is now documented in PR #33. The roadmap records this certificate independently of #31, gives the separate and combined coefficient implications, and places review of this finite certificate before any canonical constant integration.