check_note.py: exact checks for OWR-4990373-005 (python 3.13.5)

[1] graph facts
      B: n=6 m=8 degrees=[3, 1, 3, 3, 3, 3] |Aut|=4 orbits=[[0], [1], [2, 3], [4, 5]]
PASS  B connected, simple, not vertex-transitive
      C10: n=10 m=15 degrees=[3, 3, 3, 3, 3, 3, 3, 3, 3, 3] |Aut|=32 orbits=[[0, 1], [2, 3, 6, 7], [4, 5, 8, 9]]
PASS  C10 connected, simple, not vertex-transitive
      A: n=6 m=10 degrees=[2, 4, 4, 3, 3, 4] |Aut|=4 orbits=[[0], [1, 2], [3, 4], [5]]
PASS  A connected, simple, not vertex-transitive
PASS  B: degrees (3,1,3,3,3,3), |Aut| = 4, orbits {0},{1},{2,3},{4,5}
PASS  C10: 3-regular, |Aut| = 32, orbits {0,1},{2,3,6,7},{4,5,8,9}
PASS  A: degrees (2,4,4,3,3,4)

[2] Lemma 2.3: every flip lowers the number of disagreeing edges
PASS  B: energy drops at every flip (64 states)
PASS  C10: energy drops at every flip (1024 states)
PASS  A: energy drops at every flip (64 states)
PASS  K5: energy drops at every flip (32 states)
PASS  Bminus45: energy drops at every flip (64 states)
PASS  A: under the coin rule some flips (k = d/2) would leave the energy unchanged (104 pairs)

[3] limits f_p(inf) by the absorption recursion (independent of the closed forms)
PASS  B, p=61/100: f(inf) = 41541389119/62500000000 (= 0.664662225904) = constant term of the closed form
PASS  C10, p=7/10: f(inf) = 90794489017687/115200000000000 (= 0.788146606056) = constant term of the closed form
PASS  A, p=7/10: f(inf) = 1016603/1250000 (= 0.813282400000) = constant term of the closed form

[4] Theorem 3.1 (graph B), all p
PASS  B: terms are exactly (k,i) in {(0,1),(1,1),(1,2),(3,1),(5,1),(5,2)}
PASS  B: computed coefficients = claimed polynomials at the 7 nodes j/8 (degree <= 6)
PASS  B: direct exact polynomials = claimed polynomials (8 extra points, degree <= 6)
PASS  B: interpolation through the 7 nodes = direct polynomials
PASS  B: f(inf) = p^2 (28p^3 - 70p^2 - 94p + 211)/75
PASS  B: f(0) = p, i.e. sum_k c_{k,1} = p
PASS  Corollary 3.2: (4+r)/4 + 7r/24 = 1 + 13r/24 and 16*13/(9*24) = 26/27
PASS  Corollary 3.2 at p = 61/100: threshold 16/(9r)+26/27 = 60206/7137 = 8.4358 < t0 = 223/25

[5] graph B, p = 61/100, t0 = 223/25: two-sided uniformization enclosure (Lambda = 6, K = 220)
      f(t0) - f(inf) in [9.3891186962e-07, 9.3891186962e-07], width 2.49e-65
PASS  B: lower bound L > f(inf) (overshoot certified)

[6] Theorem 4.1 (graph C10), all p
PASS  C10: 19 terms, k <= 10, i <= 3
PASS  C10: computed coefficients = table polynomials at the 11 nodes j/12 (degree <= 10)
PASS  C10: direct exact polynomials = table polynomials (12 extra points)
PASS  C10: interpolation through the 11 nodes = direct polynomials
PASS  C10: at k = 1 only i = 1, 2 occur (c_{1,i} = 0 at the 11 nodes for i >= 3)
PASS  C10: 80905p^4-161810p^3-5274599p^2+5355504p+5556600 = 80905r^2+5355504r+5556600
PASS  C10, p = 7/10: c_{1,2} = 1485516389/20000000000

[7] graph C10, p = 7/10, t0 = 3: two-sided uniformization enclosure (Lambda = 10, K = 150)
      f(3) - f(inf) in [3.4740871122e-03, 3.4740871122e-03], width 2.69e-55
PASS  C10: lower bound L > f(inf) + 3.474e-3

[8] graph A (ABB self-inclusion rule at even degree), all p and p = 7/10, t0 = 27/5
PASS  A: computed coefficients = claimed polynomials at the 7 nodes j/8 (degree <= 6)
PASS  A: at k = 1 the top term is i = 3: c_{1,3} = (4/3) r^2 w, i.e. (2/3) r^2 w t^2 e^{-t}
      f(t0) - f(inf) in [4.7769136507e-04, 4.7769136507e-04], width 4.00e-58
PASS  A: lower bound L > f(inf) + 4.776e-4

[9] consistency with known facts
PASS  K5 (ABB Prop. 3.10, formula (3.7)): closed form = p e^{-t} + (1-e^{-t}) P[Bin(5,p) >= 3]
PASS  symmetry f_{1-p} = 1 - f_p, coefficientwise (B, C10, A, K5; n+1 nodes each)
PASS  FLOAT: f_p(t) >= p - 1e-12 for p = 0.50..0.99, t = 0..40 (Mossel-Neeman-Tamuz bound; min -1.1e-16)

[10] control: graph B without the edge 45 at p = 61/100, t0 = 223/25
      f(t0) - f(inf) in [-3.021371e-05, -3.021371e-05]
PASS  Bminus45: c_{1,2} < 0 and upper bound < f(inf): no overshoot (the certificate detects the change)

TOTAL failures: 0   (3.1 s)
