Erdős formalization fidelity: review

Exhaustive registered search over primes in 10428401..10428600 completed with a bounded negative result; the maximum factorial-residue fiber multiplicity found was 12 at p=10428581, residue=5141590.

Completed the exact bounded search over primes in 10428201..10428400 and produced the required artifact; no witness with multiplicity at least 16 was found, and the best multiplicity in-range was 10 at p=10428241, residue=3789711.

The producer Receipt and bounded result remain preserved, but the durable Engine gate has zero independent attachments and no surviving adversarial probe. Verifier success alone is not scientific acceptance.

Retire the unsupported prelaunch active-policy byte pair after preserving its content roots and confirming it admitted no state.

Retire unsupported prelaunch policy bytes without changing scientific state.

The exact remaining Erdős 730 gate is the exhaustive common-multiplicity event cover (23), followed by an explicit delta > 0 proving uniformly for X >= 2^57 that FirstPowerFar(X)/X + ShortTop(X)/X <= 1779/2500 - delta; neither step is proved at the pinned commit.

At first power, subtracting the fixed block shift leaves a multiple of the square prime modulus.

ExplicitDicksonAP12PrimeTupleSupplyK2 is the still-open assertion that for every U there is u >= U for which 48(12u)+29, 76(12u)+65, 38(12u)+23, and 48(12u)+41 are all prime; even this supplies only k=2, so the other fixed k >= 2 cases remain.

theorem erdosK2_of_explicitDicksonAP12PrimeTupleSupply (hSupply : ExplicitDicksonAP12PrimeTupleSupplyK2) : erdosFixed 2

The exact C2 residual is a universal no-surviving reduced-divisor split theorem; beyond that internal kernel, T4, full T6 and T7, the global kernel, and all later rungs remain unclaimed.

Coprime-refined existence-level C2 bridge. The extra coprimality condition is automatic from the split product identity, but recording it here matches the exact reduced-divisor obstruction used in the C2 analysis.

The remaining mathematical content for the pinned Erdős 686 refutation is exactly OddThueTail1000Hypothesis and LargeKSmoothHypothesis; equivalently, it is FinalResidual686Hypothesis.

The explicit final residual interface is logically equivalent to the conjunction of the updated odd-tail and large-smoothness hypotheses.

Conditional reduction of the r=5 case: if every balanced coloring of K_26 has extension demand exceeding 25 at some vertex, the Erdos-Gyarfas conjecture holds for r=5.

For Sidon sets A with |A| ~ N^{1/2}, the sumset A+A is equidistributed over residue classes mod m: each class holds ~1/m of A+A.

After the d = 2s - 2 closure, the one-stub all-nonbridge RL residual has 5 <= s and d <= 2s - 3; the multi-stub pair inequality and the final connected or 2-connected core remain separate obligations.

At d equal to twice the slack minus two, fully nonbridge corridor geometry, the rooted cut condition, injective simple demand pairs, legality, and same-color endpoints imply the exact RL internal-cost budget across all five canonical two-defect shapes.

duplicate of the catalog problem-finding, unlinked; the finite confirmation lives in the reproducible witness, not a standalone finding

Applied locally from proposal creation

duplicate of the catalog problem-finding, unlinked; the finite confirmation lives in the reproducible witness, not a standalone finding

Applied locally from proposal creation

duplicate of the catalog problem-finding, unlinked; the finite confirmation lives in the reproducible witness, not a standalone finding

Applied locally from proposal creation

duplicate of the catalog problem-finding, unlinked; the finite confirmation lives in the reproducible witness, not a standalone finding

Applied locally from proposal creation

duplicate of the catalog problem-finding, unlinked; the finite confirmation lives in the reproducible witness, not a standalone finding

Applied locally from proposal creation

duplicate of the catalog problem-finding, unlinked; the finite confirmation lives in the reproducible witness, not a standalone finding

Applied locally from proposal creation

Erdős #475 (distinct partial sums), finite confirmation: for every prime p ∈ {2,3,5,7,11,13}, all nonempty A ⊆ F_p\{0} admit an ordering with distinct partial sums mod p (subset counts 1,3,15,63,1023,4095 checked exhaustively). The question over all primes is the open problem.

accepted via sign

Erdős #366, finite confirmation: no 2-full n with n+1 3-full in [1, 10000000]. The question over all integers is the open problem.

accepted via sign

Erdős #364, finite confirmation: no three consecutive powerful integers in [1, 1000000] (consecutive powerful pairs do occur, e.g. 8,9). The question over all integers is the open problem.

accepted via sign

Erdős #306, finite confirmation: 64 reduced a/b (b squarefree) each expand as distinct squarefree-semiprime Egyptian unit fractions. The question over all positive rationals is the open problem.

accepted via sign