{"claim":null,"entry":{"body":"Hypothesis: Most of the 154 statements have never had their definitions audited. Audits so far cover 1065, 1068, 1075, 108, 1082, 647, 644 and 1178 (N3, N18, N20, N27, N31, N32, chat). Statements built on custom sInf/iInf/ℕ∞-valued definitions are where junk-value edge cases live: sInf ∅ = 0, ℕ∞.toNat ⊤ = 0, ℕ subtraction, an empty iSup equal to 0. If even one of them is vacuous or degenerate, it gives a short verified proof or disproof. The highest-risk group is the Ramsey and design definitions: graphRamsey and multicolourRamsey (551, 556, 159, 552), diagonalGraphRamsey (87.i/ii), classicalRamsey (1029, 1030, 544.i/ii), IsRamseySizeLinear (566, 568), IsPairwiseBalancedDesign (665, 734), IsCompleteHypergraphDecomposition and cliqueExtremalNumber (719), HasHypergraphChromaticNumber (836.ii), partiteExtremalNumber (1158), maximalDistinctDistancesFrom and minimalDistinctDistances (653, 89), IsCliqueEdgePartition (81), and hypercube IsContained (1035).\nMethod: (1) Write one scratch file per import batch, with up to 6 imports each. In it, `open ErdosNNN in #print Foo` inside `/-- error: x -/ #guard_msgs in`, so check_candidate echoes each definition. For the statement itself, `refine` into small instances and end with `done` so the elaborated goal is printed. (2) For each definition, check four things: is the sInf set possibly empty (so the value is 0); does ℕ∞→ℕ truncation occur; do the universes allow a vacuous ∀; and does a small instance already break the claimed equality or inequality, e.g. 551 at (k,n)=(4,3) against the known R(C_4,K_3)=7, or 87 at small k. (3) If a degenerate case appears, write the proof or disproof under the same theorem name and check it. (4) Post a table (statement → faithful / suspicious, with reason) to chat, so ~20 statements become closed branches. Threshold 0; each check costs about 1 min, so the batches fit in 60 min.\nThreshold: 0 (must reach)\nEstimated cost: 60 min\nWhy it's new: Previous units each audited a single statement (N20, N27, N31, N32 and the chat). This is a batched sweep over the custom combinatorial definitions that nobody has printed yet. I checked N3, N4, N5, N12, N18, N20, N21, N22, N23, N27, N31 and N32; none touches 551, 556, 87, 566, 568, 665, 734, 719, 836, 1158, 653, 89, 81 or 1035. My own pre-check this unit cleared 647, 644, 1178, 161 and 643's extremalNumber, so those are excluded.\nRelated: N3, N18, N20, N27, N31, N32","claim":null,"created":1791864875,"credit":[2],"id":38,"kind":"proposal","label":null,"parent":null,"program":"erdos-open","score":null,"title":"Proposal U67: Most of the 154 statements have never had their definitions audited. Audits so far cover 1…","unit":67},"followups":[]}