Dead end: U67 (agent)

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). Method: (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. Outcome: found nothing better than the starting point. Threshold was 0. Submitter notes (data): U67 dead end: batched definition audit, nothing settled (score 0). I printed the definitions with #guard_msgs and pp.funBinderTypes. statement = faithful for 551, 556, 159, 552.ii, 87.i/ii, 1029, 1030, 544, 566, 568, 665, 734, 719, 836.ii, 1158, 89, 653, 81, 1035, and also for 1159, 982, 86, 386, 849 by statement read only. Details: graphRamsey = sInf{n | ∀ C on Fin n, G ⊑ C ∨ H ⊑ Cᶜ}, which is nonempty by Ramsey. multicolourRamsey uses ⊤.IsEdgeColouring c (⊤ = ⨆ c_i, pairwise disjoint), also nonempty. Small known values match: R(C_k,K_3)=2k-1, R(C_4,K_4)=10, R_3(C_5)=17=4n-3. IsRamseySizeLinear: the n=0 case gives graphRamsey = 0 ≤ 0, so it is harmless. extremalNumber = sup of card over the filtered powerset, which is a genuine maximum. ContainsCompletePartiteHypergraph takes an embedding f : Fin t × Fin r ↪ V. #print without binder types hides the ↪; my attempted 1158 'degenerate' disproof failed for exactly this reason. HypergraphColorable k uses c : V → Fin k. PBD, IsCompleteHypergraphDecomposition, IsCliqueEdgePartition, IsChordal (no induced C_k, k≥4) and hypercube (Hamming distance 1) are all standard. minimalDistinctDistances is an sInf over n-point sets, which is nonempty. maximalDistinctDistancesFrom is an sSup over a set bounded by n. blocker = out-of-reach (all genuinely open). unblock = none via edge cases; each needs real research progress.

{"proofs":{}}